# HG changeset patch
# User nipkow
# Date 1527165767 -7200
# Node ID 035c78bb0a6675e8b5e9c5b42daa6410b353c1a0
# Parent  61188c781cddb7326825aa92d1310542a066859f
reorganization, everything based on Tree2 now

diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/Data_Structures/Set2_BST2_Join.thy
--- a/src/HOL/Data_Structures/Set2_BST2_Join.thy	Thu May 24 09:18:29 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,359 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section "Join-Based BST2 Implementation of Sets"
-
-theory Set2_BST2_Join
-imports
-  Isin2
-begin
-
-text \<open>Based on theory @{theory Tree2}, otherwise same as theory @{file "Set2_BST_Join.thy"}.\<close>
-
-text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
-\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
-All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
-and an element \<open>x\<close> such that \<open>l < x < r\<close>.
-
-The theory is based on theory @{theory Tree2} where nodes have an additional field.
-This field is ignored here but it means that this theory can be instantiated
-with red-black trees (see theory @{file "Set2_BST2_Join_RBT.thy"}) and other balanced trees.
-This approach is very concrete and fixes the type of trees.
-Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
-and recursion operators on it.\<close>
-
-locale Set2_BST2_Join =
-fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
-fixes inv :: "('a,'b) tree \<Rightarrow> bool"
-assumes inv_Leaf: "inv \<langle>\<rangle>"
-assumes set_join: "set_tree (join t1 x t2) = Set.insert x (set_tree t1 \<union> set_tree t2)"
-assumes 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)"
-assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
-assumes inv_Node: "\<lbrakk> inv (Node h l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
-begin
-
-declare set_join [simp]
-
-subsection "\<open>split_min\<close>"
-
-fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
-"split_min (Node _ l x r) =
-  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
-
-lemma split_min_set:
-  "\<lbrakk> split_min t = (x,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
-next
-  case Leaf thus ?case by simp
-qed
-
-lemma split_min_bst:
-  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
-next
-  case Leaf thus ?case by simp
-qed
-
-lemma split_min_inv:
-  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
-next
-  case Leaf thus ?case by simp
-qed
-
-
-subsection "\<open>join2\<close>"
-
-definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
-"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
-
-lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
-by(simp add: join2_def split_min_set split: prod.split)
-
-lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
-  \<Longrightarrow> bst (join2 l r)"
-by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
-
-lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
-by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
-
-
-subsection "\<open>split\<close>"
-
-fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
-"split Leaf k = (Leaf, False, Leaf)" |
-"split (Node _ l a r) k =
-  (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
-   if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
-   else (l, True, r))"
-
-lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
-  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
-  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
-proof(induction t arbitrary: l kin r)
-  case Leaf thus ?case by simp
-next
-  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
-qed
-
-lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
-proof(induction t arbitrary: l kin r)
-  case Leaf thus ?case by simp
-next
-  case Node
-  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
-qed
-
-declare split.simps[simp del]
-
-
-subsection "\<open>insert\<close>"
-
-definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
-"insert k t = (let (l,_,r) = split t k in join l k r)"
-
-lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
-by(auto simp add: insert_def split split: prod.split)
-
-lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
-by(auto simp add: insert_def bst_join dest: split split: prod.split)
-
-lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
-by(force simp: insert_def inv_join dest: split_inv split: prod.split)
-
-
-subsection "\<open>delete\<close>"
-
-definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
-"delete k t = (let (l,_,r) = split t k in join2 l r)"
-
-lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
-by(auto simp: delete_def split split: prod.split)
-
-lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
-by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
-
-lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
-by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
-
-
-subsection "\<open>union\<close>"
-
-fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
-"union t1 t2 =
-  (if t1 = Leaf then t2 else
-   if t2 = Leaf then t1 else
-   case t1 of Node _ l1 k r1 \<Rightarrow>
-   let (l2,_ ,r2) = split t2 k;
-       l' = union l1 l2; r' = union r1 r2
-   in join l' k r')"
-
-declare union.simps [simp del]
-
-lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  then show ?case
-    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
-qed
-
-lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
-        split: tree.split prod.split)
-qed
-
-lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp:union.simps[of t1 t2] inv_join split_inv
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-subsection "\<open>inter\<close>"
-
-fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
-"inter t1 t2 =
-  (if t1 = Leaf then Leaf else
-   if t2 = Leaf then Leaf else
-   case t1 of Node _ l1 k r1 \<Rightarrow>
-   let (l2,kin,r2) = split t2 k;
-       l' = inter l1 l2; r' = inter r1 r2
-   in if kin then join l' k r' else join2 l' r')"
-
-declare inter.simps [simp del]
-
-lemma set_tree_inter:
-  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  show ?case
-  proof (cases t1)
-    case Leaf thus ?thesis by (simp add: inter.simps)
-  next
-    case [simp]: (Node _ l1 k r1)
-    show ?thesis
-    proof (cases "t2 = Leaf")
-      case True thus ?thesis by (simp add: inter.simps)
-    next
-      case False
-      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
-      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
-      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
-      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
-      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
-           **: "?L2 \<inter> ?R2 = {}" "k \<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> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
-        by(simp add: t2)
-      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
-        using * ** by auto
-      also have "\<dots> = set_tree (inter t1 t2)"
-      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
-      finally show ?thesis by simp
-    qed
-  qed
-qed
-
-lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
-        intro!: bst_join bst_join2 split: tree.split prod.split)
-qed
-
-lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-subsection "\<open>diff\<close>"
-
-fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
-"diff t1 t2 =
-  (if t1 = Leaf then Leaf else
-   if t2 = Leaf then t1 else
-   case t2 of Node _ l2 k r2 \<Rightarrow>
-   let (l1,_,r1) = split t1 k;
-       l' = diff l1 l2; r' = diff r1 r2
-   in join2 l' r')"
-
-declare diff.simps [simp del]
-
-lemma set_tree_diff:
-  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  show ?case
-  proof (cases t2)
-    case Leaf thus ?thesis by (simp add: diff.simps)
-  next
-    case [simp]: (Node _ l2 k r2)
-    show ?thesis
-    proof (cases "t1 = Leaf")
-      case True thus ?thesis by (simp add: diff.simps)
-    next
-      case False
-      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
-      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
-      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
-      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
-           **: "k \<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"
-        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
-      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
-        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
-      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
-        by(simp add: t1)
-      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
-        using ** by auto
-      also have "\<dots> = set_tree (diff t1 t2)"
-      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
-      finally show ?thesis by simp
-    qed
-  qed
-qed
-
-lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
-        intro!: bst_join bst_join2 split: tree.split prod.split)
-qed
-
-lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-text \<open>Locale @{locale Set2_BST2_Join} implements locale @{locale Set2}:\<close>
-
-sublocale Set2
-where empty = Leaf and insert = insert and delete = delete and isin = isin
-and union = union and inter = inter and diff = diff
-and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
-proof (standard, goal_cases)
-  case 1 show ?case by (simp)
-next
-  case 2 thus ?case by(simp add: isin_set_tree)
-next
-  case 3 thus ?case by (simp add: set_tree_insert)
-next
-  case 4 thus ?case by (simp add: set_tree_delete)
-next
-  case 5 thus ?case by (simp add: inv_Leaf)
-next
-  case 6 thus ?case by (simp add: bst_insert inv_insert)
-next
-  case 7 thus ?case by (simp add: bst_delete inv_delete)
-next
-  case 8 thus ?case by(simp add: set_tree_union)
-next
-  case 9 thus ?case by(simp add: set_tree_inter)
-next
-  case 10 thus ?case by(simp add: set_tree_diff)
-next
-  case 11 thus ?case by (simp add: bst_union inv_union)
-next
-  case 12 thus ?case by (simp add: bst_inter inv_inter)
-next
-  case 13 thus ?case by (simp add: bst_diff inv_diff)
-qed
-
-end
-
-interpretation unbal: Set2_BST2_Join
-where join = "\<lambda>l x r. Node () l x r" and inv = "\<lambda>t. True"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by simp
-next
-  case 3 thus ?case by simp
-next
-  case 4 thus ?case by simp
-next
-  case 5 thus ?case by simp
-qed
-
-end
\ No newline at end of file
diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
--- a/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy	Thu May 24 09:18:29 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section "Join-Based BST2 Implementation of Sets via RBTs"
-
-theory Set2_BST2_Join_RBT
-imports
-  Set2_BST2_Join
-  RBT_Set
-begin
-
-subsection "Code"
-
-text \<open>
-Function \<open>joinL\<close> joins two trees (and an element).
-Precondition: @{prop "bheight l \<le> bheight r"}.
-Method:
-Descend along the left spine of \<open>r\<close>
-until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
-then combine them into a new red node.
-\<close>
-fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"joinL l x r =
-  (if bheight l = bheight r then R l x r
-   else case r of
-     B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
-     R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
-
-fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"joinR l x r =
-  (if bheight l \<le> bheight r then R l x r
-   else case l of
-     B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
-     R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
-
-fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"join l x r =
-  (if bheight l > bheight r
-   then paint Black (joinR l x r)
-   else if bheight l < bheight r
-   then paint Black (joinL l x r)
-   else B l x r)"
-
-declare joinL.simps[simp del]
-declare joinR.simps[simp del]
-
-text \<open>
-One would expect @{const joinR} to be be completely dual to @{const joinL}.
-Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
-is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
-the two versions behave exactly the same, including complexity. Thus from a programmer's
-perspective they are equivalent. However, not from a verifier's perspective:
-the total version of @{const joinR} is easier
-to reason about because lemmas about it may not require preconditions. In particular
-@{prop"set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"}
-is provable outright and hence also
-@{prop"set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"}.
-This is necessary because locale @{locale Set2_BST2_Join} unconditionally assumes
-exactly that. Adding preconditions to this assumptions significantly complicates
-the proofs within @{locale Set2_BST2_Join}, which we want to avoid.
-
-Why not work with the partial version of @{const joinR} and add the precondition
-@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
-we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
-are only called under the respective precondition. But function @{const bheight}
-makes the difference: it descends along the left spine, just like @{const joinL}.
-Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
-may change all the time. Thus we would need the further precondition @{prop "invh l"}.
-This is what we really wanted to avoid in order to satisfy the unconditional assumption
-in @{locale Set2_BST2_Join}.
-\<close>
-
-subsection "Properties"
-
-subsubsection "Color and height invariants"
-
-lemma invc2_joinL:
- "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
-  invc2 (joinL l x r)
-  \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))"
-proof (induct l x r rule: joinL.induct)
-  case (1 l x r) thus ?case
-    by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
-qed
-
-lemma invc2_joinR:
-  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
-  invc2 (joinR l x r)
-  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
-proof (induct l x r rule: joinR.induct)
-  case (1 l x r) thus ?case
-    by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
-qed
-
-lemma bheight_joinL:
-  "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r"
-proof (induct l x r rule: joinL.induct)
-  case (1 l x r) thus ?case
-    by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split)
-qed
-
-lemma invh_joinL:
-  "\<lbrakk> invh l;  invh r;  bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)"
-proof (induct l x r rule: joinL.induct)
-  case (1 l x r) thus ?case
-    by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
-qed
-
-lemma bheight_baliR:
-  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
-by (cases "(l,a,r)" rule: baliR.cases) auto
-
-lemma bheight_joinR:
-  "\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
-proof (induct l x r rule: joinR.induct)
-  case (1 l x r) thus ?case
-    by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split)
-qed
-
-lemma invh_joinR:
-  "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)"
-proof (induct l x r rule: joinR.induct)
-  case (1 l x r) thus ?case
-    by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r]
-        split!: tree.split color.split)
-qed
-
-(* unused *)
-lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
-by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
-    color_paint_Black)
-
-text \<open>To make sure the the black height is not increased unnecessarily:\<close>
-
-lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1"
-by(cases t) auto
-
-lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
-using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
-  bheight_joinL[of l r x] bheight_joinR[of l r x]
-by(auto simp: max_def rbt_def)
-
-
-subsubsection "Inorder properties"
-
-text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
-
-lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
-proof(induction l x r rule: joinL.induct)
-  case (1 l x r)
-  thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
-qed
-
-lemma inorder_joinR:
-  "inorder(joinR l x r) = inorder l @ x # inorder r"
-proof(induction l x r rule: joinR.induct)
-  case (1 l x r)
-  thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
-qed
-
-lemma "inorder(join l x r) = inorder l @ x # inorder r"
-by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
-      dest!: arg_cong[where f = inorder])
-
-
-subsubsection "Set and bst properties"
-
-lemma set_baliL:
-  "set_tree(baliL l a r) = Set.insert a (set_tree l \<union> set_tree r)"
-by(cases "(l,a,r)" rule: baliL.cases) (auto)
-
-lemma set_joinL:
-  "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = Set.insert x (set_tree l \<union> set_tree r)"
-proof(induction l x r rule: joinL.induct)
-  case (1 l x r)
-  thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
-qed
-
-lemma set_baliR:
-  "set_tree(baliR l a r) = Set.insert a (set_tree l \<union> set_tree r)"
-by(cases "(l,a,r)" rule: baliR.cases) (auto)
-
-lemma set_joinR:
-  "set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"
-proof(induction l x r rule: joinR.induct)
-  case (1 l x r)
-  thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
-qed
-
-lemma set_paint: "set_tree (paint c t) = set_tree t"
-by (cases t) auto
-
-lemma set_join: "set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"
-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)
-
-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)
-
-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)
-  thus ?case
-    by(auto simp: set_baliL joinL.simps[of l x 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)
-  thus ?case
-    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
-        split!: tree.splits color.splits)
-qed
-
-lemma bst_paint: "bst (paint c t) = bst t"
-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)"
-by(auto simp: bst_paint bst_joinL bst_joinR)
-
-
-subsubsection "Interpretation of @{locale Set2_BST2_Join} with Red-Black Tree"
-
-global_interpretation RBT: Set2_BST2_Join
-where join = join and inv = "\<lambda>t. invc t \<and> invh t"
-defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
-and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 show ?case by (rule set_join)
-next
-  case 3 thus ?case by (rule bst_join)
-next
-  case 4 thus ?case
-    by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
-next
-  case 5 thus ?case by simp
-qed
-
-text \<open>The invariant does not guarantee that the root node is black. This is not required
-to guarantee that the height is logarithmic in the size --- Exercise.\<close>
-
-end
\ No newline at end of file
diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/Data_Structures/Set2_BST_Join.thy
--- a/src/HOL/Data_Structures/Set2_BST_Join.thy	Thu May 24 09:18:29 2018 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,364 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-section "Join-Based BST Implementation of Sets"
-
-theory Set2_BST_Join
-imports
-  "HOL-Library.Tree"
-  Cmp
-  Set_Specs
-begin
-
-text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
-\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
-All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
-and an element \<open>x\<close> such that \<open>l < x < r\<close>.
-
-This theory illustrates the idea but is not suitable for an efficient implementation where
-\<open>join\<close> balances the tree in some manner because type @{typ "'a tree"} in theory @{theory Tree}
-has no additional fields for recording balance information. See theory \<open>Set2_BST2_Join\<close> for that.\<close>
-
-text \<open>Function \<open>isin\<close> can also be expressed via \<open>join\<close> but this is more direct:\<close>
-
-fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
-"isin Leaf x = False" |
-"isin (Node l a r) x =
-  (case cmp x a of
-     LT \<Rightarrow> isin l x |
-     EQ \<Rightarrow> True |
-     GT \<Rightarrow> isin r x)"
-
-lemma isin_set: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
-by (induction t) (auto)
-
-
-locale Set2_BST_Join =
-fixes join :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
-assumes set_join: "set_tree (join t1 x t2) = Set.insert x (set_tree t1 \<union> set_tree t2)"
-assumes 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)"
-fixes inv :: "'a tree \<Rightarrow> bool"
-assumes inv_Leaf: "inv \<langle>\<rangle>"
-assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
-assumes inv_Node: "\<lbrakk> inv (Node l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
-begin
-
-declare set_join [simp]
-
-subsection "\<open>split_min\<close>"
-
-fun split_min :: "'a tree \<Rightarrow> 'a \<times> 'a tree" where
-"split_min (Node l x r) =
-  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
-
-lemma split_min_set:
-  "\<lbrakk> split_min t = (x,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
-   x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(auto split: prod.splits if_splits)
-next
-  case Leaf thus ?case by simp
-qed
-
-lemma split_min_bst:
-  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
-next
-  case Leaf thus ?case by simp
-qed
-
-lemma split_min_inv:
-  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
-proof(induction t arbitrary: t')
-  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
-next
-  case Leaf thus ?case by simp
-qed
-
-
-subsection "\<open>join2\<close>"
-
-definition join2 :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
-
-lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
-by(simp add: join2_def split_min_set split: prod.split)
-
-lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
-  \<Longrightarrow> bst (join2 l r)"
-by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
-
-lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
-by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
-
-
-subsection "\<open>split\<close>"
-
-fun split :: "'a tree \<Rightarrow> 'a \<Rightarrow> 'a tree \<times> bool \<times> 'a tree" where
-"split Leaf k = (Leaf, False, Leaf)" |
-"split (Node l a r) k =
-  (case cmp k a of
-    LT \<Rightarrow> let (l1,b,l2) = split l k in (l1, b, join l2 a r) |
-    GT \<Rightarrow> let (r1,b,r2) = split r k in (join l a r1, b, r2) |
-    EQ \<Rightarrow> (l, True, r))"
-
-lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
-  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
-  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
-proof(induction t arbitrary: l kin r)
-  case Leaf thus ?case by simp
-next
-  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
-qed
-
-lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
-proof(induction t arbitrary: l kin r)
-  case Leaf thus ?case by simp
-next
-  case Node
-  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
-qed
-
-declare split.simps[simp del]
-
-
-subsection "\<open>insert\<close>"
-
-definition insert :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"insert k t = (let (l,_,r) = split t k in join l k r)"
-
-lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
-by(auto simp add: insert_def split split: prod.split)
-
-lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
-by(auto simp add: insert_def bst_join dest: split split: prod.split)
-
-lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
-by(force simp: insert_def inv_join dest: split_inv split: prod.split)
-
-
-subsection "\<open>delete\<close>"
-
-definition delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"delete k t = (let (l,_,r) = split t k in join2 l r)"
-
-lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
-by(auto simp: delete_def split split: prod.split)
-
-lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
-by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
-
-lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
-by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
-
-
-subsection "\<open>union\<close>"
-
-fun union :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"union t1 t2 =
-  (if t1 = Leaf then t2 else
-   if t2 = Leaf then t1 else
-   case t1 of Node l1 k r1 \<Rightarrow>
-   let (l2,_ ,r2) = split t2 k;
-       l' = union l1 l2; r' = union r1 r2
-   in join l' k r')"
-
-declare union.simps [simp del]
-
-lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  then show ?case
-    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
-qed
-
-lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
-        split: tree.split prod.split)
-qed
-
-lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
-proof(induction t1 t2 rule: union.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp:union.simps[of t1 t2] inv_join split_inv
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-subsection "\<open>inter\<close>"
-
-fun inter :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"inter t1 t2 =
-  (if t1 = Leaf then Leaf else
-   if t2 = Leaf then Leaf else
-   case t1 of Node l1 k r1 \<Rightarrow>
-   let (l2,kin,r2) = split t2 k;
-       l' = inter l1 l2; r' = inter r1 r2
-   in if kin then join l' k r' else join2 l' r')"
-
-declare inter.simps [simp del]
-
-lemma set_tree_inter:
-  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  show ?case
-  proof (cases t1)
-    case Leaf thus ?thesis by (simp add: inter.simps)
-  next
-    case [simp]: (Node l1 k r1)
-    show ?thesis
-    proof (cases "t2 = Leaf")
-      case True thus ?thesis by (simp add: inter.simps)
-    next
-      case False
-      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
-      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
-      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
-      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
-      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
-           **: "?L2 \<inter> ?R2 = {}" "k \<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> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
-        by(simp add: t2)
-      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
-        using * ** by auto
-      also have "\<dots> = set_tree (inter t1 t2)"
-      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
-      finally show ?thesis by simp
-    qed
-  qed
-qed
-
-lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
-        intro!: bst_join bst_join2 split: tree.split prod.split)
-qed
-
-lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
-proof(induction t1 t2 rule: inter.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-subsection "\<open>diff\<close>"
-
-fun diff :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"diff t1 t2 =
-  (if t1 = Leaf then Leaf else
-   if t2 = Leaf then t1 else
-   case t2 of Node l2 k r2 \<Rightarrow>
-   let (l1,_,r1) = split t1 k;
-       l' = diff l1 l2; r' = diff r1 r2
-   in join2 l' r')"
-
-declare diff.simps [simp del]
-
-lemma set_tree_diff:
-  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  show ?case
-  proof (cases t2)
-    case Leaf thus ?thesis by (simp add: diff.simps)
-  next
-    case [simp]: (Node l2 k r2)
-    show ?thesis
-    proof (cases "t1 = Leaf")
-      case True thus ?thesis by (simp add: diff.simps)
-    next
-      case False
-      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
-      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
-      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
-      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
-           **: "k \<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"
-        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
-      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
-        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
-      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
-        by(simp add: t1)
-      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
-        using ** by auto
-      also have "\<dots> = set_tree (diff t1 t2)"
-      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
-      finally show ?thesis by simp
-    qed
-  qed
-qed
-
-lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
-        intro!: bst_join bst_join2 split: tree.split prod.split)
-qed
-
-lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
-proof(induction t1 t2 rule: diff.induct)
-  case (1 t1 t2)
-  thus ?case
-    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
-        split!: tree.split prod.split dest: inv_Node)
-qed
-
-text \<open>Locale @{locale Set2_BST_Join} implements locale @{locale Set2}:\<close>
-
-sublocale Set2
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and  union = union and inter = inter and diff = diff
-and set = set_tree and invar = "\<lambda>t. bst t \<and> inv t"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by (simp add: isin_set)
-next
-  case 3 thus ?case by (simp add: set_tree_insert)
-next
-  case 4 thus ?case by (simp add: set_tree_delete)
-next
-  case 5 thus ?case by (simp add: inv_Leaf)
-next
-  case 6 thus ?case by (simp add: inv_insert bst_insert)
-next
-  case 7 thus ?case by (simp add: inv_delete bst_delete)
-next
-  case 8 thus ?case by (simp add: set_tree_union)
-next
-  case 9 thus ?case by (simp add: set_tree_inter)
-next
-  case 10 thus ?case by (simp add: set_tree_diff)
-next
-  case 11 thus ?case by (simp add: bst_union inv_union)
-next
-  case 12 thus ?case by (simp add: bst_inter inv_inter)
-next
-  case 13 thus ?case by (simp add: bst_diff inv_diff)
-qed
-
-end (* Set2_BST_Join *)
-
-text \<open>Interpretation of @{locale Set2_BST_Join} with unbalanced binary trees:\<close>
-
-interpretation Set2_BST_Join where join = Node and inv = "\<lambda>t. True"
-proof (standard, goal_cases)
-qed auto
-
-end
\ No newline at end of file
diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/Data_Structures/Set2_Join.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Set2_Join.thy	Thu May 24 14:42:47 2018 +0200
@@ -0,0 +1,357 @@
+(* Author: Tobias Nipkow *)
+
+section "Join-Based Implementation of Sets"
+
+theory Set2_Join
+imports
+  Isin2
+begin
+
+text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
+\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
+All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close>
+and an element \<open>x\<close> such that \<open>l < x < r\<close>.
+
+The theory is based on theory @{theory Tree2} where nodes have an additional field.
+This field is ignored here but it means that this theory can be instantiated
+with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees.
+This approach is very concrete and fixes the type of trees.
+Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
+and recursion operators on it.\<close>
+
+locale Set2_Join =
+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 inv_Leaf: "inv \<langle>\<rangle>"
+assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
+assumes inv_Node: "\<lbrakk> inv (Node h l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
+begin
+
+declare set_join [simp]
+
+subsection "\<open>split_min\<close>"
+
+fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
+"split_min (Node _ l x r) =
+  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
+
+lemma split_min_set:
+  "\<lbrakk> split_min t = (x,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
+proof(induction t arbitrary: t')
+  case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
+next
+  case Leaf thus ?case by simp
+qed
+
+lemma split_min_bst:
+  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
+proof(induction t arbitrary: t')
+  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
+next
+  case Leaf thus ?case by simp
+qed
+
+lemma split_min_inv:
+  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
+proof(induction t arbitrary: t')
+  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
+next
+  case Leaf thus ?case by simp
+qed
+
+
+subsection "\<open>join2\<close>"
+
+definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
+
+lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
+by(simp add: join2_def split_min_set split: prod.split)
+
+lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
+  \<Longrightarrow> bst (join2 l r)"
+by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
+
+lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
+by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
+
+
+subsection "\<open>split\<close>"
+
+fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
+"split Leaf k = (Leaf, False, Leaf)" |
+"split (Node _ l a r) k =
+  (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
+   if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
+   else (l, True, r))"
+
+lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
+  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
+  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
+proof(induction t arbitrary: l kin r)
+  case Leaf thus ?case by simp
+next
+  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
+qed
+
+lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
+proof(induction t arbitrary: l kin r)
+  case Leaf thus ?case by simp
+next
+  case Node
+  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
+qed
+
+declare split.simps[simp del]
+
+
+subsection "\<open>insert\<close>"
+
+definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+"insert k t = (let (l,_,r) = split t k in join l k r)"
+
+lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
+by(auto simp add: insert_def split split: prod.split)
+
+lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
+by(auto simp add: insert_def bst_join dest: split split: prod.split)
+
+lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
+by(force simp: insert_def inv_join dest: split_inv split: prod.split)
+
+
+subsection "\<open>delete\<close>"
+
+definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
+"delete k t = (let (l,_,r) = split t k in join2 l r)"
+
+lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
+by(auto simp: delete_def split split: prod.split)
+
+lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
+by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
+
+lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
+by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
+
+
+subsection "\<open>union\<close>"
+
+fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+"union t1 t2 =
+  (if t1 = Leaf then t2 else
+   if t2 = Leaf then t1 else
+   case t1 of Node _ l1 k r1 \<Rightarrow>
+   let (l2,_ ,r2) = split t2 k;
+       l' = union l1 l2; r' = union r1 r2
+   in join l' k r')"
+
+declare union.simps [simp del]
+
+lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
+proof(induction t1 t2 rule: union.induct)
+  case (1 t1 t2)
+  then show ?case
+    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
+qed
+
+lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
+proof(induction t1 t2 rule: union.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
+        split: tree.split prod.split)
+qed
+
+lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
+proof(induction t1 t2 rule: union.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(auto simp:union.simps[of t1 t2] inv_join split_inv
+        split!: tree.split prod.split dest: inv_Node)
+qed
+
+subsection "\<open>inter\<close>"
+
+fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+"inter t1 t2 =
+  (if t1 = Leaf then Leaf else
+   if t2 = Leaf then Leaf else
+   case t1 of Node _ l1 k r1 \<Rightarrow>
+   let (l2,kin,r2) = split t2 k;
+       l' = inter l1 l2; r' = inter r1 r2
+   in if kin then join l' k r' else join2 l' r')"
+
+declare inter.simps [simp del]
+
+lemma set_tree_inter:
+  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
+proof(induction t1 t2 rule: inter.induct)
+  case (1 t1 t2)
+  show ?case
+  proof (cases t1)
+    case Leaf thus ?thesis by (simp add: inter.simps)
+  next
+    case [simp]: (Node _ l1 k r1)
+    show ?thesis
+    proof (cases "t2 = Leaf")
+      case True thus ?thesis by (simp add: inter.simps)
+    next
+      case False
+      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
+      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
+      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
+      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
+      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
+           **: "?L2 \<inter> ?R2 = {}" "k \<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> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
+        by(simp add: t2)
+      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
+        using * ** by auto
+      also have "\<dots> = set_tree (inter t1 t2)"
+      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
+      finally show ?thesis by simp
+    qed
+  qed
+qed
+
+lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
+proof(induction t1 t2 rule: inter.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
+        intro!: bst_join bst_join2 split: tree.split prod.split)
+qed
+
+lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
+proof(induction t1 t2 rule: inter.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+        split!: tree.split prod.split dest: inv_Node)
+qed
+
+subsection "\<open>diff\<close>"
+
+fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
+"diff t1 t2 =
+  (if t1 = Leaf then Leaf else
+   if t2 = Leaf then t1 else
+   case t2 of Node _ l2 k r2 \<Rightarrow>
+   let (l1,_,r1) = split t1 k;
+       l' = diff l1 l2; r' = diff r1 r2
+   in join2 l' r')"
+
+declare diff.simps [simp del]
+
+lemma set_tree_diff:
+  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
+proof(induction t1 t2 rule: diff.induct)
+  case (1 t1 t2)
+  show ?case
+  proof (cases t2)
+    case Leaf thus ?thesis by (simp add: diff.simps)
+  next
+    case [simp]: (Node _ l2 k r2)
+    show ?thesis
+    proof (cases "t1 = Leaf")
+      case True thus ?thesis by (simp add: diff.simps)
+    next
+      case False
+      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
+      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
+      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
+      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
+           **: "k \<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"
+        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
+      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
+        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
+      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
+        by(simp add: t1)
+      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
+        using ** by auto
+      also have "\<dots> = set_tree (diff t1 t2)"
+      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
+      finally show ?thesis by simp
+    qed
+  qed
+qed
+
+lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
+proof(induction t1 t2 rule: diff.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
+        intro!: bst_join bst_join2 split: tree.split prod.split)
+qed
+
+lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
+proof(induction t1 t2 rule: diff.induct)
+  case (1 t1 t2)
+  thus ?case
+    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
+        split!: tree.split prod.split dest: inv_Node)
+qed
+
+text \<open>Locale @{locale Set2_Join} implements locale @{locale Set2}:\<close>
+
+sublocale Set2
+where empty = Leaf and insert = insert and delete = delete and isin = isin
+and union = union and inter = inter and diff = diff
+and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
+proof (standard, goal_cases)
+  case 1 show ?case by (simp)
+next
+  case 2 thus ?case by(simp add: isin_set_tree)
+next
+  case 3 thus ?case by (simp add: set_tree_insert)
+next
+  case 4 thus ?case by (simp add: set_tree_delete)
+next
+  case 5 thus ?case by (simp add: inv_Leaf)
+next
+  case 6 thus ?case by (simp add: bst_insert inv_insert)
+next
+  case 7 thus ?case by (simp add: bst_delete inv_delete)
+next
+  case 8 thus ?case by(simp add: set_tree_union)
+next
+  case 9 thus ?case by(simp add: set_tree_inter)
+next
+  case 10 thus ?case by(simp add: set_tree_diff)
+next
+  case 11 thus ?case by (simp add: bst_union inv_union)
+next
+  case 12 thus ?case by (simp add: bst_inter inv_inter)
+next
+  case 13 thus ?case by (simp add: bst_diff inv_diff)
+qed
+
+end
+
+interpretation unbal: Set2_Join
+where join = "\<lambda>l x r. Node () l x r" and inv = "\<lambda>t. True"
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by simp
+next
+  case 3 thus ?case by simp
+next
+  case 4 thus ?case by simp
+next
+  case 5 thus ?case by simp
+qed
+
+end
\ No newline at end of file
diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/Data_Structures/Set2_Join_RBT.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Thu May 24 14:42:47 2018 +0200
@@ -0,0 +1,256 @@
+(* Author: Tobias Nipkow *)
+
+section "Join-Based Implementation of Sets via RBTs"
+
+theory Set2_Join_RBT
+imports
+  Set2_Join
+  RBT_Set
+begin
+
+subsection "Code"
+
+text \<open>
+Function \<open>joinL\<close> joins two trees (and an element).
+Precondition: @{prop "bheight l \<le> bheight r"}.
+Method:
+Descend along the left spine of \<open>r\<close>
+until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
+then combine them into a new red node.
+\<close>
+fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"joinL l x r =
+  (if bheight l = bheight r then R l x r
+   else case r of
+     B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
+     R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
+
+fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"joinR l x r =
+  (if bheight l \<le> bheight r then R l x r
+   else case l of
+     B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
+     R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
+
+fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"join l x r =
+  (if bheight l > bheight r
+   then paint Black (joinR l x r)
+   else if bheight l < bheight r
+   then paint Black (joinL l x r)
+   else B l x r)"
+
+declare joinL.simps[simp del]
+declare joinR.simps[simp del]
+
+text \<open>
+One would expect @{const joinR} to be be completely dual to @{const joinL}.
+Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
+is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
+the two versions behave exactly the same, including complexity. Thus from a programmer's
+perspective they are equivalent. However, not from a verifier's perspective:
+the total version of @{const joinR} is easier
+to reason about because lemmas about it may not require preconditions. In particular
+@{prop"set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"}
+is provable outright and hence also
+@{prop"set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"}.
+This is necessary because locale @{locale Set2_Join} unconditionally assumes
+exactly that. Adding preconditions to this assumptions significantly complicates
+the proofs within @{locale Set2_Join}, which we want to avoid.
+
+Why not work with the partial version of @{const joinR} and add the precondition
+@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
+we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
+are only called under the respective precondition. But function @{const bheight}
+makes the difference: it descends along the left spine, just like @{const joinL}.
+Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
+may change all the time. Thus we would need the further precondition @{prop "invh l"}.
+This is what we really wanted to avoid in order to satisfy the unconditional assumption
+in @{locale Set2_Join}.
+\<close>
+
+subsection "Properties"
+
+subsubsection "Color and height invariants"
+
+lemma invc2_joinL:
+ "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
+  invc2 (joinL l x r)
+  \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))"
+proof (induct l x r rule: joinL.induct)
+  case (1 l x r) thus ?case
+    by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
+qed
+
+lemma invc2_joinR:
+  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
+  invc2 (joinR l x r)
+  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
+proof (induct l x r rule: joinR.induct)
+  case (1 l x r) thus ?case
+    by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
+qed
+
+lemma bheight_joinL:
+  "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r"
+proof (induct l x r rule: joinL.induct)
+  case (1 l x r) thus ?case
+    by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split)
+qed
+
+lemma invh_joinL:
+  "\<lbrakk> invh l;  invh r;  bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)"
+proof (induct l x r rule: joinL.induct)
+  case (1 l x r) thus ?case
+    by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
+qed
+
+lemma bheight_baliR:
+  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
+by (cases "(l,a,r)" rule: baliR.cases) auto
+
+lemma bheight_joinR:
+  "\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
+proof (induct l x r rule: joinR.induct)
+  case (1 l x r) thus ?case
+    by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split)
+qed
+
+lemma invh_joinR:
+  "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)"
+proof (induct l x r rule: joinR.induct)
+  case (1 l x r) thus ?case
+    by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r]
+        split!: tree.split color.split)
+qed
+
+(* unused *)
+lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
+by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
+    color_paint_Black)
+
+text \<open>To make sure the the black height is not increased unnecessarily:\<close>
+
+lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1"
+by(cases t) auto
+
+lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
+using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
+  bheight_joinL[of l r x] bheight_joinR[of l r x]
+by(auto simp: max_def rbt_def)
+
+
+subsubsection "Inorder properties"
+
+text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
+
+lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
+proof(induction l x r rule: joinL.induct)
+  case (1 l x r)
+  thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
+qed
+
+lemma inorder_joinR:
+  "inorder(joinR l x r) = inorder l @ x # inorder r"
+proof(induction l x r rule: joinR.induct)
+  case (1 l x r)
+  thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
+qed
+
+lemma "inorder(join l x r) = inorder l @ x # inorder r"
+by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
+      dest!: arg_cong[where f = inorder])
+
+
+subsubsection "Set and bst properties"
+
+lemma set_baliL:
+  "set_tree(baliL l a r) = set_tree l \<union> {a} \<union> set_tree r"
+by(cases "(l,a,r)" rule: baliL.cases) (auto)
+
+lemma set_joinL:
+  "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = set_tree l \<union> {x} \<union> set_tree r"
+proof(induction l x r rule: joinL.induct)
+  case (1 l x r)
+  thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
+qed
+
+lemma set_baliR:
+  "set_tree(baliR l a r) = set_tree l \<union> {a} \<union> set_tree r"
+by(cases "(l,a,r)" rule: baliR.cases) (auto)
+
+lemma set_joinR:
+  "set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"
+proof(induction l x r rule: joinR.induct)
+  case (1 l x r)
+  thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
+qed
+
+lemma set_paint: "set_tree (paint c t) = set_tree t"
+by (cases t) auto
+
+lemma set_join: "set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"
+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)
+
+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)
+
+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)
+  thus ?case
+    by(auto simp: set_baliL joinL.simps[of l x 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)
+  thus ?case
+    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
+        split!: tree.splits color.splits)
+qed
+
+lemma bst_paint: "bst (paint c t) = bst t"
+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)"
+by(auto simp: bst_paint bst_joinL bst_joinR)
+
+
+subsubsection "Interpretation of @{locale Set2_Join} with Red-Black Tree"
+
+global_interpretation RBT: Set2_Join
+where join = join and inv = "\<lambda>t. invc t \<and> invh t"
+defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
+and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
+proof (standard, goal_cases)
+  case 1 show ?case by (rule set_join)
+next
+  case 2 thus ?case by (rule bst_join)
+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)
+next
+  case 5 thus ?case by simp
+qed
+
+text \<open>The invariant does not guarantee that the root node is black. This is not required
+to guarantee that the height is logarithmic in the size --- Exercise.\<close>
+
+end
\ No newline at end of file
diff -r 61188c781cdd -r 035c78bb0a66 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu May 24 09:18:29 2018 +0200
+++ b/src/HOL/ROOT	Thu May 24 14:42:47 2018 +0200
@@ -200,8 +200,7 @@
     Tree234_Map
     Brother12_Map
     AA_Map
-    Set2_BST_Join
-    Set2_BST2_Join_RBT
+    Set2_Join_RBT
     Leftist_Heap
     Binomial_Heap
   document_files "root.tex" "root.bib"