I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
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
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
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