1(* Author: Tobias Nipkow *) 2 3section "AVL Tree Implementation of Maps" 4 5theory AVL_Map 6imports 7 AVL_Set 8 Lookup2 9begin 10 11fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where 12"update x y Leaf = Node Leaf (x,y) 1 Leaf" | 13"update x y (Node l (a,b) h r) = (case cmp x a of 14 EQ \<Rightarrow> Node l (x,y) h r | 15 LT \<Rightarrow> balL (update x y l) (a,b) r | 16 GT \<Rightarrow> balR l (a,b) (update x y r))" 17 18fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where 19"delete _ Leaf = Leaf" | 20"delete x (Node l (a,b) h r) = (case cmp x a of 21 EQ \<Rightarrow> del_root (Node l (a,b) h r) | 22 LT \<Rightarrow> balR (delete x l) (a,b) r | 23 GT \<Rightarrow> balL l (a,b) (delete x r))" 24 25 26subsection \<open>Functional Correctness\<close> 27 28theorem inorder_update: 29 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" 30by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) 31 32 33theorem inorder_delete: 34 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" 35by(induction t) 36 (auto simp: del_list_simps inorder_balL inorder_balR 37 inorder_del_root inorder_split_maxD split: prod.splits) 38 39 40subsection \<open>AVL invariants\<close> 41 42 43subsubsection \<open>Insertion maintains AVL balance\<close> 44 45theorem avl_update: 46 assumes "avl t" 47 shows "avl(update x y t)" 48 "(height (update x y t) = height t \<or> height (update x y t) = height t + 1)" 49using assms 50proof (induction x y t rule: update.induct) 51 case eq2: (2 x y l a b h r) 52 case 1 53 show ?case 54 proof(cases "x = a") 55 case True with eq2 1 show ?thesis by simp 56 next 57 case False 58 with eq2 1 show ?thesis 59 proof(cases "x<a") 60 case True with eq2 1 show ?thesis by (auto simp add:avl_balL) 61 next 62 case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR) 63 qed 64 qed 65 case 2 66 show ?case 67 proof(cases "x = a") 68 case True with eq2 1 show ?thesis by simp 69 next 70 case False 71 show ?thesis 72 proof(cases "x<a") 73 case True 74 show ?thesis 75 proof(cases "height (update x y l) = height r + 2") 76 case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) 77 next 78 case True 79 hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or> 80 (height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B") 81 using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all 82 thus ?thesis 83 proof 84 assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) 85 next 86 assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith 87 qed 88 qed 89 next 90 case False 91 show ?thesis 92 proof(cases "height (update x y r) = height l + 2") 93 case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) 94 next 95 case True 96 hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or> 97 (height (balR l (a,b) (update x y r)) = height l + 3)" (is "?A \<or> ?B") 98 using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all 99 thus ?thesis 100 proof 101 assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) 102 next 103 assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith 104 qed 105 qed 106 qed 107 qed 108qed simp_all 109 110 111subsubsection \<open>Deletion maintains AVL balance\<close> 112 113theorem avl_delete: 114 assumes "avl t" 115 shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" 116using assms 117proof (induct t) 118 case (Node l n h r) 119 obtain a b where [simp]: "n = (a,b)" by fastforce 120 case 1 121 show ?case 122 proof(cases "x = a") 123 case True with Node 1 show ?thesis by (auto simp:avl_del_root) 124 next 125 case False 126 show ?thesis 127 proof(cases "x<a") 128 case True with Node 1 show ?thesis by (auto simp add:avl_balR) 129 next 130 case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL) 131 qed 132 qed 133 case 2 134 show ?case 135 proof(cases "x = a") 136 case True 137 with 1 have "height (Node l n h r) = height(del_root (Node l n h r)) 138 \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1" 139 by (subst height_del_root,simp_all) 140 with True show ?thesis by simp 141 next 142 case False 143 show ?thesis 144 proof(cases "x<a") 145 case True 146 show ?thesis 147 proof(cases "height r = height (delete x l) + 2") 148 case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def) 149 next 150 case True 151 hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or> 152 height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B") 153 using Node 2 by (intro height_balR) auto 154 thus ?thesis 155 proof 156 assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) 157 next 158 assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) 159 qed 160 qed 161 next 162 case False 163 show ?thesis 164 proof(cases "height l = height (delete x r) + 2") 165 case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def) 166 next 167 case True 168 hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or> 169 height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B") 170 using Node 2 by (intro height_balL) auto 171 thus ?thesis 172 proof 173 assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) 174 next 175 assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) 176 qed 177 qed 178 qed 179 qed 180qed simp_all 181 182 183interpretation M: Map_by_Ordered 184where empty = empty and lookup = lookup and update = update and delete = delete 185and inorder = inorder and inv = avl 186proof (standard, goal_cases) 187 case 1 show ?case by (simp add: empty_def) 188next 189 case 2 thus ?case by(simp add: lookup_map_of) 190next 191 case 3 thus ?case by(simp add: inorder_update) 192next 193 case 4 thus ?case by(simp add: inorder_delete) 194next 195 case 5 show ?case by (simp add: empty_def) 196next 197 case 6 thus ?case by(simp add: avl_update(1)) 198next 199 case 7 thus ?case by(simp add: avl_delete(1)) 200qed 201 202end 203