Week 9 homework 2

Definitions File

theory Defs
  imports "HOL-Data_Structures.Tree2"
  "HOL-Data_Structures.Cmp"
  "HOL-Data_Structures.List_Ins_Del"
begin

datatype color = Red | Black

type_synonym 'a rbt = "('a,color * nat)tree"

text \<open>

Define a function for accessing the new field:
\<close>

fun bh :: "'a rbt \<Rightarrow> nat" where
"bh Leaf = 0" |
"bh (Node l a (c,h) r) = h"


abbreviation R where "R l a h r \<equiv> Node l a (Red,h) r"
abbreviation B where "B l a h r \<equiv> Node l a (Black,h) r"

abbreviation rd where "rd l a r \<equiv> Node l a (Red,bh l) r"
abbreviation bk where "bk l a r \<equiv> Node l a (Black,Suc(bh l)) r"

end

Template File

theory Submission
  imports Defs
begin

definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"insert _ = undefined"

fun invh2 :: "'a rbt \<Rightarrow> bool" where
  "invh2 _ = undefined"

definition rbt :: "'a rbt \<Rightarrow> bool" where
  "rbt _ = undefined"

lemma inorder_insert:
  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
  sorry

theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma inorder_insert:
  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
  by(rule inorder_insert)

theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
  by(rule rbt_insert)

end