62 qed |
62 qed |
63 |
63 |
64 |
64 |
65 subsection "\<open>join2\<close>" |
65 subsection "\<open>join2\<close>" |
66 |
66 |
67 definition join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
67 fun join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
68 "join2 l r = (if r = Leaf then l else let (m,r') = split_min r in join l m r')" |
68 "join2 l \<langle>\<rangle> = l" | |
|
69 "join2 l r = (let (m,r') = split_min r in join l m r')" |
69 |
70 |
70 lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r" |
71 lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r" |
71 by(simp add: join2_def split_min_set split: prod.split) |
72 by(cases r)(simp_all add: split_min_set split: prod.split) |
72 |
73 |
73 lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk> |
74 lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk> |
74 \<Longrightarrow> bst (join2 l r)" |
75 \<Longrightarrow> bst (join2 l r)" |
75 by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split) |
76 by(cases r)(simp_all add: bst_join split_min_set split_min_bst split: prod.split) |
76 |
77 |
77 lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)" |
78 lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)" |
78 by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split) |
79 by(cases r)(simp_all add: inv_join split_min_set split_min_inv split: prod.split) |
79 |
80 |
80 |
81 |
81 subsection "\<open>split\<close>" |
82 subsection "\<open>split\<close>" |
82 |
83 |
83 fun split :: "('a*'b)tree \<Rightarrow> 'a \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where |
84 fun split :: "('a*'b)tree \<Rightarrow> 'a \<Rightarrow> ('a*'b)tree \<times> bool \<times> ('a*'b)tree" where |