# HG changeset patch
# User nipkow
# Date 1600425190 -7200
# Node ID 88880eecd7fe302f9dce36237a9f97f0ee2c6116
# Parent  71a8935eb5da612f37ee607cb0f630661b587005
tuned

diff -r 71a8935eb5da -r 88880eecd7fe src/HOL/Data_Structures/Set2_Join.thy
--- 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)"
         by(simp add: t2)
-      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"
diff -r 71a8935eb5da -r 88880eecd7fe src/HOL/Data_Structures/Set2_Join_RBT.thy
--- 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"