121 lemma inorder_upd: |
121 lemma inorder_upd: |
122 "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)" |
122 "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)" |
123 by(induction t) |
123 by(induction t) |
124 (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits) |
124 (auto simp: upd_list_simps, auto simp: upd_list_simps split: up\<^sub>i.splits) |
125 |
125 |
126 lemma inorder_update_234: |
126 lemma inorder_update: |
127 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
127 "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
128 by(simp add: update_def inorder_upd) |
128 by(simp add: update_def inorder_upd) |
129 |
129 |
130 lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
130 lemma inorder_del: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
131 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
131 inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
132 by(induction t rule: del.induct) |
132 by(induction t rule: del.induct) |
133 (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits) |
133 (auto simp: del_list_simps inorder_nodes split_minD split!: if_splits prod.splits) |
134 (* 30 secs (2016) *) |
134 (* 30 secs (2016) *) |
135 |
135 |
136 lemma inorder_delete_234: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
136 lemma inorder_delete: "\<lbrakk> bal t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
137 inorder(delete x t) = del_list x (inorder t)" |
137 inorder(delete x t) = del_list x (inorder t)" |
138 by(simp add: delete_def inorder_del) |
138 by(simp add: delete_def inorder_del) |
139 |
139 |
140 |
140 |
141 subsection \<open>Balancedness\<close> |
141 subsection \<open>Balancedness\<close> |
158 by(simp add: delete_def bal_tree\<^sub>d_del) |
158 by(simp add: delete_def bal_tree\<^sub>d_del) |
159 |
159 |
160 |
160 |
161 subsection \<open>Overall Correctness\<close> |
161 subsection \<open>Overall Correctness\<close> |
162 |
162 |
163 interpretation Map_by_Ordered |
163 interpretation M: Map_by_Ordered |
164 where empty = empty and lookup = lookup and update = update and delete = delete |
164 where empty = empty and lookup = lookup and update = update and delete = delete |
165 and inorder = inorder and inv = bal |
165 and inorder = inorder and inv = bal |
166 proof (standard, goal_cases) |
166 proof (standard, goal_cases) |
167 case 2 thus ?case by(simp add: lookup_map_of) |
167 case 2 thus ?case by(simp add: lookup_map_of) |
168 next |
168 next |
169 case 3 thus ?case by(simp add: inorder_update_234) |
169 case 3 thus ?case by(simp add: inorder_update) |
170 next |
170 next |
171 case 4 thus ?case by(simp add: inorder_delete_234) |
171 case 4 thus ?case by(simp add: inorder_delete) |
172 next |
172 next |
173 case 6 thus ?case by(simp add: bal_update) |
173 case 6 thus ?case by(simp add: bal_update) |
174 next |
174 next |
175 case 7 thus ?case by(simp add: bal_delete) |
175 case 7 thus ?case by(simp add: bal_delete) |
176 qed (simp add: empty_def)+ |
176 qed (simp add: empty_def)+ |