equal
deleted
inserted
replaced
27 assumes inv_Leaf: "inv \<langle>\<rangle>" |
27 assumes inv_Leaf: "inv \<langle>\<rangle>" |
28 assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l a r)" |
28 assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l a r)" |
29 assumes inv_Node: "\<lbrakk> inv (Node l (a,b) r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r" |
29 assumes inv_Node: "\<lbrakk> inv (Node l (a,b) r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r" |
30 begin |
30 begin |
31 |
31 |
32 declare set_join [simp] |
32 declare set_join [simp] Let_def[simp] |
33 |
33 |
34 subsection "\<open>split_min\<close>" |
34 subsection "\<open>split_min\<close>" |
35 |
35 |
36 fun split_min :: "('a*'b) tree \<Rightarrow> 'a \<times> ('a*'b) tree" where |
36 fun split_min :: "('a*'b) tree \<Rightarrow> 'a \<times> ('a*'b) tree" where |
37 "split_min (Node l (a, _) r) = |
37 "split_min (Node l (a, _) r) = |
225 |
225 |
226 lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)" |
226 lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)" |
227 proof(induction t1 t2 rule: inter.induct) |
227 proof(induction t1 t2 rule: inter.induct) |
228 case (1 t1 t2) |
228 case (1 t1 t2) |
229 thus ?case |
229 thus ?case |
230 by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def |
230 by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split |
231 intro!: bst_join bst_join2 split: tree.split prod.split) |
231 intro!: bst_join bst_join2 split: tree.split prod.split) |
232 qed |
232 qed |
233 |
233 |
234 lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)" |
234 lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)" |
235 proof(induction t1 t2 rule: inter.induct) |
235 proof(induction t1 t2 rule: inter.induct) |
236 case (1 t1 t2) |
236 case (1 t1 t2) |
237 thus ?case |
237 thus ?case |
238 by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def |
238 by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv |
239 split!: tree.split prod.split dest: inv_Node) |
239 split!: tree.split prod.split dest: inv_Node) |
240 qed |
240 qed |
241 |
241 |
242 subsection "\<open>diff\<close>" |
242 subsection "\<open>diff\<close>" |
243 |
243 |
289 |
289 |
290 lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)" |
290 lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)" |
291 proof(induction t1 t2 rule: diff.induct) |
291 proof(induction t1 t2 rule: diff.induct) |
292 case (1 t1 t2) |
292 case (1 t1 t2) |
293 thus ?case |
293 thus ?case |
294 by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def |
294 by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split |
295 intro!: bst_join bst_join2 split: tree.split prod.split) |
295 intro!: bst_join bst_join2 split: tree.split prod.split) |
296 qed |
296 qed |
297 |
297 |
298 lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)" |
298 lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)" |
299 proof(induction t1 t2 rule: diff.induct) |
299 proof(induction t1 t2 rule: diff.induct) |
300 case (1 t1 t2) |
300 case (1 t1 t2) |
301 thus ?case |
301 thus ?case |
302 by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def |
302 by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv |
303 split!: tree.split prod.split dest: inv_Node) |
303 split!: tree.split prod.split dest: inv_Node) |
304 qed |
304 qed |
305 |
305 |
306 text \<open>Locale \<^locale>\<open>Set2_Join\<close> implements locale \<^locale>\<open>Set2\<close>:\<close> |
306 text \<open>Locale \<^locale>\<open>Set2_Join\<close> implements locale \<^locale>\<open>Set2\<close>:\<close> |
307 |
307 |