src/HOL/Data_Structures/Tree23_Set.thy
 author nipkow Wed Jun 13 15:24:20 2018 +0200 (10 months ago) changeset 68440 6826718f732d parent 68431 b294e095f64c child 69597 ff784d5a5bfb permissions -rw-r--r--
qualify interpretations to avoid clashes
 nipkow@61640 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61640 ` 2` nipkow@62130 ` 3` ```section \2-3 Tree Implementation of Sets\ ``` nipkow@61640 ` 4` nipkow@61640 ` 5` ```theory Tree23_Set ``` nipkow@61640 ` 6` ```imports ``` nipkow@61640 ` 7` ``` Tree23 ``` nipkow@61640 ` 8` ``` Cmp ``` nipkow@67965 ` 9` ``` Set_Specs ``` nipkow@61640 ` 10` ```begin ``` nipkow@61640 ` 11` nipkow@68109 ` 12` ```declare sorted_wrt.simps(2)[simp del] ``` nipkow@68109 ` 13` nipkow@68431 ` 14` ```definition empty :: "'a tree23" where ``` nipkow@68431 ` 15` ```"empty = Leaf" ``` nipkow@68431 ` 16` nipkow@63411 ` 17` ```fun isin :: "'a::linorder tree23 \ 'a \ bool" where ``` nipkow@61640 ` 18` ```"isin Leaf x = False" | ``` nipkow@61640 ` 19` ```"isin (Node2 l a r) x = ``` nipkow@61678 ` 20` ``` (case cmp x a of ``` nipkow@61678 ` 21` ``` LT \ isin l x | ``` nipkow@61678 ` 22` ``` EQ \ True | ``` nipkow@61678 ` 23` ``` GT \ isin r x)" | ``` nipkow@61640 ` 24` ```"isin (Node3 l a m b r) x = ``` nipkow@61678 ` 25` ``` (case cmp x a of ``` nipkow@61678 ` 26` ``` LT \ isin l x | ``` nipkow@61678 ` 27` ``` EQ \ True | ``` nipkow@61678 ` 28` ``` GT \ ``` nipkow@61678 ` 29` ``` (case cmp x b of ``` nipkow@61678 ` 30` ``` LT \ isin m x | ``` nipkow@61678 ` 31` ``` EQ \ True | ``` nipkow@61678 ` 32` ``` GT \ isin r x))" ``` nipkow@61640 ` 33` nipkow@61640 ` 34` ```datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23" ``` nipkow@61640 ` 35` nipkow@61640 ` 36` ```fun tree\<^sub>i :: "'a up\<^sub>i \ 'a tree23" where ``` nipkow@61640 ` 37` ```"tree\<^sub>i (T\<^sub>i t) = t" | ``` nipkow@61709 ` 38` ```"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" ``` nipkow@61640 ` 39` nipkow@63411 ` 40` ```fun ins :: "'a::linorder \ 'a tree23 \ 'a up\<^sub>i" where ``` nipkow@61640 ` 41` ```"ins x Leaf = Up\<^sub>i Leaf x Leaf" | ``` nipkow@61640 ` 42` ```"ins x (Node2 l a r) = ``` nipkow@61640 ` 43` ``` (case cmp x a of ``` nipkow@61678 ` 44` ``` LT \ ``` nipkow@61678 ` 45` ``` (case ins x l of ``` nipkow@61678 ` 46` ``` T\<^sub>i l' => T\<^sub>i (Node2 l' a r) | ``` nipkow@61678 ` 47` ``` Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) | ``` nipkow@61640 ` 48` ``` EQ \ T\<^sub>i (Node2 l x r) | ``` nipkow@61678 ` 49` ``` GT \ ``` nipkow@61678 ` 50` ``` (case ins x r of ``` nipkow@61678 ` 51` ``` T\<^sub>i r' => T\<^sub>i (Node2 l a r') | ``` nipkow@61678 ` 52` ``` Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" | ``` nipkow@61640 ` 53` ```"ins x (Node3 l a m b r) = ``` nipkow@61640 ` 54` ``` (case cmp x a of ``` nipkow@61678 ` 55` ``` LT \ ``` nipkow@61678 ` 56` ``` (case ins x l of ``` nipkow@61678 ` 57` ``` T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) | ``` nipkow@61678 ` 58` ``` Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) | ``` nipkow@61640 ` 59` ``` EQ \ T\<^sub>i (Node3 l a m b r) | ``` nipkow@61678 ` 60` ``` GT \ ``` nipkow@61678 ` 61` ``` (case cmp x b of ``` nipkow@61678 ` 62` ``` GT \ ``` nipkow@61678 ` 63` ``` (case ins x r of ``` nipkow@61678 ` 64` ``` T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') | ``` nipkow@61678 ` 65` ``` Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) | ``` nipkow@61678 ` 66` ``` EQ \ T\<^sub>i (Node3 l a m b r) | ``` nipkow@61678 ` 67` ``` LT \ ``` nipkow@61678 ` 68` ``` (case ins x m of ``` nipkow@61678 ` 69` ``` T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) | ``` nipkow@61678 ` 70` ``` Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))" ``` nipkow@61640 ` 71` nipkow@61640 ` 72` ```hide_const insert ``` nipkow@61640 ` 73` nipkow@63411 ` 74` ```definition insert :: "'a::linorder \ 'a tree23 \ 'a tree23" where ``` nipkow@61640 ` 75` ```"insert x t = tree\<^sub>i(ins x t)" ``` nipkow@61640 ` 76` nipkow@61640 ` 77` ```datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23" ``` nipkow@61640 ` 78` nipkow@61640 ` 79` ```fun tree\<^sub>d :: "'a up\<^sub>d \ 'a tree23" where ``` nipkow@61709 ` 80` ```"tree\<^sub>d (T\<^sub>d t) = t" | ``` nipkow@61709 ` 81` ```"tree\<^sub>d (Up\<^sub>d t) = t" ``` nipkow@61640 ` 82` nipkow@61640 ` 83` ```(* Variation: return None to signal no-change *) ``` nipkow@61640 ` 84` nipkow@61640 ` 85` ```fun node21 :: "'a up\<^sub>d \ 'a \ 'a tree23 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 86` ```"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" | ``` nipkow@61640 ` 87` ```"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" | ``` nipkow@61640 ` 88` ```"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))" ``` nipkow@61640 ` 89` nipkow@61640 ` 90` ```fun node22 :: "'a tree23 \ 'a \ 'a up\<^sub>d \ 'a up\<^sub>d" where ``` nipkow@61640 ` 91` ```"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" | ``` nipkow@61640 ` 92` ```"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" | ``` nipkow@61640 ` 93` ```"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))" ``` nipkow@61640 ` 94` nipkow@61640 ` 95` ```fun node31 :: "'a up\<^sub>d \ 'a \ 'a tree23 \ 'a \ 'a tree23 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 96` ```"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | ``` nipkow@61640 ` 97` ```"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" | ``` nipkow@61640 ` 98` ```"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" ``` nipkow@61640 ` 99` nipkow@61640 ` 100` ```fun node32 :: "'a tree23 \ 'a \ 'a up\<^sub>d \ 'a \ 'a tree23 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 101` ```"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" | ``` nipkow@61640 ` 102` ```"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | ``` nipkow@61640 ` 103` ```"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" ``` nipkow@61640 ` 104` nipkow@61640 ` 105` ```fun node33 :: "'a tree23 \ 'a \ 'a tree23 \ 'a \ 'a up\<^sub>d \ 'a up\<^sub>d" where ``` nipkow@61640 ` 106` ```"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" | ``` nipkow@61640 ` 107` ```"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" | ``` nipkow@61640 ` 108` ```"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" ``` nipkow@61640 ` 109` nipkow@68020 ` 110` ```fun split_min :: "'a tree23 \ 'a * 'a up\<^sub>d" where ``` nipkow@68020 ` 111` ```"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" | ``` nipkow@68020 ` 112` ```"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" | ``` nipkow@68020 ` 113` ```"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" | ``` nipkow@68020 ` 114` ```"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" ``` nipkow@61640 ` 115` nipkow@68020 ` 116` ```text \In the base cases of \split_min\ and \del\ it is enough to check if one subtree is a \Leaf\, ``` nipkow@67038 ` 117` ```in which case balancedness implies that so are the others. Exercise.\ ``` nipkow@67038 ` 118` nipkow@63411 ` 119` ```fun del :: "'a::linorder \ 'a tree23 \ 'a up\<^sub>d" where ``` nipkow@61640 ` 120` ```"del x Leaf = T\<^sub>d Leaf" | ``` nipkow@61678 ` 121` ```"del x (Node2 Leaf a Leaf) = ``` nipkow@61678 ` 122` ``` (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" | ``` nipkow@61678 ` 123` ```"del x (Node3 Leaf a Leaf b Leaf) = ``` nipkow@61678 ` 124` ``` T\<^sub>d(if x = a then Node2 Leaf b Leaf else ``` nipkow@61678 ` 125` ``` if x = b then Node2 Leaf a Leaf ``` nipkow@61678 ` 126` ``` else Node3 Leaf a Leaf b Leaf)" | ``` nipkow@61678 ` 127` ```"del x (Node2 l a r) = ``` nipkow@61678 ` 128` ``` (case cmp x a of ``` nipkow@61678 ` 129` ``` LT \ node21 (del x l) a r | ``` nipkow@61678 ` 130` ``` GT \ node22 l a (del x r) | ``` nipkow@68020 ` 131` ``` EQ \ let (a',t) = split_min r in node22 l a' t)" | ``` nipkow@61678 ` 132` ```"del x (Node3 l a m b r) = ``` nipkow@61678 ` 133` ``` (case cmp x a of ``` nipkow@61678 ` 134` ``` LT \ node31 (del x l) a m b r | ``` nipkow@68020 ` 135` ``` EQ \ let (a',m') = split_min m in node32 l a' m' b r | ``` nipkow@61678 ` 136` ``` GT \ ``` nipkow@61678 ` 137` ``` (case cmp x b of ``` nipkow@61640 ` 138` ``` LT \ node32 l a (del x m) b r | ``` nipkow@68020 ` 139` ``` EQ \ let (b',r') = split_min r in node33 l a m b' r' | ``` nipkow@61640 ` 140` ``` GT \ node33 l a m b (del x r)))" ``` nipkow@61640 ` 141` nipkow@63411 ` 142` ```definition delete :: "'a::linorder \ 'a tree23 \ 'a tree23" where ``` nipkow@61640 ` 143` ```"delete x t = tree\<^sub>d(del x t)" ``` nipkow@61640 ` 144` nipkow@61640 ` 145` nipkow@61640 ` 146` ```subsection "Functional Correctness" ``` nipkow@61640 ` 147` nipkow@61640 ` 148` ```subsubsection "Proofs for isin" ``` nipkow@61640 ` 149` nipkow@67929 ` 150` ```lemma isin_set: "sorted(inorder t) \ isin t x = (x \ set (inorder t))" ``` nipkow@67929 ` 151` ```by (induction t) (auto simp: isin_simps ball_Un) ``` nipkow@61640 ` 152` nipkow@61640 ` 153` nipkow@61640 ` 154` ```subsubsection "Proofs for insert" ``` nipkow@61640 ` 155` nipkow@61640 ` 156` ```lemma inorder_ins: ``` nipkow@61640 ` 157` ``` "sorted(inorder t) \ inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" ``` nipkow@61640 ` 158` ```by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) ``` nipkow@61640 ` 159` nipkow@61640 ` 160` ```lemma inorder_insert: ``` nipkow@61640 ` 161` ``` "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" ``` nipkow@61640 ` 162` ```by(simp add: insert_def inorder_ins) ``` nipkow@61640 ` 163` nipkow@61640 ` 164` nipkow@61640 ` 165` ```subsubsection "Proofs for delete" ``` nipkow@61640 ` 166` nipkow@61640 ` 167` ```lemma inorder_node21: "height r > 0 \ ``` nipkow@61640 ` 168` ``` inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r" ``` nipkow@61640 ` 169` ```by(induct l' a r rule: node21.induct) auto ``` nipkow@61640 ` 170` nipkow@61640 ` 171` ```lemma inorder_node22: "height l > 0 \ ``` nipkow@61640 ` 172` ``` inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')" ``` nipkow@61640 ` 173` ```by(induct l a r' rule: node22.induct) auto ``` nipkow@61640 ` 174` nipkow@61640 ` 175` ```lemma inorder_node31: "height m > 0 \ ``` nipkow@61640 ` 176` ``` inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r" ``` nipkow@61640 ` 177` ```by(induct l' a m b r rule: node31.induct) auto ``` nipkow@61640 ` 178` nipkow@61640 ` 179` ```lemma inorder_node32: "height r > 0 \ ``` nipkow@61640 ` 180` ``` inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r" ``` nipkow@61640 ` 181` ```by(induct l a m' b r rule: node32.induct) auto ``` nipkow@61640 ` 182` nipkow@61640 ` 183` ```lemma inorder_node33: "height m > 0 \ ``` nipkow@61640 ` 184` ``` inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')" ``` nipkow@61640 ` 185` ```by(induct l a m b r' rule: node33.induct) auto ``` nipkow@61640 ` 186` nipkow@61640 ` 187` ```lemmas inorder_nodes = inorder_node21 inorder_node22 ``` nipkow@61640 ` 188` ``` inorder_node31 inorder_node32 inorder_node33 ``` nipkow@61640 ` 189` nipkow@68020 ` 190` ```lemma split_minD: ``` nipkow@68020 ` 191` ``` "split_min t = (x,t') \ bal t \ height t > 0 \ ``` nipkow@61640 ` 192` ``` x # inorder(tree\<^sub>d t') = inorder t" ``` nipkow@68020 ` 193` ```by(induction t arbitrary: t' rule: split_min.induct) ``` nipkow@61640 ` 194` ``` (auto simp: inorder_nodes split: prod.splits) ``` nipkow@61640 ` 195` nipkow@61640 ` 196` ```lemma inorder_del: "\ bal t ; sorted(inorder t) \ \ ``` nipkow@61640 ` 197` ``` inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" ``` nipkow@61640 ` 198` ```by(induction t rule: del.induct) ``` nipkow@68020 ` 199` ``` (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) ``` nipkow@61640 ` 200` nipkow@61640 ` 201` ```lemma inorder_delete: "\ bal t ; sorted(inorder t) \ \ ``` nipkow@61640 ` 202` ``` inorder(delete x t) = del_list x (inorder t)" ``` nipkow@61640 ` 203` ```by(simp add: delete_def inorder_del) ``` nipkow@61640 ` 204` nipkow@61640 ` 205` nipkow@61640 ` 206` ```subsection \Balancedness\ ``` nipkow@61640 ` 207` nipkow@61640 ` 208` nipkow@61640 ` 209` ```subsubsection "Proofs for insert" ``` nipkow@61640 ` 210` wenzelm@67406 ` 211` ```text\First a standard proof that @{const ins} preserves @{const bal}.\ ``` nipkow@61640 ` 212` nipkow@61640 ` 213` ```instantiation up\<^sub>i :: (type)height ``` nipkow@61640 ` 214` ```begin ``` nipkow@61640 ` 215` nipkow@61640 ` 216` ```fun height_up\<^sub>i :: "'a up\<^sub>i \ nat" where ``` nipkow@61640 ` 217` ```"height (T\<^sub>i t) = height t" | ``` nipkow@61640 ` 218` ```"height (Up\<^sub>i l a r) = height l" ``` nipkow@61640 ` 219` nipkow@61640 ` 220` ```instance .. ``` nipkow@61640 ` 221` nipkow@61640 ` 222` ```end ``` nipkow@61640 ` 223` nipkow@61640 ` 224` ```lemma bal_ins: "bal t \ bal (tree\<^sub>i(ins a t)) \ height(ins a t) = height t" ``` nipkow@63636 ` 225` ```by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *) ``` nipkow@61640 ` 226` wenzelm@67406 ` 227` ```text\Now an alternative proof (by Brian Huffman) that runs faster because ``` wenzelm@67406 ` 228` ```two properties (balance and height) are combined in one predicate.\ ``` nipkow@61640 ` 229` nipkow@61640 ` 230` ```inductive full :: "nat \ 'a tree23 \ bool" where ``` nipkow@61640 ` 231` ```"full 0 Leaf" | ``` nipkow@61640 ` 232` ```"\full n l; full n r\ \ full (Suc n) (Node2 l p r)" | ``` nipkow@61640 ` 233` ```"\full n l; full n m; full n r\ \ full (Suc n) (Node3 l p m q r)" ``` nipkow@61640 ` 234` nipkow@61640 ` 235` ```inductive_cases full_elims: ``` nipkow@61640 ` 236` ``` "full n Leaf" ``` nipkow@61640 ` 237` ``` "full n (Node2 l p r)" ``` nipkow@61640 ` 238` ``` "full n (Node3 l p m q r)" ``` nipkow@61640 ` 239` nipkow@61640 ` 240` ```inductive_cases full_0_elim: "full 0 t" ``` nipkow@61640 ` 241` ```inductive_cases full_Suc_elim: "full (Suc n) t" ``` nipkow@61640 ` 242` nipkow@61640 ` 243` ```lemma full_0_iff [simp]: "full 0 t \ t = Leaf" ``` nipkow@61640 ` 244` ``` by (auto elim: full_0_elim intro: full.intros) ``` nipkow@61640 ` 245` nipkow@61640 ` 246` ```lemma full_Leaf_iff [simp]: "full n Leaf \ n = 0" ``` nipkow@61640 ` 247` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 248` nipkow@61640 ` 249` ```lemma full_Suc_Node2_iff [simp]: ``` nipkow@61640 ` 250` ``` "full (Suc n) (Node2 l p r) \ full n l \ full n r" ``` nipkow@61640 ` 251` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 252` nipkow@61640 ` 253` ```lemma full_Suc_Node3_iff [simp]: ``` nipkow@61640 ` 254` ``` "full (Suc n) (Node3 l p m q r) \ full n l \ full n m \ full n r" ``` nipkow@61640 ` 255` ``` by (auto elim: full_elims intro: full.intros) ``` nipkow@61640 ` 256` nipkow@61640 ` 257` ```lemma full_imp_height: "full n t \ height t = n" ``` nipkow@61640 ` 258` ``` by (induct set: full, simp_all) ``` nipkow@61640 ` 259` nipkow@61640 ` 260` ```lemma full_imp_bal: "full n t \ bal t" ``` nipkow@61640 ` 261` ``` by (induct set: full, auto dest: full_imp_height) ``` nipkow@61640 ` 262` nipkow@61640 ` 263` ```lemma bal_imp_full: "bal t \ full (height t) t" ``` nipkow@61640 ` 264` ``` by (induct t, simp_all) ``` nipkow@61640 ` 265` nipkow@61640 ` 266` ```lemma bal_iff_full: "bal t \ (\n. full n t)" ``` nipkow@61640 ` 267` ``` by (auto elim!: bal_imp_full full_imp_bal) ``` nipkow@61640 ` 268` wenzelm@67406 ` 269` ```text \The @{const "insert"} function either preserves the height of the ``` nipkow@61640 ` 270` ```tree, or increases it by one. The constructor returned by the @{term ``` nipkow@61640 ` 271` ```"insert"} function determines which: A return value of the form @{term ``` nipkow@61640 ` 272` ```"T\<^sub>i t"} indicates that the height will be the same. A value of the ``` wenzelm@67406 ` 273` ```form @{term "Up\<^sub>i l p r"} indicates an increase in height.\ ``` nipkow@61640 ` 274` nipkow@61640 ` 275` ```fun full\<^sub>i :: "nat \ 'a up\<^sub>i \ bool" where ``` nipkow@61640 ` 276` ```"full\<^sub>i n (T\<^sub>i t) \ full n t" | ``` nipkow@61640 ` 277` ```"full\<^sub>i n (Up\<^sub>i l p r) \ full n l \ full n r" ``` nipkow@61640 ` 278` nipkow@61640 ` 279` ```lemma full\<^sub>i_ins: "full n t \ full\<^sub>i n (ins a t)" ``` nipkow@61640 ` 280` ```by (induct rule: full.induct) (auto split: up\<^sub>i.split) ``` nipkow@61640 ` 281` wenzelm@67406 ` 282` ```text \The @{const insert} operation preserves balance.\ ``` nipkow@61640 ` 283` nipkow@61640 ` 284` ```lemma bal_insert: "bal t \ bal (insert a t)" ``` nipkow@61640 ` 285` ```unfolding bal_iff_full insert_def ``` nipkow@61640 ` 286` ```apply (erule exE) ``` nipkow@61640 ` 287` ```apply (drule full\<^sub>i_ins [of _ _ a]) ``` nipkow@61640 ` 288` ```apply (cases "ins a t") ``` nipkow@61640 ` 289` ```apply (auto intro: full.intros) ``` nipkow@61640 ` 290` ```done ``` nipkow@61640 ` 291` nipkow@61640 ` 292` nipkow@61640 ` 293` ```subsection "Proofs for delete" ``` nipkow@61640 ` 294` nipkow@61640 ` 295` ```instantiation up\<^sub>d :: (type)height ``` nipkow@61640 ` 296` ```begin ``` nipkow@61640 ` 297` nipkow@61640 ` 298` ```fun height_up\<^sub>d :: "'a up\<^sub>d \ nat" where ``` nipkow@61640 ` 299` ```"height (T\<^sub>d t) = height t" | ``` nipkow@61640 ` 300` ```"height (Up\<^sub>d t) = height t + 1" ``` nipkow@61640 ` 301` nipkow@61640 ` 302` ```instance .. ``` nipkow@61640 ` 303` nipkow@61640 ` 304` ```end ``` nipkow@61640 ` 305` nipkow@61640 ` 306` ```lemma bal_tree\<^sub>d_node21: ``` nipkow@61640 ` 307` ``` "\bal r; bal (tree\<^sub>d l'); height r = height l' \ \ bal (tree\<^sub>d (node21 l' a r))" ``` nipkow@61640 ` 308` ```by(induct l' a r rule: node21.induct) auto ``` nipkow@61640 ` 309` nipkow@61640 ` 310` ```lemma bal_tree\<^sub>d_node22: ``` nipkow@61640 ` 311` ``` "\bal(tree\<^sub>d r'); bal l; height r' = height l \ \ bal (tree\<^sub>d (node22 l a r'))" ``` nipkow@61640 ` 312` ```by(induct l a r' rule: node22.induct) auto ``` nipkow@61640 ` 313` nipkow@61640 ` 314` ```lemma bal_tree\<^sub>d_node31: ``` nipkow@61640 ` 315` ``` "\ bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \ ``` nipkow@61640 ` 316` ``` \ bal (tree\<^sub>d (node31 l' a m b r))" ``` nipkow@61640 ` 317` ```by(induct l' a m b r rule: node31.induct) auto ``` nipkow@61640 ` 318` nipkow@61640 ` 319` ```lemma bal_tree\<^sub>d_node32: ``` nipkow@61640 ` 320` ``` "\ bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \ ``` nipkow@61640 ` 321` ``` \ bal (tree\<^sub>d (node32 l a m' b r))" ``` nipkow@61640 ` 322` ```by(induct l a m' b r rule: node32.induct) auto ``` nipkow@61640 ` 323` nipkow@61640 ` 324` ```lemma bal_tree\<^sub>d_node33: ``` nipkow@61640 ` 325` ``` "\ bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \ ``` nipkow@61640 ` 326` ``` \ bal (tree\<^sub>d (node33 l a m b r'))" ``` nipkow@61640 ` 327` ```by(induct l a m b r' rule: node33.induct) auto ``` nipkow@61640 ` 328` nipkow@61640 ` 329` ```lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22 ``` nipkow@61640 ` 330` ``` bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33 ``` nipkow@61640 ` 331` nipkow@61640 ` 332` ```lemma height'_node21: ``` nipkow@61640 ` 333` ``` "height r > 0 \ height(node21 l' a r) = max (height l') (height r) + 1" ``` nipkow@61640 ` 334` ```by(induct l' a r rule: node21.induct)(simp_all) ``` nipkow@61640 ` 335` nipkow@61640 ` 336` ```lemma height'_node22: ``` nipkow@61640 ` 337` ``` "height l > 0 \ height(node22 l a r') = max (height l) (height r') + 1" ``` nipkow@61640 ` 338` ```by(induct l a r' rule: node22.induct)(simp_all) ``` nipkow@61640 ` 339` nipkow@61640 ` 340` ```lemma height'_node31: ``` nipkow@61640 ` 341` ``` "height m > 0 \ height(node31 l a m b r) = ``` nipkow@61640 ` 342` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 343` ```by(induct l a m b r rule: node31.induct)(simp_all add: max_def) ``` nipkow@61640 ` 344` nipkow@61640 ` 345` ```lemma height'_node32: ``` nipkow@61640 ` 346` ``` "height r > 0 \ height(node32 l a m b r) = ``` nipkow@61640 ` 347` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 348` ```by(induct l a m b r rule: node32.induct)(simp_all add: max_def) ``` nipkow@61640 ` 349` nipkow@61640 ` 350` ```lemma height'_node33: ``` nipkow@61640 ` 351` ``` "height m > 0 \ height(node33 l a m b r) = ``` nipkow@61640 ` 352` ``` max (height l) (max (height m) (height r)) + 1" ``` nipkow@61640 ` 353` ```by(induct l a m b r rule: node33.induct)(simp_all add: max_def) ``` nipkow@61640 ` 354` nipkow@61640 ` 355` ```lemmas heights = height'_node21 height'_node22 ``` nipkow@61640 ` 356` ``` height'_node31 height'_node32 height'_node33 ``` nipkow@61640 ` 357` nipkow@68020 ` 358` ```lemma height_split_min: ``` nipkow@68020 ` 359` ``` "split_min t = (x, t') \ height t > 0 \ bal t \ height t' = height t" ``` nipkow@68020 ` 360` ```by(induct t arbitrary: x t' rule: split_min.induct) ``` nipkow@61640 ` 361` ``` (auto simp: heights split: prod.splits) ``` nipkow@61640 ` 362` nipkow@61640 ` 363` ```lemma height_del: "bal t \ height(del x t) = height t" ``` nipkow@61640 ` 364` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 365` ``` (auto simp: heights max_def height_split_min split: prod.splits) ``` nipkow@61640 ` 366` nipkow@68020 ` 367` ```lemma bal_split_min: ``` nipkow@68020 ` 368` ``` "\ split_min t = (x, t'); bal t; height t > 0 \ \ bal (tree\<^sub>d t')" ``` nipkow@68020 ` 369` ```by(induct t arbitrary: x t' rule: split_min.induct) ``` nipkow@68020 ` 370` ``` (auto simp: heights height_split_min bals split: prod.splits) ``` nipkow@61640 ` 371` nipkow@61640 ` 372` ```lemma bal_tree\<^sub>d_del: "bal t \ bal(tree\<^sub>d(del x t))" ``` nipkow@61640 ` 373` ```by(induction x t rule: del.induct) ``` nipkow@68020 ` 374` ``` (auto simp: bals bal_split_min height_del height_split_min split: prod.splits) ``` nipkow@61640 ` 375` nipkow@61640 ` 376` ```corollary bal_delete: "bal t \ bal(delete x t)" ``` nipkow@61640 ` 377` ```by(simp add: delete_def bal_tree\<^sub>d_del) ``` nipkow@61640 ` 378` nipkow@61640 ` 379` nipkow@61640 ` 380` ```subsection \Overall Correctness\ ``` nipkow@61640 ` 381` nipkow@68440 ` 382` ```interpretation S: Set_by_Ordered ``` nipkow@68431 ` 383` ```where empty = empty and isin = isin and insert = insert and delete = delete ``` nipkow@61640 ` 384` ```and inorder = inorder and inv = bal ``` nipkow@61640 ` 385` ```proof (standard, goal_cases) ``` nipkow@61640 ` 386` ``` case 2 thus ?case by(simp add: isin_set) ``` nipkow@61640 ` 387` ```next ``` nipkow@61640 ` 388` ``` case 3 thus ?case by(simp add: inorder_insert) ``` nipkow@61640 ` 389` ```next ``` nipkow@61640 ` 390` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61640 ` 391` ```next ``` nipkow@61640 ` 392` ``` case 6 thus ?case by(simp add: bal_insert) ``` nipkow@61640 ` 393` ```next ``` nipkow@61640 ` 394` ``` case 7 thus ?case by(simp add: bal_delete) ``` nipkow@68431 ` 395` ```qed (simp add: empty_def)+ ``` nipkow@61640 ` 396` nipkow@61640 ` 397` ```end ```