move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
1 (* Title: HOL/Library/RBT_Set.thy
5 header {* Implementation of sets using RBT trees *}
8 imports RBT Product_Lexorder
12 Users should be aware that by including this file all code equations
13 outside of List.thy using 'a list as an implenentation of sets cannot be
14 used for code generation. If such equations are not needed, they can be
15 deleted from the code generator. Otherwise, a user has to provide their
16 own equations using RBT trees.
19 section {* Definition of code datatype constructors *}
21 definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
22 where "Set t = {x . lookup t x = Some ()}"
24 definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set"
25 where [simp]: "Coset t = - Set t"
28 section {* Deletion of already existing code equations *}
30 lemma [code, code del]:
31 "Set.empty = Set.empty" ..
33 lemma [code, code del]:
34 "Set.is_empty = Set.is_empty" ..
36 lemma [code, code del]:
37 "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
39 lemma [code, code del]:
40 "Set.member = Set.member" ..
42 lemma [code, code del]:
43 "Set.insert = Set.insert" ..
45 lemma [code, code del]:
46 "Set.remove = Set.remove" ..
48 lemma [code, code del]:
51 lemma [code, code del]:
52 "Set.filter = Set.filter" ..
54 lemma [code, code del]:
57 lemma [code, code del]:
58 "Set.subset_eq = Set.subset_eq" ..
60 lemma [code, code del]:
63 lemma [code, code del]:
66 lemma [code, code del]:
67 "can_select = can_select" ..
69 lemma [code, code del]:
70 "Set.union = Set.union" ..
72 lemma [code, code del]:
73 "minus_set_inst.minus_set = minus_set_inst.minus_set" ..
75 lemma [code, code del]:
76 "Set.inter = Set.inter" ..
78 lemma [code, code del]:
81 lemma [code, code del]:
82 "the_elem = the_elem" ..
84 lemma [code, code del]:
87 lemma [code, code del]:
90 lemma [code, code del]:
91 "Product_Type.product = Product_Type.product" ..
93 lemma [code, code del]:
96 lemma [code, code del]:
99 lemma [code, code del]:
102 lemma [code, code del]:
103 "relcomp = relcomp" ..
105 lemma [code, code del]:
108 lemma [code, code del]:
111 lemma [code, code del]:
112 "Inf_fin = Inf_fin" ..
114 lemma [code, code del]:
117 lemma [code, code del]:
120 lemma [code, code del]:
121 "Sup_fin = Sup_fin" ..
123 lemma [code, code del]:
126 lemma [code, code del]:
127 "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
129 lemma [code, code del]:
130 "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
132 lemma [code, code del]:
133 "sorted_list_of_set = sorted_list_of_set" ..
135 lemma [code, code del]:
136 "List.map_project = List.map_project" ..
138 lemma [code, code del]:
139 "List.Bleast = List.Bleast" ..
144 subsection {* Auxiliary lemmas *}
146 lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
147 by (auto simp: not_Some_eq[THEN iffD1])
149 lemma Set_set_keys: "Set x = dom (lookup x)"
150 by (auto simp: Set_def)
152 lemma finite_Set [simp, intro!]: "finite (Set x)"
153 by (simp add: Set_set_keys)
155 lemma set_keys: "Set t = set(keys t)"
156 by (simp add: Set_set_keys lookup_keys)
158 subsection {* fold and filter *}
160 lemma finite_fold_rbt_fold_eq:
161 assumes "comp_fun_commute f"
162 shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
164 have *: "remdups (entries t) = entries t"
165 using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
166 show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
169 definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b"
170 where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
172 lemma fold_keys_def_alt:
173 "fold_keys f t s = List.fold f (keys t) s"
174 by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
176 lemma finite_fold_fold_keys:
177 assumes "comp_fun_commute f"
178 shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
181 interpret comp_fun_commute f by fact
182 have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
183 moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
184 ultimately show ?thesis
185 by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq
186 comp_comp_fun_commute)
189 definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
190 "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
192 lemma Set_filter_rbt_filter:
193 "Set.filter P (Set t) = rbt_filter P t"
194 by (simp add: fold_keys_def Set_filter_fold rbt_filter_def
195 finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
198 subsection {* foldi and Ball *}
200 lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
201 by (induction t) auto
203 lemma rbt_foldi_fold_conj:
204 "RBT_Impl.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t val"
205 proof (induction t arbitrary: val)
206 case (Branch c t1) then show ?case
207 by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False)
210 lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
211 unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
214 subsection {* foldi and Bex *}
216 lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
217 by (induction t) auto
219 lemma rbt_foldi_fold_disj:
220 "RBT_Impl.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t val"
221 proof (induction t arbitrary: val)
222 case (Branch c t1) then show ?case
223 by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True)
226 lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
227 unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
230 subsection {* folding over non empty trees and selecting the minimal and maximal element *}
234 (* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
236 definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a"
237 where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
241 definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
242 where "rbt_min t = rbt_fold1_keys min t"
244 lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys rt) \<Longrightarrow> k \<le> x)"
245 by (auto simp: rbt_greater_prop less_imp_le)
247 lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys lt) \<Longrightarrow> x \<le> k)"
248 by (auto simp: rbt_less_prop less_imp_le)
251 fixes k :: "_ :: linorder"
252 shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k"
253 by (induct xs) (auto simp add: min_def)
256 "is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
257 by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
259 fun rbt_min_opt where
260 "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
261 "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
263 lemma rbt_min_opt_Branch:
264 "t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1"
267 lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
268 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
269 assumes "P rbt.Empty"
270 assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
271 assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
276 apply (case_tac "t1 = rbt.Empty")
280 lemma rbt_min_opt_in_set:
281 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
282 assumes "t \<noteq> rbt.Empty"
283 shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
284 using assms by (induction t rule: rbt_min_opt.induct) (auto)
286 lemma rbt_min_opt_is_min:
287 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
288 assumes "rbt_sorted t"
289 assumes "t \<noteq> rbt.Empty"
290 shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
292 proof (induction t rule: rbt_min_opt_induct)
294 then show ?case by simp
297 then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
299 case (left_non_empty c t1 k v t2 y)
300 then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
301 with left_non_empty show ?case
303 case goal1 then show ?case
304 by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
306 case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
308 case goal3 show ?case
310 from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
311 moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
312 ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
317 lemma rbt_min_eq_rbt_min_opt:
318 assumes "t \<noteq> RBT_Impl.Empty"
320 shows "rbt_min t = rbt_min_opt t"
322 from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
323 with assms show ?thesis
324 by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min
325 Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set)
330 definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a"
331 where "rbt_max t = rbt_fold1_keys max t"
334 fixes k :: "_ :: linorder"
335 shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k"
336 by (induct xs) (auto simp add: max_def)
338 lemma fold_max_rev_eq:
339 fixes xs :: "('a :: linorder) list"
340 assumes "xs \<noteq> []"
341 shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))"
342 using assms by (simp add: Max.set_eq_fold [symmetric])
345 assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)"
346 shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
348 have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
349 using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
350 then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
353 fun rbt_max_opt where
354 "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
355 "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
357 lemma rbt_max_opt_Branch:
358 "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2"
361 lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
362 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
363 assumes "P rbt.Empty"
364 assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
365 assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
370 apply (case_tac "t2 = rbt.Empty")
374 lemma rbt_max_opt_in_set:
375 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
376 assumes "t \<noteq> rbt.Empty"
377 shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
378 using assms by (induction t rule: rbt_max_opt.induct) (auto)
380 lemma rbt_max_opt_is_max:
381 fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
382 assumes "rbt_sorted t"
383 assumes "t \<noteq> rbt.Empty"
384 shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
386 proof (induction t rule: rbt_max_opt_induct)
388 then show ?case by simp
391 then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
393 case (right_non_empty c t1 k v t2 y)
394 then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
395 with right_non_empty show ?case
397 case goal1 then show ?case
398 by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
400 case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
402 case goal3 show ?case
404 from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
405 moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
406 ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
411 lemma rbt_max_eq_rbt_max_opt:
412 assumes "t \<noteq> RBT_Impl.Empty"
414 shows "rbt_max t = rbt_max_opt t"
416 from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all
417 with assms show ?thesis
418 by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max
419 Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set)
425 lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
426 is rbt_fold1_keys by simp
428 lemma fold1_keys_def_alt:
429 "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
430 by transfer (simp add: rbt_fold1_keys_def)
432 lemma finite_fold1_fold1_keys:
433 assumes "semilattice f"
434 assumes "\<not> is_empty t"
435 shows "semilattice_set.F f (Set t) = fold1_keys f t"
437 from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
438 show ?thesis using assms
439 by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
444 lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
446 lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
448 lemma r_min_alt_def: "r_min t = fold1_keys min t"
449 by transfer (simp add: rbt_min_def)
451 lemma r_min_eq_r_min_opt:
452 assumes "\<not> (is_empty t)"
453 shows "r_min t = r_min_opt t"
454 using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
456 lemma fold_keys_min_top_eq:
457 fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
458 assumes "\<not> (is_empty t)"
459 shows "fold_keys min t top = fold1_keys min t"
461 have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top =
462 List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
463 by (simp add: hd_Cons_tl[symmetric])
464 { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
465 have "List.fold min (x#xs) top = List.fold min xs x"
466 by (simp add: inf_min[symmetric])
468 show ?thesis using assms
469 unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
482 lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
484 lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
486 lemma r_max_alt_def: "r_max t = fold1_keys max t"
487 by transfer (simp add: rbt_max_def)
489 lemma r_max_eq_r_max_opt:
490 assumes "\<not> (is_empty t)"
491 shows "r_max t = r_max_opt t"
492 using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
494 lemma fold_keys_max_bot_eq:
495 fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
496 assumes "\<not> (is_empty t)"
497 shows "fold_keys max t bot = fold1_keys max t"
499 have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot =
500 List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
501 by (simp add: hd_Cons_tl[symmetric])
502 { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
503 have "List.fold max (x#xs) bot = List.fold max xs x"
504 by (simp add: sup_max[symmetric])
506 show ?thesis using assms
507 unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
519 section {* Code equations *}
521 code_datatype Set Coset
523 declare set.simps[code]
525 lemma empty_Set [code]:
526 "Set.empty = Set RBT.empty"
527 by (auto simp: Set_def)
529 lemma UNIV_Coset [code]:
530 "UNIV = Coset RBT.empty"
531 by (auto simp: Set_def)
533 lemma is_empty_Set [code]:
534 "Set.is_empty (Set t) = RBT.is_empty t"
535 unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
537 lemma compl_code [code]:
538 "- Set xs = Coset xs"
539 "- Coset xs = Set xs"
540 by (simp_all add: Set_def)
542 lemma member_code [code]:
543 "x \<in> (Set t) = (RBT.lookup t x = Some ())"
544 "x \<in> (Coset t) = (RBT.lookup t x = None)"
545 by (simp_all add: Set_def)
547 lemma insert_code [code]:
548 "Set.insert x (Set t) = Set (RBT.insert x () t)"
549 "Set.insert x (Coset t) = Coset (RBT.delete x t)"
550 by (auto simp: Set_def)
552 lemma remove_code [code]:
553 "Set.remove x (Set t) = Set (RBT.delete x t)"
554 "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
555 by (auto simp: Set_def)
557 lemma union_Set [code]:
558 "Set t \<union> A = fold_keys Set.insert t A"
560 interpret comp_fun_idem Set.insert
561 by (fact comp_fun_idem_insert)
562 from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
563 show ?thesis by (auto simp add: union_fold_insert)
566 lemma inter_Set [code]:
567 "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
568 by (simp add: inter_Set_filter Set_filter_rbt_filter)
570 lemma minus_Set [code]:
571 "A - Set t = fold_keys Set.remove t A"
573 interpret comp_fun_idem Set.remove
574 by (fact comp_fun_idem_remove)
575 from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
576 show ?thesis by (auto simp add: minus_fold_remove)
579 lemma union_Coset [code]:
580 "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
582 have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
583 show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
586 lemma union_Set_Set [code]:
587 "Set t1 \<union> Set t2 = Set (union t1 t2)"
588 by (auto simp add: lookup_union map_add_Some_iff Set_def)
590 lemma inter_Coset [code]:
591 "A \<inter> Coset t = fold_keys Set.remove t A"
592 by (simp add: Diff_eq [symmetric] minus_Set)
594 lemma inter_Coset_Coset [code]:
595 "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
596 by (auto simp add: lookup_union map_add_Some_iff Set_def)
598 lemma minus_Coset [code]:
599 "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
600 by (simp add: inter_Set[simplified Int_commute])
602 lemma filter_Set [code]:
603 "Set.filter P (Set t) = (rbt_filter P t)"
604 by (auto simp add: Set_filter_rbt_filter)
606 lemma image_Set [code]:
607 "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
609 have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
610 then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
613 lemma Ball_Set [code]:
614 "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
616 have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
618 by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
621 lemma Bex_Set [code]:
622 "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
624 have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
626 by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
629 lemma subset_code [code]:
630 "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
631 "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
634 lemma subset_Coset_empty_Set_empty [code]:
635 "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of
636 (rbt.Empty, rbt.Empty) => False |
637 (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
639 have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
640 by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
641 have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
643 by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
646 text {* A frequent case – avoid intermediate sets *}
648 "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
649 by (simp add: subset_code Ball_Set)
651 lemma card_Set [code]:
652 "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
653 by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const)
655 lemma setsum_Set [code]:
656 "setsum f (Set xs) = fold_keys (plus o f) xs 0"
658 have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
660 by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
663 lemma the_elem_set [code]:
664 fixes t :: "('a :: linorder, unit) rbt"
665 shows "the_elem (Set t) = (case impl_of t of
666 (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
667 | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
670 fix x :: "'a :: linorder"
671 let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty"
672 have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
673 then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
675 have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x"
676 by (subst(asm) RBT_inverse[symmetric, OF *])
677 (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
680 by(auto split: rbt.split unit.split color.split)
683 lemma Pow_Set [code]:
684 "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
685 by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
687 lemma product_Set [code]:
688 "Product_Type.product (Set t1) (Set t2) =
689 fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
691 have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
692 show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]
693 by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
696 lemma Id_on_Set [code]:
697 "Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
699 have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
701 by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
704 lemma Image_Set [code]:
705 "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
706 by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
708 lemma trancl_set_ntrancl [code]:
709 "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
710 by (simp add: finite_trancl_ntranl)
712 lemma relcomp_Set[code]:
713 "(Set t1) O (Set t2) = fold_keys
714 (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
716 interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
717 have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
718 by default (auto simp add: fun_eq_iff)
719 show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
720 by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
724 "wf (Set t) = acyclic (Set t)"
725 by (simp add: wf_iff_acyclic_if_finite)
727 lemma Min_fin_set_fold [code]:
730 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
733 have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
734 with finite_fold1_fold1_keys [OF *, folded Min_def]
736 by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric])
739 lemma Inf_fin_set_fold [code]:
740 "Inf_fin (Set t) = Min (Set t)"
741 by (simp add: inf_min Inf_fin_def Min_def)
744 fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
745 shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
747 have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
748 then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
749 by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
751 by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
754 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
755 declare Inf'_def[symmetric, code_unfold]
756 declare Inf_Set_fold[folded Inf'_def, code]
758 lemma INFI_Set_fold [code]:
759 fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
760 shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
762 have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
763 by default (auto simp add: fun_eq_iff ac_simps)
765 by (auto simp: INF_fold_inf finite_fold_fold_keys)
768 lemma Max_fin_set_fold [code]:
771 then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
774 have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
775 with finite_fold1_fold1_keys [OF *, folded Max_def]
777 by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric])
780 lemma Sup_fin_set_fold [code]:
781 "Sup_fin (Set t) = Max (Set t)"
782 by (simp add: sup_max Sup_fin_def Max_def)
785 fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
786 shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
788 have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
789 then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
790 by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
792 by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
795 definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
796 declare Sup'_def[symmetric, code_unfold]
797 declare Sup_Set_fold[folded Sup'_def, code]
799 lemma SUPR_Set_fold [code]:
800 fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
801 shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
803 have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
804 by default (auto simp add: fun_eq_iff ac_simps)
806 by (auto simp: SUP_fold_sup finite_fold_fold_keys)
809 lemma sorted_list_set[code]:
810 "sorted_list_of_set (Set t) = keys t"
811 by (auto simp add: set_keys intro: sorted_distinct_set_unique)
813 lemma Bleast_code [code]:
814 "Bleast (Set t) P = (case filter P (keys t) of
815 x#xs \<Rightarrow> x |
816 [] \<Rightarrow> abort_Bleast (Set t) P)"
817 proof (cases "filter P (keys t)")
818 case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
821 have "(LEAST x. x \<in> Set t \<and> P x) = x"
822 proof (rule Least_equality)
823 show "x \<in> Set t \<and> P x" using Cons[symmetric]
824 by(auto simp add: set_keys Cons_eq_filter_iff)
826 fix y assume "y : Set t \<and> P y"
827 then show "x \<le> y" using Cons[symmetric]
828 by(auto simp add: set_keys Cons_eq_filter_iff)
829 (metis sorted_Cons sorted_append sorted_keys)
831 thus ?thesis using Cons by (simp add: Bleast_def)
835 hide_const (open) RBT_Set.Set RBT_Set.Coset