src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Tue May 29 20:01:50 2018 +0200 (11 months ago) changeset 68313 56c57e91edf9 parent 68023 75130777ece4 child 68342 b80734daf7ed permissions -rw-r--r--
slicker proof
 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@68313 ` 458` ```text \By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\ ``` nipkow@63411 ` 459` nipkow@68313 ` 460` ```lemma height_invers: ``` nipkow@63411 ` 461` ``` "(height t = 0) = (t = Leaf)" ``` nipkow@63411 ` 462` ``` "avl t \ (height t = Suc h) = (\ l a r . t = Node (Suc h) l a r)" ``` nipkow@63411 ` 463` ```by (induction t) auto ``` nipkow@63411 ` 464` nipkow@68313 ` 465` ```text \Any AVL tree of height \h\ has at least \fib (h+2)\ leaves:\ ``` nipkow@63411 ` 466` nipkow@68313 ` 467` ```lemma avl_fib_bound: "avl t \ height t = h \ fib (h+2) \ size1 t" ``` nipkow@68313 ` 468` ```proof (induction h arbitrary: t rule: fib.induct) ``` nipkow@68313 ` 469` ``` case 1 thus ?case by (simp add: height_invers) ``` nipkow@63411 ` 470` ```next ``` nipkow@68313 ` 471` ``` case 2 thus ?case by (cases t) (auto simp: height_invers) ``` nipkow@63411 ` 472` ```next ``` nipkow@68313 ` 473` ``` case (3 h) ``` nipkow@68313 ` 474` ``` from "3.prems" obtain l a r where ``` nipkow@68313 ` 475` ``` [simp]: "t = Node (Suc(Suc h)) l a r" "avl l" "avl r" ``` nipkow@68313 ` 476` ``` and C: " ``` nipkow@68313 ` 477` ``` height r = Suc h \ height l = Suc h ``` nipkow@68313 ` 478` ``` \ height r = Suc h \ height l = h ``` nipkow@68313 ` 479` ``` \ height r = h \ height l = Suc h" (is "?C1 \ ?C2 \ ?C3") ``` nipkow@68313 ` 480` ``` by (cases t) (simp, fastforce) ``` nipkow@68313 ` 481` ``` { ``` nipkow@68313 ` 482` ``` assume ?C1 ``` nipkow@68313 ` 483` ``` with "3.IH"(1) ``` nipkow@68313 ` 484` ``` have "fib (h + 3) \ size1 l" "fib (h + 3) \ size1 r" ``` nipkow@68313 ` 485` ``` by (simp_all add: eval_nat_numeral) ``` nipkow@68313 ` 486` ``` hence ?case by (auto simp: eval_nat_numeral) ``` nipkow@68313 ` 487` ``` } moreover { ``` nipkow@68313 ` 488` ``` assume ?C2 ``` nipkow@68313 ` 489` ``` hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto ``` nipkow@68313 ` 490` ``` } moreover { ``` nipkow@68313 ` 491` ``` assume ?C3 ``` nipkow@68313 ` 492` ``` hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto ``` nipkow@68313 ` 493` ``` } ultimately show ?case using C by blast ``` nipkow@68313 ` 494` ```qed ``` nipkow@68313 ` 495` nipkow@68313 ` 496` ```lemma fib_alt_induct [consumes 1, case_names 1 2 rec]: ``` nipkow@68313 ` 497` ``` assumes "n > 0" "P 1" "P 2" "\n. n > 0 \ P n \ P (Suc n) \ P (Suc (Suc n))" ``` nipkow@68313 ` 498` ``` shows "P n" ``` nipkow@68313 ` 499` ``` using assms(1) ``` nipkow@68313 ` 500` ```proof (induction n rule: fib.induct) ``` nipkow@68313 ` 501` ``` case (3 n) ``` nipkow@68313 ` 502` ``` thus ?case using assms by (cases n) (auto simp: eval_nat_numeral) ``` nipkow@68313 ` 503` ```qed (insert assms, auto) ``` nipkow@68313 ` 504` nipkow@68313 ` 505` ```text \An exponential lower bound for @{const fib}:\ ``` nipkow@63411 ` 506` nipkow@68313 ` 507` ```lemma fib_lowerbound: ``` nipkow@68313 ` 508` ``` defines "\ \ (1 + sqrt 5) / 2" ``` nipkow@68313 ` 509` ``` defines "c \ 1 / \ ^ 2" ``` nipkow@68313 ` 510` ``` assumes "n > 0" ``` nipkow@68313 ` 511` ``` shows "real (fib n) \ c * \ ^ n" ``` nipkow@68313 ` 512` ```proof - ``` nipkow@68313 ` 513` ``` have "\ > 1" by (simp add: \_def) ``` nipkow@68313 ` 514` ``` hence "c > 0" by (simp add: c_def) ``` nipkow@68313 ` 515` ``` from \n > 0\ show ?thesis ``` nipkow@68313 ` 516` ``` proof (induction n rule: fib_alt_induct) ``` nipkow@68313 ` 517` ``` case (rec n) ``` nipkow@68313 ` 518` ``` have "c * \ ^ Suc (Suc n) = \ ^ 2 * (c * \ ^ n)" ``` nipkow@68313 ` 519` ``` by (simp add: field_simps power2_eq_square) ``` nipkow@68313 ` 520` ``` also have "\ \ (\ + 1) * (c * \ ^ n)" ``` nipkow@68313 ` 521` ``` by (rule mult_right_mono) (insert \c > 0\, simp_all add: \_def power2_eq_square field_simps) ``` nipkow@68313 ` 522` ``` also have "\ = c * \ ^ Suc n + c * \ ^ n" ``` nipkow@68313 ` 523` ``` by (simp add: field_simps) ``` nipkow@68313 ` 524` ``` also have "\ \ real (fib (Suc n)) + real (fib n)" ``` nipkow@68313 ` 525` ``` by (intro add_mono rec.IH) ``` nipkow@68313 ` 526` ``` finally show ?case by simp ``` nipkow@68313 ` 527` ``` qed (insert \\ > 1\, simp_all add: c_def power2_eq_square eval_nat_numeral) ``` nipkow@68313 ` 528` ```qed ``` nipkow@68313 ` 529` nipkow@68313 ` 530` ```text \The size of an AVL tree is (at least) exponential in its height:\ ``` nipkow@68313 ` 531` nipkow@68313 ` 532` ```lemma avl_lowerbound: ``` nipkow@68313 ` 533` ``` defines "\ \ (1 + sqrt 5) / 2" ``` nipkow@68313 ` 534` ``` assumes "avl t" ``` nipkow@68313 ` 535` ``` shows "real (size1 t) \ \ ^ (height t)" ``` nipkow@68313 ` 536` ```proof - ``` nipkow@68313 ` 537` ``` have "\ > 0" by(simp add: \_def add_pos_nonneg) ``` nipkow@68313 ` 538` ``` hence "\ ^ height t = (1 / \ ^ 2) * \ ^ (height t + 2)" ``` nipkow@68313 ` 539` ``` by(simp add: field_simps power2_eq_square) ``` nipkow@68313 ` 540` ``` also have "\ \ real (fib (height t + 2))" ``` nipkow@68313 ` 541` ``` using fib_lowerbound[of "height t + 2"] by(simp add: \_def) ``` nipkow@68313 ` 542` ``` also have "\ \ real (size1 t)" ``` nipkow@68313 ` 543` ``` using avl_fib_bound[of t "height t"] assms by simp ``` nipkow@68313 ` 544` ``` finally show ?thesis . ``` nipkow@68313 ` 545` ```qed ``` nipkow@63411 ` 546` nipkow@61232 ` 547` ```end ```