reorganization, everything based on Tree2 now
authornipkow
Thu May 24 14:42:47 2018 +0200 (21 months ago)
changeset 68261035c78bb0a66
parent 68260 61188c781cdd
child 68262 d231238bd977
reorganization, everything based on Tree2 now
src/HOL/Data_Structures/Set2_BST2_Join.thy
src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy
src/HOL/Data_Structures/Set2_BST_Join.thy
src/HOL/Data_Structures/Set2_Join.thy
src/HOL/Data_Structures/Set2_Join_RBT.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Data_Structures/Set2_BST2_Join.thy	Thu May 24 09:18:29 2018 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,359 +0,0 @@
     1.4 -(* Author: Tobias Nipkow *)
     1.5 -
     1.6 -section "Join-Based BST2 Implementation of Sets"
     1.7 -
     1.8 -theory Set2_BST2_Join
     1.9 -imports
    1.10 -  Isin2
    1.11 -begin
    1.12 -
    1.13 -text \<open>Based on theory @{theory Tree2}, otherwise same as theory @{file "Set2_BST_Join.thy"}.\<close>
    1.14 -
    1.15 -text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
    1.16 -\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
    1.17 -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>
    1.18 -and an element \<open>x\<close> such that \<open>l < x < r\<close>.
    1.19 -
    1.20 -The theory is based on theory @{theory Tree2} where nodes have an additional field.
    1.21 -This field is ignored here but it means that this theory can be instantiated
    1.22 -with red-black trees (see theory @{file "Set2_BST2_Join_RBT.thy"}) and other balanced trees.
    1.23 -This approach is very concrete and fixes the type of trees.
    1.24 -Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
    1.25 -and recursion operators on it.\<close>
    1.26 -
    1.27 -locale Set2_BST2_Join =
    1.28 -fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
    1.29 -fixes inv :: "('a,'b) tree \<Rightarrow> bool"
    1.30 -assumes inv_Leaf: "inv \<langle>\<rangle>"
    1.31 -assumes set_join: "set_tree (join t1 x t2) = Set.insert x (set_tree t1 \<union> set_tree t2)"
    1.32 -assumes bst_join:
    1.33 -  "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < k; \<forall>y \<in> set_tree r. k < y \<rbrakk>
    1.34 -  \<Longrightarrow> bst (join l k r)"
    1.35 -assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
    1.36 -assumes inv_Node: "\<lbrakk> inv (Node h l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
    1.37 -begin
    1.38 -
    1.39 -declare set_join [simp]
    1.40 -
    1.41 -subsection "\<open>split_min\<close>"
    1.42 -
    1.43 -fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
    1.44 -"split_min (Node _ l x r) =
    1.45 -  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
    1.46 -
    1.47 -lemma split_min_set:
    1.48 -  "\<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')"
    1.49 -proof(induction t arbitrary: t')
    1.50 -  case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
    1.51 -next
    1.52 -  case Leaf thus ?case by simp
    1.53 -qed
    1.54 -
    1.55 -lemma split_min_bst:
    1.56 -  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
    1.57 -proof(induction t arbitrary: t')
    1.58 -  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
    1.59 -next
    1.60 -  case Leaf thus ?case by simp
    1.61 -qed
    1.62 -
    1.63 -lemma split_min_inv:
    1.64 -  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
    1.65 -proof(induction t arbitrary: t')
    1.66 -  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
    1.67 -next
    1.68 -  case Leaf thus ?case by simp
    1.69 -qed
    1.70 -
    1.71 -
    1.72 -subsection "\<open>join2\<close>"
    1.73 -
    1.74 -definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
    1.75 -"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
    1.76 -
    1.77 -lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
    1.78 -by(simp add: join2_def split_min_set split: prod.split)
    1.79 -
    1.80 -lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
    1.81 -  \<Longrightarrow> bst (join2 l r)"
    1.82 -by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
    1.83 -
    1.84 -lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
    1.85 -by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
    1.86 -
    1.87 -
    1.88 -subsection "\<open>split\<close>"
    1.89 -
    1.90 -fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
    1.91 -"split Leaf k = (Leaf, False, Leaf)" |
    1.92 -"split (Node _ l a r) k =
    1.93 -  (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
    1.94 -   if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
    1.95 -   else (l, True, r))"
    1.96 -
    1.97 -lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
    1.98 -  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
    1.99 -  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
   1.100 -proof(induction t arbitrary: l kin r)
   1.101 -  case Leaf thus ?case by simp
   1.102 -next
   1.103 -  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
   1.104 -qed
   1.105 -
   1.106 -lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
   1.107 -proof(induction t arbitrary: l kin r)
   1.108 -  case Leaf thus ?case by simp
   1.109 -next
   1.110 -  case Node
   1.111 -  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
   1.112 -qed
   1.113 -
   1.114 -declare split.simps[simp del]
   1.115 -
   1.116 -
   1.117 -subsection "\<open>insert\<close>"
   1.118 -
   1.119 -definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
   1.120 -"insert k t = (let (l,_,r) = split t k in join l k r)"
   1.121 -
   1.122 -lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
   1.123 -by(auto simp add: insert_def split split: prod.split)
   1.124 -
   1.125 -lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
   1.126 -by(auto simp add: insert_def bst_join dest: split split: prod.split)
   1.127 -
   1.128 -lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
   1.129 -by(force simp: insert_def inv_join dest: split_inv split: prod.split)
   1.130 -
   1.131 -
   1.132 -subsection "\<open>delete\<close>"
   1.133 -
   1.134 -definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
   1.135 -"delete k t = (let (l,_,r) = split t k in join2 l r)"
   1.136 -
   1.137 -lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
   1.138 -by(auto simp: delete_def split split: prod.split)
   1.139 -
   1.140 -lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
   1.141 -by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
   1.142 -
   1.143 -lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
   1.144 -by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
   1.145 -
   1.146 -
   1.147 -subsection "\<open>union\<close>"
   1.148 -
   1.149 -fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   1.150 -"union t1 t2 =
   1.151 -  (if t1 = Leaf then t2 else
   1.152 -   if t2 = Leaf then t1 else
   1.153 -   case t1 of Node _ l1 k r1 \<Rightarrow>
   1.154 -   let (l2,_ ,r2) = split t2 k;
   1.155 -       l' = union l1 l2; r' = union r1 r2
   1.156 -   in join l' k r')"
   1.157 -
   1.158 -declare union.simps [simp del]
   1.159 -
   1.160 -lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
   1.161 -proof(induction t1 t2 rule: union.induct)
   1.162 -  case (1 t1 t2)
   1.163 -  then show ?case
   1.164 -    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
   1.165 -qed
   1.166 -
   1.167 -lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
   1.168 -proof(induction t1 t2 rule: union.induct)
   1.169 -  case (1 t1 t2)
   1.170 -  thus ?case
   1.171 -    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
   1.172 -        split: tree.split prod.split)
   1.173 -qed
   1.174 -
   1.175 -lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
   1.176 -proof(induction t1 t2 rule: union.induct)
   1.177 -  case (1 t1 t2)
   1.178 -  thus ?case
   1.179 -    by(auto simp:union.simps[of t1 t2] inv_join split_inv
   1.180 -        split!: tree.split prod.split dest: inv_Node)
   1.181 -qed
   1.182 -
   1.183 -subsection "\<open>inter\<close>"
   1.184 -
   1.185 -fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   1.186 -"inter t1 t2 =
   1.187 -  (if t1 = Leaf then Leaf else
   1.188 -   if t2 = Leaf then Leaf else
   1.189 -   case t1 of Node _ l1 k r1 \<Rightarrow>
   1.190 -   let (l2,kin,r2) = split t2 k;
   1.191 -       l' = inter l1 l2; r' = inter r1 r2
   1.192 -   in if kin then join l' k r' else join2 l' r')"
   1.193 -
   1.194 -declare inter.simps [simp del]
   1.195 -
   1.196 -lemma set_tree_inter:
   1.197 -  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
   1.198 -proof(induction t1 t2 rule: inter.induct)
   1.199 -  case (1 t1 t2)
   1.200 -  show ?case
   1.201 -  proof (cases t1)
   1.202 -    case Leaf thus ?thesis by (simp add: inter.simps)
   1.203 -  next
   1.204 -    case [simp]: (Node _ l1 k r1)
   1.205 -    show ?thesis
   1.206 -    proof (cases "t2 = Leaf")
   1.207 -      case True thus ?thesis by (simp add: inter.simps)
   1.208 -    next
   1.209 -      case False
   1.210 -      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
   1.211 -      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
   1.212 -      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
   1.213 -      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
   1.214 -      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
   1.215 -           **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   1.216 -        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
   1.217 -      have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
   1.218 -        using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   1.219 -      have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
   1.220 -        using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   1.221 -      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
   1.222 -        by(simp add: t2)
   1.223 -      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
   1.224 -        using * ** by auto
   1.225 -      also have "\<dots> = set_tree (inter t1 t2)"
   1.226 -      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
   1.227 -      finally show ?thesis by simp
   1.228 -    qed
   1.229 -  qed
   1.230 -qed
   1.231 -
   1.232 -lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
   1.233 -proof(induction t1 t2 rule: inter.induct)
   1.234 -  case (1 t1 t2)
   1.235 -  thus ?case
   1.236 -    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
   1.237 -        intro!: bst_join bst_join2 split: tree.split prod.split)
   1.238 -qed
   1.239 -
   1.240 -lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
   1.241 -proof(induction t1 t2 rule: inter.induct)
   1.242 -  case (1 t1 t2)
   1.243 -  thus ?case
   1.244 -    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   1.245 -        split!: tree.split prod.split dest: inv_Node)
   1.246 -qed
   1.247 -
   1.248 -subsection "\<open>diff\<close>"
   1.249 -
   1.250 -fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   1.251 -"diff t1 t2 =
   1.252 -  (if t1 = Leaf then Leaf else
   1.253 -   if t2 = Leaf then t1 else
   1.254 -   case t2 of Node _ l2 k r2 \<Rightarrow>
   1.255 -   let (l1,_,r1) = split t1 k;
   1.256 -       l' = diff l1 l2; r' = diff r1 r2
   1.257 -   in join2 l' r')"
   1.258 -
   1.259 -declare diff.simps [simp del]
   1.260 -
   1.261 -lemma set_tree_diff:
   1.262 -  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
   1.263 -proof(induction t1 t2 rule: diff.induct)
   1.264 -  case (1 t1 t2)
   1.265 -  show ?case
   1.266 -  proof (cases t2)
   1.267 -    case Leaf thus ?thesis by (simp add: diff.simps)
   1.268 -  next
   1.269 -    case [simp]: (Node _ l2 k r2)
   1.270 -    show ?thesis
   1.271 -    proof (cases "t1 = Leaf")
   1.272 -      case True thus ?thesis by (simp add: diff.simps)
   1.273 -    next
   1.274 -      case False
   1.275 -      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
   1.276 -      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
   1.277 -      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
   1.278 -      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
   1.279 -           **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   1.280 -        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
   1.281 -      have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
   1.282 -        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   1.283 -      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
   1.284 -        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   1.285 -      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
   1.286 -        by(simp add: t1)
   1.287 -      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
   1.288 -        using ** by auto
   1.289 -      also have "\<dots> = set_tree (diff t1 t2)"
   1.290 -      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
   1.291 -      finally show ?thesis by simp
   1.292 -    qed
   1.293 -  qed
   1.294 -qed
   1.295 -
   1.296 -lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
   1.297 -proof(induction t1 t2 rule: diff.induct)
   1.298 -  case (1 t1 t2)
   1.299 -  thus ?case
   1.300 -    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
   1.301 -        intro!: bst_join bst_join2 split: tree.split prod.split)
   1.302 -qed
   1.303 -
   1.304 -lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
   1.305 -proof(induction t1 t2 rule: diff.induct)
   1.306 -  case (1 t1 t2)
   1.307 -  thus ?case
   1.308 -    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   1.309 -        split!: tree.split prod.split dest: inv_Node)
   1.310 -qed
   1.311 -
   1.312 -text \<open>Locale @{locale Set2_BST2_Join} implements locale @{locale Set2}:\<close>
   1.313 -
   1.314 -sublocale Set2
   1.315 -where empty = Leaf and insert = insert and delete = delete and isin = isin
   1.316 -and union = union and inter = inter and diff = diff
   1.317 -and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
   1.318 -proof (standard, goal_cases)
   1.319 -  case 1 show ?case by (simp)
   1.320 -next
   1.321 -  case 2 thus ?case by(simp add: isin_set_tree)
   1.322 -next
   1.323 -  case 3 thus ?case by (simp add: set_tree_insert)
   1.324 -next
   1.325 -  case 4 thus ?case by (simp add: set_tree_delete)
   1.326 -next
   1.327 -  case 5 thus ?case by (simp add: inv_Leaf)
   1.328 -next
   1.329 -  case 6 thus ?case by (simp add: bst_insert inv_insert)
   1.330 -next
   1.331 -  case 7 thus ?case by (simp add: bst_delete inv_delete)
   1.332 -next
   1.333 -  case 8 thus ?case by(simp add: set_tree_union)
   1.334 -next
   1.335 -  case 9 thus ?case by(simp add: set_tree_inter)
   1.336 -next
   1.337 -  case 10 thus ?case by(simp add: set_tree_diff)
   1.338 -next
   1.339 -  case 11 thus ?case by (simp add: bst_union inv_union)
   1.340 -next
   1.341 -  case 12 thus ?case by (simp add: bst_inter inv_inter)
   1.342 -next
   1.343 -  case 13 thus ?case by (simp add: bst_diff inv_diff)
   1.344 -qed
   1.345 -
   1.346 -end
   1.347 -
   1.348 -interpretation unbal: Set2_BST2_Join
   1.349 -where join = "\<lambda>l x r. Node () l x r" and inv = "\<lambda>t. True"
   1.350 -proof (standard, goal_cases)
   1.351 -  case 1 show ?case by simp
   1.352 -next
   1.353 -  case 2 thus ?case by simp
   1.354 -next
   1.355 -  case 3 thus ?case by simp
   1.356 -next
   1.357 -  case 4 thus ?case by simp
   1.358 -next
   1.359 -  case 5 thus ?case by simp
   1.360 -qed
   1.361 -
   1.362 -end
   1.363 \ No newline at end of file
     2.1 --- a/src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy	Thu May 24 09:18:29 2018 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,256 +0,0 @@
     2.4 -(* Author: Tobias Nipkow *)
     2.5 -
     2.6 -section "Join-Based BST2 Implementation of Sets via RBTs"
     2.7 -
     2.8 -theory Set2_BST2_Join_RBT
     2.9 -imports
    2.10 -  Set2_BST2_Join
    2.11 -  RBT_Set
    2.12 -begin
    2.13 -
    2.14 -subsection "Code"
    2.15 -
    2.16 -text \<open>
    2.17 -Function \<open>joinL\<close> joins two trees (and an element).
    2.18 -Precondition: @{prop "bheight l \<le> bheight r"}.
    2.19 -Method:
    2.20 -Descend along the left spine of \<open>r\<close>
    2.21 -until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
    2.22 -then combine them into a new red node.
    2.23 -\<close>
    2.24 -fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    2.25 -"joinL l x r =
    2.26 -  (if bheight l = bheight r then R l x r
    2.27 -   else case r of
    2.28 -     B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
    2.29 -     R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
    2.30 -
    2.31 -fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    2.32 -"joinR l x r =
    2.33 -  (if bheight l \<le> bheight r then R l x r
    2.34 -   else case l of
    2.35 -     B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
    2.36 -     R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
    2.37 -
    2.38 -fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    2.39 -"join l x r =
    2.40 -  (if bheight l > bheight r
    2.41 -   then paint Black (joinR l x r)
    2.42 -   else if bheight l < bheight r
    2.43 -   then paint Black (joinL l x r)
    2.44 -   else B l x r)"
    2.45 -
    2.46 -declare joinL.simps[simp del]
    2.47 -declare joinR.simps[simp del]
    2.48 -
    2.49 -text \<open>
    2.50 -One would expect @{const joinR} to be be completely dual to @{const joinL}.
    2.51 -Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
    2.52 -is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
    2.53 -the two versions behave exactly the same, including complexity. Thus from a programmer's
    2.54 -perspective they are equivalent. However, not from a verifier's perspective:
    2.55 -the total version of @{const joinR} is easier
    2.56 -to reason about because lemmas about it may not require preconditions. In particular
    2.57 -@{prop"set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"}
    2.58 -is provable outright and hence also
    2.59 -@{prop"set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"}.
    2.60 -This is necessary because locale @{locale Set2_BST2_Join} unconditionally assumes
    2.61 -exactly that. Adding preconditions to this assumptions significantly complicates
    2.62 -the proofs within @{locale Set2_BST2_Join}, which we want to avoid.
    2.63 -
    2.64 -Why not work with the partial version of @{const joinR} and add the precondition
    2.65 -@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
    2.66 -we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
    2.67 -are only called under the respective precondition. But function @{const bheight}
    2.68 -makes the difference: it descends along the left spine, just like @{const joinL}.
    2.69 -Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
    2.70 -may change all the time. Thus we would need the further precondition @{prop "invh l"}.
    2.71 -This is what we really wanted to avoid in order to satisfy the unconditional assumption
    2.72 -in @{locale Set2_BST2_Join}.
    2.73 -\<close>
    2.74 -
    2.75 -subsection "Properties"
    2.76 -
    2.77 -subsubsection "Color and height invariants"
    2.78 -
    2.79 -lemma invc2_joinL:
    2.80 - "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
    2.81 -  invc2 (joinL l x r)
    2.82 -  \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))"
    2.83 -proof (induct l x r rule: joinL.induct)
    2.84 -  case (1 l x r) thus ?case
    2.85 -    by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
    2.86 -qed
    2.87 -
    2.88 -lemma invc2_joinR:
    2.89 -  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
    2.90 -  invc2 (joinR l x r)
    2.91 -  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
    2.92 -proof (induct l x r rule: joinR.induct)
    2.93 -  case (1 l x r) thus ?case
    2.94 -    by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
    2.95 -qed
    2.96 -
    2.97 -lemma bheight_joinL:
    2.98 -  "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r"
    2.99 -proof (induct l x r rule: joinL.induct)
   2.100 -  case (1 l x r) thus ?case
   2.101 -    by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split)
   2.102 -qed
   2.103 -
   2.104 -lemma invh_joinL:
   2.105 -  "\<lbrakk> invh l;  invh r;  bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)"
   2.106 -proof (induct l x r rule: joinL.induct)
   2.107 -  case (1 l x r) thus ?case
   2.108 -    by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
   2.109 -qed
   2.110 -
   2.111 -lemma bheight_baliR:
   2.112 -  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
   2.113 -by (cases "(l,a,r)" rule: baliR.cases) auto
   2.114 -
   2.115 -lemma bheight_joinR:
   2.116 -  "\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
   2.117 -proof (induct l x r rule: joinR.induct)
   2.118 -  case (1 l x r) thus ?case
   2.119 -    by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split)
   2.120 -qed
   2.121 -
   2.122 -lemma invh_joinR:
   2.123 -  "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)"
   2.124 -proof (induct l x r rule: joinR.induct)
   2.125 -  case (1 l x r) thus ?case
   2.126 -    by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r]
   2.127 -        split!: tree.split color.split)
   2.128 -qed
   2.129 -
   2.130 -(* unused *)
   2.131 -lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
   2.132 -by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
   2.133 -    color_paint_Black)
   2.134 -
   2.135 -text \<open>To make sure the the black height is not increased unnecessarily:\<close>
   2.136 -
   2.137 -lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1"
   2.138 -by(cases t) auto
   2.139 -
   2.140 -lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
   2.141 -using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
   2.142 -  bheight_joinL[of l r x] bheight_joinR[of l r x]
   2.143 -by(auto simp: max_def rbt_def)
   2.144 -
   2.145 -
   2.146 -subsubsection "Inorder properties"
   2.147 -
   2.148 -text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
   2.149 -
   2.150 -lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
   2.151 -proof(induction l x r rule: joinL.induct)
   2.152 -  case (1 l x r)
   2.153 -  thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
   2.154 -qed
   2.155 -
   2.156 -lemma inorder_joinR:
   2.157 -  "inorder(joinR l x r) = inorder l @ x # inorder r"
   2.158 -proof(induction l x r rule: joinR.induct)
   2.159 -  case (1 l x r)
   2.160 -  thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
   2.161 -qed
   2.162 -
   2.163 -lemma "inorder(join l x r) = inorder l @ x # inorder r"
   2.164 -by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
   2.165 -      dest!: arg_cong[where f = inorder])
   2.166 -
   2.167 -
   2.168 -subsubsection "Set and bst properties"
   2.169 -
   2.170 -lemma set_baliL:
   2.171 -  "set_tree(baliL l a r) = Set.insert a (set_tree l \<union> set_tree r)"
   2.172 -by(cases "(l,a,r)" rule: baliL.cases) (auto)
   2.173 -
   2.174 -lemma set_joinL:
   2.175 -  "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = Set.insert x (set_tree l \<union> set_tree r)"
   2.176 -proof(induction l x r rule: joinL.induct)
   2.177 -  case (1 l x r)
   2.178 -  thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
   2.179 -qed
   2.180 -
   2.181 -lemma set_baliR:
   2.182 -  "set_tree(baliR l a r) = Set.insert a (set_tree l \<union> set_tree r)"
   2.183 -by(cases "(l,a,r)" rule: baliR.cases) (auto)
   2.184 -
   2.185 -lemma set_joinR:
   2.186 -  "set_tree (joinR l x r) = Set.insert x (set_tree l \<union> set_tree r)"
   2.187 -proof(induction l x r rule: joinR.induct)
   2.188 -  case (1 l x r)
   2.189 -  thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
   2.190 -qed
   2.191 -
   2.192 -lemma set_paint: "set_tree (paint c t) = set_tree t"
   2.193 -by (cases t) auto
   2.194 -
   2.195 -lemma set_join: "set_tree (join l x r) = Set.insert x (set_tree l \<union> set_tree r)"
   2.196 -by(simp add: set_joinL set_joinR set_paint)
   2.197 -
   2.198 -lemma bst_baliL:
   2.199 -  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
   2.200 -   \<Longrightarrow> bst (baliL l k r)"
   2.201 -by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un)
   2.202 -
   2.203 -lemma bst_baliR:
   2.204 -  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
   2.205 -   \<Longrightarrow> bst (baliR l k r)"
   2.206 -by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un)
   2.207 -
   2.208 -lemma bst_joinL:
   2.209 -  "\<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>
   2.210 -  \<Longrightarrow> bst (joinL l k r)"
   2.211 -proof(induction l k r rule: joinL.induct)
   2.212 -  case (1 l x r)
   2.213 -  thus ?case
   2.214 -    by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL
   2.215 -        split!: tree.splits color.splits)
   2.216 -qed
   2.217 -
   2.218 -lemma bst_joinR:
   2.219 -  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
   2.220 -  \<Longrightarrow> bst (joinR l k r)"
   2.221 -proof(induction l k r rule: joinR.induct)
   2.222 -  case (1 l x r)
   2.223 -  thus ?case
   2.224 -    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
   2.225 -        split!: tree.splits color.splits)
   2.226 -qed
   2.227 -
   2.228 -lemma bst_paint: "bst (paint c t) = bst t"
   2.229 -by(cases t) auto
   2.230 -
   2.231 -lemma bst_join:
   2.232 -  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
   2.233 -  \<Longrightarrow> bst (join l k r)"
   2.234 -by(auto simp: bst_paint bst_joinL bst_joinR)
   2.235 -
   2.236 -
   2.237 -subsubsection "Interpretation of @{locale Set2_BST2_Join} with Red-Black Tree"
   2.238 -
   2.239 -global_interpretation RBT: Set2_BST2_Join
   2.240 -where join = join and inv = "\<lambda>t. invc t \<and> invh t"
   2.241 -defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
   2.242 -and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
   2.243 -proof (standard, goal_cases)
   2.244 -  case 1 show ?case by simp
   2.245 -next
   2.246 -  case 2 show ?case by (rule set_join)
   2.247 -next
   2.248 -  case 3 thus ?case by (rule bst_join)
   2.249 -next
   2.250 -  case 4 thus ?case
   2.251 -    by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
   2.252 -next
   2.253 -  case 5 thus ?case by simp
   2.254 -qed
   2.255 -
   2.256 -text \<open>The invariant does not guarantee that the root node is black. This is not required
   2.257 -to guarantee that the height is logarithmic in the size --- Exercise.\<close>
   2.258 -
   2.259 -end
   2.260 \ No newline at end of file
     3.1 --- a/src/HOL/Data_Structures/Set2_BST_Join.thy	Thu May 24 09:18:29 2018 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,364 +0,0 @@
     3.4 -(* Author: Tobias Nipkow *)
     3.5 -
     3.6 -section "Join-Based BST Implementation of Sets"
     3.7 -
     3.8 -theory Set2_BST_Join
     3.9 -imports
    3.10 -  "HOL-Library.Tree"
    3.11 -  Cmp
    3.12 -  Set_Specs
    3.13 -begin
    3.14 -
    3.15 -text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
    3.16 -\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
    3.17 -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>
    3.18 -and an element \<open>x\<close> such that \<open>l < x < r\<close>.
    3.19 -
    3.20 -This theory illustrates the idea but is not suitable for an efficient implementation where
    3.21 -\<open>join\<close> balances the tree in some manner because type @{typ "'a tree"} in theory @{theory Tree}
    3.22 -has no additional fields for recording balance information. See theory \<open>Set2_BST2_Join\<close> for that.\<close>
    3.23 -
    3.24 -text \<open>Function \<open>isin\<close> can also be expressed via \<open>join\<close> but this is more direct:\<close>
    3.25 -
    3.26 -fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
    3.27 -"isin Leaf x = False" |
    3.28 -"isin (Node l a r) x =
    3.29 -  (case cmp x a of
    3.30 -     LT \<Rightarrow> isin l x |
    3.31 -     EQ \<Rightarrow> True |
    3.32 -     GT \<Rightarrow> isin r x)"
    3.33 -
    3.34 -lemma isin_set: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
    3.35 -by (induction t) (auto)
    3.36 -
    3.37 -
    3.38 -locale Set2_BST_Join =
    3.39 -fixes join :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
    3.40 -assumes set_join: "set_tree (join t1 x t2) = Set.insert x (set_tree t1 \<union> set_tree t2)"
    3.41 -assumes bst_join:
    3.42 -  "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < k; \<forall>y \<in> set_tree r. k < y \<rbrakk>
    3.43 -  \<Longrightarrow> bst (join l k r)"
    3.44 -fixes inv :: "'a tree \<Rightarrow> bool"
    3.45 -assumes inv_Leaf: "inv \<langle>\<rangle>"
    3.46 -assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
    3.47 -assumes inv_Node: "\<lbrakk> inv (Node l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
    3.48 -begin
    3.49 -
    3.50 -declare set_join [simp]
    3.51 -
    3.52 -subsection "\<open>split_min\<close>"
    3.53 -
    3.54 -fun split_min :: "'a tree \<Rightarrow> 'a \<times> 'a tree" where
    3.55 -"split_min (Node l x r) =
    3.56 -  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
    3.57 -
    3.58 -lemma split_min_set:
    3.59 -  "\<lbrakk> split_min t = (x,t');  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
    3.60 -   x \<in> set_tree t \<and> set_tree t = Set.insert x (set_tree t')"
    3.61 -proof(induction t arbitrary: t')
    3.62 -  case Node thus ?case by(auto split: prod.splits if_splits)
    3.63 -next
    3.64 -  case Leaf thus ?case by simp
    3.65 -qed
    3.66 -
    3.67 -lemma split_min_bst:
    3.68 -  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
    3.69 -proof(induction t arbitrary: t')
    3.70 -  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
    3.71 -next
    3.72 -  case Leaf thus ?case by simp
    3.73 -qed
    3.74 -
    3.75 -lemma split_min_inv:
    3.76 -  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
    3.77 -proof(induction t arbitrary: t')
    3.78 -  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
    3.79 -next
    3.80 -  case Leaf thus ?case by simp
    3.81 -qed
    3.82 -
    3.83 -
    3.84 -subsection "\<open>join2\<close>"
    3.85 -
    3.86 -definition join2 :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
    3.87 -"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
    3.88 -
    3.89 -lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
    3.90 -by(simp add: join2_def split_min_set split: prod.split)
    3.91 -
    3.92 -lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
    3.93 -  \<Longrightarrow> bst (join2 l r)"
    3.94 -by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
    3.95 -
    3.96 -lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
    3.97 -by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
    3.98 -
    3.99 -
   3.100 -subsection "\<open>split\<close>"
   3.101 -
   3.102 -fun split :: "'a tree \<Rightarrow> 'a \<Rightarrow> 'a tree \<times> bool \<times> 'a tree" where
   3.103 -"split Leaf k = (Leaf, False, Leaf)" |
   3.104 -"split (Node l a r) k =
   3.105 -  (case cmp k a of
   3.106 -    LT \<Rightarrow> let (l1,b,l2) = split l k in (l1, b, join l2 a r) |
   3.107 -    GT \<Rightarrow> let (r1,b,r2) = split r k in (join l a r1, b, r2) |
   3.108 -    EQ \<Rightarrow> (l, True, r))"
   3.109 -
   3.110 -lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
   3.111 -  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
   3.112 -  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
   3.113 -proof(induction t arbitrary: l kin r)
   3.114 -  case Leaf thus ?case by simp
   3.115 -next
   3.116 -  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
   3.117 -qed
   3.118 -
   3.119 -lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
   3.120 -proof(induction t arbitrary: l kin r)
   3.121 -  case Leaf thus ?case by simp
   3.122 -next
   3.123 -  case Node
   3.124 -  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
   3.125 -qed
   3.126 -
   3.127 -declare split.simps[simp del]
   3.128 -
   3.129 -
   3.130 -subsection "\<open>insert\<close>"
   3.131 -
   3.132 -definition insert :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   3.133 -"insert k t = (let (l,_,r) = split t k in join l k r)"
   3.134 -
   3.135 -lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
   3.136 -by(auto simp add: insert_def split split: prod.split)
   3.137 -
   3.138 -lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
   3.139 -by(auto simp add: insert_def bst_join dest: split split: prod.split)
   3.140 -
   3.141 -lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
   3.142 -by(force simp: insert_def inv_join dest: split_inv split: prod.split)
   3.143 -
   3.144 -
   3.145 -subsection "\<open>delete\<close>"
   3.146 -
   3.147 -definition delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   3.148 -"delete k t = (let (l,_,r) = split t k in join2 l r)"
   3.149 -
   3.150 -lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
   3.151 -by(auto simp: delete_def split split: prod.split)
   3.152 -
   3.153 -lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
   3.154 -by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
   3.155 -
   3.156 -lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
   3.157 -by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
   3.158 -
   3.159 -
   3.160 -subsection "\<open>union\<close>"
   3.161 -
   3.162 -fun union :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   3.163 -"union t1 t2 =
   3.164 -  (if t1 = Leaf then t2 else
   3.165 -   if t2 = Leaf then t1 else
   3.166 -   case t1 of Node l1 k r1 \<Rightarrow>
   3.167 -   let (l2,_ ,r2) = split t2 k;
   3.168 -       l' = union l1 l2; r' = union r1 r2
   3.169 -   in join l' k r')"
   3.170 -
   3.171 -declare union.simps [simp del]
   3.172 -
   3.173 -lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
   3.174 -proof(induction t1 t2 rule: union.induct)
   3.175 -  case (1 t1 t2)
   3.176 -  then show ?case
   3.177 -    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
   3.178 -qed
   3.179 -
   3.180 -lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
   3.181 -proof(induction t1 t2 rule: union.induct)
   3.182 -  case (1 t1 t2)
   3.183 -  thus ?case
   3.184 -    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
   3.185 -        split: tree.split prod.split)
   3.186 -qed
   3.187 -
   3.188 -lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
   3.189 -proof(induction t1 t2 rule: union.induct)
   3.190 -  case (1 t1 t2)
   3.191 -  thus ?case
   3.192 -    by(auto simp:union.simps[of t1 t2] inv_join split_inv
   3.193 -        split!: tree.split prod.split dest: inv_Node)
   3.194 -qed
   3.195 -
   3.196 -subsection "\<open>inter\<close>"
   3.197 -
   3.198 -fun inter :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   3.199 -"inter t1 t2 =
   3.200 -  (if t1 = Leaf then Leaf else
   3.201 -   if t2 = Leaf then Leaf else
   3.202 -   case t1 of Node l1 k r1 \<Rightarrow>
   3.203 -   let (l2,kin,r2) = split t2 k;
   3.204 -       l' = inter l1 l2; r' = inter r1 r2
   3.205 -   in if kin then join l' k r' else join2 l' r')"
   3.206 -
   3.207 -declare inter.simps [simp del]
   3.208 -
   3.209 -lemma set_tree_inter:
   3.210 -  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
   3.211 -proof(induction t1 t2 rule: inter.induct)
   3.212 -  case (1 t1 t2)
   3.213 -  show ?case
   3.214 -  proof (cases t1)
   3.215 -    case Leaf thus ?thesis by (simp add: inter.simps)
   3.216 -  next
   3.217 -    case [simp]: (Node l1 k r1)
   3.218 -    show ?thesis
   3.219 -    proof (cases "t2 = Leaf")
   3.220 -      case True thus ?thesis by (simp add: inter.simps)
   3.221 -    next
   3.222 -      case False
   3.223 -      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
   3.224 -      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
   3.225 -      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
   3.226 -      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
   3.227 -      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
   3.228 -           **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   3.229 -        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
   3.230 -      have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
   3.231 -        using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   3.232 -      have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
   3.233 -        using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   3.234 -      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
   3.235 -        by(simp add: t2)
   3.236 -      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
   3.237 -        using * ** by auto
   3.238 -      also have "\<dots> = set_tree (inter t1 t2)"
   3.239 -      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
   3.240 -      finally show ?thesis by simp
   3.241 -    qed
   3.242 -  qed
   3.243 -qed
   3.244 -
   3.245 -lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
   3.246 -proof(induction t1 t2 rule: inter.induct)
   3.247 -  case (1 t1 t2)
   3.248 -  thus ?case
   3.249 -    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
   3.250 -        intro!: bst_join bst_join2 split: tree.split prod.split)
   3.251 -qed
   3.252 -
   3.253 -lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
   3.254 -proof(induction t1 t2 rule: inter.induct)
   3.255 -  case (1 t1 t2)
   3.256 -  thus ?case
   3.257 -    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   3.258 -        split!: tree.split prod.split dest: inv_Node)
   3.259 -qed
   3.260 -
   3.261 -subsection "\<open>diff\<close>"
   3.262 -
   3.263 -fun diff :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
   3.264 -"diff t1 t2 =
   3.265 -  (if t1 = Leaf then Leaf else
   3.266 -   if t2 = Leaf then t1 else
   3.267 -   case t2 of Node l2 k r2 \<Rightarrow>
   3.268 -   let (l1,_,r1) = split t1 k;
   3.269 -       l' = diff l1 l2; r' = diff r1 r2
   3.270 -   in join2 l' r')"
   3.271 -
   3.272 -declare diff.simps [simp del]
   3.273 -
   3.274 -lemma set_tree_diff:
   3.275 -  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
   3.276 -proof(induction t1 t2 rule: diff.induct)
   3.277 -  case (1 t1 t2)
   3.278 -  show ?case
   3.279 -  proof (cases t2)
   3.280 -    case Leaf thus ?thesis by (simp add: diff.simps)
   3.281 -  next
   3.282 -    case [simp]: (Node l2 k r2)
   3.283 -    show ?thesis
   3.284 -    proof (cases "t1 = Leaf")
   3.285 -      case True thus ?thesis by (simp add: diff.simps)
   3.286 -    next
   3.287 -      case False
   3.288 -      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
   3.289 -      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
   3.290 -      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
   3.291 -      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
   3.292 -           **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   3.293 -        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
   3.294 -      have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
   3.295 -        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   3.296 -      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
   3.297 -        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   3.298 -      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
   3.299 -        by(simp add: t1)
   3.300 -      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
   3.301 -        using ** by auto
   3.302 -      also have "\<dots> = set_tree (diff t1 t2)"
   3.303 -      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
   3.304 -      finally show ?thesis by simp
   3.305 -    qed
   3.306 -  qed
   3.307 -qed
   3.308 -
   3.309 -lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
   3.310 -proof(induction t1 t2 rule: diff.induct)
   3.311 -  case (1 t1 t2)
   3.312 -  thus ?case
   3.313 -    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
   3.314 -        intro!: bst_join bst_join2 split: tree.split prod.split)
   3.315 -qed
   3.316 -
   3.317 -lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
   3.318 -proof(induction t1 t2 rule: diff.induct)
   3.319 -  case (1 t1 t2)
   3.320 -  thus ?case
   3.321 -    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   3.322 -        split!: tree.split prod.split dest: inv_Node)
   3.323 -qed
   3.324 -
   3.325 -text \<open>Locale @{locale Set2_BST_Join} implements locale @{locale Set2}:\<close>
   3.326 -
   3.327 -sublocale Set2
   3.328 -where empty = Leaf and isin = isin and insert = insert and delete = delete
   3.329 -and  union = union and inter = inter and diff = diff
   3.330 -and set = set_tree and invar = "\<lambda>t. bst t \<and> inv t"
   3.331 -proof (standard, goal_cases)
   3.332 -  case 1 show ?case by simp
   3.333 -next
   3.334 -  case 2 thus ?case by (simp add: isin_set)
   3.335 -next
   3.336 -  case 3 thus ?case by (simp add: set_tree_insert)
   3.337 -next
   3.338 -  case 4 thus ?case by (simp add: set_tree_delete)
   3.339 -next
   3.340 -  case 5 thus ?case by (simp add: inv_Leaf)
   3.341 -next
   3.342 -  case 6 thus ?case by (simp add: inv_insert bst_insert)
   3.343 -next
   3.344 -  case 7 thus ?case by (simp add: inv_delete bst_delete)
   3.345 -next
   3.346 -  case 8 thus ?case by (simp add: set_tree_union)
   3.347 -next
   3.348 -  case 9 thus ?case by (simp add: set_tree_inter)
   3.349 -next
   3.350 -  case 10 thus ?case by (simp add: set_tree_diff)
   3.351 -next
   3.352 -  case 11 thus ?case by (simp add: bst_union inv_union)
   3.353 -next
   3.354 -  case 12 thus ?case by (simp add: bst_inter inv_inter)
   3.355 -next
   3.356 -  case 13 thus ?case by (simp add: bst_diff inv_diff)
   3.357 -qed
   3.358 -
   3.359 -end (* Set2_BST_Join *)
   3.360 -
   3.361 -text \<open>Interpretation of @{locale Set2_BST_Join} with unbalanced binary trees:\<close>
   3.362 -
   3.363 -interpretation Set2_BST_Join where join = Node and inv = "\<lambda>t. True"
   3.364 -proof (standard, goal_cases)
   3.365 -qed auto
   3.366 -
   3.367 -end
   3.368 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Data_Structures/Set2_Join.thy	Thu May 24 14:42:47 2018 +0200
     4.3 @@ -0,0 +1,357 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +section "Join-Based Implementation of Sets"
     4.7 +
     4.8 +theory Set2_Join
     4.9 +imports
    4.10 +  Isin2
    4.11 +begin
    4.12 +
    4.13 +text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>,
    4.14 +\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees.
    4.15 +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>
    4.16 +and an element \<open>x\<close> such that \<open>l < x < r\<close>.
    4.17 +
    4.18 +The theory is based on theory @{theory Tree2} where nodes have an additional field.
    4.19 +This field is ignored here but it means that this theory can be instantiated
    4.20 +with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees.
    4.21 +This approach is very concrete and fixes the type of trees.
    4.22 +Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition
    4.23 +and recursion operators on it.\<close>
    4.24 +
    4.25 +locale Set2_Join =
    4.26 +fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree"
    4.27 +fixes inv :: "('a,'b) tree \<Rightarrow> bool"
    4.28 +assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r"
    4.29 +assumes bst_join:
    4.30 +  "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < a; \<forall>y \<in> set_tree r. a < y \<rbrakk>
    4.31 +  \<Longrightarrow> bst (join l a r)"
    4.32 +assumes inv_Leaf: "inv \<langle>\<rangle>"
    4.33 +assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
    4.34 +assumes inv_Node: "\<lbrakk> inv (Node h l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
    4.35 +begin
    4.36 +
    4.37 +declare set_join [simp]
    4.38 +
    4.39 +subsection "\<open>split_min\<close>"
    4.40 +
    4.41 +fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
    4.42 +"split_min (Node _ l x r) =
    4.43 +  (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
    4.44 +
    4.45 +lemma split_min_set:
    4.46 +  "\<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')"
    4.47 +proof(induction t arbitrary: t')
    4.48 +  case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node)
    4.49 +next
    4.50 +  case Leaf thus ?case by simp
    4.51 +qed
    4.52 +
    4.53 +lemma split_min_bst:
    4.54 +  "\<lbrakk> split_min t = (x,t');  bst t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')"
    4.55 +proof(induction t arbitrary: t')
    4.56 +  case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits)
    4.57 +next
    4.58 +  case Leaf thus ?case by simp
    4.59 +qed
    4.60 +
    4.61 +lemma split_min_inv:
    4.62 +  "\<lbrakk> split_min t = (x,t');  inv t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow>  inv t'"
    4.63 +proof(induction t arbitrary: t')
    4.64 +  case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node)
    4.65 +next
    4.66 +  case Leaf thus ?case by simp
    4.67 +qed
    4.68 +
    4.69 +
    4.70 +subsection "\<open>join2\<close>"
    4.71 +
    4.72 +definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
    4.73 +"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')"
    4.74 +
    4.75 +lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
    4.76 +by(simp add: join2_def split_min_set split: prod.split)
    4.77 +
    4.78 +lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
    4.79 +  \<Longrightarrow> bst (join2 l r)"
    4.80 +by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
    4.81 +
    4.82 +lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
    4.83 +by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
    4.84 +
    4.85 +
    4.86 +subsection "\<open>split\<close>"
    4.87 +
    4.88 +fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
    4.89 +"split Leaf k = (Leaf, False, Leaf)" |
    4.90 +"split (Node _ l a r) k =
    4.91 +  (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
    4.92 +   if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
    4.93 +   else (l, True, r))"
    4.94 +
    4.95 +lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow>
    4.96 +  set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x}
    4.97 +  \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r"
    4.98 +proof(induction t arbitrary: l kin r)
    4.99 +  case Leaf thus ?case by simp
   4.100 +next
   4.101 +  case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join)
   4.102 +qed
   4.103 +
   4.104 +lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r"
   4.105 +proof(induction t arbitrary: l kin r)
   4.106 +  case Leaf thus ?case by simp
   4.107 +next
   4.108 +  case Node
   4.109 +  thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node)
   4.110 +qed
   4.111 +
   4.112 +declare split.simps[simp del]
   4.113 +
   4.114 +
   4.115 +subsection "\<open>insert\<close>"
   4.116 +
   4.117 +definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
   4.118 +"insert k t = (let (l,_,r) = split t k in join l k r)"
   4.119 +
   4.120 +lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)"
   4.121 +by(auto simp add: insert_def split split: prod.split)
   4.122 +
   4.123 +lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)"
   4.124 +by(auto simp add: insert_def bst_join dest: split split: prod.split)
   4.125 +
   4.126 +lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)"
   4.127 +by(force simp: insert_def inv_join dest: split_inv split: prod.split)
   4.128 +
   4.129 +
   4.130 +subsection "\<open>delete\<close>"
   4.131 +
   4.132 +definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where
   4.133 +"delete k t = (let (l,_,r) = split t k in join2 l r)"
   4.134 +
   4.135 +lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}"
   4.136 +by(auto simp: delete_def split split: prod.split)
   4.137 +
   4.138 +lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)"
   4.139 +by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split)
   4.140 +
   4.141 +lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)"
   4.142 +by(force simp: delete_def inv_join2 dest: split_inv split: prod.split)
   4.143 +
   4.144 +
   4.145 +subsection "\<open>union\<close>"
   4.146 +
   4.147 +fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   4.148 +"union t1 t2 =
   4.149 +  (if t1 = Leaf then t2 else
   4.150 +   if t2 = Leaf then t1 else
   4.151 +   case t1 of Node _ l1 k r1 \<Rightarrow>
   4.152 +   let (l2,_ ,r2) = split t2 k;
   4.153 +       l' = union l1 l2; r' = union r1 r2
   4.154 +   in join l' k r')"
   4.155 +
   4.156 +declare union.simps [simp del]
   4.157 +
   4.158 +lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2"
   4.159 +proof(induction t1 t2 rule: union.induct)
   4.160 +  case (1 t1 t2)
   4.161 +  then show ?case
   4.162 +    by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split)
   4.163 +qed
   4.164 +
   4.165 +lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)"
   4.166 +proof(induction t1 t2 rule: union.induct)
   4.167 +  case (1 t1 t2)
   4.168 +  thus ?case
   4.169 +    by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 
   4.170 +        split: tree.split prod.split)
   4.171 +qed
   4.172 +
   4.173 +lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)"
   4.174 +proof(induction t1 t2 rule: union.induct)
   4.175 +  case (1 t1 t2)
   4.176 +  thus ?case
   4.177 +    by(auto simp:union.simps[of t1 t2] inv_join split_inv
   4.178 +        split!: tree.split prod.split dest: inv_Node)
   4.179 +qed
   4.180 +
   4.181 +subsection "\<open>inter\<close>"
   4.182 +
   4.183 +fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   4.184 +"inter t1 t2 =
   4.185 +  (if t1 = Leaf then Leaf else
   4.186 +   if t2 = Leaf then Leaf else
   4.187 +   case t1 of Node _ l1 k r1 \<Rightarrow>
   4.188 +   let (l2,kin,r2) = split t2 k;
   4.189 +       l' = inter l1 l2; r' = inter r1 r2
   4.190 +   in if kin then join l' k r' else join2 l' r')"
   4.191 +
   4.192 +declare inter.simps [simp del]
   4.193 +
   4.194 +lemma set_tree_inter:
   4.195 +  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2"
   4.196 +proof(induction t1 t2 rule: inter.induct)
   4.197 +  case (1 t1 t2)
   4.198 +  show ?case
   4.199 +  proof (cases t1)
   4.200 +    case Leaf thus ?thesis by (simp add: inter.simps)
   4.201 +  next
   4.202 +    case [simp]: (Node _ l1 k r1)
   4.203 +    show ?thesis
   4.204 +    proof (cases "t2 = Leaf")
   4.205 +      case True thus ?thesis by (simp add: inter.simps)
   4.206 +    next
   4.207 +      case False
   4.208 +      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1"
   4.209 +      have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce)
   4.210 +      obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast
   4.211 +      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}"
   4.212 +      have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and
   4.213 +           **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   4.214 +        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force)
   4.215 +      have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2"
   4.216 +        using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   4.217 +      have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2"
   4.218 +        using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   4.219 +      have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)"
   4.220 +        by(simp add: t2)
   4.221 +      also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
   4.222 +        using * ** by auto
   4.223 +      also have "\<dots> = set_tree (inter t1 t2)"
   4.224 +      using IHl IHr sp inter.simps[of t1 t2] False by(simp)
   4.225 +      finally show ?thesis by simp
   4.226 +    qed
   4.227 +  qed
   4.228 +qed
   4.229 +
   4.230 +lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)"
   4.231 +proof(induction t1 t2 rule: inter.induct)
   4.232 +  case (1 t1 t2)
   4.233 +  thus ?case
   4.234 +    by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def
   4.235 +        intro!: bst_join bst_join2 split: tree.split prod.split)
   4.236 +qed
   4.237 +
   4.238 +lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)"
   4.239 +proof(induction t1 t2 rule: inter.induct)
   4.240 +  case (1 t1 t2)
   4.241 +  thus ?case
   4.242 +    by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   4.243 +        split!: tree.split prod.split dest: inv_Node)
   4.244 +qed
   4.245 +
   4.246 +subsection "\<open>diff\<close>"
   4.247 +
   4.248 +fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where
   4.249 +"diff t1 t2 =
   4.250 +  (if t1 = Leaf then Leaf else
   4.251 +   if t2 = Leaf then t1 else
   4.252 +   case t2 of Node _ l2 k r2 \<Rightarrow>
   4.253 +   let (l1,_,r1) = split t1 k;
   4.254 +       l' = diff l1 l2; r' = diff r1 r2
   4.255 +   in join2 l' r')"
   4.256 +
   4.257 +declare diff.simps [simp del]
   4.258 +
   4.259 +lemma set_tree_diff:
   4.260 +  "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2"
   4.261 +proof(induction t1 t2 rule: diff.induct)
   4.262 +  case (1 t1 t2)
   4.263 +  show ?case
   4.264 +  proof (cases t2)
   4.265 +    case Leaf thus ?thesis by (simp add: diff.simps)
   4.266 +  next
   4.267 +    case [simp]: (Node _ l2 k r2)
   4.268 +    show ?thesis
   4.269 +    proof (cases "t1 = Leaf")
   4.270 +      case True thus ?thesis by (simp add: diff.simps)
   4.271 +    next
   4.272 +      case False
   4.273 +      let ?L2 = "set_tree l2" let ?R2 = "set_tree r2"
   4.274 +      obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast
   4.275 +      let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}"
   4.276 +      have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and
   4.277 +           **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}"
   4.278 +        using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force)
   4.279 +      have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2"
   4.280 +        using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   4.281 +      have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2"
   4.282 +        using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp
   4.283 +      have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2  \<union> {k})"
   4.284 +        by(simp add: t1)
   4.285 +      also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)"
   4.286 +        using ** by auto
   4.287 +      also have "\<dots> = set_tree (diff t1 t2)"
   4.288 +      using IHl IHr sp diff.simps[of t1 t2] False by(simp)
   4.289 +      finally show ?thesis by simp
   4.290 +    qed
   4.291 +  qed
   4.292 +qed
   4.293 +
   4.294 +lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)"
   4.295 +proof(induction t1 t2 rule: diff.induct)
   4.296 +  case (1 t1 t2)
   4.297 +  thus ?case
   4.298 +    by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def
   4.299 +        intro!: bst_join bst_join2 split: tree.split prod.split)
   4.300 +qed
   4.301 +
   4.302 +lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)"
   4.303 +proof(induction t1 t2 rule: diff.induct)
   4.304 +  case (1 t1 t2)
   4.305 +  thus ?case
   4.306 +    by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def
   4.307 +        split!: tree.split prod.split dest: inv_Node)
   4.308 +qed
   4.309 +
   4.310 +text \<open>Locale @{locale Set2_Join} implements locale @{locale Set2}:\<close>
   4.311 +
   4.312 +sublocale Set2
   4.313 +where empty = Leaf and insert = insert and delete = delete and isin = isin
   4.314 +and union = union and inter = inter and diff = diff
   4.315 +and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t"
   4.316 +proof (standard, goal_cases)
   4.317 +  case 1 show ?case by (simp)
   4.318 +next
   4.319 +  case 2 thus ?case by(simp add: isin_set_tree)
   4.320 +next
   4.321 +  case 3 thus ?case by (simp add: set_tree_insert)
   4.322 +next
   4.323 +  case 4 thus ?case by (simp add: set_tree_delete)
   4.324 +next
   4.325 +  case 5 thus ?case by (simp add: inv_Leaf)
   4.326 +next
   4.327 +  case 6 thus ?case by (simp add: bst_insert inv_insert)
   4.328 +next
   4.329 +  case 7 thus ?case by (simp add: bst_delete inv_delete)
   4.330 +next
   4.331 +  case 8 thus ?case by(simp add: set_tree_union)
   4.332 +next
   4.333 +  case 9 thus ?case by(simp add: set_tree_inter)
   4.334 +next
   4.335 +  case 10 thus ?case by(simp add: set_tree_diff)
   4.336 +next
   4.337 +  case 11 thus ?case by (simp add: bst_union inv_union)
   4.338 +next
   4.339 +  case 12 thus ?case by (simp add: bst_inter inv_inter)
   4.340 +next
   4.341 +  case 13 thus ?case by (simp add: bst_diff inv_diff)
   4.342 +qed
   4.343 +
   4.344 +end
   4.345 +
   4.346 +interpretation unbal: Set2_Join
   4.347 +where join = "\<lambda>l x r. Node () l x r" and inv = "\<lambda>t. True"
   4.348 +proof (standard, goal_cases)
   4.349 +  case 1 show ?case by simp
   4.350 +next
   4.351 +  case 2 thus ?case by simp
   4.352 +next
   4.353 +  case 3 thus ?case by simp
   4.354 +next
   4.355 +  case 4 thus ?case by simp
   4.356 +next
   4.357 +  case 5 thus ?case by simp
   4.358 +qed
   4.359 +
   4.360 +end
   4.361 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Thu May 24 14:42:47 2018 +0200
     5.3 @@ -0,0 +1,256 @@
     5.4 +(* Author: Tobias Nipkow *)
     5.5 +
     5.6 +section "Join-Based Implementation of Sets via RBTs"
     5.7 +
     5.8 +theory Set2_Join_RBT
     5.9 +imports
    5.10 +  Set2_Join
    5.11 +  RBT_Set
    5.12 +begin
    5.13 +
    5.14 +subsection "Code"
    5.15 +
    5.16 +text \<open>
    5.17 +Function \<open>joinL\<close> joins two trees (and an element).
    5.18 +Precondition: @{prop "bheight l \<le> bheight r"}.
    5.19 +Method:
    5.20 +Descend along the left spine of \<open>r\<close>
    5.21 +until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
    5.22 +then combine them into a new red node.
    5.23 +\<close>
    5.24 +fun joinL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    5.25 +"joinL l x r =
    5.26 +  (if bheight l = bheight r then R l x r
    5.27 +   else case r of
    5.28 +     B l' x' r' \<Rightarrow> baliL (joinL l x l') x' r' |
    5.29 +     R l' x' r' \<Rightarrow> R (joinL l x l') x' r')"
    5.30 +
    5.31 +fun joinR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    5.32 +"joinR l x r =
    5.33 +  (if bheight l \<le> bheight r then R l x r
    5.34 +   else case l of
    5.35 +     B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
    5.36 +     R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
    5.37 +
    5.38 +fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    5.39 +"join l x r =
    5.40 +  (if bheight l > bheight r
    5.41 +   then paint Black (joinR l x r)
    5.42 +   else if bheight l < bheight r
    5.43 +   then paint Black (joinL l x r)
    5.44 +   else B l x r)"
    5.45 +
    5.46 +declare joinL.simps[simp del]
    5.47 +declare joinR.simps[simp del]
    5.48 +
    5.49 +text \<open>
    5.50 +One would expect @{const joinR} to be be completely dual to @{const joinL}.
    5.51 +Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
    5.52 +is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
    5.53 +the two versions behave exactly the same, including complexity. Thus from a programmer's
    5.54 +perspective they are equivalent. However, not from a verifier's perspective:
    5.55 +the total version of @{const joinR} is easier
    5.56 +to reason about because lemmas about it may not require preconditions. In particular
    5.57 +@{prop"set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"}
    5.58 +is provable outright and hence also
    5.59 +@{prop"set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"}.
    5.60 +This is necessary because locale @{locale Set2_Join} unconditionally assumes
    5.61 +exactly that. Adding preconditions to this assumptions significantly complicates
    5.62 +the proofs within @{locale Set2_Join}, which we want to avoid.
    5.63 +
    5.64 +Why not work with the partial version of @{const joinR} and add the precondition
    5.65 +@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
    5.66 +we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
    5.67 +are only called under the respective precondition. But function @{const bheight}
    5.68 +makes the difference: it descends along the left spine, just like @{const joinL}.
    5.69 +Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
    5.70 +may change all the time. Thus we would need the further precondition @{prop "invh l"}.
    5.71 +This is what we really wanted to avoid in order to satisfy the unconditional assumption
    5.72 +in @{locale Set2_Join}.
    5.73 +\<close>
    5.74 +
    5.75 +subsection "Properties"
    5.76 +
    5.77 +subsubsection "Color and height invariants"
    5.78 +
    5.79 +lemma invc2_joinL:
    5.80 + "\<lbrakk> invc l; invc r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
    5.81 +  invc2 (joinL l x r)
    5.82 +  \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow> invc(joinL l x r))"
    5.83 +proof (induct l x r rule: joinL.induct)
    5.84 +  case (1 l x r) thus ?case
    5.85 +    by(auto simp: invc_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
    5.86 +qed
    5.87 +
    5.88 +lemma invc2_joinR:
    5.89 +  "\<lbrakk> invc l; invh l; invc r; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
    5.90 +  invc2 (joinR l x r)
    5.91 +  \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow> invc(joinR l x r))"
    5.92 +proof (induct l x r rule: joinR.induct)
    5.93 +  case (1 l x r) thus ?case
    5.94 +    by(fastforce simp: invc_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
    5.95 +qed
    5.96 +
    5.97 +lemma bheight_joinL:
    5.98 +  "\<lbrakk> invh l; invh r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (joinL l x r) = bheight r"
    5.99 +proof (induct l x r rule: joinL.induct)
   5.100 +  case (1 l x r) thus ?case
   5.101 +    by(auto simp: bheight_baliL joinL.simps[of l x r] split!: tree.split)
   5.102 +qed
   5.103 +
   5.104 +lemma invh_joinL:
   5.105 +  "\<lbrakk> invh l;  invh r;  bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> invh (joinL l x r)"
   5.106 +proof (induct l x r rule: joinL.induct)
   5.107 +  case (1 l x r) thus ?case
   5.108 +    by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
   5.109 +qed
   5.110 +
   5.111 +lemma bheight_baliR:
   5.112 +  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
   5.113 +by (cases "(l,a,r)" rule: baliR.cases) auto
   5.114 +
   5.115 +lemma bheight_joinR:
   5.116 +  "\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
   5.117 +proof (induct l x r rule: joinR.induct)
   5.118 +  case (1 l x r) thus ?case
   5.119 +    by(fastforce simp: bheight_baliR joinR.simps[of l x r] split!: tree.split)
   5.120 +qed
   5.121 +
   5.122 +lemma invh_joinR:
   5.123 +  "\<lbrakk> invh l; invh r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> invh (joinR l x r)"
   5.124 +proof (induct l x r rule: joinR.induct)
   5.125 +  case (1 l x r) thus ?case
   5.126 +    by(fastforce simp: invh_baliR bheight_joinR joinR.simps[of l x r]
   5.127 +        split!: tree.split color.split)
   5.128 +qed
   5.129 +
   5.130 +(* unused *)
   5.131 +lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
   5.132 +by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
   5.133 +    color_paint_Black)
   5.134 +
   5.135 +text \<open>To make sure the the black height is not increased unnecessarily:\<close>
   5.136 +
   5.137 +lemma bheight_paint_Black: "bheight(paint Black t) \<le> bheight t + 1"
   5.138 +by(cases t) auto
   5.139 +
   5.140 +lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
   5.141 +using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
   5.142 +  bheight_joinL[of l r x] bheight_joinR[of l r x]
   5.143 +by(auto simp: max_def rbt_def)
   5.144 +
   5.145 +
   5.146 +subsubsection "Inorder properties"
   5.147 +
   5.148 +text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
   5.149 +
   5.150 +lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
   5.151 +proof(induction l x r rule: joinL.induct)
   5.152 +  case (1 l x r)
   5.153 +  thus ?case by(auto simp: inorder_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
   5.154 +qed
   5.155 +
   5.156 +lemma inorder_joinR:
   5.157 +  "inorder(joinR l x r) = inorder l @ x # inorder r"
   5.158 +proof(induction l x r rule: joinR.induct)
   5.159 +  case (1 l x r)
   5.160 +  thus ?case by (force simp: inorder_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
   5.161 +qed
   5.162 +
   5.163 +lemma "inorder(join l x r) = inorder l @ x # inorder r"
   5.164 +by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
   5.165 +      dest!: arg_cong[where f = inorder])
   5.166 +
   5.167 +
   5.168 +subsubsection "Set and bst properties"
   5.169 +
   5.170 +lemma set_baliL:
   5.171 +  "set_tree(baliL l a r) = set_tree l \<union> {a} \<union> set_tree r"
   5.172 +by(cases "(l,a,r)" rule: baliL.cases) (auto)
   5.173 +
   5.174 +lemma set_joinL:
   5.175 +  "bheight l \<le> bheight r \<Longrightarrow> set_tree (joinL l x r) = set_tree l \<union> {x} \<union> set_tree r"
   5.176 +proof(induction l x r rule: joinL.induct)
   5.177 +  case (1 l x r)
   5.178 +  thus ?case by(auto simp: set_baliL joinL.simps[of l x r] split!: tree.splits color.splits)
   5.179 +qed
   5.180 +
   5.181 +lemma set_baliR:
   5.182 +  "set_tree(baliR l a r) = set_tree l \<union> {a} \<union> set_tree r"
   5.183 +by(cases "(l,a,r)" rule: baliR.cases) (auto)
   5.184 +
   5.185 +lemma set_joinR:
   5.186 +  "set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"
   5.187 +proof(induction l x r rule: joinR.induct)
   5.188 +  case (1 l x r)
   5.189 +  thus ?case by(force simp: set_baliR joinR.simps[of l x r] split!: tree.splits color.splits)
   5.190 +qed
   5.191 +
   5.192 +lemma set_paint: "set_tree (paint c t) = set_tree t"
   5.193 +by (cases t) auto
   5.194 +
   5.195 +lemma set_join: "set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"
   5.196 +by(simp add: set_joinL set_joinR set_paint)
   5.197 +
   5.198 +lemma bst_baliL:
   5.199 +  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
   5.200 +   \<Longrightarrow> bst (baliL l k r)"
   5.201 +by(cases "(l,k,r)" rule: baliL.cases) (auto simp: ball_Un)
   5.202 +
   5.203 +lemma bst_baliR:
   5.204 +  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>x\<in>set_tree r. k < x\<rbrakk>
   5.205 +   \<Longrightarrow> bst (baliR l k r)"
   5.206 +by(cases "(l,k,r)" rule: baliR.cases) (auto simp: ball_Un)
   5.207 +
   5.208 +lemma bst_joinL:
   5.209 +  "\<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>
   5.210 +  \<Longrightarrow> bst (joinL l k r)"
   5.211 +proof(induction l k r rule: joinL.induct)
   5.212 +  case (1 l x r)
   5.213 +  thus ?case
   5.214 +    by(auto simp: set_baliL joinL.simps[of l x r] set_joinL ball_Un intro!: bst_baliL
   5.215 +        split!: tree.splits color.splits)
   5.216 +qed
   5.217 +
   5.218 +lemma bst_joinR:
   5.219 +  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
   5.220 +  \<Longrightarrow> bst (joinR l k r)"
   5.221 +proof(induction l k r rule: joinR.induct)
   5.222 +  case (1 l x r)
   5.223 +  thus ?case
   5.224 +    by(auto simp: set_baliR joinR.simps[of l x r] set_joinR ball_Un intro!: bst_baliR
   5.225 +        split!: tree.splits color.splits)
   5.226 +qed
   5.227 +
   5.228 +lemma bst_paint: "bst (paint c t) = bst t"
   5.229 +by(cases t) auto
   5.230 +
   5.231 +lemma bst_join:
   5.232 +  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < k; \<forall>y\<in>set_tree r. k < y \<rbrakk>
   5.233 +  \<Longrightarrow> bst (join l k r)"
   5.234 +by(auto simp: bst_paint bst_joinL bst_joinR)
   5.235 +
   5.236 +
   5.237 +subsubsection "Interpretation of @{locale Set2_Join} with Red-Black Tree"
   5.238 +
   5.239 +global_interpretation RBT: Set2_Join
   5.240 +where join = join and inv = "\<lambda>t. invc t \<and> invh t"
   5.241 +defines insert_rbt = RBT.insert and delete_rbt = RBT.delete and split_rbt = RBT.split
   5.242 +and join2_rbt = RBT.join2 and split_min_rbt = RBT.split_min
   5.243 +proof (standard, goal_cases)
   5.244 +  case 1 show ?case by (rule set_join)
   5.245 +next
   5.246 +  case 2 thus ?case by (rule bst_join)
   5.247 +next
   5.248 +  case 3 show ?case by simp
   5.249 +next
   5.250 +  case 4 thus ?case
   5.251 +    by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
   5.252 +next
   5.253 +  case 5 thus ?case by simp
   5.254 +qed
   5.255 +
   5.256 +text \<open>The invariant does not guarantee that the root node is black. This is not required
   5.257 +to guarantee that the height is logarithmic in the size --- Exercise.\<close>
   5.258 +
   5.259 +end
   5.260 \ No newline at end of file
     6.1 --- a/src/HOL/ROOT	Thu May 24 09:18:29 2018 +0200
     6.2 +++ b/src/HOL/ROOT	Thu May 24 14:42:47 2018 +0200
     6.3 @@ -200,8 +200,7 @@
     6.4      Tree234_Map
     6.5      Brother12_Map
     6.6      AA_Map
     6.7 -    Set2_BST_Join
     6.8 -    Set2_BST2_Join_RBT
     6.9 +    Set2_Join_RBT
    6.10      Leftist_Heap
    6.11      Binomial_Heap
    6.12    document_files "root.tex" "root.bib"