# HG changeset patch
# User nipkow
# Date 1566287302 -7200
# Node ID 17909568216ef9460accbb8ff8f22b380a424efe
# Parent  ea860617fac193bcbf7223d35cf4b900e375c9e0# Parent  7beee08eb16334d1a36b6a4331e5272e79a13aa5
merged

diff -r ea860617fac1 -r 17909568216e src/HOL/Data_Structures/Set2_Join.thy
--- a/src/HOL/Data_Structures/Set2_Join.thy	Mon Aug 19 21:37:34 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Tue Aug 20 09:48:22 2019 +0200
@@ -23,12 +23,10 @@
 fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
 fixes inv :: "('a,'b) tree \<Rightarrow> bool"
 assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r"
-assumes bst_join:
-  "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < a; \<forall>y \<in> set_tree r. a < y \<rbrakk>
-  \<Longrightarrow> bst (join l a r)"
+assumes bst_join: "bst (Node l a b r) \<Longrightarrow> bst (join l a r)"
 assumes inv_Leaf: "inv \<langle>\<rangle>"
 assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l a r)"
-assumes inv_Node: "\<lbrakk> inv (Node l a h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
+assumes inv_Node: "\<lbrakk> inv (Node l a b r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
 begin
 
 declare set_join [simp]
@@ -40,7 +38,7 @@
   (if l = Leaf then (a,r) else let (m,l') = split_min l in (m, join l' a r))"
 
 lemma split_min_set:
-  "\<lbrakk> split_min t = (m,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> m \<in> set_tree t \<and> set_tree t = Set.insert m (set_tree t')"
+  "\<lbrakk> split_min t = (m,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> m \<in> set_tree t \<and> set_tree t = {m} \<union> set_tree t'"
 proof(induction t arbitrary: t')
   case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
 next
@@ -115,7 +113,7 @@
 definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
 "insert x t = (let (l,_,r) = split t x in join l x r)"
 
-lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
+lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = {x} \<union> set_tree t"
 by(auto simp add: insert_def split split: prod.split)
 
 lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
diff -r ea860617fac1 -r 17909568216e src/HOL/Data_Structures/Set2_Join_RBT.thy
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Mon Aug 19 21:37:34 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Aug 20 09:48:22 2019 +0200
@@ -168,32 +168,32 @@
 by(simp add: set_joinL set_joinR set_paint)
 
 lemma bst_baliL:
-  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
-   \<Longrightarrow> bst (baliL l k r)"
-by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un)
+  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>x\<in>set_tree r. a < x\<rbrakk>
+   \<Longrightarrow> bst (baliL l a r)"
+by(cases "(l,a,r)" rule: baliL.cases) (auto simp: ball_Un)
 
 lemma bst_baliR:
-  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
-   \<Longrightarrow> bst (baliR l k r)"
-by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un)
+  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>x\<in>set_tree r. a < x\<rbrakk>
+   \<Longrightarrow> bst (baliR l a r)"
+by(cases "(l,a,r)" rule: baliR.cases) (auto simp: ball_Un)
 
 lemma bst_joinL:
-  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y; bheight l \<le> bheight r\<rbrakk>
-  \<Longrightarrow> bst (joinL l k r)"
-proof(induction l k r rule: joinL.induct)
-  case (1 l x r)
+  "\<lbrakk>bst (Node l a n r); bheight l \<le> bheight r\<rbrakk>
+  \<Longrightarrow> bst (joinL l a r)"
+proof(induction l a r rule: joinL.induct)
+  case (1 l a r)
   thus ?case
-    by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL
+    by(auto simp: set_baliL joinL.simps[of l a r] set_joinL ball_Un intro!: bst_baliL
         split!: tree.splits color.splits)
 qed
 
 lemma bst_joinR:
-  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
-  \<Longrightarrow> bst (joinR l k r)"
-proof(induction l k r rule: joinR.induct)
-  case (1 l x r)
+  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>y\<in>set_tree r. a < y \<rbrakk>
+  \<Longrightarrow> bst (joinR l a r)"
+proof(induction l a r rule: joinR.induct)
+  case (1 l a r)
   thus ?case
-    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
+    by(auto simp: set_baliR joinR.simps[of l a r] set_joinR ball_Un intro!: bst_baliR
         split!: tree.splits color.splits)
 qed
 
@@ -201,10 +201,11 @@
 by(cases t) auto
 
 lemma bst_join:
-  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
-  \<Longrightarrow> bst (join l k r)"
+  "bst (Node l a n r) \<Longrightarrow> bst (join l a r)"
 by(auto simp: bst_paint bst_joinL bst_joinR)
 
+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 invc_paint_Black invh_joinL invh_joinR invh_paint)
 
 subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
 
@@ -215,12 +216,11 @@
 proof (standard, goal_cases)
   case 1 show ?case by (rule set_join)
 next
-  case 2 thus ?case by (rule bst_join)
+  case 2 thus ?case by (simp add: bst_join del: join.simps)
 next
   case 3 show ?case by simp
 next
-  case 4 thus ?case
-    by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
+  case 4 thus ?case by (simp add: inv_join del: join.simps)
 next
   case 5 thus ?case by simp
 qed