60247
|
1 |
(* Title: HOL/Cardinals/Bounded_Set.thy
|
59747
|
2 |
Author: Dmitriy Traytel, TU Muenchen
|
|
3 |
Copyright 2015
|
|
4 |
|
|
5 |
Bounded powerset type.
|
|
6 |
*)
|
|
7 |
|
|
8 |
section \<open>Sets Strictly Bounded by an Infinite Cardinal\<close>
|
|
9 |
|
|
10 |
theory Bounded_Set
|
|
11 |
imports Cardinals
|
|
12 |
begin
|
|
13 |
|
|
14 |
typedef ('a, 'k) bset ("_ set[_]" [22, 21] 21) =
|
|
15 |
"{A :: 'a set. |A| <o natLeq +c |UNIV :: 'k set|}"
|
|
16 |
morphisms set_bset Abs_bset
|
|
17 |
by (rule exI[of _ "{}"]) (auto simp: card_of_empty4 csum_def)
|
|
18 |
|
|
19 |
setup_lifting type_definition_bset
|
|
20 |
|
|
21 |
lift_definition map_bset ::
|
|
22 |
"('a \<Rightarrow> 'b) \<Rightarrow> 'a set['k] \<Rightarrow> 'b set['k]" is image
|
|
23 |
using card_of_image ordLeq_ordLess_trans by blast
|
|
24 |
|
|
25 |
lift_definition rel_bset ::
|
|
26 |
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool" is rel_set
|
|
27 |
.
|
|
28 |
|
|
29 |
lift_definition bempty :: "'a set['k]" is "{}"
|
|
30 |
by (auto simp: card_of_empty4 csum_def)
|
|
31 |
|
|
32 |
lift_definition binsert :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> 'a set['k]" is "insert"
|
|
33 |
using infinite_card_of_insert ordIso_ordLess_trans Field_card_of Field_natLeq UNIV_Plus_UNIV
|
|
34 |
csum_def finite_Plus_UNIV_iff finite_insert finite_ordLess_infinite2 infinite_UNIV_nat by metis
|
|
35 |
|
|
36 |
definition bsingleton where
|
|
37 |
"bsingleton x = binsert x bempty"
|
|
38 |
|
|
39 |
lemma set_bset_to_set_bset: "|A| <o natLeq +c |UNIV :: 'k set| \<Longrightarrow>
|
|
40 |
set_bset (the_inv set_bset A :: 'a set['k]) = A"
|
|
41 |
apply (rule f_the_inv_into_f[unfolded inj_on_def])
|
|
42 |
apply (simp add: set_bset_inject range_eqI Abs_bset_inverse[symmetric])
|
|
43 |
apply (rule range_eqI Abs_bset_inverse[symmetric] CollectI)+
|
|
44 |
.
|
|
45 |
|
|
46 |
lemma rel_bset_aux_infinite:
|
|
47 |
fixes a :: "'a set['k]" and b :: "'b set['k]"
|
|
48 |
shows "(\<forall>t \<in> set_bset a. \<exists>u \<in> set_bset b. R t u) \<and> (\<forall>u \<in> set_bset b. \<exists>t \<in> set_bset a. R t u) \<longleftrightarrow>
|
|
49 |
((BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset fst))\<inverse>\<inverse> OO
|
|
50 |
BNF_Def.Grp {a. set_bset a \<subseteq> {(a, b). R a b}} (map_bset snd)) a b" (is "?L \<longleftrightarrow> ?R")
|
|
51 |
proof
|
|
52 |
assume ?L
|
63040
|
53 |
define R' :: "('a \<times> 'b) set['k]"
|
|
54 |
where "R' = the_inv set_bset (Collect (case_prod R) \<inter> (set_bset a \<times> set_bset b))"
|
|
55 |
(is "_ = the_inv set_bset ?L'")
|
59747
|
56 |
have "|?L'| <o natLeq +c |UNIV :: 'k set|"
|
|
57 |
unfolding csum_def Field_natLeq
|
|
58 |
by (intro ordLeq_ordLess_trans[OF card_of_mono1[OF Int_lower2]]
|
|
59 |
card_of_Times_ordLess_infinite)
|
|
60 |
(simp, (transfer, simp add: csum_def Field_natLeq)+)
|
|
61 |
hence *: "set_bset R' = ?L'" unfolding R'_def by (intro set_bset_to_set_bset)
|
|
62 |
show ?R unfolding Grp_def relcompp.simps conversep.simps
|
|
63 |
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
|
63167
|
64 |
from * show "a = map_bset fst R'" using conjunct1[OF \<open>?L\<close>]
|
59747
|
65 |
by (transfer, auto simp add: image_def Int_def split: prod.splits)
|
63167
|
66 |
from * show "b = map_bset snd R'" using conjunct2[OF \<open>?L\<close>]
|
59747
|
67 |
by (transfer, auto simp add: image_def Int_def split: prod.splits)
|
|
68 |
qed (auto simp add: *)
|
|
69 |
next
|
|
70 |
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
|
|
71 |
by transfer force
|
|
72 |
qed
|
|
73 |
|
|
74 |
bnf "'a set['k]"
|
|
75 |
map: map_bset
|
|
76 |
sets: set_bset
|
|
77 |
bd: "natLeq +c |UNIV :: 'k set|"
|
|
78 |
wits: bempty
|
|
79 |
rel: rel_bset
|
|
80 |
proof -
|
|
81 |
show "map_bset id = id" by (rule ext, transfer) simp
|
|
82 |
next
|
|
83 |
fix f g
|
|
84 |
show "map_bset (f o g) = map_bset f o map_bset g" by (rule ext, transfer) auto
|
|
85 |
next
|
|
86 |
fix X f g
|
|
87 |
assume "\<And>z. z \<in> set_bset X \<Longrightarrow> f z = g z"
|
|
88 |
then show "map_bset f X = map_bset g X" by transfer force
|
|
89 |
next
|
|
90 |
fix f
|
|
91 |
show "set_bset \<circ> map_bset f = op ` f \<circ> set_bset" by (rule ext, transfer) auto
|
|
92 |
next
|
|
93 |
fix X :: "'a set['k]"
|
|
94 |
show "|set_bset X| \<le>o natLeq +c |UNIV :: 'k set|"
|
|
95 |
by transfer (blast dest: ordLess_imp_ordLeq)
|
|
96 |
next
|
|
97 |
fix R S
|
|
98 |
show "rel_bset R OO rel_bset S \<le> rel_bset (R OO S)"
|
|
99 |
by (rule predicate2I, transfer) (auto simp: rel_set_OO[symmetric])
|
|
100 |
next
|
|
101 |
fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
|
62324
|
102 |
show "rel_bset R = ((\<lambda>x y. \<exists>z. set_bset z \<subseteq> {(x, y). R x y} \<and>
|
|
103 |
map_bset fst z = x \<and> map_bset snd z = y) :: 'a set['k] \<Rightarrow> 'b set['k] \<Rightarrow> bool)"
|
|
104 |
by (simp add: rel_bset_def map_fun_def o_def rel_set_def
|
|
105 |
rel_bset_aux_infinite[unfolded OO_Grp_alt])
|
59747
|
106 |
next
|
|
107 |
fix x
|
|
108 |
assume "x \<in> set_bset bempty"
|
|
109 |
then show False by transfer simp
|
|
110 |
qed (simp_all add: card_order_csum natLeq_card_order cinfinite_csum natLeq_cinfinite)
|
|
111 |
|
|
112 |
|
|
113 |
lemma map_bset_bempty[simp]: "map_bset f bempty = bempty"
|
|
114 |
by transfer auto
|
|
115 |
|
|
116 |
lemma map_bset_binsert[simp]: "map_bset f (binsert x X) = binsert (f x) (map_bset f X)"
|
|
117 |
by transfer auto
|
|
118 |
|
|
119 |
lemma map_bset_bsingleton: "map_bset f (bsingleton x) = bsingleton (f x)"
|
|
120 |
unfolding bsingleton_def by simp
|
|
121 |
|
|
122 |
lemma bempty_not_binsert: "bempty \<noteq> binsert x X" "binsert x X \<noteq> bempty"
|
|
123 |
by (transfer, auto)+
|
|
124 |
|
|
125 |
lemma bempty_not_bsingleton[simp]: "bempty \<noteq> bsingleton x" "bsingleton x \<noteq> bempty"
|
|
126 |
unfolding bsingleton_def by (simp_all add: bempty_not_binsert)
|
|
127 |
|
|
128 |
lemma bsingleton_inj[simp]: "bsingleton x = bsingleton y \<longleftrightarrow> x = y"
|
|
129 |
unfolding bsingleton_def by transfer auto
|
|
130 |
|
|
131 |
lemma rel_bsingleton[simp]:
|
|
132 |
"rel_bset R (bsingleton x1) (bsingleton x2) = R x1 x2"
|
|
133 |
unfolding bsingleton_def
|
|
134 |
by transfer (auto simp: rel_set_def)
|
|
135 |
|
|
136 |
lemma rel_bset_bsingleton[simp]:
|
|
137 |
"rel_bset R (bsingleton x1) = (\<lambda>X. X \<noteq> bempty \<and> (\<forall>x2\<in>set_bset X. R x1 x2))"
|
|
138 |
"rel_bset R X (bsingleton x2) = (X \<noteq> bempty \<and> (\<forall>x1\<in>set_bset X. R x1 x2))"
|
|
139 |
unfolding bsingleton_def fun_eq_iff
|
|
140 |
by (transfer, force simp add: rel_set_def)+
|
|
141 |
|
|
142 |
lemma rel_bset_bempty[simp]:
|
|
143 |
"rel_bset R bempty X = (X = bempty)"
|
|
144 |
"rel_bset R Y bempty = (Y = bempty)"
|
|
145 |
by (transfer, simp add: rel_set_def)+
|
|
146 |
|
|
147 |
definition bset_of_option where
|
|
148 |
"bset_of_option = case_option bempty bsingleton"
|
|
149 |
|
|
150 |
lift_definition bgraph :: "('a \<Rightarrow> 'b option) \<Rightarrow> ('a \<times> 'b) set['a set]" is
|
|
151 |
"\<lambda>f. {(a, b). f a = Some b}"
|
|
152 |
proof -
|
|
153 |
fix f :: "'a \<Rightarrow> 'b option"
|
|
154 |
have "|{(a, b). f a = Some b}| \<le>o |UNIV :: 'a set|"
|
|
155 |
by (rule surj_imp_ordLeq[of _ "\<lambda>x. (x, the (f x))"]) auto
|
|
156 |
also have "|UNIV :: 'a set| <o |UNIV :: 'a set set|"
|
|
157 |
by simp
|
|
158 |
also have "|UNIV :: 'a set set| \<le>o natLeq +c |UNIV :: 'a set set|"
|
|
159 |
by (rule ordLeq_csum2) simp
|
|
160 |
finally show "|{(a, b). f a = Some b}| <o natLeq +c |UNIV :: 'a set set|" .
|
|
161 |
qed
|
|
162 |
|
|
163 |
lemma rel_bset_False[simp]: "rel_bset (\<lambda>x y. False) x y = (x = bempty \<and> y = bempty)"
|
|
164 |
by transfer (auto simp: rel_set_def)
|
|
165 |
|
|
166 |
lemma rel_bset_of_option[simp]:
|
|
167 |
"rel_bset R (bset_of_option x1) (bset_of_option x2) = rel_option R x1 x2"
|
|
168 |
unfolding bset_of_option_def bsingleton_def[abs_def]
|
|
169 |
by transfer (auto simp: rel_set_def split: option.splits)
|
|
170 |
|
|
171 |
lemma rel_bgraph[simp]:
|
|
172 |
"rel_bset (rel_prod (op =) R) (bgraph f1) (bgraph f2) = rel_fun (op =) (rel_option R) f1 f2"
|
|
173 |
apply transfer
|
|
174 |
apply (auto simp: rel_fun_def rel_option_iff rel_set_def split: option.splits)
|
|
175 |
using option.collapse apply fastforce+
|
|
176 |
done
|
|
177 |
|
|
178 |
lemma set_bset_bsingleton[simp]:
|
|
179 |
"set_bset (bsingleton x) = {x}"
|
|
180 |
unfolding bsingleton_def by transfer auto
|
|
181 |
|
|
182 |
lemma binsert_absorb[simp]: "binsert a (binsert a x) = binsert a x"
|
|
183 |
by transfer simp
|
|
184 |
|
|
185 |
lemma map_bset_eq_bempty_iff[simp]: "map_bset f X = bempty \<longleftrightarrow> X = bempty"
|
|
186 |
by transfer auto
|
|
187 |
|
|
188 |
lemma map_bset_eq_bsingleton_iff[simp]:
|
|
189 |
"map_bset f X = bsingleton x \<longleftrightarrow> (set_bset X \<noteq> {} \<and> (\<forall>y \<in> set_bset X. f y = x))"
|
|
190 |
unfolding bsingleton_def by transfer auto
|
|
191 |
|
|
192 |
lift_definition bCollect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set['a set]" is Collect
|
|
193 |
apply (rule ordLeq_ordLess_trans[OF card_of_mono1[OF subset_UNIV]])
|
|
194 |
apply (rule ordLess_ordLeq_trans[OF card_of_set_type])
|
|
195 |
apply (rule ordLeq_csum2[OF card_of_Card_order])
|
|
196 |
done
|
|
197 |
|
|
198 |
lift_definition bmember :: "'a \<Rightarrow> 'a set['k] \<Rightarrow> bool" is "op \<in>" .
|
|
199 |
|
|
200 |
lemma bmember_bCollect[simp]: "bmember a (bCollect P) = P a"
|
|
201 |
by transfer simp
|
|
202 |
|
|
203 |
lemma bset_eq_iff: "A = B \<longleftrightarrow> (\<forall>a. bmember a A = bmember a B)"
|
|
204 |
by transfer auto
|
|
205 |
|
|
206 |
(* FIXME: Lifting does not work with dead variables,
|
|
207 |
that is why we are hiding the below setup in a locale*)
|
|
208 |
locale bset_lifting
|
|
209 |
begin
|
|
210 |
|
|
211 |
declare bset.rel_eq[relator_eq]
|
|
212 |
declare bset.rel_mono[relator_mono]
|
|
213 |
declare bset.rel_compp[symmetric, relator_distr]
|
|
214 |
declare bset.rel_transfer[transfer_rule]
|
|
215 |
|
|
216 |
lemma bset_quot_map[quot_map]: "Quotient R Abs Rep T \<Longrightarrow>
|
|
217 |
Quotient (rel_bset R) (map_bset Abs) (map_bset Rep) (rel_bset T)"
|
|
218 |
unfolding Quotient_alt_def5 bset.rel_Grp[of UNIV, simplified, symmetric]
|
|
219 |
bset.rel_conversep[symmetric] bset.rel_compp[symmetric]
|
|
220 |
by (auto elim: bset.rel_mono_strong)
|
|
221 |
|
|
222 |
lemma set_relator_eq_onp [relator_eq_onp]:
|
|
223 |
"rel_bset (eq_onp P) = eq_onp (\<lambda>A. Ball (set_bset A) P)"
|
|
224 |
unfolding fun_eq_iff eq_onp_def by transfer (auto simp: rel_set_def)
|
|
225 |
|
|
226 |
end
|
|
227 |
|
|
228 |
end
|