author nipkow Fri, 18 Sep 2020 12:33:10 +0200 changeset 72269 88880eecd7fe parent 72268 71a8935eb5da child 72271 7e90e1d178b5 child 72272 6931ab4f1a47
tuned
```--- a/src/HOL/Data_Structures/Set2_Join.thy	Fri Sep 18 08:02:19 2020 +0100
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Fri Sep 18 12:33:10 2020 +0200
@@ -204,17 +204,17 @@
let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
have *: "a \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
obtain l2 ain r2 where sp: "split t2 a = (l2,ain,r2)" using prod_cases3 by blast
-      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if ain then {a} else {}"
-      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
+      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?A = "if ain then {a} else {}"
+      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?A" and
**: "?L2 \<inter> ?R2 = {}" "a \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
using "1.IH"(1)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
using "1.IH"(2)[OF _ False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
-      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {a}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
+      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {a}) \<inter> (?L2 \<union> ?R2 \<union> ?A)"
-      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
+      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?A"
using * ** by auto
also have "\<dots> = set_tree (inter t1 t2)"
using IHl IHr sp inter.simps[of t1 t2] False by(simp)
@@ -268,8 +268,8 @@
case False
let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
obtain l1 ain r1 where sp: "split t1 a = (l1,ain,r1)" using prod_cases3 by blast
-      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if ain then {a} else {}"
-      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
+      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?A = "if ain then {a} else {}"
+      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?A" and
**: "a \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"```
```--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Fri Sep 18 08:02:19 2020 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Fri Sep 18 12:33:10 2020 +0200
@@ -219,7 +219,7 @@
by(auto simp: bst_paint bst_joinL bst_joinR join_def)

lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"
-by (simp add: invc2_joinL invc2_joinR invh_joinL invh_joinR invh_paint join_def)
+by (simp add: inv_joinL inv_joinR invh_paint join_def)

subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
```