src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Thu Nov 05 08:27:14 2015 +0100 (2015-11-05) changeset 61581 00d9682e8dd7 parent 61428 5e1938107371 child 61588 1d2907d0ed73 permissions -rw-r--r--
Convertd to 3-way comparisons
 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@61581 ` 9` ```imports Cmp 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@61581 ` 29` ```definition balL :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61581 ` 30` ```"balL 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@61581 ` 38` ```definition balR :: "'a avl_tree \ 'a \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61581 ` 39` ```"balR 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@61581 ` 47` ```fun insert :: "'a::cmp \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 48` ```"insert x Leaf = Node 1 Leaf x Leaf" | ``` nipkow@61581 ` 49` ```"insert x (Node h l a r) = (case cmp x a of ``` nipkow@61581 ` 50` ``` EQ \ Node h l a r | ``` nipkow@61581 ` 51` ``` LT \ balL (insert x l) a r | ``` nipkow@61581 ` 52` ``` GT \ balR l a (insert x r))" ``` nipkow@61232 ` 53` nipkow@61232 ` 54` ```fun delete_max :: "'a avl_tree \ 'a avl_tree * 'a" where ``` nipkow@61232 ` 55` ```"delete_max (Node _ l a Leaf) = (l,a)" | ``` nipkow@61581 ` 56` ```"delete_max (Node _ l a r) = ``` nipkow@61581 ` 57` ``` (let (r',a') = delete_max r in (balL l a r', a'))" ``` nipkow@61232 ` 58` nipkow@61232 ` 59` ```lemmas delete_max_induct = delete_max.induct[case_names Leaf Node] ``` nipkow@61232 ` 60` nipkow@61232 ` 61` ```fun delete_root :: "'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 62` ```"delete_root (Node h Leaf a r) = r" | ``` nipkow@61232 ` 63` ```"delete_root (Node h l a Leaf) = l" | ``` nipkow@61232 ` 64` ```"delete_root (Node h l a r) = ``` nipkow@61581 ` 65` ``` (let (l', a') = delete_max l in balR l' a' r)" ``` nipkow@61232 ` 66` nipkow@61232 ` 67` ```lemmas delete_root_cases = delete_root.cases[case_names Leaf_t Node_Leaf Node_Node] ``` nipkow@61232 ` 68` nipkow@61581 ` 69` ```fun delete :: "'a::cmp \ 'a avl_tree \ 'a avl_tree" where ``` nipkow@61232 ` 70` ```"delete _ Leaf = Leaf" | ``` nipkow@61581 ` 71` ```"delete x (Node h l a r) = (case cmp x a of ``` nipkow@61581 ` 72` ``` EQ \ delete_root (Node h l a r) | ``` nipkow@61581 ` 73` ``` LT \ balR (delete x l) a r | ``` nipkow@61581 ` 74` ``` GT \ balL l a (delete x r))" ``` nipkow@61232 ` 75` nipkow@61232 ` 76` nipkow@61232 ` 77` ```subsection {* Functional Correctness Proofs *} ``` nipkow@61232 ` 78` nipkow@61232 ` 79` ```text{* Very different from the AFP/AVL proofs *} ``` nipkow@61232 ` 80` nipkow@61232 ` 81` nipkow@61232 ` 82` ```subsubsection "Proofs for insert" ``` nipkow@61232 ` 83` nipkow@61581 ` 84` ```lemma inorder_balL: ``` nipkow@61581 ` 85` ``` "inorder (balL l a r) = inorder l @ a # inorder r" ``` nipkow@61581 ` 86` ```by (auto simp: node_def balL_def split:tree.splits) ``` nipkow@61232 ` 87` nipkow@61581 ` 88` ```lemma inorder_balR: ``` nipkow@61581 ` 89` ``` "inorder (balR l a r) = inorder l @ a # inorder r" ``` nipkow@61581 ` 90` ```by (auto simp: node_def balR_def split:tree.splits) ``` nipkow@61232 ` 91` nipkow@61232 ` 92` ```theorem inorder_insert: ``` nipkow@61232 ` 93` ``` "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" ``` nipkow@61232 ` 94` ```by (induct t) ``` nipkow@61581 ` 95` ``` (auto simp: ins_list_simps inorder_balL inorder_balR) ``` nipkow@61232 ` 96` nipkow@61232 ` 97` nipkow@61232 ` 98` ```subsubsection "Proofs for delete" ``` nipkow@61232 ` 99` nipkow@61232 ` 100` ```lemma inorder_delete_maxD: ``` nipkow@61232 ` 101` ``` "\ delete_max t = (t',a); t \ Leaf \ \ ``` nipkow@61232 ` 102` ``` inorder t' @ [a] = inorder t" ``` nipkow@61232 ` 103` ```by(induction t arbitrary: t' rule: delete_max.induct) ``` nipkow@61581 ` 104` ``` (auto simp: inorder_balL split: prod.splits tree.split) ``` nipkow@61232 ` 105` nipkow@61232 ` 106` ```lemma inorder_delete_root: ``` nipkow@61232 ` 107` ``` "inorder (delete_root (Node h l a r)) = inorder l @ inorder r" ``` nipkow@61232 ` 108` ```by(induction "Node h l a r" arbitrary: l a r h rule: delete_root.induct) ``` nipkow@61581 ` 109` ``` (auto simp: inorder_balR inorder_delete_maxD split: prod.splits) ``` nipkow@61232 ` 110` nipkow@61232 ` 111` ```theorem inorder_delete: ``` nipkow@61232 ` 112` ``` "sorted(inorder t) \ inorder (delete x t) = del_list x (inorder t)" ``` nipkow@61232 ` 113` ```by(induction t) ``` nipkow@61581 ` 114` ``` (auto simp: del_list_simps inorder_balL inorder_balR ``` nipkow@61232 ` 115` ``` inorder_delete_root inorder_delete_maxD split: prod.splits) ``` nipkow@61232 ` 116` nipkow@61232 ` 117` nipkow@61232 ` 118` ```subsubsection "Overall functional correctness" ``` nipkow@61232 ` 119` nipkow@61232 ` 120` ```interpretation Set_by_Ordered ``` nipkow@61232 ` 121` ```where empty = Leaf and isin = isin and insert = insert and delete = delete ``` nipkow@61232 ` 122` ```and inorder = inorder and wf = "\_. True" ``` nipkow@61232 ` 123` ```proof (standard, goal_cases) ``` nipkow@61232 ` 124` ``` case 1 show ?case by simp ``` nipkow@61232 ` 125` ```next ``` nipkow@61232 ` 126` ``` case 2 thus ?case by(simp add: isin_set) ``` nipkow@61232 ` 127` ```next ``` nipkow@61232 ` 128` ``` case 3 thus ?case by(simp add: inorder_insert) ``` nipkow@61232 ` 129` ```next ``` nipkow@61232 ` 130` ``` case 4 thus ?case by(simp add: inorder_delete) ``` nipkow@61428 ` 131` ```qed (rule TrueI)+ ``` nipkow@61232 ` 132` nipkow@61232 ` 133` nipkow@61232 ` 134` ```subsection {* AVL invariants *} ``` nipkow@61232 ` 135` nipkow@61232 ` 136` ```text{* Essentially the AFP/AVL proofs *} ``` nipkow@61232 ` 137` nipkow@61232 ` 138` nipkow@61232 ` 139` ```subsubsection {* Insertion maintains AVL balance *} ``` nipkow@61232 ` 140` nipkow@61232 ` 141` ```declare Let_def [simp] ``` nipkow@61232 ` 142` nipkow@61232 ` 143` ```lemma [simp]: "avl t \ ht t = height t" ``` nipkow@61232 ` 144` ```by (induct t) simp_all ``` nipkow@61232 ` 145` nipkow@61581 ` 146` ```lemma height_balL: ``` nipkow@61232 ` 147` ``` "\ height l = height r + 2; avl l; avl r \ \ ``` nipkow@61581 ` 148` ``` height (balL l a r) = height r + 2 \ ``` nipkow@61581 ` 149` ``` height (balL l a r) = height r + 3" ``` nipkow@61581 ` 150` ```by (cases l) (auto simp:node_def balL_def split:tree.split) ``` nipkow@61232 ` 151` ``` ``` nipkow@61581 ` 152` ```lemma height_balR: ``` nipkow@61232 ` 153` ``` "\ height r = height l + 2; avl l; avl r \ \ ``` nipkow@61581 ` 154` ``` height (balR l a r) = height l + 2 \ ``` nipkow@61581 ` 155` ``` height (balR l a r) = height l + 3" ``` nipkow@61581 ` 156` ```by (cases r) (auto simp add:node_def balR_def split:tree.split) ``` nipkow@61232 ` 157` nipkow@61232 ` 158` ```lemma [simp]: "height(node l a r) = max (height l) (height r) + 1" ``` nipkow@61232 ` 159` ```by (simp add: node_def) ``` nipkow@61232 ` 160` nipkow@61232 ` 161` ```lemma avl_node: ``` nipkow@61232 ` 162` ``` "\ avl l; avl r; ``` nipkow@61232 ` 163` ``` height l = height r \ height l = height r + 1 \ height r = height l + 1 ``` nipkow@61232 ` 164` ``` \ \ avl(node l a r)" ``` nipkow@61232 ` 165` ```by (auto simp add:max_def node_def) ``` nipkow@61232 ` 166` nipkow@61581 ` 167` ```lemma height_balL2: ``` nipkow@61232 ` 168` ``` "\ avl l; avl r; height l \ height r + 2 \ \ ``` nipkow@61581 ` 169` ``` height (balL l a r) = (1 + max (height l) (height r))" ``` nipkow@61581 ` 170` ```by (cases l, cases r) (simp_all add: balL_def) ``` nipkow@61232 ` 171` nipkow@61581 ` 172` ```lemma height_balR2: ``` nipkow@61232 ` 173` ``` "\ avl l; avl r; height r \ height l + 2 \ \ ``` nipkow@61581 ` 174` ``` height (balR l a r) = (1 + max (height l) (height r))" ``` nipkow@61581 ` 175` ```by (cases l, cases r) (simp_all add: balR_def) ``` nipkow@61232 ` 176` nipkow@61581 ` 177` ```lemma avl_balL: ``` nipkow@61232 ` 178` ``` assumes "avl l" "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 179` ``` \ height r = height l + 1 \ height l = height r + 2" ``` nipkow@61581 ` 180` ``` shows "avl(balL l a r)" ``` nipkow@61232 ` 181` ```proof(cases l) ``` nipkow@61232 ` 182` ``` case Leaf ``` nipkow@61581 ` 183` ``` with assms show ?thesis by (simp add: node_def balL_def) ``` nipkow@61232 ` 184` ```next ``` nipkow@61232 ` 185` ``` case (Node ln ll lr lh) ``` nipkow@61232 ` 186` ``` with assms show ?thesis ``` nipkow@61232 ` 187` ``` proof(cases "height l = height r + 2") ``` nipkow@61232 ` 188` ``` case True ``` nipkow@61232 ` 189` ``` from True Node assms show ?thesis ``` nipkow@61581 ` 190` ``` by (auto simp: balL_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 191` ``` next ``` nipkow@61232 ` 192` ``` case False ``` nipkow@61581 ` 193` ``` with assms show ?thesis by (simp add: avl_node balL_def) ``` nipkow@61232 ` 194` ``` qed ``` nipkow@61232 ` 195` ```qed ``` nipkow@61232 ` 196` nipkow@61581 ` 197` ```lemma avl_balR: ``` nipkow@61232 ` 198` ``` assumes "avl l" and "avl r" and "height l = height r \ height l = height r + 1 ``` nipkow@61232 ` 199` ``` \ height r = height l + 1 \ height r = height l + 2" ``` nipkow@61581 ` 200` ``` shows "avl(balR l a r)" ``` nipkow@61232 ` 201` ```proof(cases r) ``` nipkow@61232 ` 202` ``` case Leaf ``` nipkow@61581 ` 203` ``` with assms show ?thesis by (simp add: node_def balR_def) ``` nipkow@61232 ` 204` ```next ``` nipkow@61232 ` 205` ``` case (Node rn rl rr rh) ``` nipkow@61232 ` 206` ``` with assms show ?thesis ``` nipkow@61232 ` 207` ``` proof(cases "height r = height l + 2") ``` nipkow@61232 ` 208` ``` case True ``` nipkow@61232 ` 209` ``` from True Node assms show ?thesis ``` nipkow@61581 ` 210` ``` by (auto simp: balR_def intro!: avl_node split: tree.split) arith+ ``` nipkow@61232 ` 211` ``` next ``` nipkow@61232 ` 212` ``` case False ``` nipkow@61581 ` 213` ``` with assms show ?thesis by (simp add: balR_def avl_node) ``` nipkow@61232 ` 214` ``` qed ``` nipkow@61232 ` 215` ```qed ``` nipkow@61232 ` 216` nipkow@61232 ` 217` ```(* It appears that these two properties need to be proved simultaneously: *) ``` nipkow@61232 ` 218` nipkow@61232 ` 219` ```text{* Insertion maintains the AVL property: *} ``` nipkow@61232 ` 220` nipkow@61232 ` 221` ```theorem avl_insert_aux: ``` nipkow@61232 ` 222` ``` assumes "avl t" ``` nipkow@61232 ` 223` ``` shows "avl(insert x t)" ``` nipkow@61232 ` 224` ``` "(height (insert x t) = height t \ height (insert x t) = height t + 1)" ``` nipkow@61232 ` 225` ```using assms ``` nipkow@61232 ` 226` ```proof (induction t) ``` nipkow@61232 ` 227` ``` case (Node h l a r) ``` nipkow@61232 ` 228` ``` case 1 ``` nipkow@61232 ` 229` ``` with Node show ?case ``` nipkow@61232 ` 230` ``` proof(cases "x = a") ``` nipkow@61232 ` 231` ``` case True ``` nipkow@61232 ` 232` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 233` ``` next ``` nipkow@61232 ` 234` ``` case False ``` nipkow@61232 ` 235` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 236` ``` proof(cases "xa` show ?thesis by (auto simp add:avl_balR) ``` nipkow@61232 ` 242` ``` qed ``` nipkow@61232 ` 243` ``` qed ``` nipkow@61232 ` 244` ``` case 2 ``` nipkow@61232 ` 245` ``` from 2 Node show ?case ``` nipkow@61232 ` 246` ``` proof(cases "x = a") ``` nipkow@61232 ` 247` ``` case True ``` nipkow@61232 ` 248` ``` with Node 1 show ?thesis by simp ``` nipkow@61232 ` 249` ``` next ``` nipkow@61232 ` 250` ``` case False ``` nipkow@61232 ` 251` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 252` ``` proof(cases "x ``` nipkow@61581 ` 260` ``` (height (balL (insert x l) a r) = height r + 3)" (is "?A \ ?B") ``` nipkow@61581 ` 261` ``` using Node 2 by (intro height_balL) simp_all ``` nipkow@61232 ` 262` ``` thus ?thesis ``` nipkow@61232 ` 263` ``` proof ``` nipkow@61232 ` 264` ``` assume ?A ``` nipkow@61232 ` 265` ``` with 2 `x < a` show ?thesis by (auto) ``` nipkow@61232 ` 266` ``` next ``` nipkow@61232 ` 267` ``` assume ?B ``` nipkow@61232 ` 268` ``` with True 1 Node(2) `x < a` show ?thesis by (simp) arith ``` nipkow@61232 ` 269` ``` qed ``` nipkow@61232 ` 270` ``` qed ``` nipkow@61232 ` 271` ``` next ``` nipkow@61232 ` 272` ``` case False ``` nipkow@61232 ` 273` ``` with Node 2 show ?thesis ``` nipkow@61232 ` 274` ``` proof(cases "height (insert x r) = height l + 2") ``` nipkow@61232 ` 275` ``` case False ``` nipkow@61581 ` 276` ``` with Node 2 `\x < a` show ?thesis by (auto simp: height_balR2) ``` nipkow@61232 ` 277` ``` next ``` nipkow@61232 ` 278` ``` case True ``` nipkow@61581 ` 279` ``` hence "(height (balR l a (insert x r)) = height l + 2) \ ``` nipkow@61581 ` 280` ``` (height (balR l a (insert x r)) = height l + 3)" (is "?A \ ?B") ``` nipkow@61581 ` 281` ``` using Node 2 by (intro height_balR) simp_all ``` nipkow@61232 ` 282` ``` thus ?thesis ``` nipkow@61232 ` 283` ``` proof ``` nipkow@61232 ` 284` ``` assume ?A ``` nipkow@61232 ` 285` ``` with 2 `\x < a` show ?thesis by (auto) ``` nipkow@61232 ` 286` ``` next ``` nipkow@61232 ` 287` ``` assume ?B ``` nipkow@61232 ` 288` ``` with True 1 Node(4) `\x < a` show ?thesis by (simp) arith ``` nipkow@61232 ` 289` ``` qed ``` nipkow@61232 ` 290` ``` qed ``` nipkow@61232 ` 291` ``` qed ``` nipkow@61232 ` 292` ``` qed ``` nipkow@61232 ` 293` ```qed simp_all ``` nipkow@61232 ` 294` nipkow@61232 ` 295` nipkow@61232 ` 296` ```subsubsection {* Deletion maintains AVL balance *} ``` nipkow@61232 ` 297` nipkow@61232 ` 298` ```lemma avl_delete_max: ``` nipkow@61232 ` 299` ``` assumes "avl x" and "x \ Leaf" ``` nipkow@61232 ` 300` ``` shows "avl (fst (delete_max x))" "height x = height(fst (delete_max x)) \ ``` nipkow@61232 ` 301` ``` height x = height(fst (delete_max x)) + 1" ``` nipkow@61232 ` 302` ```using assms ``` nipkow@61232 ` 303` ```proof (induct x rule: delete_max_induct) ``` nipkow@61232 ` 304` ``` case (Node h l a rh rl b rr) ``` nipkow@61232 ` 305` ``` case 1 ``` nipkow@61232 ` 306` ``` with Node have "avl l" "avl (fst (delete_max (Node rh rl b rr)))" by auto ``` nipkow@61581 ` 307` ``` with 1 Node have "avl (balL l a (fst (delete_max (Node rh rl b rr))))" ``` nipkow@61581 ` 308` ``` by (intro avl_balL) fastforce+ ``` nipkow@61232 ` 309` ``` thus ?case ``` nipkow@61581 ` 310` ``` by (auto simp: height_balL height_balL2 ``` nipkow@61232 ` 311` ``` linorder_class.max.absorb1 linorder_class.max.absorb2 ``` nipkow@61232 ` 312` ``` split:prod.split) ``` nipkow@61232 ` 313` ```next ``` nipkow@61232 ` 314` ``` case (Node h l a rh rl b rr) ``` nipkow@61232 ` 315` ``` case 2 ``` nipkow@61232 ` 316` ``` let ?r = "Node rh rl b rr" ``` nipkow@61232 ` 317` ``` let ?r' = "fst (delete_max ?r)" ``` nipkow@61232 ` 318` ``` from `avl x` Node 2 have "avl l" and "avl ?r" by simp_all ``` nipkow@61581 ` 319` ``` thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] ``` nipkow@61232 ` 320` ``` apply (auto split:prod.splits simp del:avl.simps) by arith+ ``` nipkow@61232 ` 321` ```qed auto ``` nipkow@61232 ` 322` nipkow@61232 ` 323` ```lemma avl_delete_root: ``` nipkow@61232 ` 324` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61232 ` 325` ``` shows "avl(delete_root t)" ``` nipkow@61232 ` 326` ```using assms ``` nipkow@61232 ` 327` ```proof (cases t rule:delete_root_cases) ``` nipkow@61232 ` 328` ``` case (Node_Node h lh ll ln lr n rh rl rn rr) ``` nipkow@61232 ` 329` ``` let ?l = "Node lh ll ln lr" ``` nipkow@61232 ` 330` ``` let ?r = "Node rh rl rn rr" ``` nipkow@61232 ` 331` ``` let ?l' = "fst (delete_max ?l)" ``` nipkow@61232 ` 332` ``` from `avl t` and Node_Node have "avl ?r" by simp ``` nipkow@61232 ` 333` ``` from `avl t` and Node_Node have "avl ?l" by simp ``` nipkow@61232 ` 334` ``` hence "avl(?l')" "height ?l = height(?l') \ ``` nipkow@61232 ` 335` ``` height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+ ``` nipkow@61232 ` 336` ``` with `avl t` Node_Node have "height ?l' = height ?r \ height ?l' = height ?r + 1 ``` nipkow@61232 ` 337` ``` \ height ?r = height ?l' + 1 \ height ?r = height ?l' + 2" by fastforce ``` nipkow@61581 ` 338` ``` with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(delete_max ?l)) ?r)" ``` nipkow@61581 ` 339` ``` by (rule avl_balR) ``` nipkow@61232 ` 340` ``` with Node_Node show ?thesis by (auto split:prod.splits) ``` nipkow@61232 ` 341` ```qed simp_all ``` nipkow@61232 ` 342` nipkow@61232 ` 343` ```lemma height_delete_root: ``` nipkow@61232 ` 344` ``` assumes "avl t" and "t \ Leaf" ``` nipkow@61232 ` 345` ``` shows "height t = height(delete_root t) \ height t = height(delete_root t) + 1" ``` nipkow@61232 ` 346` ```using assms ``` nipkow@61232 ` 347` ```proof (cases t rule: delete_root_cases) ``` nipkow@61232 ` 348` ``` case (Node_Node h lh ll ln lr n rh rl rn rr) ``` nipkow@61232 ` 349` ``` let ?l = "Node lh ll ln lr" ``` nipkow@61232 ` 350` ``` let ?r = "Node rh rl rn rr" ``` nipkow@61232 ` 351` ``` let ?l' = "fst (delete_max ?l)" ``` nipkow@61581 ` 352` ``` let ?t' = "balR ?l' (snd(delete_max ?l)) ?r" ``` nipkow@61232 ` 353` ``` from `avl t` and Node_Node have "avl ?r" by simp ``` nipkow@61232 ` 354` ``` from `avl t` and Node_Node have "avl ?l" by simp ``` nipkow@61232 ` 355` ``` hence "avl(?l')" by (rule avl_delete_max,simp) ``` nipkow@61232 ` 356` ``` have l'_height: "height ?l = height ?l' \ height ?l = height ?l' + 1" using `avl ?l` by (intro avl_delete_max) auto ``` nipkow@61232 ` 357` ``` have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp ``` nipkow@61232 ` 358` ``` have "height t = height ?t' \ height t = height ?t' + 1" using `avl t` Node_Node ``` nipkow@61232 ` 359` ``` proof(cases "height ?r = height ?l' + 2") ``` nipkow@61232 ` 360` ``` case False ``` nipkow@61581 ` 361` ``` show ?thesis using l'_height t_height False by (subst height_balR2[OF `avl ?l'` `avl ?r` False])+ arith ``` nipkow@61232 ` 362` ``` next ``` nipkow@61232 ` 363` ``` case True ``` nipkow@61232 ` 364` ``` show ?thesis ``` nipkow@61581 ` 365` ``` proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (delete_max ?l)"]]) ``` nipkow@61232 ` 366` ``` case 1 ``` nipkow@61232 ` 367` ``` thus ?thesis using l'_height t_height True by arith ``` nipkow@61232 ` 368` ``` next ``` nipkow@61232 ` 369` ``` case 2 ``` nipkow@61232 ` 370` ``` thus ?thesis using l'_height t_height True by arith ``` nipkow@61232 ` 371` ``` qed ``` nipkow@61232 ` 372` ``` qed ``` nipkow@61232 ` 373` ``` thus ?thesis using Node_Node by (auto split:prod.splits) ``` nipkow@61232 ` 374` ```qed simp_all ``` nipkow@61232 ` 375` nipkow@61232 ` 376` ```text{* Deletion maintains the AVL property: *} ``` nipkow@61232 ` 377` nipkow@61232 ` 378` ```theorem avl_delete_aux: ``` nipkow@61232 ` 379` ``` assumes "avl t" ``` nipkow@61232 ` 380` ``` shows "avl(delete x t)" and "height t = (height (delete x t)) \ height t = height (delete x t) + 1" ``` nipkow@61232 ` 381` ```using assms ``` nipkow@61232 ` 382` ```proof (induct t) ``` nipkow@61232 ` 383` ``` case (Node h l n r) ``` nipkow@61232 ` 384` ``` case 1 ``` nipkow@61232 ` 385` ``` with Node show ?case ``` nipkow@61232 ` 386` ``` proof(cases "x = n") ``` nipkow@61232 ` 387` ``` case True ``` nipkow@61232 ` 388` ``` with Node 1 show ?thesis by (auto simp:avl_delete_root) ``` nipkow@61232 ` 389` ``` next ``` nipkow@61232 ` 390` ``` case False ``` nipkow@61232 ` 391` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 392` ``` proof(cases "xn` show ?thesis by (auto simp add:avl_balL) ``` nipkow@61232 ` 398` ``` qed ``` nipkow@61232 ` 399` ``` qed ``` nipkow@61232 ` 400` ``` case 2 ``` nipkow@61232 ` 401` ``` with Node show ?case ``` nipkow@61232 ` 402` ``` proof(cases "x = n") ``` nipkow@61232 ` 403` ``` case True ``` nipkow@61232 ` 404` ``` with 1 have "height (Node h l n r) = height(delete_root (Node h l n r)) ``` nipkow@61232 ` 405` ``` \ height (Node h l n r) = height(delete_root (Node h l n r)) + 1" ``` nipkow@61232 ` 406` ``` by (subst height_delete_root,simp_all) ``` nipkow@61232 ` 407` ``` with True show ?thesis by simp ``` nipkow@61232 ` 408` ``` next ``` nipkow@61232 ` 409` ``` case False ``` nipkow@61232 ` 410` ``` with Node 1 show ?thesis ``` nipkow@61232 ` 411` ``` proof(cases "x ``` nipkow@61581 ` 419` ``` height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \ ?B") ``` nipkow@61581 ` 420` ``` using Node 2 by (intro height_balR) auto ``` nipkow@61232 ` 421` ``` thus ?thesis ``` nipkow@61232 ` 422` ``` proof ``` nipkow@61232 ` 423` ``` assume ?A ``` nipkow@61581 ` 424` ``` with `x < n` Node 2 show ?thesis by(auto simp: balR_def) ``` nipkow@61232 ` 425` ``` next ``` nipkow@61232 ` 426` ``` assume ?B ``` nipkow@61581 ` 427` ``` with `x < n` Node 2 show ?thesis by(auto simp: balR_def) ``` nipkow@61232 ` 428` ``` qed ``` nipkow@61232 ` 429` ``` qed ``` nipkow@61232 ` 430` ``` next ``` nipkow@61232 ` 431` ``` case False ``` nipkow@61232 ` 432` ``` show ?thesis ``` nipkow@61232 ` 433` ``` proof(cases "height l = height (delete x r) + 2") ``` nipkow@61581 ` 434` ``` case False with Node 1 `\x < n` `x \ n` show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 435` ``` next ``` nipkow@61232 ` 436` ``` case True ``` nipkow@61581 ` 437` ``` hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \ ``` nipkow@61581 ` 438` ``` height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \ ?B") ``` nipkow@61581 ` 439` ``` using Node 2 by (intro height_balL) auto ``` nipkow@61232 ` 440` ``` thus ?thesis ``` nipkow@61232 ` 441` ``` proof ``` nipkow@61232 ` 442` ``` assume ?A ``` nipkow@61581 ` 443` ``` with `\x < n` `x \ n` Node 2 show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 444` ``` next ``` nipkow@61232 ` 445` ``` assume ?B ``` nipkow@61581 ` 446` ``` with `\x < n` `x \ n` Node 2 show ?thesis by(auto simp: balL_def) ``` nipkow@61232 ` 447` ``` qed ``` nipkow@61232 ` 448` ``` qed ``` nipkow@61232 ` 449` ``` qed ``` nipkow@61232 ` 450` ``` qed ``` nipkow@61232 ` 451` ```qed simp_all ``` nipkow@61232 ` 452` nipkow@61232 ` 453` ```end ```