1(* Author: Tobias Nipkow *) 2 3section "Join-Based Implementation of Sets" 4 5theory Set2_Join 6imports 7 Isin2 8begin 9 10text \<open>This theory implements the set operations \<open>insert\<close>, \<open>delete\<close>, 11\<open>union\<close>, \<open>inter\<close>section and \<open>diff\<close>erence. The implementation is based on binary search trees. 12All operations are reduced to a single operation \<open>join l x r\<close> that joins two BSTs \<open>l\<close> and \<open>r\<close> 13and an element \<open>x\<close> such that \<open>l < x < r\<close>. 14 15The theory is based on theory @{theory "HOL-Data_Structures.Tree2"} where nodes have an additional field. 16This field is ignored here but it means that this theory can be instantiated 17with red-black trees (see theory @{file "Set2_Join_RBT.thy"}) and other balanced trees. 18This approach is very concrete and fixes the type of trees. 19Alternatively, one could assume some abstract type @{typ 't} of trees with suitable decomposition 20and recursion operators on it.\<close> 21 22locale Set2_Join = 23fixes join :: "('a::linorder,'b) tree \<Rightarrow> 'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" 24fixes inv :: "('a,'b) tree \<Rightarrow> bool" 25assumes set_join: "set_tree (join l a r) = set_tree l \<union> {a} \<union> set_tree r" 26assumes bst_join: 27 "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. x < a; \<forall>y \<in> set_tree r. a < y \<rbrakk> 28 \<Longrightarrow> bst (join l a r)" 29assumes inv_Leaf: "inv \<langle>\<rangle>" 30assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)" 31assumes inv_Node: "\<lbrakk> inv (Node l x h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r" 32begin 33 34declare set_join [simp] 35 36subsection "\<open>split_min\<close>" 37 38fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where 39"split_min (Node l x _ r) = 40 (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))" 41 42lemma split_min_set: 43 "\<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')" 44proof(induction t arbitrary: t') 45 case Node thus ?case by(auto split: prod.splits if_splits dest: inv_Node) 46next 47 case Leaf thus ?case by simp 48qed 49 50lemma split_min_bst: 51 "\<lbrakk> split_min t = (x,t'); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> bst t' \<and> (\<forall>x' \<in> set_tree t'. x < x')" 52proof(induction t arbitrary: t') 53 case Node thus ?case by(fastforce simp: split_min_set bst_join split: prod.splits if_splits) 54next 55 case Leaf thus ?case by simp 56qed 57 58lemma split_min_inv: 59 "\<lbrakk> split_min t = (x,t'); inv t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inv t'" 60proof(induction t arbitrary: t') 61 case Node thus ?case by(auto simp: inv_join split: prod.splits if_splits dest: inv_Node) 62next 63 case Leaf thus ?case by simp 64qed 65 66 67subsection "\<open>join2\<close>" 68 69definition join2 :: "('a,'b) tree \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where 70"join2 l r = (if r = Leaf then l else let (x,r') = split_min r in join l x r')" 71 72lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r" 73by(simp add: join2_def split_min_set split: prod.split) 74 75lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk> 76 \<Longrightarrow> bst (join2 l r)" 77by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split) 78 79lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)" 80by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split) 81 82 83subsection "\<open>split\<close>" 84 85fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where 86"split Leaf k = (Leaf, False, Leaf)" | 87"split (Node l a _ r) k = 88 (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else 89 if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2) 90 else (l, True, r))" 91 92lemma split: "split t k = (l,kin,r) \<Longrightarrow> bst t \<Longrightarrow> 93 set_tree l = {x \<in> set_tree t. x < k} \<and> set_tree r = {x \<in> set_tree t. k < x} 94 \<and> (kin = (k \<in> set_tree t)) \<and> bst l \<and> bst r" 95proof(induction t arbitrary: l kin r) 96 case Leaf thus ?case by simp 97next 98 case Node thus ?case by(force split!: prod.splits if_splits intro!: bst_join) 99qed 100 101lemma split_inv: "split t k = (l,kin,r) \<Longrightarrow> inv t \<Longrightarrow> inv l \<and> inv r" 102proof(induction t arbitrary: l kin r) 103 case Leaf thus ?case by simp 104next 105 case Node 106 thus ?case by(force simp: inv_join split!: prod.splits if_splits dest!: inv_Node) 107qed 108 109declare split.simps[simp del] 110 111 112subsection "\<open>insert\<close>" 113 114definition insert :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where 115"insert k t = (let (l,_,r) = split t k in join l k r)" 116 117lemma set_tree_insert: "bst t \<Longrightarrow> set_tree (insert x t) = Set.insert x (set_tree t)" 118by(auto simp add: insert_def split split: prod.split) 119 120lemma bst_insert: "bst t \<Longrightarrow> bst (insert x t)" 121by(auto simp add: insert_def bst_join dest: split split: prod.split) 122 123lemma inv_insert: "inv t \<Longrightarrow> inv (insert x t)" 124by(force simp: insert_def inv_join dest: split_inv split: prod.split) 125 126 127subsection "\<open>delete\<close>" 128 129definition delete :: "'a \<Rightarrow> ('a,'b) tree \<Rightarrow> ('a,'b) tree" where 130"delete k t = (let (l,_,r) = split t k in join2 l r)" 131 132lemma set_tree_delete: "bst t \<Longrightarrow> set_tree (delete k t) = set_tree t - {k}" 133by(auto simp: delete_def split split: prod.split) 134 135lemma bst_delete: "bst t \<Longrightarrow> bst (delete x t)" 136by(force simp add: delete_def intro: bst_join2 dest: split split: prod.split) 137 138lemma inv_delete: "inv t \<Longrightarrow> inv (delete x t)" 139by(force simp: delete_def inv_join2 dest: split_inv split: prod.split) 140 141 142subsection "\<open>union\<close>" 143 144fun union :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where 145"union t1 t2 = 146 (if t1 = Leaf then t2 else 147 if t2 = Leaf then t1 else 148 case t1 of Node l1 k _ r1 \<Rightarrow> 149 let (l2,_ ,r2) = split t2 k; 150 l' = union l1 l2; r' = union r1 r2 151 in join l' k r')" 152 153declare union.simps [simp del] 154 155lemma set_tree_union: "bst t2 \<Longrightarrow> set_tree (union t1 t2) = set_tree t1 \<union> set_tree t2" 156proof(induction t1 t2 rule: union.induct) 157 case (1 t1 t2) 158 then show ?case 159 by (auto simp: union.simps[of t1 t2] split split: tree.split prod.split) 160qed 161 162lemma bst_union: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (union t1 t2)" 163proof(induction t1 t2 rule: union.induct) 164 case (1 t1 t2) 165 thus ?case 166 by(fastforce simp: union.simps[of t1 t2] set_tree_union split intro!: bst_join 167 split: tree.split prod.split) 168qed 169 170lemma inv_union: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (union t1 t2)" 171proof(induction t1 t2 rule: union.induct) 172 case (1 t1 t2) 173 thus ?case 174 by(auto simp:union.simps[of t1 t2] inv_join split_inv 175 split!: tree.split prod.split dest: inv_Node) 176qed 177 178subsection "\<open>inter\<close>" 179 180fun inter :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where 181"inter t1 t2 = 182 (if t1 = Leaf then Leaf else 183 if t2 = Leaf then Leaf else 184 case t1 of Node l1 k _ r1 \<Rightarrow> 185 let (l2,kin,r2) = split t2 k; 186 l' = inter l1 l2; r' = inter r1 r2 187 in if kin then join l' k r' else join2 l' r')" 188 189declare inter.simps [simp del] 190 191lemma set_tree_inter: 192 "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (inter t1 t2) = set_tree t1 \<inter> set_tree t2" 193proof(induction t1 t2 rule: inter.induct) 194 case (1 t1 t2) 195 show ?case 196 proof (cases t1) 197 case Leaf thus ?thesis by (simp add: inter.simps) 198 next 199 case [simp]: (Node l1 k _ r1) 200 show ?thesis 201 proof (cases "t2 = Leaf") 202 case True thus ?thesis by (simp add: inter.simps) 203 next 204 case False 205 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" 206 have *: "k \<notin> ?L1 \<union> ?R1" using \<open>bst t1\<close> by (fastforce) 207 obtain l2 kin r2 where sp: "split t2 k = (l2,kin,r2)" using prod_cases3 by blast 208 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" let ?K = "if kin then {k} else {}" 209 have t2: "set_tree t2 = ?L2 \<union> ?R2 \<union> ?K" and 210 **: "?L2 \<inter> ?R2 = {}" "k \<notin> ?L2 \<union> ?R2" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" 211 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force, force) 212 have IHl: "set_tree (inter l1 l2) = set_tree l1 \<inter> set_tree l2" 213 using "1.IH"(1)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp 214 have IHr: "set_tree (inter r1 r2) = set_tree r1 \<inter> set_tree r2" 215 using "1.IH"(2)[OF _ False _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp 216 have "set_tree t1 \<inter> set_tree t2 = (?L1 \<union> ?R1 \<union> {k}) \<inter> (?L2 \<union> ?R2 \<union> ?K)" 217 by(simp add: t2) 218 also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K" 219 using * ** by auto 220 also have "\<dots> = set_tree (inter t1 t2)" 221 using IHl IHr sp inter.simps[of t1 t2] False by(simp) 222 finally show ?thesis by simp 223 qed 224 qed 225qed 226 227lemma bst_inter: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (inter t1 t2)" 228proof(induction t1 t2 rule: inter.induct) 229 case (1 t1 t2) 230 thus ?case 231 by(fastforce simp: inter.simps[of t1 t2] set_tree_inter split Let_def 232 intro!: bst_join bst_join2 split: tree.split prod.split) 233qed 234 235lemma inv_inter: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (inter t1 t2)" 236proof(induction t1 t2 rule: inter.induct) 237 case (1 t1 t2) 238 thus ?case 239 by(auto simp: inter.simps[of t1 t2] inv_join inv_join2 split_inv Let_def 240 split!: tree.split prod.split dest: inv_Node) 241qed 242 243subsection "\<open>diff\<close>" 244 245fun diff :: "('a,'b)tree \<Rightarrow> ('a,'b)tree \<Rightarrow> ('a,'b)tree" where 246"diff t1 t2 = 247 (if t1 = Leaf then Leaf else 248 if t2 = Leaf then t1 else 249 case t2 of Node l2 k _ r2 \<Rightarrow> 250 let (l1,_,r1) = split t1 k; 251 l' = diff l1 l2; r' = diff r1 r2 252 in join2 l' r')" 253 254declare diff.simps [simp del] 255 256lemma set_tree_diff: 257 "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> set_tree (diff t1 t2) = set_tree t1 - set_tree t2" 258proof(induction t1 t2 rule: diff.induct) 259 case (1 t1 t2) 260 show ?case 261 proof (cases t2) 262 case Leaf thus ?thesis by (simp add: diff.simps) 263 next 264 case [simp]: (Node l2 k _ r2) 265 show ?thesis 266 proof (cases "t1 = Leaf") 267 case True thus ?thesis by (simp add: diff.simps) 268 next 269 case False 270 let ?L2 = "set_tree l2" let ?R2 = "set_tree r2" 271 obtain l1 kin r1 where sp: "split t1 k = (l1,kin,r1)" using prod_cases3 by blast 272 let ?L1 = "set_tree l1" let ?R1 = "set_tree r1" let ?K = "if kin then {k} else {}" 273 have t1: "set_tree t1 = ?L1 \<union> ?R1 \<union> ?K" and 274 **: "k \<notin> ?L1 \<union> ?R1" "?L1 \<inter> ?R2 = {}" "?L2 \<inter> ?R1 = {}" 275 using split[OF sp] \<open>bst t1\<close> \<open>bst t2\<close> by (force, force, force, force) 276 have IHl: "set_tree (diff l1 l2) = set_tree l1 - set_tree l2" 277 using "1.IH"(1)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp 278 have IHr: "set_tree (diff r1 r2) = set_tree r1 - set_tree r2" 279 using "1.IH"(2)[OF False _ _ sp[symmetric]] "1.prems"(1,2) split[OF sp] by simp 280 have "set_tree t1 - set_tree t2 = (?L1 \<union> ?R1) - (?L2 \<union> ?R2 \<union> {k})" 281 by(simp add: t1) 282 also have "\<dots> = (?L1 - ?L2) \<union> (?R1 - ?R2)" 283 using ** by auto 284 also have "\<dots> = set_tree (diff t1 t2)" 285 using IHl IHr sp diff.simps[of t1 t2] False by(simp) 286 finally show ?thesis by simp 287 qed 288 qed 289qed 290 291lemma bst_diff: "\<lbrakk> bst t1; bst t2 \<rbrakk> \<Longrightarrow> bst (diff t1 t2)" 292proof(induction t1 t2 rule: diff.induct) 293 case (1 t1 t2) 294 thus ?case 295 by(fastforce simp: diff.simps[of t1 t2] set_tree_diff split Let_def 296 intro!: bst_join bst_join2 split: tree.split prod.split) 297qed 298 299lemma inv_diff: "\<lbrakk> inv t1; inv t2 \<rbrakk> \<Longrightarrow> inv (diff t1 t2)" 300proof(induction t1 t2 rule: diff.induct) 301 case (1 t1 t2) 302 thus ?case 303 by(auto simp: diff.simps[of t1 t2] inv_join inv_join2 split_inv Let_def 304 split!: tree.split prod.split dest: inv_Node) 305qed 306 307text \<open>Locale @{locale Set2_Join} implements locale @{locale Set2}:\<close> 308 309sublocale Set2 310where empty = Leaf and insert = insert and delete = delete and isin = isin 311and union = union and inter = inter and diff = diff 312and set = set_tree and invar = "\<lambda>t. inv t \<and> bst t" 313proof (standard, goal_cases) 314 case 1 show ?case by (simp) 315next 316 case 2 thus ?case by(simp add: isin_set_tree) 317next 318 case 3 thus ?case by (simp add: set_tree_insert) 319next 320 case 4 thus ?case by (simp add: set_tree_delete) 321next 322 case 5 thus ?case by (simp add: inv_Leaf) 323next 324 case 6 thus ?case by (simp add: bst_insert inv_insert) 325next 326 case 7 thus ?case by (simp add: bst_delete inv_delete) 327next 328 case 8 thus ?case by(simp add: set_tree_union) 329next 330 case 9 thus ?case by(simp add: set_tree_inter) 331next 332 case 10 thus ?case by(simp add: set_tree_diff) 333next 334 case 11 thus ?case by (simp add: bst_union inv_union) 335next 336 case 12 thus ?case by (simp add: bst_inter inv_inter) 337next 338 case 13 thus ?case by (simp add: bst_diff inv_diff) 339qed 340 341end 342 343interpretation unbal: Set2_Join 344where join = "\<lambda>l x r. Node l x () r" and inv = "\<lambda>t. True" 345proof (standard, goal_cases) 346 case 1 show ?case by simp 347next 348 case 2 thus ?case by simp 349next 350 case 3 thus ?case by simp 351next 352 case 4 thus ?case by simp 353next 354 case 5 thus ?case by simp 355qed 356 357end