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.

Homework 8

This is the task corresponding to homework 8.

Resources

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```

Terms and Conditions