src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Tue Oct 13 17:06:37 2015 +0200 (2015-10-13) changeset 61428 5e1938107371 parent 61232 c46faf9762f7 child 61581 00d9682e8dd7 permissions -rw-r--r--
 nipkow@61232 ` 1` ```(* ``` nipkow@61232 ` 2` ```Author: Tobias Nipkow ``` nipkow@61232 ` 3` ```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@61232 ` 9` ```imports Isin2 ``` nipkow@61232 ` 10` ```begin ``` nipkow@61232 ` 11` nipkow@61232 ` 12` ```type_synonym 'a avl_tree = "('a,nat) tree" ``` nipkow@61232 ` 13` nipkow@61232 ` 14` ```text {* Invariant: *} ``` nipkow@61232 ` 15` nipkow@61232 ` 16` ```fun avl :: "'a avl_tree \ bool" where ``` nipkow@61232 ` 17` ```"avl Leaf = True" | ``` nipkow@61232 ` 18` ```"avl (Node h l a r) = ``` nipkow@61232 ` 19` ``` ((height l = height r \ height l = height r + 1 \ height r = height l + 1) \ ``` nipkow@61232 ` 20` ``` h = max (height l) (height r) + 1 \ avl l \ avl r)" ``` nipkow@61232 ` 21` nipkow@61232 ` 22` ```fun ht :: "'a avl_tree \ nat" where ``` nipkow@61232 ` 23` ```"ht Leaf = 0" | ``` nipkow@61232 ` 24` ```"ht (Node h l a r) = h" ``` nipkow@61232 ` 25` nipkow@61232 ` 26` ```definition node :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 27` ```"node l a r = Node (max (ht l) (ht r) + 1) l a r" ``` nipkow@61232 ` 28` nipkow@61232 ` 29` ```definition node_bal_l :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 30` ```"node_bal_l l a r = ( ``` nipkow@61232 ` 31` ``` if ht l = ht r + 2 then (case l of ``` nipkow@61232 ` 32` ``` Node _ bl b br \ (if ht bl < ht br ``` nipkow@61232 ` 33` ``` then case br of ``` nipkow@61232 ` 34` ``` Node _ cl c cr \ node (node bl b cl) c (node cr a r) ``` nipkow@61232 ` 35` ``` else node bl b (node br a r))) ``` nipkow@61232 ` 36` ``` else node l a r)" ``` nipkow@61232 ` 37` nipkow@61232 ` 38` ```definition node_bal_r :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 39` ```"node_bal_r l a r = ( ``` nipkow@61232 ` 40` ``` if ht r = ht l + 2 then (case r of ``` nipkow@61232 ` 41` ``` Node _ bl b br \ (if ht bl > ht br ``` nipkow@61232 ` 42` ``` then case bl of ``` nipkow@61232 ` 43` ``` Node _ cl c cr \ node (node l a cl) c (node cr b br) ``` nipkow@61232 ` 44` ``` else node (node l a bl) b br)) ``` nipkow@61232 ` 45` ``` else node l a r)" ``` nipkow@61232 ` 46` nipkow@61232 ` 47` ```fun insert :: "'a::order \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 48` ```"insert x Leaf = Node 1 Leaf x Leaf" | ``` nipkow@61232 ` 49` ```"insert x (Node h l a r) = ``` nipkow@61232 ` 50` ``` (if x=a then Node h l a r ``` nipkow@61232 ` 51` ``` else if x 'a avl_tree * 'a" where ``` nipkow@61232 ` 56` ```"delete_max (Node _ l a Leaf) = (l,a)" | ``` nipkow@61232 ` 57` ```"delete_max (Node _ l a r) = ( ``` nipkow@61232 ` 58` ``` let (r',a') = delete_max r in ``` nipkow@61232 ` 59` ``` (node_bal_l l a r', a'))" ``` nipkow@61232 ` 60` nipkow@61232 ` 61` ```lemmas delete_max_induct = delete_max.induct[case_names Leaf Node] ``` nipkow@61232 ` 62` nipkow@61232 ` 63` ```fun delete_root :: "'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 64` ```"delete_root (Node h Leaf a r) = r" | ``` nipkow@61232 ` 65` ```"delete_root (Node h l a Leaf) = l" | ``` nipkow@61232 ` 66` ```"delete_root (Node h l a r) = ``` nipkow@61232 ` 67` ``` (let (l', a') = delete_max l in node_bal_r l' a' r)" ``` nipkow@61232 ` 68` nipkow@61232 ` 69` ```lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node] ``` nipkow@61232 ` 70` nipkow@61232 ` 71` ```fun delete :: "'a::order \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 72` ```"delete _ Leaf = Leaf" | ``` nipkow@61232 ` 73` ```"delete x (Node h l a r) = ( ``` nipkow@61232 ` 74` ``` if x = a then delete_root (Node h l a r) ``` nipkow@61232 ` 75` ``` else if x < a then node_bal_r (delete x l) a r ``` nipkow@61232 ` 76` ``` else node_bal_l l a (delete x r))" ``` nipkow@61232 ` 77` nipkow@61232 ` 78` nipkow@61232 ` 79` ```subsection {* Functional Correctness Proofs *} ``` nipkow@61232 ` 80` nipkow@61232 ` 81` ```text{* Very different from the AFP/AVL proofs *} ``` nipkow@61232 ` 82` nipkow@61232 ` 83` nipkow@61232 ` 84` ```subsubsection "Proofs for insert" ``` nipkow@61232 ` 85` nipkow@61232 ` 86` ```lemma inorder_node_bal_l: ``` nipkow@61232 ` 87` ``` "inorder (node_bal_l l a r) = inorder l @ a # inorder r" ``` nipkow@61232 ` 88` ```by (auto simp: node_def node_bal_l_def split:tree.splits) ``` nipkow@61232 ` 89` nipkow@61232 ` 90` ```lemma inorder_node_bal_r: ``` nipkow@61232 ` 91` ``` "inorder (node_bal_r l a r) = inorder l @ a # inorder r" ``` nipkow@61232 ` 92` ```by (auto simp: node_def node_bal_r_def split:tree.splits) ``` nipkow@61232 ` 93` nipkow@61232 ` 94` ```theorem inorder_insert: ``` nipkow@61232 ` 95` ``` "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" ``` nipkow@61232 ` 96` ```by (induct t) ``` nipkow@61232 ` 97` ``` (auto simp: ins_list_simps inorder_node_bal_l inorder_node_bal_r) ``` nipkow@61232 ` 98` nipkow@61232 ` 99` nipkow@61232 ` 100` ```subsubsection "Proofs for delete" ``` nipkow@61232 ` 101` nipkow@61232 ` 102` ```lemma inorder_delete_maxD: ``` nipkow@61232 ` 103` ``` "\ delete_max t = (t',a); t \ Leaf \ \ ``` nipkow@61232 ` 104` ``` inorder t' @ [a] = inorder t" ``` nipkow@61232 ` 105` ```by(induction t arbitrary: t' rule: delete_max.induct) ``` nipkow@61232 ` 106` ``` (auto simp: inorder_node_bal_l split: prod.splits tree.split) ``` nipkow@61232 ` 107` nipkow@61232 ` 108` ```lemma inorder_delete_root: ``` nipkow@61232 ` 109` ``` "inorder (delete_root (Node h l a r)) = inorder l @ inorder r" ``` nipkow@61232 ` 110` ```by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct) ``` nipkow@61232 ` 111` ``` (auto simp: inorder_node_bal_r inorder_delete_maxD split: prod.splits) ``` nipkow@61232 ` 112` nipkow@61232 ` 113` ```theorem inorder_delete: ``` nipkow@61232 ` 114` ``` "sorted(inorder t) \ inorder (delete x t) = del_list x (inorder t)" ``` nipkow@61232 ` 115` ```by(induction t) ``` nipkow@61232 ` 116` ``` (auto simp: del_list_simps inorder_node_bal_l inorder_node_bal_r ``` nipkow@61232 ` 117` ``` inorder_delete_root inorder_delete_maxD split: prod.splits) ``` nipkow@61232 ` 118` nipkow@61232 ` 119` nipkow@61232 ` 120` ```subsubsection "Overall functional correctness" ``` nipkow@61232 ` 121` nipkow@61232 ` 122` ```interpretation Set_by_Ordered ``` nipkow@61232 ` 123` ```where empty = Leaf and isin = isin and insert = insert and delete = delete ``` nipkow@61232 ` 124` ```and inorder = inorder and wf = "\_. True" ``` nipkow@61232 ` 125` ```proof (standard, goal_cases) ``` nipkow@61232 ` 126` ``` case 1 show ?case by simp ``` nipkow@61232 ` 127` ```next ``` nipkow@61232 ` 128` ``` case 2 thus ?case by(simp add: isin_set) ``` nipkow@61232 ` 129` ```next ``` nipkow@61232 ` 130` ``` case 3 thus ?case by(simp add: inorder_insert) ``` nipkow@61232 ` 131` ```next ``` nipkow@61232 ` 132` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61428 ` 133` ```qed (rule TrueI)+ ``` nipkow@61232 ` 134` nipkow@61232 ` 135` nipkow@61232 ` 136` ```subsection {* AVL invariants *} ``` nipkow@61232 ` 137` nipkow@61232 ` 138` ```text{* Essentially the AFP/AVL proofs *} ``` nipkow@61232 ` 139` nipkow@61232 ` 140` nipkow@61232 ` 141` ```subsubsection {* Insertion maintains AVL balance *} ``` nipkow@61232 ` 142` nipkow@61232 ` 143` ```declare Let_def [simp] ``` nipkow@61232 ` 144` nipkow@61232 ` 145` ```lemma [simp]: "avl t \ ht t = height t" ``` nipkow@61232 ` 146` ```by (induct t) simp_all ``` nipkow@61232 ` 147` nipkow@61232 ` 148` ```lemma height_node_bal_l: ``` nipkow@61232 ` 149` ``` "\ height l = height r + 2; avl l; avl r \ \ ``` nipkow@61232 ` 150` ``` height (node_bal_l l a r) = height r + 2 \ ``` nipkow@61232 ` 151` ``` height (node_bal_l l a r) = height r + 3" ``` nipkow@61232 ` 152` ```by (cases l) (auto simp:node_def node_bal_l_def split:tree.split) ``` nipkow@61232 ` 153` ``` ``` nipkow@61232 ` 154` ```lemma height_node_bal_r: ``` nipkow@61232 ` 155` ``` "\ height r = height l + 2; avl l; avl r \ \ ``` nipkow@61232 ` 156` ``` height (node_bal_r l a r) = height l + 2 \ ``` nipkow@61232 ` 157` ``` height (node_bal_r l a r) = height l + 3" ``` nipkow@61232 ` 158` ```by (cases r) (auto simp add:node_def node_bal_r_def split:tree.split) ``` nipkow@61232 ` 159` nipkow@61232 ` 160` ```lemma [simp]: "height(node l a r) = max (height l) (height r) + 1" ``` nipkow@61232 ` 161` ```by (simp add: node_def) ``` nipkow@61232 ` 162` nipkow@61232 ` 163` ```lemma avl_node: ``` nipkow@61232 ` 164` ``` "\ avl l; avl r; ``` nipkow@61232 ` 165` ``` height l = height r \ height l = height r + 1 \ height r = height l + 1 ``` nipkow@61232 ` 166` ``` \ \ avl(node l a r)" ``` nipkow@61232 ` 167` ```by (auto simp add:max_def node_def) ``` nipkow@61232 ` 168` nipkow@61232 ` 169` ```lemma height_node_bal_l2: ``` nipkow@61232 ` 170` ``` "\ avl l; avl r; height l \ height r + 2 \ \ ``` nipkow@61232 ` 171` ``` height (node_bal_l l a r) = (1 + max (height l) (height r))" ``` nipkow@61232 ` 172` ```by (cases l, cases r) (simp_all add: node_bal_l_def) ``` nipkow@61232 ` 173` nipkow@61232 ` 174` ```lemma height_node_bal_r2: ``` nipkow@61232 ` 175` ``` "\ avl l; avl r; height r \ height l + 2 \ \ ``` nipkow@61232 ` 176` ``` height (node_bal_r l a r) = (1 + max (height l) (height r))" ``` nipkow@61232 ` 177` ```by (cases l, cases r) (simp_all add: node_bal_r_def) ``` nipkow@61232 ` 178` nipkow@61232 ` 179` ```lemma avl_node_bal_l: ``` nipkow@61232 ` 180` ``` assumes "avl l" "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 181` ``` \ height r = height l + 1 \ height l = height r + 2" ``` nipkow@61232 ` 182` ``` shows "avl(node_bal_l l a r)" ``` nipkow@61232 ` 183` ```proof(cases l) ``` nipkow@61232 ` 184` ``` case Leaf ``` nipkow@61232 ` 185` ``` with assms show ?thesis by (simp add: node_def node_bal_l_def) ``` nipkow@61232 ` 186` ```next ``` nipkow@61232 ` 187` ``` case (Node ln ll lr lh) ``` nipkow@61232 ` 188` ``` with assms show ?thesis ``` nipkow@61232 ` 189` ``` proof(cases "height l = height r + 2") ``` nipkow@61232 ` 190` ``` case True ``` nipkow@61232 ` 191` ``` from True Node assms show ?thesis ``` nipkow@61232 ` 192` ``` by (auto simp: node_bal_l_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 193` ``` next ``` nipkow@61232 ` 194` ``` case False ``` nipkow@61232 ` 195` ``` with assms show ?thesis by (simp add: avl_node node_bal_l_def) ``` nipkow@61232 ` 196` ``` qed ``` nipkow@61232 ` 197` ```qed ``` nipkow@61232 ` 198` nipkow@61232 ` 199` ```lemma avl_node_bal_r: ``` nipkow@61232 ` 200` ``` assumes "avl l" and "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 201` ``` \ height r = height l + 1 \ height r = height l + 2" ``` nipkow@61232 ` 202` ``` shows "avl(node_bal_r l a r)" ``` nipkow@61232 ` 203` ```proof(cases r) ``` nipkow@61232 ` 204` ``` case Leaf ``` nipkow@61232 ` 205` ``` with assms show ?thesis by (simp add: node_def node_bal_r_def) ``` nipkow@61232 ` 206` ```next ``` nipkow@61232 ` 207` ``` case (Node rn rl rr rh) ``` nipkow@61232 ` 208` ``` with assms show ?thesis ``` nipkow@61232 ` 209` ``` proof(cases "height r = height l + 2") ``` nipkow@61232 ` 210` ``` case True ``` nipkow@61232 ` 211` ``` from True Node assms show ?thesis ``` nipkow@61232 ` 212` ``` by (auto simp: node_bal_r_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 213` ``` next ``` nipkow@61232 ` 214` ``` case False ``` nipkow@61232 ` 215` ``` with assms show ?thesis by (simp add: node_bal_r_def avl_node) ``` nipkow@61232 ` 216` ``` qed ``` nipkow@61232 ` 217` ```qed ``` nipkow@61232 ` 218` nipkow@61232 ` 219` ```(* It appears that these two properties need to be proved simultaneously: *) ``` nipkow@61232 ` 220` nipkow@61232 ` 221` ```text{* Insertion maintains the AVL property: *} ``` nipkow@61232 ` 222` nipkow@61232 ` 223` ```theorem avl_insert_aux: ``` nipkow@61232 ` 224` ``` assumes "avl t" ``` nipkow@61232 ` 225` ``` shows "avl(insert x t)" ``` nipkow@61232 ` 226` ``` "(height (insert x t) = height t \ height (insert x t) = height t + 1)" ``` nipkow@61232 ` 227` ```using assms ``` nipkow@61232 ` 228` ```proof (induction t) ``` nipkow@61232 ` 229` ``` case (Node h l a r) ``` nipkow@61232 ` 230` ``` case 1 ``` nipkow@61232 ` 231` ``` with Node show ?case ``` nipkow@61232 ` 232` ``` proof(cases "x = a") ``` nipkow@61232 ` 233` ``` case True ``` nipkow@61232 ` 234` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 235` ``` next ``` nipkow@61232 ` 236` ``` case False ``` nipkow@61232 ` 237` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 238` ``` proof(cases "xa` show ?thesis by (auto simp add:avl_node_bal_r) ``` nipkow@61232 ` 244` ``` qed ``` nipkow@61232 ` 245` ``` qed ``` nipkow@61232 ` 246` ``` case 2 ``` nipkow@61232 ` 247` ``` from 2 Node show ?case ``` nipkow@61232 ` 248` ``` proof(cases "x = a") ``` nipkow@61232 ` 249` ``` case True ``` nipkow@61232 ` 250` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 251` ``` next ``` nipkow@61232 ` 252` ``` case False ``` nipkow@61232 ` 253` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 254` ``` proof(cases "x ``` nipkow@61232 ` 262` ``` (height (node_bal_l (insert x l) a r) = height r + 3)" (is "?A \ ?B") ``` nipkow@61232 ` 263` ``` using Node 2 by (intro height_node_bal_l) simp_all ``` nipkow@61232 ` 264` ``` thus ?thesis ``` nipkow@61232 ` 265` ``` proof ``` nipkow@61232 ` 266` ``` assume ?A ``` nipkow@61232 ` 267` ``` with 2 `x < a` show ?thesis by (auto) ``` nipkow@61232 ` 268` ``` next ``` nipkow@61232 ` 269` ``` assume ?B ``` nipkow@61232 ` 270` ``` with True 1 Node(2) `x < a` show ?thesis by (simp) arith ``` nipkow@61232 ` 271` ``` qed ``` nipkow@61232 ` 272` ``` qed ``` nipkow@61232 ` 273` ``` next ``` nipkow@61232 ` 274` ``` case False ``` nipkow@61232 ` 275` ``` with Node 2 show ?thesis ``` nipkow@61232 ` 276` ``` proof(cases "height (insert x r) = height l + 2") ``` nipkow@61232 ` 277` ``` case False ``` nipkow@61232 ` 278` ``` with Node 2 `\x < a` show ?thesis by (auto simp: height_node_bal_r2) ``` nipkow@61232 ` 279` ``` next ``` nipkow@61232 ` 280` ``` case True ``` nipkow@61232 ` 281` ``` hence "(height (node_bal_r l a (insert x r)) = height l + 2) \ ``` nipkow@61232 ` 282` ``` (height (node_bal_r l a (insert x r)) = height l + 3)" (is "?A \ ?B") ``` nipkow@61232 ` 283` ``` using Node 2 by (intro height_node_bal_r) simp_all ``` nipkow@61232 ` 284` ``` thus ?thesis ``` nipkow@61232 ` 285` ``` proof ``` nipkow@61232 ` 286` ``` assume ?A ``` nipkow@61232 ` 287` ``` with 2 `\x < a` show ?thesis by (auto) ``` nipkow@61232 ` 288` ``` next ``` nipkow@61232 ` 289` ``` assume ?B ``` nipkow@61232 ` 290` ``` with True 1 Node(4) `\x < a` show ?thesis by (simp) arith ``` nipkow@61232 ` 291` ``` qed ``` nipkow@61232 ` 292` ``` qed ``` nipkow@61232 ` 293` ``` qed ``` nipkow@61232 ` 294` ``` qed ``` nipkow@61232 ` 295` ```qed simp_all ``` nipkow@61232 ` 296` nipkow@61232 ` 297` nipkow@61232 ` 298` ```subsubsection {* Deletion maintains AVL balance *} ``` nipkow@61232 ` 299` nipkow@61232 ` 300` ```lemma avl_delete_max: ``` nipkow@61232 ` 301` ``` assumes "avl x" and "x \ Leaf" ``` nipkow@61232 ` 302` ``` shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \ ``` nipkow@61232 ` 303` ``` height x = height(fst (delete_max x)) + 1" ``` nipkow@61232 ` 304` ```using assms ``` nipkow@61232 ` 305` ```proof (induct x rule: delete_max_induct) ``` nipkow@61232 ` 306` ``` case (Node h l a rh rl b rr) ``` nipkow@61232 ` 307` ``` case 1 ``` nipkow@61232 ` 308` ``` with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto ``` nipkow@61232 ` 309` ``` with 1 Node have "avl (node_bal_l l a (fst (delete_max (Node rh rl b rr))))" ``` nipkow@61232 ` 310` ``` by (intro avl_node_bal_l) fastforce+ ``` nipkow@61232 ` 311` ``` thus ?case ``` nipkow@61232 ` 312` ``` by (auto simp: height_node_bal_l height_node_bal_l2 ``` nipkow@61232 ` 313` ``` linorder_class.max.absorb1 linorder_class.max.absorb2 ``` nipkow@61232 ` 314` ``` split:prod.split) ``` nipkow@61232 ` 315` ```next ``` nipkow@61232 ` 316` ``` case (Node h l a rh rl b rr) ``` nipkow@61232 ` 317` ``` case 2 ``` nipkow@61232 ` 318` ``` let ?r = "Node rh rl b rr" ``` nipkow@61232 ` 319` ``` let ?r' = "fst (delete_max ?r)" ``` nipkow@61232 ` 320` ``` from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all ``` nipkow@61232 ` 321` ``` thus ?case using Node 2 height_node_bal_l[of l ?r' a] height_node_bal_l2[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@61232 ` 325` ```lemma avl_delete_root: ``` nipkow@61232 ` 326` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61232 ` 327` ``` shows "avl(delete_root t)" ``` nipkow@61232 ` 328` ```using assms ``` nipkow@61232 ` 329` ```proof (cases t rule:delete_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@61232 ` 333` ``` let ?l' = "fst (delete_max ?l)" ``` nipkow@61232 ` 334` ``` from `avl t` and Node_Node have "avl ?r" by simp ``` nipkow@61232 ` 335` ``` from `avl t` and Node_Node have "avl ?l" by simp ``` nipkow@61232 ` 336` ``` hence "avl(?l')" "height ?l = height(?l') \ ``` nipkow@61232 ` 337` ``` height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+ ``` nipkow@61232 ` 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@61232 ` 340` ``` with `avl ?l'` `avl ?r` have "avl(node_bal_r ?l' (snd(delete_max ?l)) ?r)" ``` nipkow@61232 ` 341` ``` by (rule avl_node_bal_r) ``` nipkow@61232 ` 342` ``` with Node_Node show ?thesis by (auto split:prod.splits) ``` nipkow@61232 ` 343` ```qed simp_all ``` nipkow@61232 ` 344` nipkow@61232 ` 345` ```lemma height_delete_root: ``` nipkow@61232 ` 346` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61232 ` 347` ``` shows "height t = height(delete_root t) \ height t = height(delete_root t) + 1" ``` nipkow@61232 ` 348` ```using assms ``` nipkow@61232 ` 349` ```proof (cases t rule: delete_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@61232 ` 353` ``` let ?l' = "fst (delete_max ?l)" ``` nipkow@61232 ` 354` ``` let ?t' = "node_bal_r ?l' (snd(delete_max ?l)) ?r" ``` nipkow@61232 ` 355` ``` from `avl t` and Node_Node have "avl ?r" by simp ``` nipkow@61232 ` 356` ``` from `avl t` and Node_Node have "avl ?l" by simp ``` nipkow@61232 ` 357` ``` hence "avl(?l')" by (rule avl_delete_max,simp) ``` nipkow@61232 ` 358` ``` have l'_height: "height ?l = height ?l' \ height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto ``` nipkow@61232 ` 359` ``` have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp ``` nipkow@61232 ` 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 ``` nipkow@61232 ` 363` ``` show ?thesis using l'_height t_height False by (subst height_node_bal_r2[OF `avl ?l'` `avl ?r` False])+ arith ``` nipkow@61232 ` 364` ``` next ``` nipkow@61232 ` 365` ``` case True ``` nipkow@61232 ` 366` ``` show ?thesis ``` nipkow@61232 ` 367` ``` proof(cases rule: disjE[OF height_node_bal_r[OF True `avl ?l'` `avl ?r`, of "snd (delete_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` nipkow@61232 ` 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@61232 ` 390` ``` with Node 1 show ?thesis by (auto simp:avl_delete_root) ``` nipkow@61232 ` 391` ``` next ``` nipkow@61232 ` 392` ``` case False ``` nipkow@61232 ` 393` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 394` ``` proof(cases "xn` show ?thesis by (auto simp add:avl_node_bal_l) ``` 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@61232 ` 406` ``` with 1 have "height (Node h l n r) = height(delete_root (Node h l n r)) ``` nipkow@61232 ` 407` ``` \ height (Node h l n r) = height(delete_root (Node h l n r)) + 1" ``` nipkow@61232 ` 408` ``` by (subst height_delete_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 "x ``` nipkow@61232 ` 421` ``` height (node_bal_r (delete x l) n r) = height (delete x l) + 3" (is "?A \ ?B") ``` nipkow@61232 ` 422` ``` using Node 2 by (intro height_node_bal_r) auto ``` nipkow@61232 ` 423` ``` thus ?thesis ``` nipkow@61232 ` 424` ``` proof ``` nipkow@61232 ` 425` ``` assume ?A ``` nipkow@61232 ` 426` ``` with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_def) ``` nipkow@61232 ` 427` ``` next ``` nipkow@61232 ` 428` ``` assume ?B ``` nipkow@61232 ` 429` ``` with `x < n` Node 2 show ?thesis by(auto simp: node_bal_r_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") ``` nipkow@61232 ` 436` ``` case False with Node 1 `\x < n` `x \ n` show ?thesis by(auto simp: node_bal_l_def) ``` nipkow@61232 ` 437` ``` next ``` nipkow@61232 ` 438` ``` case True ``` nipkow@61232 ` 439` ``` hence "(height (node_bal_l l n (delete x r)) = height (delete x r) + 2) \ ``` nipkow@61232 ` 440` ``` height (node_bal_l l n (delete x r)) = height (delete x r) + 3" (is "?A \ ?B") ``` nipkow@61232 ` 441` ``` using Node 2 by (intro height_node_bal_l) auto ``` nipkow@61232 ` 442` ``` thus ?thesis ``` nipkow@61232 ` 443` ``` proof ``` nipkow@61232 ` 444` ``` assume ?A ``` nipkow@61232 ` 445` ``` with `\x < n` `x \ n` Node 2 show ?thesis by(auto simp: node_bal_l_def) ``` nipkow@61232 ` 446` ``` next ``` nipkow@61232 ` 447` ``` assume ?B ``` nipkow@61232 ` 448` ``` with `\x < n` `x \ n` Node 2 show ?thesis by(auto simp: node_bal_l_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@61232 ` 455` ```end ```