86 (case cmp x a of |
86 (case cmp x a of |
87 LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) | |
87 LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) | |
88 GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) | |
88 GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) | |
89 EQ \<Rightarrow> (l, True, r))" |
89 EQ \<Rightarrow> (l, True, r))" |
90 |
90 |
91 lemma split: "split t x = (l,xin,r) \<Longrightarrow> bst t \<Longrightarrow> |
91 lemma split: "split t x = (l,b,r) \<Longrightarrow> bst t \<Longrightarrow> |
92 set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a} |
92 set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a} |
93 \<and> (xin = (x \<in> set_tree t)) \<and> bst l \<and> bst r" |
93 \<and> (b = (x \<in> set_tree t)) \<and> bst l \<and> bst r" |
94 proof(induction t arbitrary: l xin r rule: tree2_induct) |
94 proof(induction t arbitrary: l b r rule: tree2_induct) |
95 case Leaf thus ?case by simp |
95 case Leaf thus ?case by simp |
96 next |
96 next |
97 case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join) |
97 case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join) |
98 qed |
98 qed |
99 |
99 |
100 lemma split_inv: "split t x = (l,xin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r" |
100 lemma split_inv: "split t x = (l,b,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r" |
101 proof(induction t arbitrary: l xin r rule: tree2_induct) |
101 proof(induction t arbitrary: l b r rule: tree2_induct) |
102 case Leaf thus ?case by simp |
102 case Leaf thus ?case by simp |
103 next |
103 next |
104 case Node |
104 case Node |
105 thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node) |
105 thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node) |
106 qed |
106 qed |
179 fun inter :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where |
179 fun inter :: "('a*'b)tree \<Rightarrow> ('a*'b)tree \<Rightarrow> ('a*'b)tree" where |
180 "inter t1 t2 = |
180 "inter t1 t2 = |
181 (if t1 = Leaf then Leaf else |
181 (if t1 = Leaf then Leaf else |
182 if t2 = Leaf then Leaf else |
182 if t2 = Leaf then Leaf else |
183 case t1 of Node l1 (a, _) r1 \<Rightarrow> |
183 case t1 of Node l1 (a, _) r1 \<Rightarrow> |
184 let (l2,ain,r2) = split t2 a; |
184 let (l2,b,r2) = split t2 a; |
185 l' = inter l1 l2; r' = inter r1 r2 |
185 l' = inter l1 l2; r' = inter r1 r2 |
186 in if ain then join l' a r' else join2 l' r')" |
186 in if b then join l' a r' else join2 l' r')" |
187 |
187 |
188 declare inter.simps [simp del] |
188 declare inter.simps [simp del] |
189 |
189 |
190 lemma set_tree_inter: |
190 lemma set_tree_inter: |
191 "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2" |
191 "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2" |
201 case True thus ?thesis by (simp add: inter.simps) |
201 case True thus ?thesis by (simp add: inter.simps) |
202 next |
202 next |
203 case False |
203 case False |
204 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" |
204 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" |
205 have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce) |
205 have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce) |
206 obtain l2 ain r2 where sp: "split t2 a = (l2,ain,r2)" using prod_cases3 by blast |
206 obtain l2 b r2 where sp: "split t2 a = (l2,b,r2)" using prod_cases3 by blast |
207 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?A = "if ain then {a} else {}" |
207 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?A = "if b then {a} else {}" |
208 have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?A" and |
208 have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?A" and |
209 **: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" |
209 **: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" |
210 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force) |
210 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force) |
211 have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2" |
211 have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2" |
212 using "1.IH"(1)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp |
212 using "1.IH"(1)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp |
265 proof (cases "t1 = Leaf") |
265 proof (cases "t1 = Leaf") |
266 case True thus ?thesis by (simp add: diff.simps) |
266 case True thus ?thesis by (simp add: diff.simps) |
267 next |
267 next |
268 case False |
268 case False |
269 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" |
269 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" |
270 obtain l1 ain r1 where sp: "split t1 a = (l1,ain,r1)" using prod_cases3 by blast |
270 obtain l1 b r1 where sp: "split t1 a = (l1,b,r1)" using prod_cases3 by blast |
271 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?A = "if ain then {a} else {}" |
271 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?A = "if b then {a} else {}" |
272 have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?A" and |
272 have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?A" and |
273 **: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" |
273 **: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" |
274 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force) |
274 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force) |
275 have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2" |
275 have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2" |
276 using "1.IH"(1)[OF False _ _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp |
276 using "1.IH"(1)[OF False _ _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp |