src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Mon Apr 23 08:09:50 2018 +0200 (15 months ago) changeset 68023 75130777ece4 parent 67967 5a4280946a25 child 68313 56c57e91edf9 permissions -rw-r--r--
del_max -> split_max
 nipkow@61232 ` 1` ```(* ``` nipkow@63411 ` 2` ```Author: Tobias Nipkow, Daniel StÃ¼we ``` nipkow@63411 ` 3` ```Largely derived from AFP entry AVL. ``` nipkow@61232 ` 4` ```*) ``` nipkow@61232 ` 5` nipkow@61232 ` 6` ```section "AVL Tree Implementation of Sets" ``` nipkow@61232 ` 7` nipkow@61232 ` 8` ```theory AVL_Set ``` nipkow@63411 ` 9` ```imports ``` nipkow@67964 ` 10` ``` Cmp ``` nipkow@67964 ` 11` ``` Isin2 ``` wenzelm@66453 ` 12` ``` "HOL-Number_Theory.Fib" ``` nipkow@61232 ` 13` ```begin ``` nipkow@61232 ` 14` nipkow@61232 ` 15` ```type_synonym 'a avl_tree = "('a,nat) tree" ``` nipkow@61232 ` 16` wenzelm@67406 ` 17` ```text \Invariant:\ ``` nipkow@61232 ` 18` nipkow@61232 ` 19` ```fun avl :: "'a avl_tree \ bool" where ``` nipkow@61232 ` 20` ```"avl Leaf = True" | ``` nipkow@61232 ` 21` ```"avl (Node h l a r) = ``` nipkow@61232 ` 22` ``` ((height l = height r \ height l = height r + 1 \ height r = height l + 1) \ ``` nipkow@61232 ` 23` ``` h = max (height l) (height r) + 1 \ avl l \ avl r)" ``` nipkow@61232 ` 24` nipkow@61232 ` 25` ```fun ht :: "'a avl_tree \ nat" where ``` nipkow@61232 ` 26` ```"ht Leaf = 0" | ``` nipkow@61232 ` 27` ```"ht (Node h l a r) = h" ``` nipkow@61232 ` 28` nipkow@61232 ` 29` ```definition node :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 30` ```"node l a r = Node (max (ht l) (ht r) + 1) l a r" ``` nipkow@61232 ` 31` nipkow@61581 ` 32` ```definition balL :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61678 ` 33` ```"balL l a r = ``` nipkow@61678 ` 34` ``` (if ht l = ht r + 2 then ``` nipkow@61678 ` 35` ``` case l of ``` nipkow@61678 ` 36` ``` Node _ bl b br \ ``` nipkow@61678 ` 37` ``` if ht bl < ht br then ``` nipkow@61678 ` 38` ``` case br of ``` nipkow@61678 ` 39` ``` Node _ cl c cr \ node (node bl b cl) c (node cr a r) ``` nipkow@61678 ` 40` ``` else node bl b (node br a r) ``` nipkow@61678 ` 41` ``` else node l a r)" ``` nipkow@61232 ` 42` nipkow@61581 ` 43` ```definition balR :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61678 ` 44` ```"balR l a r = ``` nipkow@61678 ` 45` ``` (if ht r = ht l + 2 then ``` nipkow@61678 ` 46` ``` case r of ``` nipkow@61678 ` 47` ``` Node _ bl b br \ ``` nipkow@61678 ` 48` ``` if ht bl > ht br then ``` nipkow@61678 ` 49` ``` case bl of ``` nipkow@61678 ` 50` ``` Node _ cl c cr \ node (node l a cl) c (node cr b br) ``` nipkow@61678 ` 51` ``` else node (node l a bl) b br ``` nipkow@61232 ` 52` ``` else node l a r)" ``` nipkow@61232 ` 53` nipkow@63411 ` 54` ```fun insert :: "'a::linorder \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 55` ```"insert x Leaf = Node 1 Leaf x Leaf" | ``` nipkow@61581 ` 56` ```"insert x (Node h l a r) = (case cmp x a of ``` nipkow@61581 ` 57` ``` EQ \ Node h l a r | ``` nipkow@61581 ` 58` ``` LT \ balL (insert x l) a r | ``` nipkow@61581 ` 59` ``` GT \ balR l a (insert x r))" ``` nipkow@61232 ` 60` nipkow@68023 ` 61` ```fun split_max :: "'a avl_tree \ 'a avl_tree * 'a" where ``` nipkow@68023 ` 62` ```"split_max (Node _ l a r) = ``` nipkow@68023 ` 63` ``` (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))" ``` nipkow@61232 ` 64` nipkow@68023 ` 65` ```lemmas split_max_induct = split_max.induct[case_names Node Leaf] ``` nipkow@61232 ` 66` nipkow@61647 ` 67` ```fun del_root :: "'a avl_tree \ 'a avl_tree" where ``` nipkow@61647 ` 68` ```"del_root (Node h Leaf a r) = r" | ``` nipkow@61647 ` 69` ```"del_root (Node h l a Leaf) = l" | ``` nipkow@68023 ` 70` ```"del_root (Node h l a r) = (let (l', a') = split_max l in balR l' a' r)" ``` nipkow@61232 ` 71` nipkow@61647 ` 72` ```lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node] ``` nipkow@61232 ` 73` nipkow@63411 ` 74` ```fun delete :: "'a::linorder \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 75` ```"delete _ Leaf = Leaf" | ``` nipkow@61678 ` 76` ```"delete x (Node h l a r) = ``` nipkow@61678 ` 77` ``` (case cmp x a of ``` nipkow@61678 ` 78` ``` EQ \ del_root (Node h l a r) | ``` nipkow@61678 ` 79` ``` LT \ balR (delete x l) a r | ``` nipkow@61678 ` 80` ``` GT \ balL l a (delete x r))" ``` nipkow@61232 ` 81` nipkow@61232 ` 82` wenzelm@67406 ` 83` ```subsection \Functional Correctness Proofs\ ``` nipkow@61232 ` 84` wenzelm@67406 ` 85` ```text\Very different from the AFP/AVL proofs\ ``` nipkow@61232 ` 86` nipkow@61232 ` 87` nipkow@61232 ` 88` ```subsubsection "Proofs for insert" ``` nipkow@61232 ` 89` nipkow@61581 ` 90` ```lemma inorder_balL: ``` nipkow@61581 ` 91` ``` "inorder (balL l a r) = inorder l @ a # inorder r" ``` nipkow@61581 ` 92` ```by (auto simp: node_def balL_def split:tree.splits) ``` nipkow@61232 ` 93` nipkow@61581 ` 94` ```lemma inorder_balR: ``` nipkow@61581 ` 95` ``` "inorder (balR l a r) = inorder l @ a # inorder r" ``` nipkow@61581 ` 96` ```by (auto simp: node_def balR_def split:tree.splits) ``` nipkow@61232 ` 97` nipkow@61232 ` 98` ```theorem inorder_insert: ``` nipkow@61232 ` 99` ``` "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" ``` nipkow@61232 ` 100` ```by (induct t) ``` nipkow@61581 ` 101` ``` (auto simp: ins_list_simps inorder_balL inorder_balR) ``` nipkow@61232 ` 102` nipkow@61232 ` 103` nipkow@61232 ` 104` ```subsubsection "Proofs for delete" ``` nipkow@61232 ` 105` nipkow@68023 ` 106` ```lemma inorder_split_maxD: ``` nipkow@68023 ` 107` ``` "\ split_max t = (t',a); t \ Leaf \ \ ``` nipkow@61232 ` 108` ``` inorder t' @ [a] = inorder t" ``` nipkow@68023 ` 109` ```by(induction t arbitrary: t' rule: split_max.induct) ``` nipkow@61647 ` 110` ``` (auto simp: inorder_balL split: if_splits prod.splits tree.split) ``` nipkow@61232 ` 111` nipkow@61647 ` 112` ```lemma inorder_del_root: ``` nipkow@61647 ` 113` ``` "inorder (del_root (Node h l a r)) = inorder l @ inorder r" ``` nipkow@62526 ` 114` ```by(cases "Node h l a r" rule: del_root.cases) ``` nipkow@68023 ` 115` ``` (auto simp: inorder_balL inorder_balR inorder_split_maxD split: if_splits prod.splits) ``` nipkow@61232 ` 116` nipkow@61232 ` 117` ```theorem inorder_delete: ``` nipkow@61232 ` 118` ``` "sorted(inorder t) \ inorder (delete x t) = del_list x (inorder t)" ``` nipkow@61232 ` 119` ```by(induction t) ``` nipkow@61581 ` 120` ``` (auto simp: del_list_simps inorder_balL inorder_balR ``` nipkow@68023 ` 121` ``` inorder_del_root inorder_split_maxD split: prod.splits) ``` nipkow@61232 ` 122` nipkow@61232 ` 123` nipkow@61232 ` 124` ```subsubsection "Overall functional correctness" ``` nipkow@61232 ` 125` nipkow@61232 ` 126` ```interpretation Set_by_Ordered ``` nipkow@61232 ` 127` ```where empty = Leaf and isin = isin and insert = insert and delete = delete ``` nipkow@61588 ` 128` ```and inorder = inorder and inv = "\_. True" ``` nipkow@61232 ` 129` ```proof (standard, goal_cases) ``` nipkow@61232 ` 130` ``` case 1 show ?case by simp ``` nipkow@61232 ` 131` ```next ``` nipkow@67967 ` 132` ``` case 2 thus ?case by(simp add: isin_set_inorder) ``` nipkow@61232 ` 133` ```next ``` nipkow@61232 ` 134` ``` case 3 thus ?case by(simp add: inorder_insert) ``` nipkow@61232 ` 135` ```next ``` nipkow@61232 ` 136` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61428 ` 137` ```qed (rule TrueI)+ ``` nipkow@61232 ` 138` nipkow@61232 ` 139` wenzelm@67406 ` 140` ```subsection \AVL invariants\ ``` nipkow@61232 ` 141` wenzelm@67406 ` 142` ```text\Essentially the AFP/AVL proofs\ ``` nipkow@61232 ` 143` nipkow@61232 ` 144` wenzelm@67406 ` 145` ```subsubsection \Insertion maintains AVL balance\ ``` nipkow@61232 ` 146` nipkow@61232 ` 147` ```declare Let_def [simp] ``` nipkow@61232 ` 148` nipkow@61232 ` 149` ```lemma [simp]: "avl t \ ht t = height t" ``` nipkow@61232 ` 150` ```by (induct t) simp_all ``` nipkow@61232 ` 151` nipkow@61581 ` 152` ```lemma height_balL: ``` nipkow@61232 ` 153` ``` "\ height l = height r + 2; avl l; avl r \ \ ``` nipkow@61581 ` 154` ``` height (balL l a r) = height r + 2 \ ``` nipkow@61581 ` 155` ``` height (balL l a r) = height r + 3" ``` nipkow@61581 ` 156` ```by (cases l) (auto simp:node_def balL_def split:tree.split) ``` nipkow@61232 ` 157` ``` ``` nipkow@61581 ` 158` ```lemma height_balR: ``` nipkow@61232 ` 159` ``` "\ height r = height l + 2; avl l; avl r \ \ ``` nipkow@61581 ` 160` ``` height (balR l a r) = height l + 2 \ ``` nipkow@61581 ` 161` ``` height (balR l a r) = height l + 3" ``` nipkow@61581 ` 162` ```by (cases r) (auto simp add:node_def balR_def split:tree.split) ``` nipkow@61232 ` 163` nipkow@61232 ` 164` ```lemma [simp]: "height(node l a r) = max (height l) (height r) + 1" ``` nipkow@61232 ` 165` ```by (simp add: node_def) ``` nipkow@61232 ` 166` nipkow@61232 ` 167` ```lemma avl_node: ``` nipkow@61232 ` 168` ``` "\ avl l; avl r; ``` nipkow@61232 ` 169` ``` height l = height r \ height l = height r + 1 \ height r = height l + 1 ``` nipkow@61232 ` 170` ``` \ \ avl(node l a r)" ``` nipkow@61232 ` 171` ```by (auto simp add:max_def node_def) ``` nipkow@61232 ` 172` nipkow@61581 ` 173` ```lemma height_balL2: ``` nipkow@61232 ` 174` ``` "\ avl l; avl r; height l \ height r + 2 \ \ ``` nipkow@61581 ` 175` ``` height (balL l a r) = (1 + max (height l) (height r))" ``` nipkow@61581 ` 176` ```by (cases l, cases r) (simp_all add: balL_def) ``` nipkow@61232 ` 177` nipkow@61581 ` 178` ```lemma height_balR2: ``` nipkow@61232 ` 179` ``` "\ avl l; avl r; height r \ height l + 2 \ \ ``` nipkow@61581 ` 180` ``` height (balR l a r) = (1 + max (height l) (height r))" ``` nipkow@61581 ` 181` ```by (cases l, cases r) (simp_all add: balR_def) ``` nipkow@61232 ` 182` nipkow@61581 ` 183` ```lemma avl_balL: ``` nipkow@61232 ` 184` ``` assumes "avl l" "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 185` ``` \ height r = height l + 1 \ height l = height r + 2" ``` nipkow@61581 ` 186` ``` shows "avl(balL l a r)" ``` nipkow@61232 ` 187` ```proof(cases l) ``` nipkow@61232 ` 188` ``` case Leaf ``` nipkow@61581 ` 189` ``` with assms show ?thesis by (simp add: node_def balL_def) ``` nipkow@61232 ` 190` ```next ``` nipkow@61232 ` 191` ``` case (Node ln ll lr lh) ``` nipkow@61232 ` 192` ``` with assms show ?thesis ``` nipkow@61232 ` 193` ``` proof(cases "height l = height r + 2") ``` nipkow@61232 ` 194` ``` case True ``` nipkow@61232 ` 195` ``` from True Node assms show ?thesis ``` nipkow@61581 ` 196` ``` by (auto simp: balL_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 197` ``` next ``` nipkow@61232 ` 198` ``` case False ``` nipkow@61581 ` 199` ``` with assms show ?thesis by (simp add: avl_node balL_def) ``` nipkow@61232 ` 200` ``` qed ``` nipkow@61232 ` 201` ```qed ``` nipkow@61232 ` 202` nipkow@61581 ` 203` ```lemma avl_balR: ``` nipkow@61232 ` 204` ``` assumes "avl l" and "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 205` ``` \ height r = height l + 1 \ height r = height l + 2" ``` nipkow@61581 ` 206` ``` shows "avl(balR l a r)" ``` nipkow@61232 ` 207` ```proof(cases r) ``` nipkow@61232 ` 208` ``` case Leaf ``` nipkow@61581 ` 209` ``` with assms show ?thesis by (simp add: node_def balR_def) ``` nipkow@61232 ` 210` ```next ``` nipkow@61232 ` 211` ``` case (Node rn rl rr rh) ``` nipkow@61232 ` 212` ``` with assms show ?thesis ``` nipkow@61232 ` 213` ``` proof(cases "height r = height l + 2") ``` nipkow@61232 ` 214` ``` case True ``` nipkow@61232 ` 215` ``` from True Node assms show ?thesis ``` nipkow@61581 ` 216` ``` by (auto simp: balR_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 217` ``` next ``` nipkow@61232 ` 218` ``` case False ``` nipkow@61581 ` 219` ``` with assms show ?thesis by (simp add: balR_def avl_node) ``` nipkow@61232 ` 220` ``` qed ``` nipkow@61232 ` 221` ```qed ``` nipkow@61232 ` 222` nipkow@61232 ` 223` ```(* It appears that these two properties need to be proved simultaneously: *) ``` nipkow@61232 ` 224` wenzelm@67406 ` 225` ```text\Insertion maintains the AVL property:\ ``` nipkow@61232 ` 226` nipkow@61232 ` 227` ```theorem avl_insert_aux: ``` nipkow@61232 ` 228` ``` assumes "avl t" ``` nipkow@61232 ` 229` ``` shows "avl(insert x t)" ``` nipkow@61232 ` 230` ``` "(height (insert x t) = height t \ height (insert x t) = height t + 1)" ``` nipkow@61232 ` 231` ```using assms ``` nipkow@61232 ` 232` ```proof (induction t) ``` nipkow@61232 ` 233` ``` case (Node h l a r) ``` nipkow@61232 ` 234` ``` case 1 ``` nipkow@61232 ` 235` ``` with Node show ?case ``` nipkow@61232 ` 236` ``` proof(cases "x = a") ``` nipkow@61232 ` 237` ``` case True ``` nipkow@61232 ` 238` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 239` ``` next ``` nipkow@61232 ` 240` ``` case False ``` nipkow@61232 ` 241` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 242` ``` proof(cases "xx\a\ show ?thesis by (auto simp add:avl_balR) ``` nipkow@61232 ` 248` ``` qed ``` nipkow@61232 ` 249` ``` qed ``` nipkow@61232 ` 250` ``` case 2 ``` nipkow@61232 ` 251` ``` from 2 Node show ?case ``` nipkow@61232 ` 252` ``` proof(cases "x = a") ``` nipkow@61232 ` 253` ``` case True ``` nipkow@61232 ` 254` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 255` ``` next ``` nipkow@61232 ` 256` ``` case False ``` nipkow@61232 ` 257` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 258` ``` proof(cases "xx < a\ show ?thesis by (auto simp: height_balL2) ``` nipkow@61232 ` 263` ``` next ``` nipkow@61232 ` 264` ``` case True ``` nipkow@61581 ` 265` ``` hence "(height (balL (insert x l) a r) = height r + 2) \ ``` nipkow@61581 ` 266` ``` (height (balL (insert x l) a r) = height r + 3)" (is "?A \ ?B") ``` nipkow@61581 ` 267` ``` using Node 2 by (intro height_balL) simp_all ``` nipkow@61232 ` 268` ``` thus ?thesis ``` nipkow@61232 ` 269` ``` proof ``` nipkow@61232 ` 270` ``` assume ?A ``` wenzelm@67406 ` 271` ``` with 2 \x < a\ show ?thesis by (auto) ``` nipkow@61232 ` 272` ``` next ``` nipkow@61232 ` 273` ``` assume ?B ``` wenzelm@67406 ` 274` ``` with True 1 Node(2) \x < a\ show ?thesis by (simp) arith ``` nipkow@61232 ` 275` ``` qed ``` nipkow@61232 ` 276` ``` qed ``` nipkow@61232 ` 277` ``` next ``` nipkow@61232 ` 278` ``` case False ``` nipkow@61232 ` 279` ``` with Node 2 show ?thesis ``` nipkow@61232 ` 280` ``` proof(cases "height (insert x r) = height l + 2") ``` nipkow@61232 ` 281` ``` case False ``` wenzelm@67406 ` 282` ``` with Node 2 \\x < a\ show ?thesis by (auto simp: height_balR2) ``` nipkow@61232 ` 283` ``` next ``` nipkow@61232 ` 284` ``` case True ``` nipkow@61581 ` 285` ``` hence "(height (balR l a (insert x r)) = height l + 2) \ ``` nipkow@61581 ` 286` ``` (height (balR l a (insert x r)) = height l + 3)" (is "?A \ ?B") ``` nipkow@61581 ` 287` ``` using Node 2 by (intro height_balR) simp_all ``` nipkow@61232 ` 288` ``` thus ?thesis ``` nipkow@61232 ` 289` ``` proof ``` nipkow@61232 ` 290` ``` assume ?A ``` wenzelm@67406 ` 291` ``` with 2 \\x < a\ show ?thesis by (auto) ``` nipkow@61232 ` 292` ``` next ``` nipkow@61232 ` 293` ``` assume ?B ``` wenzelm@67406 ` 294` ``` with True 1 Node(4) \\x < a\ show ?thesis by (simp) arith ``` nipkow@61232 ` 295` ``` qed ``` nipkow@61232 ` 296` ``` qed ``` nipkow@61232 ` 297` ``` qed ``` nipkow@61232 ` 298` ``` qed ``` nipkow@61232 ` 299` ```qed simp_all ``` nipkow@61232 ` 300` nipkow@61232 ` 301` wenzelm@67406 ` 302` ```subsubsection \Deletion maintains AVL balance\ ``` nipkow@61232 ` 303` nipkow@68023 ` 304` ```lemma avl_split_max: ``` nipkow@61232 ` 305` ``` assumes "avl x" and "x \ Leaf" ``` nipkow@68023 ` 306` ``` shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \ ``` nipkow@68023 ` 307` ``` height x = height(fst (split_max x)) + 1" ``` nipkow@61232 ` 308` ```using assms ``` nipkow@68023 ` 309` ```proof (induct x rule: split_max_induct) ``` nipkow@61647 ` 310` ``` case (Node h l a r) ``` nipkow@61232 ` 311` ``` case 1 ``` nipkow@61647 ` 312` ``` thus ?case using Node ``` nipkow@61647 ` 313` ``` by (auto simp: height_balL height_balL2 avl_balL ``` nipkow@61232 ` 314` ``` linorder_class.max.absorb1 linorder_class.max.absorb2 ``` nipkow@61232 ` 315` ``` split:prod.split) ``` nipkow@61232 ` 316` ```next ``` nipkow@61647 ` 317` ``` case (Node h l a r) ``` nipkow@61232 ` 318` ``` case 2 ``` nipkow@68023 ` 319` ``` let ?r' = "fst (split_max r)" ``` wenzelm@67406 ` 320` ``` from \avl x\ Node 2 have "avl l" and "avl r" by simp_all ``` nipkow@61581 ` 321` ``` thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] ``` nipkow@61232 ` 322` ``` apply (auto split:prod.splits simp del:avl.simps) by arith+ ``` nipkow@61232 ` 323` ```qed auto ``` nipkow@61232 ` 324` nipkow@61647 ` 325` ```lemma avl_del_root: ``` nipkow@61232 ` 326` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61647 ` 327` ``` shows "avl(del_root t)" ``` nipkow@61232 ` 328` ```using assms ``` nipkow@61647 ` 329` ```proof (cases t rule:del_root_cases) ``` nipkow@61232 ` 330` ``` case (Node_Node h lh ll ln lr n rh rl rn rr) ``` nipkow@61232 ` 331` ``` let ?l = "Node lh ll ln lr" ``` nipkow@61232 ` 332` ``` let ?r = "Node rh rl rn rr" ``` nipkow@68023 ` 333` ``` let ?l' = "fst (split_max ?l)" ``` wenzelm@67406 ` 334` ``` from \avl t\ and Node_Node have "avl ?r" by simp ``` wenzelm@67406 ` 335` ``` from \avl t\ and Node_Node have "avl ?l" by simp ``` nipkow@61232 ` 336` ``` hence "avl(?l')" "height ?l = height(?l') \ ``` nipkow@68023 ` 337` ``` height ?l = height(?l') + 1" by (rule avl_split_max,simp)+ ``` wenzelm@67406 ` 338` ``` with \avl t\ Node_Node have "height ?l' = height ?r \ height ?l' = height ?r + 1 ``` nipkow@61232 ` 339` ``` \ height ?r = height ?l' + 1 \ height ?r = height ?l' + 2" by fastforce ``` nipkow@68023 ` 340` ``` with \avl ?l'\ \avl ?r\ have "avl(balR ?l' (snd(split_max ?l)) ?r)" ``` nipkow@61581 ` 341` ``` by (rule avl_balR) ``` nipkow@61232 ` 342` ``` with Node_Node show ?thesis by (auto split:prod.splits) ``` nipkow@61232 ` 343` ```qed simp_all ``` nipkow@61232 ` 344` nipkow@61647 ` 345` ```lemma height_del_root: ``` nipkow@61232 ` 346` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61647 ` 347` ``` shows "height t = height(del_root t) \ height t = height(del_root t) + 1" ``` nipkow@61232 ` 348` ```using assms ``` nipkow@61647 ` 349` ```proof (cases t rule: del_root_cases) ``` nipkow@61232 ` 350` ``` case (Node_Node h lh ll ln lr n rh rl rn rr) ``` nipkow@61232 ` 351` ``` let ?l = "Node lh ll ln lr" ``` nipkow@61232 ` 352` ``` let ?r = "Node rh rl rn rr" ``` nipkow@68023 ` 353` ``` let ?l' = "fst (split_max ?l)" ``` nipkow@68023 ` 354` ``` let ?t' = "balR ?l' (snd(split_max ?l)) ?r" ``` wenzelm@67406 ` 355` ``` from \avl t\ and Node_Node have "avl ?r" by simp ``` wenzelm@67406 ` 356` ``` from \avl t\ and Node_Node have "avl ?l" by simp ``` nipkow@68023 ` 357` ``` hence "avl(?l')" by (rule avl_split_max,simp) ``` nipkow@68023 ` 358` ``` have l'_height: "height ?l = height ?l' \ height ?l = height ?l' + 1" using \avl ?l\ by (intro avl_split_max) auto ``` wenzelm@67406 ` 359` ``` have t_height: "height t = 1 + max (height ?l) (height ?r)" using \avl t\ Node_Node by simp ``` wenzelm@67406 ` 360` ``` have "height t = height ?t' \ height t = height ?t' + 1" using \avl t\ Node_Node ``` nipkow@61232 ` 361` ``` proof(cases "height ?r = height ?l' + 2") ``` nipkow@61232 ` 362` ``` case False ``` wenzelm@67406 ` 363` ``` show ?thesis using l'_height t_height False by (subst height_balR2[OF \avl ?l'\ \avl ?r\ False])+ arith ``` nipkow@61232 ` 364` ``` next ``` nipkow@61232 ` 365` ``` case True ``` nipkow@61232 ` 366` ``` show ?thesis ``` nipkow@68023 ` 367` ``` proof(cases rule: disjE[OF height_balR[OF True \avl ?l'\ \avl ?r\, of "snd (split_max ?l)"]]) ``` nipkow@61232 ` 368` ``` case 1 ``` nipkow@61232 ` 369` ``` thus ?thesis using l'_height t_height True by arith ``` nipkow@61232 ` 370` ``` next ``` nipkow@61232 ` 371` ``` case 2 ``` nipkow@61232 ` 372` ``` thus ?thesis using l'_height t_height True by arith ``` nipkow@61232 ` 373` ``` qed ``` nipkow@61232 ` 374` ``` qed ``` nipkow@61232 ` 375` ``` thus ?thesis using Node_Node by (auto split:prod.splits) ``` nipkow@61232 ` 376` ```qed simp_all ``` nipkow@61232 ` 377` wenzelm@67406 ` 378` ```text\Deletion maintains the AVL property:\ ``` nipkow@61232 ` 379` nipkow@61232 ` 380` ```theorem avl_delete_aux: ``` nipkow@61232 ` 381` ``` assumes "avl t" ``` nipkow@61232 ` 382` ``` shows "avl(delete x t)" and "height t = (height (delete x t)) \ height t = height (delete x t) + 1" ``` nipkow@61232 ` 383` ```using assms ``` nipkow@61232 ` 384` ```proof (induct t) ``` nipkow@61232 ` 385` ``` case (Node h l n r) ``` nipkow@61232 ` 386` ``` case 1 ``` nipkow@61232 ` 387` ``` with Node show ?case ``` nipkow@61232 ` 388` ``` proof(cases "x = n") ``` nipkow@61232 ` 389` ``` case True ``` nipkow@61647 ` 390` ``` with Node 1 show ?thesis by (auto simp:avl_del_root) ``` nipkow@61232 ` 391` ``` next ``` nipkow@61232 ` 392` ``` case False ``` nipkow@61232 ` 393` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 394` ``` proof(cases "xx\n\ show ?thesis by (auto simp add:avl_balL) ``` nipkow@61232 ` 400` ``` qed ``` nipkow@61232 ` 401` ``` qed ``` nipkow@61232 ` 402` ``` case 2 ``` nipkow@61232 ` 403` ``` with Node show ?case ``` nipkow@61232 ` 404` ``` proof(cases "x = n") ``` nipkow@61232 ` 405` ``` case True ``` nipkow@61647 ` 406` ``` with 1 have "height (Node h l n r) = height(del_root (Node h l n r)) ``` nipkow@61647 ` 407` ``` \ height (Node h l n r) = height(del_root (Node h l n r)) + 1" ``` nipkow@61647 ` 408` ``` by (subst height_del_root,simp_all) ``` nipkow@61232 ` 409` ``` with True show ?thesis by simp ``` nipkow@61232 ` 410` ``` next ``` nipkow@61232 ` 411` ``` case False ``` nipkow@61232 ` 412` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 413` ``` proof(cases "xx < n\ show ?thesis by(auto simp: balR_def) ``` nipkow@61232 ` 418` ``` next ``` nipkow@61232 ` 419` ``` case True ``` nipkow@61581 ` 420` ``` hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \ ``` nipkow@61581 ` 421` ``` height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \ ?B") ``` nipkow@61581 ` 422` ``` using Node 2 by (intro height_balR) auto ``` nipkow@61232 ` 423` ``` thus ?thesis ``` nipkow@61232 ` 424` ``` proof ``` nipkow@61232 ` 425` ``` assume ?A ``` wenzelm@67406 ` 426` ``` with \x < n\ Node 2 show ?thesis by(auto simp: balR_def) ``` nipkow@61232 ` 427` ``` next ``` nipkow@61232 ` 428` ``` assume ?B ``` wenzelm@67406 ` 429` ``` with \x < n\ Node 2 show ?thesis by(auto simp: balR_def) ``` nipkow@61232 ` 430` ``` qed ``` nipkow@61232 ` 431` ``` qed ``` nipkow@61232 ` 432` ``` next ``` nipkow@61232 ` 433` ``` case False ``` nipkow@61232 ` 434` ``` show ?thesis ``` nipkow@61232 ` 435` ``` proof(cases "height l = height (delete x r) + 2") ``` wenzelm@67406 ` 436` ``` case False with Node 1 \\x < n\ \x \ n\ show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 437` ``` next ``` nipkow@61232 ` 438` ``` case True ``` nipkow@61581 ` 439` ``` hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \ ``` nipkow@61581 ` 440` ``` height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \ ?B") ``` nipkow@61581 ` 441` ``` using Node 2 by (intro height_balL) auto ``` nipkow@61232 ` 442` ``` thus ?thesis ``` nipkow@61232 ` 443` ``` proof ``` nipkow@61232 ` 444` ``` assume ?A ``` wenzelm@67406 ` 445` ``` with \\x < n\ \x \ n\ Node 2 show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 446` ``` next ``` nipkow@61232 ` 447` ``` assume ?B ``` wenzelm@67406 ` 448` ``` with \\x < n\ \x \ n\ Node 2 show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 449` ``` qed ``` nipkow@61232 ` 450` ``` qed ``` nipkow@61232 ` 451` ``` qed ``` nipkow@61232 ` 452` ``` qed ``` nipkow@61232 ` 453` ```qed simp_all ``` nipkow@61232 ` 454` nipkow@63411 ` 455` nipkow@63411 ` 456` ```subsection \Height-Size Relation\ ``` nipkow@63411 ` 457` nipkow@63411 ` 458` ```text \By Daniel St\"uwe\ ``` nipkow@63411 ` 459` nipkow@63411 ` 460` ```fun fib_tree :: "nat \ unit avl_tree" where ``` nipkow@63411 ` 461` ```"fib_tree 0 = Leaf" | ``` nipkow@63411 ` 462` ```"fib_tree (Suc 0) = Node 1 Leaf () Leaf" | ``` nipkow@63411 ` 463` ```"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)" ``` nipkow@63411 ` 464` nipkow@63411 ` 465` ```lemma [simp]: "ht (fib_tree h) = h" ``` nipkow@63411 ` 466` ```by (induction h rule: "fib_tree.induct") auto ``` nipkow@63411 ` 467` nipkow@63411 ` 468` ```lemma [simp]: "height (fib_tree h) = h" ``` nipkow@63411 ` 469` ```by (induction h rule: "fib_tree.induct") auto ``` nipkow@63411 ` 470` nipkow@63411 ` 471` ```lemma "avl(fib_tree h)" ``` nipkow@63411 ` 472` ```by (induction h rule: "fib_tree.induct") auto ``` nipkow@63411 ` 473` nipkow@63411 ` 474` ```lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)" ``` nipkow@63411 ` 475` ```by (induction h rule: fib_tree.induct) auto ``` nipkow@63411 ` 476` nipkow@63411 ` 477` ```lemma height_invers[simp]: ``` nipkow@63411 ` 478` ``` "(height t = 0) = (t = Leaf)" ``` nipkow@63411 ` 479` ``` "avl t \ (height t = Suc h) = (\ l a r . t = Node (Suc h) l a r)" ``` nipkow@63411 ` 480` ```by (induction t) auto ``` nipkow@63411 ` 481` nipkow@63411 ` 482` ```lemma fib_Suc_lt: "fib n \ fib (Suc n)" ``` nipkow@63411 ` 483` ```by (induction n rule: fib.induct) auto ``` nipkow@63411 ` 484` nipkow@63411 ` 485` ```lemma fib_mono: "n \ m \ fib n \ fib m" ``` nipkow@63411 ` 486` ```proof (induction n arbitrary: m rule: fib.induct ) ``` nipkow@63411 ` 487` ``` case (2 m) ``` nipkow@63411 ` 488` ``` thus ?case using fib_neq_0_nat[of m] by auto ``` nipkow@63411 ` 489` ```next ``` nipkow@63411 ` 490` ``` case (3 n m) ``` nipkow@63411 ` 491` ``` from 3 obtain m' where "m = Suc (Suc m')" ``` nipkow@63411 ` 492` ``` by (metis le_Suc_ex plus_nat.simps(2)) ``` nipkow@63411 ` 493` ``` thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto ``` nipkow@63411 ` 494` ```qed simp ``` nipkow@63411 ` 495` nipkow@63411 ` 496` ```lemma size1_fib_tree_mono: ``` nipkow@63411 ` 497` ``` assumes "n \ m" ``` nipkow@63411 ` 498` ``` shows "size1 (fib_tree n) \ size1 (fib_tree m)" ``` nipkow@63411 ` 499` ```using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce ``` nipkow@63411 ` 500` nipkow@63411 ` 501` ```lemma fib_tree_minimal: "avl t \ size1 (fib_tree (ht t)) \ size1 t" ``` nipkow@63411 ` 502` ```proof (induction "ht t" arbitrary: t rule: fib_tree.induct) ``` nipkow@63411 ` 503` ``` case (2 t) ``` nipkow@63411 ` 504` ``` from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto ``` nipkow@63411 ` 505` ``` with 2 show ?case by auto ``` nipkow@63411 ` 506` ```next ``` nipkow@63411 ` 507` ``` case (3 h t) ``` nipkow@63411 ` 508` ``` note [simp] = 3(3)[symmetric] ``` nipkow@63411 ` 509` ``` from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto ``` nipkow@63411 ` 510` ``` show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) ``` nipkow@63411 ` 511` ``` case equal ``` nipkow@63411 ` 512` ``` with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto ``` nipkow@63411 ` 513` ``` with 3 have "size1 (fib_tree (ht l)) \ size1 l" by auto moreover ``` nipkow@63411 ` 514` ``` from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \ size1 r" by auto ultimately ``` nipkow@63411 ` 515` ``` show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto ``` nipkow@63411 ` 516` ``` next ``` nipkow@63411 ` 517` ``` case greater ``` nipkow@63411 ` 518` ``` with 3(3,4) have ht: "ht l = Suc h" "ht r = h" by auto ``` nipkow@63411 ` 519` ``` from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \ size1 l" by auto moreover ``` nipkow@63411 ` 520` ``` from ht 3(1,2,4) have "size1 (fib_tree h) \ size1 r" by auto ultimately ``` nipkow@63411 ` 521` ``` show ?thesis by auto ``` nipkow@63411 ` 522` ``` next ``` nipkow@63411 ` 523` ``` case less (* analogously *) ``` nipkow@63411 ` 524` ``` with 3 have ht: "ht l = h" "Suc h = ht r" by auto ``` nipkow@63411 ` 525` ``` from ht 3 have "size1 (fib_tree h) \ size1 l" by auto moreover ``` nipkow@63411 ` 526` ``` from ht 3 have "size1 (fib_tree (Suc h)) \ size1 r" by auto ultimately ``` nipkow@63411 ` 527` ``` show ?thesis by auto ``` nipkow@63411 ` 528` ``` qed ``` nipkow@63411 ` 529` ```qed auto ``` nipkow@63411 ` 530` nipkow@63411 ` 531` ```theorem avl_size_bound: "avl t \ fib(height t + 2) \ size1 t" ``` nipkow@63411 ` 532` ```using fib_tree_minimal fib_tree_size1 by fastforce ``` nipkow@63411 ` 533` nipkow@61232 ` 534` ```end ```