equal
deleted
inserted
replaced
23 GT \<Rightarrow> balL l (a,b) (delete x r))" |
23 GT \<Rightarrow> balL l (a,b) (delete x r))" |
24 |
24 |
25 |
25 |
26 subsection \<open>Functional Correctness\<close> |
26 subsection \<open>Functional Correctness\<close> |
27 |
27 |
28 theorem inorder_update_avl: |
28 theorem inorder_update: |
29 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
29 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
30 by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) |
30 by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) |
31 |
31 |
32 |
32 |
33 theorem inorder_delete_avl: |
33 theorem inorder_delete: |
34 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
34 "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
35 by(induction t) |
35 by(induction t) |
36 (auto simp: del_list_simps inorder_balL inorder_balR |
36 (auto simp: del_list_simps inorder_balL inorder_balR |
37 inorder_del_root inorder_split_maxD split: prod.splits) |
37 inorder_del_root inorder_split_maxD split: prod.splits) |
38 |
38 |
178 qed |
178 qed |
179 qed |
179 qed |
180 qed simp_all |
180 qed simp_all |
181 |
181 |
182 |
182 |
183 interpretation Map_by_Ordered |
183 interpretation M: Map_by_Ordered |
184 where empty = empty and lookup = lookup and update = update and delete = delete |
184 where empty = empty and lookup = lookup and update = update and delete = delete |
185 and inorder = inorder and inv = avl |
185 and inorder = inorder and inv = avl |
186 proof (standard, goal_cases) |
186 proof (standard, goal_cases) |
187 case 1 show ?case by (simp add: empty_def) |
187 case 1 show ?case by (simp add: empty_def) |
188 next |
188 next |
189 case 2 thus ?case by(simp add: lookup_map_of) |
189 case 2 thus ?case by(simp add: lookup_map_of) |
190 next |
190 next |
191 case 3 thus ?case by(simp add: inorder_update_avl) |
191 case 3 thus ?case by(simp add: inorder_update) |
192 next |
192 next |
193 case 4 thus ?case by(simp add: inorder_delete_avl) |
193 case 4 thus ?case by(simp add: inorder_delete) |
194 next |
194 next |
195 case 5 show ?case by (simp add: empty_def) |
195 case 5 show ?case by (simp add: empty_def) |
196 next |
196 next |
197 case 6 thus ?case by(simp add: avl_update(1)) |
197 case 6 thus ?case by(simp add: avl_update(1)) |
198 next |
198 next |