Homework 8

Definitions File

theory Defs
  imports "HOL-Data_Structures.Cmp" "HOL-Data_Structures.Set_Specs"
begin

datatype 'a itree = iLeaf | iNode "'a itree" "'a \<times> 'a" "'a itree"

fun set_itree2:: "'a::ord itree \<Rightarrow> 'a set" where
  "set_itree2 iLeaf = {}"
| "set_itree2 (iNode l (low, high) r) = {low .. high} \<union> ((set_itree2 l) \<union> (set_itree2 r))"

fun set_itree3:: "'a itree \<Rightarrow> ('a \<times> 'a) set" where 
  "set_itree3 iLeaf = {}"
| "set_itree3 (iNode l (low, high) r) = {(low, high)} \<union> ((set_itree3 l) \<union> (set_itree3 r))"

class height =
fixes height :: "'a \<Rightarrow> nat"

datatype 'a tree12 =
  Leaf ("\<langle>\<rangle>") |
  Node1 "'a tree12"  ("\<langle>_\<rangle>") |
  Node2 "'a tree12" 'a "'a tree12"  ("\<langle>_, _, _\<rangle>")

fun inorder :: "'a tree12 \<Rightarrow> 'a list" where
"inorder Leaf = []" |
"inorder (Node1 t) = inorder t" |
"inorder (Node2 l a r) = inorder l @ a # inorder r"


instantiation tree12 :: (type)height
begin

fun height_tree12 :: "'a tree12 \<Rightarrow> nat" where
"height Leaf = 0" |
"height (Node1 t) = Suc (height t)" |
"height (Node2 l _ r) = Suc (max (height l) (height r))"

instance ..

end

fun invar :: "'a tree12 => bool" where
  "invar Leaf = True" |
  "invar (Node1 t) = (case t of
    Leaf => True |
    Node1 _ => False |
    Node2 l _ r => height l = height r \<and> invar l \<and> invar r)" |
  "invar (Node2 l _ r) = (height l = height r \<and> invar l \<and> invar r)"

datatype 'a upI = TI "'a tree12" | OF "'a tree12" 'a "'a tree12"

fun treeI :: "'a upI \<Rightarrow> 'a tree12" where
"treeI (TI t) = t" |
"treeI (OF l a r) = Node2 l a r"

fun hI :: "'a upI \<Rightarrow> nat" where
"hI (TI t) = height t" |
"hI (OF l a r) = height l"


consts ibst :: "'a::linorder itree \<Rightarrow> bool"

consts delete :: "int \<Rightarrow> int itree \<Rightarrow> int itree"

consts merge :: "'a tree12 \<Rightarrow> 'a \<Rightarrow> 'a tree12 \<Rightarrow> 'a \<Rightarrow> 'a tree12 \<Rightarrow> 'a upI"

consts ins :: "'a::linorder \<Rightarrow> 'a tree12 \<Rightarrow> 'a upI"


end

Template File

theory Submission
  imports Defs
begin

fun ibst :: "'a::linorder itree \<Rightarrow> bool"  where
  "ibst _ = undefined"

fun delete :: "int \<Rightarrow> int itree \<Rightarrow> int itree"  where
  "delete _ = undefined"

value "delete 3 (iNode (iNode (iNode iLeaf (Interval 0 0) iLeaf) (Interval 1 1) (iNode iLeaf (Interval 2 4) iLeaf)) (Interval (5::nat) 6) (iLeaf))
       = iNode (iNode (iNode iLeaf (Interval 0 0) iLeaf) (Interval 1 1) (iNode iLeaf (Interval 2 2) (iNode iLeaf (Interval 4 4) iLeaf))) (Interval 5 6) iLeaf"



lemma delete_set_minus: "ibst t \<Longrightarrow> set_itree2 (delete x t) = (set_itree2 t) - {x}"
  sorry

lemma ibst_delete: "ibst t \<Longrightarrow> ibst (delete x t)"
  sorry

fun merge :: "'a tree12 \<Rightarrow> 'a \<Rightarrow> 'a tree12 \<Rightarrow> 'a \<Rightarrow> 'a tree12 \<Rightarrow> 'a upI"  where
  "merge _ = undefined"

fun ins :: "'a::linorder \<Rightarrow> 'a tree12 \<Rightarrow> 'a upI"  where
  "ins _ = undefined"

lemma inorder_merge[simp]:
  "inorder(treeI(merge l a m b r)) = (inorder l) @ a # (inorder m) @ b # (inorder r)"
  sorry

theorem invar_ins: "invar t \<Longrightarrow> invar (treeI(ins x t)) \<and> hI (ins x t) = height t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma delete_set_minus: "ibst t \<Longrightarrow> set_itree2 (delete x t) = (set_itree2 t) - {x}"
  by (rule Submission.delete_set_minus)

lemma ibst_delete: "ibst t \<Longrightarrow> ibst (delete x t)"
  by (rule Submission.ibst_delete)

lemma inorder_merge: "inorder(treeI(merge l a m b r)) = (inorder l) @ a # (inorder m) @ b # (inorder r)"
  by (rule Submission.inorder_merge)

theorem invar_ins: "invar t \<Longrightarrow> invar (treeI(ins x t)) \<and> hI (ins x t) = height t"
  by (rule Submission.invar_ins)

end