author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 66292 | 9930f4cf6c7a |
child 67091 | 1393c2340eec |
permissions | -rw-r--r-- |
53953 | 1 |
(* Title: HOL/Library/FSet.thy |
2 |
Author: Ondrej Kuncar, TU Muenchen |
|
3 |
Author: Cezary Kaliszyk and Christian Urban |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
4 |
Author: Andrei Popescu, TU Muenchen |
53953 | 5 |
*) |
6 |
||
60500 | 7 |
section \<open>Type of finite sets defined as a subtype of sets\<close> |
53953 | 8 |
|
9 |
theory FSet |
|
66262
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
10 |
imports Main Countable |
53953 | 11 |
begin |
12 |
||
60500 | 13 |
subsection \<open>Definition of the type\<close> |
53953 | 14 |
|
15 |
typedef 'a fset = "{A :: 'a set. finite A}" morphisms fset Abs_fset |
|
16 |
by auto |
|
17 |
||
18 |
setup_lifting type_definition_fset |
|
19 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
20 |
|
60500 | 21 |
subsection \<open>Basic operations and type class instantiations\<close> |
53953 | 22 |
|
23 |
(* FIXME transfer and right_total vs. bi_total *) |
|
24 |
instantiation fset :: (finite) finite |
|
25 |
begin |
|
60679 | 26 |
instance by (standard; transfer; simp) |
53953 | 27 |
end |
28 |
||
29 |
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
|
30 |
begin |
|
31 |
||
63331 | 32 |
lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp |
53953 | 33 |
|
63331 | 34 |
lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
35 |
. |
53953 | 36 |
|
37 |
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" |
|
38 |
||
39 |
lemma less_fset_transfer[transfer_rule]: |
|
63343 | 40 |
includes lifting_syntax |
63331 | 41 |
assumes [transfer_rule]: "bi_unique A" |
53953 | 42 |
shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <" |
43 |
unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover |
|
63331 | 44 |
|
53953 | 45 |
|
46 |
lift_definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is union parametric union_transfer |
|
47 |
by simp |
|
48 |
||
49 |
lift_definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is inter parametric inter_transfer |
|
50 |
by simp |
|
51 |
||
52 |
lift_definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is minus parametric Diff_transfer |
|
53 |
by simp |
|
54 |
||
55 |
instance |
|
60679 | 56 |
by (standard; transfer; auto)+ |
53953 | 57 |
|
58 |
end |
|
59 |
||
60 |
abbreviation fempty :: "'a fset" ("{||}") where "{||} \<equiv> bot" |
|
61 |
abbreviation fsubset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) where "xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
62 |
abbreviation fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) where "xs |\<subset>| ys \<equiv> xs < ys" |
|
63 |
abbreviation funion :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65) where "xs |\<union>| ys \<equiv> sup xs ys" |
|
64 |
abbreviation finter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<inter>|" 65) where "xs |\<inter>| ys \<equiv> inf xs ys" |
|
65 |
abbreviation fminus :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|-|" 65) where "xs |-| ys \<equiv> minus xs ys" |
|
66 |
||
54014 | 67 |
instantiation fset :: (equal) equal |
68 |
begin |
|
69 |
definition "HOL.equal A B \<longleftrightarrow> A |\<subseteq>| B \<and> B |\<subseteq>| A" |
|
70 |
instance by intro_classes (auto simp add: equal_fset_def) |
|
63331 | 71 |
end |
54014 | 72 |
|
53953 | 73 |
instantiation fset :: (type) conditionally_complete_lattice |
74 |
begin |
|
75 |
||
63343 | 76 |
context includes lifting_syntax |
77 |
begin |
|
53953 | 78 |
|
79 |
lemma right_total_Inf_fset_transfer: |
|
80 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A" |
|
63331 | 81 |
shows "(rel_set (rel_set A) ===> rel_set A) |
82 |
(\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {}) |
|
53953 | 83 |
(\<lambda>S. if finite (Inf S) then Inf S else {})" |
84 |
by transfer_prover |
|
85 |
||
86 |
lemma Inf_fset_transfer: |
|
87 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A" |
|
63331 | 88 |
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {}) |
53953 | 89 |
(\<lambda>A. if finite (Inf A) then Inf A else {})" |
90 |
by transfer_prover |
|
91 |
||
63331 | 92 |
lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}" |
53953 | 93 |
parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp |
94 |
||
95 |
lemma Sup_fset_transfer: |
|
96 |
assumes [transfer_rule]: "bi_unique A" |
|
55938 | 97 |
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Sup A) then Sup A else {}) |
53953 | 98 |
(\<lambda>A. if finite (Sup A) then Sup A else {})" by transfer_prover |
99 |
||
100 |
lift_definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Sup A) then Sup A else {}" |
|
101 |
parametric Sup_fset_transfer by simp |
|
102 |
||
103 |
lemma finite_Sup: "\<exists>z. finite z \<and> (\<forall>a. a \<in> X \<longrightarrow> a \<le> z) \<Longrightarrow> finite (Sup X)" |
|
104 |
by (auto intro: finite_subset) |
|
105 |
||
55938 | 106 |
lemma transfer_bdd_below[transfer_rule]: "(rel_set (pcr_fset op =) ===> op =) bdd_below bdd_below" |
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
107 |
by auto |
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
108 |
|
63343 | 109 |
end |
110 |
||
53953 | 111 |
instance |
63331 | 112 |
proof |
53953 | 113 |
fix x z :: "'a fset" |
114 |
fix X :: "'a fset set" |
|
115 |
{ |
|
63331 | 116 |
assume "x \<in> X" "bdd_below X" |
56646 | 117 |
then show "Inf X |\<subseteq>| x" by transfer auto |
53953 | 118 |
next |
119 |
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)" |
|
120 |
then show "z |\<subseteq>| Inf X" by transfer (clarsimp, blast) |
|
121 |
next |
|
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
122 |
assume "x \<in> X" "bdd_above X" |
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
123 |
then obtain z where "x \<in> X" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)" |
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
124 |
by (auto simp: bdd_above_def) |
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
125 |
then show "x |\<subseteq>| Sup X" |
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54014
diff
changeset
|
126 |
by transfer (auto intro!: finite_Sup) |
53953 | 127 |
next |
128 |
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> x |\<subseteq>| z)" |
|
129 |
then show "Sup X |\<subseteq>| z" by transfer (clarsimp, blast) |
|
130 |
} |
|
131 |
qed |
|
132 |
end |
|
133 |
||
63331 | 134 |
instantiation fset :: (finite) complete_lattice |
53953 | 135 |
begin |
136 |
||
60679 | 137 |
lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer |
138 |
by simp |
|
53953 | 139 |
|
60679 | 140 |
instance |
141 |
by (standard; transfer; auto) |
|
142 |
||
53953 | 143 |
end |
144 |
||
145 |
instantiation fset :: (finite) complete_boolean_algebra |
|
146 |
begin |
|
147 |
||
63331 | 148 |
lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus |
53953 | 149 |
parametric right_total_Compl_transfer Compl_transfer by simp |
150 |
||
60679 | 151 |
instance |
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62324
diff
changeset
|
152 |
by (standard; transfer) (simp_all add: Diff_eq) |
53953 | 153 |
|
154 |
end |
|
155 |
||
156 |
abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top" |
|
157 |
abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x" |
|
158 |
||
56646 | 159 |
declare top_fset.rep_eq[simp] |
160 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
161 |
|
60500 | 162 |
subsection \<open>Other operations\<close> |
53953 | 163 |
|
164 |
lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer |
|
165 |
by simp |
|
166 |
||
167 |
syntax |
|
168 |
"_insert_fset" :: "args => 'a fset" ("{|(_)|}") |
|
169 |
||
170 |
translations |
|
171 |
"{|x, xs|}" == "CONST finsert x {|xs|}" |
|
172 |
"{|x|}" == "CONST finsert x {||}" |
|
173 |
||
63331 | 174 |
lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
175 |
parametric member_transfer . |
53953 | 176 |
|
177 |
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
|
178 |
||
63343 | 179 |
context includes lifting_syntax |
53953 | 180 |
begin |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
181 |
|
63331 | 182 |
lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter |
53953 | 183 |
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp |
184 |
||
63331 | 185 |
lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer |
55732 | 186 |
by (simp add: finite_subset) |
53953 | 187 |
|
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
188 |
lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer . |
53953 | 189 |
|
63331 | 190 |
lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image |
53953 | 191 |
parametric image_transfer by simp |
192 |
||
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
193 |
lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem . |
53953 | 194 |
|
63331 | 195 |
lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer |
55738 | 196 |
by (simp add: Set.bind_def) |
53953 | 197 |
|
55732 | 198 |
lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp |
53953 | 199 |
|
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
200 |
lift_definition fBall :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Ball parametric Ball_transfer . |
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
201 |
lift_definition fBex :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" is Bex parametric Bex_transfer . |
53953 | 202 |
|
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55414
diff
changeset
|
203 |
lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold . |
53963 | 204 |
|
63622 | 205 |
lift_definition fset_of_list :: "'a list \<Rightarrow> 'a fset" is set by (rule finite_set) |
206 |
||
60500 | 207 |
subsection \<open>Transferred lemmas from Set.thy\<close> |
53953 | 208 |
|
209 |
lemmas fset_eqI = set_eqI[Transfer.transferred] |
|
210 |
lemmas fset_eq_iff[no_atp] = set_eq_iff[Transfer.transferred] |
|
211 |
lemmas fBallI[intro!] = ballI[Transfer.transferred] |
|
212 |
lemmas fbspec[dest?] = bspec[Transfer.transferred] |
|
213 |
lemmas fBallE[elim] = ballE[Transfer.transferred] |
|
214 |
lemmas fBexI[intro] = bexI[Transfer.transferred] |
|
215 |
lemmas rev_fBexI[intro?] = rev_bexI[Transfer.transferred] |
|
216 |
lemmas fBexCI = bexCI[Transfer.transferred] |
|
217 |
lemmas fBexE[elim!] = bexE[Transfer.transferred] |
|
218 |
lemmas fBall_triv[simp] = ball_triv[Transfer.transferred] |
|
219 |
lemmas fBex_triv[simp] = bex_triv[Transfer.transferred] |
|
220 |
lemmas fBex_triv_one_point1[simp] = bex_triv_one_point1[Transfer.transferred] |
|
221 |
lemmas fBex_triv_one_point2[simp] = bex_triv_one_point2[Transfer.transferred] |
|
222 |
lemmas fBex_one_point1[simp] = bex_one_point1[Transfer.transferred] |
|
223 |
lemmas fBex_one_point2[simp] = bex_one_point2[Transfer.transferred] |
|
224 |
lemmas fBall_one_point1[simp] = ball_one_point1[Transfer.transferred] |
|
225 |
lemmas fBall_one_point2[simp] = ball_one_point2[Transfer.transferred] |
|
226 |
lemmas fBall_conj_distrib = ball_conj_distrib[Transfer.transferred] |
|
227 |
lemmas fBex_disj_distrib = bex_disj_distrib[Transfer.transferred] |
|
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
228 |
lemmas fBall_cong[fundef_cong] = ball_cong[Transfer.transferred] |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
229 |
lemmas fBex_cong[fundef_cong] = bex_cong[Transfer.transferred] |
53964 | 230 |
lemmas fsubsetI[intro!] = subsetI[Transfer.transferred] |
231 |
lemmas fsubsetD[elim, intro?] = subsetD[Transfer.transferred] |
|
232 |
lemmas rev_fsubsetD[no_atp,intro?] = rev_subsetD[Transfer.transferred] |
|
233 |
lemmas fsubsetCE[no_atp,elim] = subsetCE[Transfer.transferred] |
|
234 |
lemmas fsubset_eq[no_atp] = subset_eq[Transfer.transferred] |
|
235 |
lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred] |
|
236 |
lemmas fsubset_refl = subset_refl[Transfer.transferred] |
|
237 |
lemmas fsubset_trans = subset_trans[Transfer.transferred] |
|
53953 | 238 |
lemmas fset_rev_mp = set_rev_mp[Transfer.transferred] |
239 |
lemmas fset_mp = set_mp[Transfer.transferred] |
|
53964 | 240 |
lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred] |
53953 | 241 |
lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred] |
53964 | 242 |
lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred] |
53953 | 243 |
lemmas fequalityD1 = equalityD1[Transfer.transferred] |
244 |
lemmas fequalityD2 = equalityD2[Transfer.transferred] |
|
245 |
lemmas fequalityE = equalityE[Transfer.transferred] |
|
246 |
lemmas fequalityCE[elim] = equalityCE[Transfer.transferred] |
|
247 |
lemmas eqfset_imp_iff = eqset_imp_iff[Transfer.transferred] |
|
248 |
lemmas eqfelem_imp_iff = eqelem_imp_iff[Transfer.transferred] |
|
249 |
lemmas fempty_iff[simp] = empty_iff[Transfer.transferred] |
|
53964 | 250 |
lemmas fempty_fsubsetI[iff] = empty_subsetI[Transfer.transferred] |
53953 | 251 |
lemmas equalsffemptyI = equals0I[Transfer.transferred] |
252 |
lemmas equalsffemptyD = equals0D[Transfer.transferred] |
|
253 |
lemmas fBall_fempty[simp] = ball_empty[Transfer.transferred] |
|
254 |
lemmas fBex_fempty[simp] = bex_empty[Transfer.transferred] |
|
255 |
lemmas fPow_iff[iff] = Pow_iff[Transfer.transferred] |
|
256 |
lemmas fPowI = PowI[Transfer.transferred] |
|
257 |
lemmas fPowD = PowD[Transfer.transferred] |
|
258 |
lemmas fPow_bottom = Pow_bottom[Transfer.transferred] |
|
259 |
lemmas fPow_top = Pow_top[Transfer.transferred] |
|
260 |
lemmas fPow_not_fempty = Pow_not_empty[Transfer.transferred] |
|
261 |
lemmas finter_iff[simp] = Int_iff[Transfer.transferred] |
|
262 |
lemmas finterI[intro!] = IntI[Transfer.transferred] |
|
263 |
lemmas finterD1 = IntD1[Transfer.transferred] |
|
264 |
lemmas finterD2 = IntD2[Transfer.transferred] |
|
265 |
lemmas finterE[elim!] = IntE[Transfer.transferred] |
|
266 |
lemmas funion_iff[simp] = Un_iff[Transfer.transferred] |
|
267 |
lemmas funionI1[elim?] = UnI1[Transfer.transferred] |
|
268 |
lemmas funionI2[elim?] = UnI2[Transfer.transferred] |
|
269 |
lemmas funionCI[intro!] = UnCI[Transfer.transferred] |
|
270 |
lemmas funionE[elim!] = UnE[Transfer.transferred] |
|
271 |
lemmas fminus_iff[simp] = Diff_iff[Transfer.transferred] |
|
272 |
lemmas fminusI[intro!] = DiffI[Transfer.transferred] |
|
273 |
lemmas fminusD1 = DiffD1[Transfer.transferred] |
|
274 |
lemmas fminusD2 = DiffD2[Transfer.transferred] |
|
275 |
lemmas fminusE[elim!] = DiffE[Transfer.transferred] |
|
276 |
lemmas finsert_iff[simp] = insert_iff[Transfer.transferred] |
|
277 |
lemmas finsertI1 = insertI1[Transfer.transferred] |
|
278 |
lemmas finsertI2 = insertI2[Transfer.transferred] |
|
279 |
lemmas finsertE[elim!] = insertE[Transfer.transferred] |
|
280 |
lemmas finsertCI[intro!] = insertCI[Transfer.transferred] |
|
53964 | 281 |
lemmas fsubset_finsert_iff = subset_insert_iff[Transfer.transferred] |
53953 | 282 |
lemmas finsert_ident = insert_ident[Transfer.transferred] |
283 |
lemmas fsingletonI[intro!,no_atp] = singletonI[Transfer.transferred] |
|
284 |
lemmas fsingletonD[dest!,no_atp] = singletonD[Transfer.transferred] |
|
285 |
lemmas fsingleton_iff = singleton_iff[Transfer.transferred] |
|
286 |
lemmas fsingleton_inject[dest!] = singleton_inject[Transfer.transferred] |
|
287 |
lemmas fsingleton_finsert_inj_eq[iff,no_atp] = singleton_insert_inj_eq[Transfer.transferred] |
|
288 |
lemmas fsingleton_finsert_inj_eq'[iff,no_atp] = singleton_insert_inj_eq'[Transfer.transferred] |
|
53964 | 289 |
lemmas fsubset_fsingletonD = subset_singletonD[Transfer.transferred] |
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62082
diff
changeset
|
290 |
lemmas fminus_single_finsert = Diff_single_insert[Transfer.transferred] |
53953 | 291 |
lemmas fdoubleton_eq_iff = doubleton_eq_iff[Transfer.transferred] |
292 |
lemmas funion_fsingleton_iff = Un_singleton_iff[Transfer.transferred] |
|
293 |
lemmas fsingleton_funion_iff = singleton_Un_iff[Transfer.transferred] |
|
294 |
lemmas fimage_eqI[simp, intro] = image_eqI[Transfer.transferred] |
|
295 |
lemmas fimageI = imageI[Transfer.transferred] |
|
296 |
lemmas rev_fimage_eqI = rev_image_eqI[Transfer.transferred] |
|
297 |
lemmas fimageE[elim!] = imageE[Transfer.transferred] |
|
298 |
lemmas Compr_fimage_eq = Compr_image_eq[Transfer.transferred] |
|
299 |
lemmas fimage_funion = image_Un[Transfer.transferred] |
|
300 |
lemmas fimage_iff = image_iff[Transfer.transferred] |
|
53964 | 301 |
lemmas fimage_fsubset_iff[no_atp] = image_subset_iff[Transfer.transferred] |
302 |
lemmas fimage_fsubsetI = image_subsetI[Transfer.transferred] |
|
53953 | 303 |
lemmas fimage_ident[simp] = image_ident[Transfer.transferred] |
62390 | 304 |
lemmas if_split_fmem1 = if_split_mem1[Transfer.transferred] |
305 |
lemmas if_split_fmem2 = if_split_mem2[Transfer.transferred] |
|
53964 | 306 |
lemmas pfsubsetI[intro!,no_atp] = psubsetI[Transfer.transferred] |
307 |
lemmas pfsubsetE[elim!,no_atp] = psubsetE[Transfer.transferred] |
|
308 |
lemmas pfsubset_finsert_iff = psubset_insert_iff[Transfer.transferred] |
|
309 |
lemmas pfsubset_eq = psubset_eq[Transfer.transferred] |
|
310 |
lemmas pfsubset_imp_fsubset = psubset_imp_subset[Transfer.transferred] |
|
311 |
lemmas pfsubset_trans = psubset_trans[Transfer.transferred] |
|
312 |
lemmas pfsubsetD = psubsetD[Transfer.transferred] |
|
313 |
lemmas pfsubset_fsubset_trans = psubset_subset_trans[Transfer.transferred] |
|
314 |
lemmas fsubset_pfsubset_trans = subset_psubset_trans[Transfer.transferred] |
|
315 |
lemmas pfsubset_imp_ex_fmem = psubset_imp_ex_mem[Transfer.transferred] |
|
53953 | 316 |
lemmas fimage_fPow_mono = image_Pow_mono[Transfer.transferred] |
317 |
lemmas fimage_fPow_surj = image_Pow_surj[Transfer.transferred] |
|
53964 | 318 |
lemmas fsubset_finsertI = subset_insertI[Transfer.transferred] |
319 |
lemmas fsubset_finsertI2 = subset_insertI2[Transfer.transferred] |
|
320 |
lemmas fsubset_finsert = subset_insert[Transfer.transferred] |
|
53953 | 321 |
lemmas funion_upper1 = Un_upper1[Transfer.transferred] |
322 |
lemmas funion_upper2 = Un_upper2[Transfer.transferred] |
|
323 |
lemmas funion_least = Un_least[Transfer.transferred] |
|
324 |
lemmas finter_lower1 = Int_lower1[Transfer.transferred] |
|
325 |
lemmas finter_lower2 = Int_lower2[Transfer.transferred] |
|
326 |
lemmas finter_greatest = Int_greatest[Transfer.transferred] |
|
53964 | 327 |
lemmas fminus_fsubset = Diff_subset[Transfer.transferred] |
328 |
lemmas fminus_fsubset_conv = Diff_subset_conv[Transfer.transferred] |
|
329 |
lemmas fsubset_fempty[simp] = subset_empty[Transfer.transferred] |
|
330 |
lemmas not_pfsubset_fempty[iff] = not_psubset_empty[Transfer.transferred] |
|
53953 | 331 |
lemmas finsert_is_funion = insert_is_Un[Transfer.transferred] |
332 |
lemmas finsert_not_fempty[simp] = insert_not_empty[Transfer.transferred] |
|
333 |
lemmas fempty_not_finsert = empty_not_insert[Transfer.transferred] |
|
334 |
lemmas finsert_absorb = insert_absorb[Transfer.transferred] |
|
335 |
lemmas finsert_absorb2[simp] = insert_absorb2[Transfer.transferred] |
|
336 |
lemmas finsert_commute = insert_commute[Transfer.transferred] |
|
53964 | 337 |
lemmas finsert_fsubset[simp] = insert_subset[Transfer.transferred] |
53953 | 338 |
lemmas finsert_inter_finsert[simp] = insert_inter_insert[Transfer.transferred] |
339 |
lemmas finsert_disjoint[simp,no_atp] = insert_disjoint[Transfer.transferred] |
|
340 |
lemmas disjoint_finsert[simp,no_atp] = disjoint_insert[Transfer.transferred] |
|
341 |
lemmas fimage_fempty[simp] = image_empty[Transfer.transferred] |
|
342 |
lemmas fimage_finsert[simp] = image_insert[Transfer.transferred] |
|
343 |
lemmas fimage_constant = image_constant[Transfer.transferred] |
|
344 |
lemmas fimage_constant_conv = image_constant_conv[Transfer.transferred] |
|
345 |
lemmas fimage_fimage = image_image[Transfer.transferred] |
|
346 |
lemmas finsert_fimage[simp] = insert_image[Transfer.transferred] |
|
347 |
lemmas fimage_is_fempty[iff] = image_is_empty[Transfer.transferred] |
|
348 |
lemmas fempty_is_fimage[iff] = empty_is_image[Transfer.transferred] |
|
349 |
lemmas fimage_cong = image_cong[Transfer.transferred] |
|
53964 | 350 |
lemmas fimage_finter_fsubset = image_Int_subset[Transfer.transferred] |
351 |
lemmas fimage_fminus_fsubset = image_diff_subset[Transfer.transferred] |
|
53953 | 352 |
lemmas finter_absorb = Int_absorb[Transfer.transferred] |
353 |
lemmas finter_left_absorb = Int_left_absorb[Transfer.transferred] |
|
354 |
lemmas finter_commute = Int_commute[Transfer.transferred] |
|
355 |
lemmas finter_left_commute = Int_left_commute[Transfer.transferred] |
|
356 |
lemmas finter_assoc = Int_assoc[Transfer.transferred] |
|
357 |
lemmas finter_ac = Int_ac[Transfer.transferred] |
|
358 |
lemmas finter_absorb1 = Int_absorb1[Transfer.transferred] |
|
359 |
lemmas finter_absorb2 = Int_absorb2[Transfer.transferred] |
|
360 |
lemmas finter_fempty_left = Int_empty_left[Transfer.transferred] |
|
361 |
lemmas finter_fempty_right = Int_empty_right[Transfer.transferred] |
|
362 |
lemmas disjoint_iff_fnot_equal = disjoint_iff_not_equal[Transfer.transferred] |
|
363 |
lemmas finter_funion_distrib = Int_Un_distrib[Transfer.transferred] |
|
364 |
lemmas finter_funion_distrib2 = Int_Un_distrib2[Transfer.transferred] |
|
53964 | 365 |
lemmas finter_fsubset_iff[no_atp, simp] = Int_subset_iff[Transfer.transferred] |
53953 | 366 |
lemmas funion_absorb = Un_absorb[Transfer.transferred] |
367 |
lemmas funion_left_absorb = Un_left_absorb[Transfer.transferred] |
|
368 |
lemmas funion_commute = Un_commute[Transfer.transferred] |
|
369 |
lemmas funion_left_commute = Un_left_commute[Transfer.transferred] |
|
370 |
lemmas funion_assoc = Un_assoc[Transfer.transferred] |
|
371 |
lemmas funion_ac = Un_ac[Transfer.transferred] |
|
372 |
lemmas funion_absorb1 = Un_absorb1[Transfer.transferred] |
|
373 |
lemmas funion_absorb2 = Un_absorb2[Transfer.transferred] |
|
374 |
lemmas funion_fempty_left = Un_empty_left[Transfer.transferred] |
|
375 |
lemmas funion_fempty_right = Un_empty_right[Transfer.transferred] |
|
376 |
lemmas funion_finsert_left[simp] = Un_insert_left[Transfer.transferred] |
|
377 |
lemmas funion_finsert_right[simp] = Un_insert_right[Transfer.transferred] |
|
378 |
lemmas finter_finsert_left = Int_insert_left[Transfer.transferred] |
|
379 |
lemmas finter_finsert_left_ifffempty[simp] = Int_insert_left_if0[Transfer.transferred] |
|
380 |
lemmas finter_finsert_left_if1[simp] = Int_insert_left_if1[Transfer.transferred] |
|
381 |
lemmas finter_finsert_right = Int_insert_right[Transfer.transferred] |
|
382 |
lemmas finter_finsert_right_ifffempty[simp] = Int_insert_right_if0[Transfer.transferred] |
|
383 |
lemmas finter_finsert_right_if1[simp] = Int_insert_right_if1[Transfer.transferred] |
|
384 |
lemmas funion_finter_distrib = Un_Int_distrib[Transfer.transferred] |
|
385 |
lemmas funion_finter_distrib2 = Un_Int_distrib2[Transfer.transferred] |
|
386 |
lemmas funion_finter_crazy = Un_Int_crazy[Transfer.transferred] |
|
53964 | 387 |
lemmas fsubset_funion_eq = subset_Un_eq[Transfer.transferred] |
53953 | 388 |
lemmas funion_fempty[iff] = Un_empty[Transfer.transferred] |
53964 | 389 |
lemmas funion_fsubset_iff[no_atp, simp] = Un_subset_iff[Transfer.transferred] |
53953 | 390 |
lemmas funion_fminus_finter = Un_Diff_Int[Transfer.transferred] |
391 |
lemmas fminus_finter2 = Diff_Int2[Transfer.transferred] |
|
392 |
lemmas funion_finter_assoc_eq = Un_Int_assoc_eq[Transfer.transferred] |
|
393 |
lemmas fBall_funion = ball_Un[Transfer.transferred] |
|
394 |
lemmas fBex_funion = bex_Un[Transfer.transferred] |
|
395 |
lemmas fminus_eq_fempty_iff[simp,no_atp] = Diff_eq_empty_iff[Transfer.transferred] |
|
396 |
lemmas fminus_cancel[simp] = Diff_cancel[Transfer.transferred] |
|
397 |
lemmas fminus_idemp[simp] = Diff_idemp[Transfer.transferred] |
|
398 |
lemmas fminus_triv = Diff_triv[Transfer.transferred] |
|
399 |
lemmas fempty_fminus[simp] = empty_Diff[Transfer.transferred] |
|
400 |
lemmas fminus_fempty[simp] = Diff_empty[Transfer.transferred] |
|
401 |
lemmas fminus_finsertffempty[simp,no_atp] = Diff_insert0[Transfer.transferred] |
|
402 |
lemmas fminus_finsert = Diff_insert[Transfer.transferred] |
|
403 |
lemmas fminus_finsert2 = Diff_insert2[Transfer.transferred] |
|
404 |
lemmas finsert_fminus_if = insert_Diff_if[Transfer.transferred] |
|
405 |
lemmas finsert_fminus1[simp] = insert_Diff1[Transfer.transferred] |
|
406 |
lemmas finsert_fminus_single[simp] = insert_Diff_single[Transfer.transferred] |
|
407 |
lemmas finsert_fminus = insert_Diff[Transfer.transferred] |
|
408 |
lemmas fminus_finsert_absorb = Diff_insert_absorb[Transfer.transferred] |
|
409 |
lemmas fminus_disjoint[simp] = Diff_disjoint[Transfer.transferred] |
|
410 |
lemmas fminus_partition = Diff_partition[Transfer.transferred] |
|
411 |
lemmas double_fminus = double_diff[Transfer.transferred] |
|
412 |
lemmas funion_fminus_cancel[simp] = Un_Diff_cancel[Transfer.transferred] |
|
413 |
lemmas funion_fminus_cancel2[simp] = Un_Diff_cancel2[Transfer.transferred] |
|
414 |
lemmas fminus_funion = Diff_Un[Transfer.transferred] |
|
415 |
lemmas fminus_finter = Diff_Int[Transfer.transferred] |
|
416 |
lemmas funion_fminus = Un_Diff[Transfer.transferred] |
|
417 |
lemmas finter_fminus = Int_Diff[Transfer.transferred] |
|
418 |
lemmas fminus_finter_distrib = Diff_Int_distrib[Transfer.transferred] |
|
419 |
lemmas fminus_finter_distrib2 = Diff_Int_distrib2[Transfer.transferred] |
|
420 |
lemmas fUNIV_bool[no_atp] = UNIV_bool[Transfer.transferred] |
|
421 |
lemmas fPow_fempty[simp] = Pow_empty[Transfer.transferred] |
|
422 |
lemmas fPow_finsert = Pow_insert[Transfer.transferred] |
|
53964 | 423 |
lemmas funion_fPow_fsubset = Un_Pow_subset[Transfer.transferred] |
53953 | 424 |
lemmas fPow_finter_eq[simp] = Pow_Int_eq[Transfer.transferred] |
53964 | 425 |
lemmas fset_eq_fsubset = set_eq_subset[Transfer.transferred] |
426 |
lemmas fsubset_iff[no_atp] = subset_iff[Transfer.transferred] |
|
427 |
lemmas fsubset_iff_pfsubset_eq = subset_iff_psubset_eq[Transfer.transferred] |
|
53953 | 428 |
lemmas all_not_fin_conv[simp] = all_not_in_conv[Transfer.transferred] |
429 |
lemmas ex_fin_conv = ex_in_conv[Transfer.transferred] |
|
430 |
lemmas fimage_mono = image_mono[Transfer.transferred] |
|
431 |
lemmas fPow_mono = Pow_mono[Transfer.transferred] |
|
432 |
lemmas finsert_mono = insert_mono[Transfer.transferred] |
|
433 |
lemmas funion_mono = Un_mono[Transfer.transferred] |
|
434 |
lemmas finter_mono = Int_mono[Transfer.transferred] |
|
435 |
lemmas fminus_mono = Diff_mono[Transfer.transferred] |
|
436 |
lemmas fin_mono = in_mono[Transfer.transferred] |
|
437 |
lemmas fthe_felem_eq[simp] = the_elem_eq[Transfer.transferred] |
|
438 |
lemmas fLeast_mono = Least_mono[Transfer.transferred] |
|
439 |
lemmas fbind_fbind = bind_bind[Transfer.transferred] |
|
440 |
lemmas fempty_fbind[simp] = empty_bind[Transfer.transferred] |
|
441 |
lemmas nonfempty_fbind_const = nonempty_bind_const[Transfer.transferred] |
|
442 |
lemmas fbind_const = bind_const[Transfer.transferred] |
|
443 |
lemmas ffmember_filter[simp] = member_filter[Transfer.transferred] |
|
444 |
lemmas fequalityI = equalityI[Transfer.transferred] |
|
63622 | 445 |
lemmas fset_of_list_simps[simp] = set_simps[Transfer.transferred] |
446 |
lemmas fset_of_list_append[simp] = set_append[Transfer.transferred] |
|
447 |
lemmas fset_of_list_rev[simp] = set_rev[Transfer.transferred] |
|
448 |
lemmas fset_of_list_map[simp] = set_map[Transfer.transferred] |
|
53953 | 449 |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
450 |
|
60500 | 451 |
subsection \<open>Additional lemmas\<close> |
53953 | 452 |
|
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
453 |
subsubsection \<open>\<open>ffUnion\<close>\<close> |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
454 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
455 |
lemmas ffUnion_funion_distrib[simp] = Union_Un_distrib[Transfer.transferred] |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
456 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
457 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
458 |
subsubsection \<open>\<open>fbind\<close>\<close> |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
459 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
460 |
lemma fbind_cong[fundef_cong]: "A = B \<Longrightarrow> (\<And>x. x |\<in>| B \<Longrightarrow> f x = g x) \<Longrightarrow> fbind A f = fbind B g" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
461 |
by transfer force |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
462 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
463 |
|
61585 | 464 |
subsubsection \<open>\<open>fsingleton\<close>\<close> |
53953 | 465 |
|
466 |
lemmas fsingletonE = fsingletonD [elim_format] |
|
467 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
468 |
|
61585 | 469 |
subsubsection \<open>\<open>femepty\<close>\<close> |
53953 | 470 |
|
471 |
lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}" |
|
472 |
by transfer auto |
|
473 |
||
474 |
(* FIXME, transferred doesn't work here *) |
|
475 |
lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P" |
|
476 |
by simp |
|
477 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
478 |
|
61585 | 479 |
subsubsection \<open>\<open>fset\<close>\<close> |
53953 | 480 |
|
53963 | 481 |
lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq |
53953 | 482 |
|
63331 | 483 |
lemma finite_fset [simp]: |
53953 | 484 |
shows "finite (fset S)" |
485 |
by transfer simp |
|
486 |
||
53963 | 487 |
lemmas fset_cong = fset_inject |
53953 | 488 |
|
489 |
lemma filter_fset [simp]: |
|
490 |
shows "fset (ffilter P xs) = Collect P \<inter> fset xs" |
|
491 |
by transfer auto |
|
492 |
||
53963 | 493 |
lemma notin_fset: "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S" by (simp add: fmember.rep_eq) |
494 |
||
495 |
lemmas inter_fset[simp] = inf_fset.rep_eq |
|
53953 | 496 |
|
53963 | 497 |
lemmas union_fset[simp] = sup_fset.rep_eq |
53953 | 498 |
|
53963 | 499 |
lemmas minus_fset[simp] = minus_fset.rep_eq |
53953 | 500 |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
501 |
|
63622 | 502 |
subsubsection \<open>\<open>ffilter\<close>\<close> |
53953 | 503 |
|
63331 | 504 |
lemma subset_ffilter: |
53953 | 505 |
"ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)" |
506 |
by transfer auto |
|
507 |
||
63331 | 508 |
lemma eq_ffilter: |
53953 | 509 |
"(ffilter P A = ffilter Q A) = (\<forall>x. x |\<in>| A \<longrightarrow> P x = Q x)" |
510 |
by transfer auto |
|
511 |
||
53964 | 512 |
lemma pfsubset_ffilter: |
63331 | 513 |
"(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow> |
53953 | 514 |
ffilter P A |\<subset>| ffilter Q A" |
515 |
unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) |
|
516 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
517 |
|
63622 | 518 |
subsubsection \<open>\<open>fset_of_list\<close>\<close> |
519 |
||
520 |
lemma fset_of_list_filter[simp]: |
|
521 |
"fset_of_list (filter P xs) = ffilter P (fset_of_list xs)" |
|
522 |
by transfer (auto simp: Set.filter_def) |
|
523 |
||
524 |
lemma fset_of_list_subset[intro]: |
|
525 |
"set xs \<subseteq> set ys \<Longrightarrow> fset_of_list xs |\<subseteq>| fset_of_list ys" |
|
526 |
by transfer simp |
|
527 |
||
528 |
lemma fset_of_list_elem: "(x |\<in>| fset_of_list xs) \<longleftrightarrow> (x \<in> set xs)" |
|
529 |
by transfer simp |
|
530 |
||
531 |
||
61585 | 532 |
subsubsection \<open>\<open>finsert\<close>\<close> |
53953 | 533 |
|
534 |
(* FIXME, transferred doesn't work here *) |
|
535 |
lemma set_finsert: |
|
536 |
assumes "x |\<in>| A" |
|
537 |
obtains B where "A = finsert x B" and "x |\<notin>| B" |
|
538 |
using assms by transfer (metis Set.set_insert finite_insert) |
|
539 |
||
540 |
lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B" |
|
63649 | 541 |
by (rule exI [where x = "A |-| {|a|}"]) blast |
53953 | 542 |
|
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
543 |
lemma finsert_eq_iff: |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
544 |
assumes "a |\<notin>| A" and "b |\<notin>| B" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
545 |
shows "(finsert a A = finsert b B) = |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
546 |
(if a = b then A = B else \<exists>C. A = finsert b C \<and> b |\<notin>| C \<and> B = finsert a C \<and> a |\<notin>| C)" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
547 |
using assms by transfer (force simp: insert_eq_iff) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
548 |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
549 |
|
61585 | 550 |
subsubsection \<open>\<open>fimage\<close>\<close> |
53953 | 551 |
|
552 |
lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)" |
|
553 |
by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff) |
|
554 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
555 |
|
60500 | 556 |
subsubsection \<open>bounded quantification\<close> |
53953 | 557 |
|
558 |
lemma bex_simps [simp, no_atp]: |
|
63331 | 559 |
"\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)" |
53953 | 560 |
"\<And>A P Q. fBex A (\<lambda>x. P \<and> Q x) = (P \<and> fBex A Q)" |
63331 | 561 |
"\<And>P. fBex {||} P = False" |
53953 | 562 |
"\<And>a B P. fBex (finsert a B) P = (P a \<or> fBex B P)" |
563 |
"\<And>A P f. fBex (f |`| A) P = fBex A (\<lambda>x. P (f x))" |
|
564 |
"\<And>A P. (\<not> fBex A P) = fBall A (\<lambda>x. \<not> P x)" |
|
565 |
by auto |
|
566 |
||
567 |
lemma ball_simps [simp, no_atp]: |
|
568 |
"\<And>A P Q. fBall A (\<lambda>x. P x \<or> Q) = (fBall A P \<or> Q)" |
|
569 |
"\<And>A P Q. fBall A (\<lambda>x. P \<or> Q x) = (P \<or> fBall A Q)" |
|
570 |
"\<And>A P Q. fBall A (\<lambda>x. P \<longrightarrow> Q x) = (P \<longrightarrow> fBall A Q)" |
|
571 |
"\<And>A P Q. fBall A (\<lambda>x. P x \<longrightarrow> Q) = (fBex A P \<longrightarrow> Q)" |
|
572 |
"\<And>P. fBall {||} P = True" |
|
573 |
"\<And>a B P. fBall (finsert a B) P = (P a \<and> fBall B P)" |
|
574 |
"\<And>A P f. fBall (f |`| A) P = fBall A (\<lambda>x. P (f x))" |
|
575 |
"\<And>A P. (\<not> fBall A P) = fBex A (\<lambda>x. \<not> P x)" |
|
576 |
by auto |
|
577 |
||
578 |
lemma atomize_fBall: |
|
579 |
"(\<And>x. x |\<in>| A ==> P x) == Trueprop (fBall A (\<lambda>x. P x))" |
|
580 |
apply (simp only: atomize_all atomize_imp) |
|
581 |
apply (rule equal_intr_rule) |
|
63622 | 582 |
by (transfer, simp)+ |
583 |
||
584 |
lemma fBall_mono[mono]: "P \<le> Q \<Longrightarrow> fBall S P \<le> fBall S Q" |
|
585 |
by auto |
|
586 |
||
53953 | 587 |
|
53963 | 588 |
end |
589 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
590 |
|
61585 | 591 |
subsubsection \<open>\<open>fcard\<close>\<close> |
53963 | 592 |
|
53964 | 593 |
(* FIXME: improve transferred to handle bounded meta quantification *) |
594 |
||
53963 | 595 |
lemma fcard_fempty: |
596 |
"fcard {||} = 0" |
|
597 |
by transfer (rule card_empty) |
|
598 |
||
599 |
lemma fcard_finsert_disjoint: |
|
600 |
"x |\<notin>| A \<Longrightarrow> fcard (finsert x A) = Suc (fcard A)" |
|
601 |
by transfer (rule card_insert_disjoint) |
|
602 |
||
603 |
lemma fcard_finsert_if: |
|
604 |
"fcard (finsert x A) = (if x |\<in>| A then fcard A else Suc (fcard A))" |
|
605 |
by transfer (rule card_insert_if) |
|
606 |
||
66265 | 607 |
lemma fcard_0_eq [simp, no_atp]: |
53963 | 608 |
"fcard A = 0 \<longleftrightarrow> A = {||}" |
609 |
by transfer (rule card_0_eq) |
|
610 |
||
611 |
lemma fcard_Suc_fminus1: |
|
612 |
"x |\<in>| A \<Longrightarrow> Suc (fcard (A |-| {|x|})) = fcard A" |
|
613 |
by transfer (rule card_Suc_Diff1) |
|
614 |
||
615 |
lemma fcard_fminus_fsingleton: |
|
616 |
"x |\<in>| A \<Longrightarrow> fcard (A |-| {|x|}) = fcard A - 1" |
|
617 |
by transfer (rule card_Diff_singleton) |
|
618 |
||
619 |
lemma fcard_fminus_fsingleton_if: |
|
620 |
"fcard (A |-| {|x|}) = (if x |\<in>| A then fcard A - 1 else fcard A)" |
|
621 |
by transfer (rule card_Diff_singleton_if) |
|
622 |
||
623 |
lemma fcard_fminus_finsert[simp]: |
|
624 |
assumes "a |\<in>| A" and "a |\<notin>| B" |
|
625 |
shows "fcard (A |-| finsert a B) = fcard (A |-| B) - 1" |
|
626 |
using assms by transfer (rule card_Diff_insert) |
|
627 |
||
628 |
lemma fcard_finsert: "fcard (finsert x A) = Suc (fcard (A |-| {|x|}))" |
|
629 |
by transfer (rule card_insert) |
|
630 |
||
631 |
lemma fcard_finsert_le: "fcard A \<le> fcard (finsert x A)" |
|
632 |
by transfer (rule card_insert_le) |
|
633 |
||
634 |
lemma fcard_mono: |
|
635 |
"A |\<subseteq>| B \<Longrightarrow> fcard A \<le> fcard B" |
|
636 |
by transfer (rule card_mono) |
|
637 |
||
638 |
lemma fcard_seteq: "A |\<subseteq>| B \<Longrightarrow> fcard B \<le> fcard A \<Longrightarrow> A = B" |
|
639 |
by transfer (rule card_seteq) |
|
640 |
||
641 |
lemma pfsubset_fcard_mono: "A |\<subset>| B \<Longrightarrow> fcard A < fcard B" |
|
642 |
by transfer (rule psubset_card_mono) |
|
643 |
||
63331 | 644 |
lemma fcard_funion_finter: |
53963 | 645 |
"fcard A + fcard B = fcard (A |\<union>| B) + fcard (A |\<inter>| B)" |
646 |
by transfer (rule card_Un_Int) |
|
647 |
||
648 |
lemma fcard_funion_disjoint: |
|
649 |
"A |\<inter>| B = {||} \<Longrightarrow> fcard (A |\<union>| B) = fcard A + fcard B" |
|
650 |
by transfer (rule card_Un_disjoint) |
|
651 |
||
652 |
lemma fcard_funion_fsubset: |
|
653 |
"B |\<subseteq>| A \<Longrightarrow> fcard (A |-| B) = fcard A - fcard B" |
|
654 |
by transfer (rule card_Diff_subset) |
|
655 |
||
656 |
lemma diff_fcard_le_fcard_fminus: |
|
657 |
"fcard A - fcard B \<le> fcard(A |-| B)" |
|
658 |
by transfer (rule diff_card_le_card_Diff) |
|
659 |
||
660 |
lemma fcard_fminus1_less: "x |\<in>| A \<Longrightarrow> fcard (A |-| {|x|}) < fcard A" |
|
661 |
by transfer (rule card_Diff1_less) |
|
662 |
||
663 |
lemma fcard_fminus2_less: |
|
664 |
"x |\<in>| A \<Longrightarrow> y |\<in>| A \<Longrightarrow> fcard (A |-| {|x|} |-| {|y|}) < fcard A" |
|
665 |
by transfer (rule card_Diff2_less) |
|
666 |
||
667 |
lemma fcard_fminus1_le: "fcard (A |-| {|x|}) \<le> fcard A" |
|
668 |
by transfer (rule card_Diff1_le) |
|
669 |
||
670 |
lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B" |
|
671 |
by transfer (rule card_psubset) |
|
672 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
673 |
|
61585 | 674 |
subsubsection \<open>\<open>ffold\<close>\<close> |
53963 | 675 |
|
676 |
(* FIXME: improve transferred to handle bounded meta quantification *) |
|
677 |
||
678 |
context comp_fun_commute |
|
679 |
begin |
|
680 |
lemmas ffold_empty[simp] = fold_empty[Transfer.transferred] |
|
681 |
||
682 |
lemma ffold_finsert [simp]: |
|
683 |
assumes "x |\<notin>| A" |
|
684 |
shows "ffold f z (finsert x A) = f x (ffold f z A)" |
|
685 |
using assms by (transfer fixing: f) (rule fold_insert) |
|
686 |
||
687 |
lemma ffold_fun_left_comm: |
|
688 |
"f x (ffold f z A) = ffold f (f x z) A" |
|
689 |
by (transfer fixing: f) (rule fold_fun_left_comm) |
|
690 |
||
691 |
lemma ffold_finsert2: |
|
56646 | 692 |
"x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A" |
53963 | 693 |
by (transfer fixing: f) (rule fold_insert2) |
694 |
||
695 |
lemma ffold_rec: |
|
696 |
assumes "x |\<in>| A" |
|
697 |
shows "ffold f z A = f x (ffold f z (A |-| {|x|}))" |
|
698 |
using assms by (transfer fixing: f) (rule fold_rec) |
|
63331 | 699 |
|
53963 | 700 |
lemma ffold_finsert_fremove: |
701 |
"ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))" |
|
702 |
by (transfer fixing: f) (rule fold_insert_remove) |
|
703 |
end |
|
704 |
||
705 |
lemma ffold_fimage: |
|
706 |
assumes "inj_on g (fset A)" |
|
707 |
shows "ffold f z (g |`| A) = ffold (f \<circ> g) z A" |
|
708 |
using assms by transfer' (rule fold_image) |
|
709 |
||
710 |
lemma ffold_cong: |
|
711 |
assumes "comp_fun_commute f" "comp_fun_commute g" |
|
712 |
"\<And>x. x |\<in>| A \<Longrightarrow> f x = g x" |
|
713 |
and "s = t" and "A = B" |
|
714 |
shows "ffold f s A = ffold g t B" |
|
715 |
using assms by transfer (metis Finite_Set.fold_cong) |
|
716 |
||
717 |
context comp_fun_idem |
|
718 |
begin |
|
719 |
||
720 |
lemma ffold_finsert_idem: |
|
56646 | 721 |
"ffold f z (finsert x A) = f x (ffold f z A)" |
53963 | 722 |
by (transfer fixing: f) (rule fold_insert_idem) |
63331 | 723 |
|
53963 | 724 |
declare ffold_finsert [simp del] ffold_finsert_idem [simp] |
63331 | 725 |
|
53963 | 726 |
lemma ffold_finsert_idem2: |
727 |
"ffold f z (finsert x A) = ffold f (f x z) A" |
|
728 |
by (transfer fixing: f) (rule fold_insert_idem2) |
|
729 |
||
730 |
end |
|
731 |
||
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
732 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
733 |
subsubsection \<open>Group operations\<close> |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
734 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
735 |
locale comm_monoid_fset = comm_monoid |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
736 |
begin |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
737 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
738 |
sublocale set: comm_monoid_set .. |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
739 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
740 |
lift_definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" is set.F . |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
741 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
742 |
lemmas cong[fundef_cong] = set.cong[Transfer.transferred] |
66261 | 743 |
|
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
744 |
lemma strong_cong[cong]: |
66261 | 745 |
assumes "A = B" "\<And>x. x |\<in>| B =simp=> g x = h x" |
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
746 |
shows "F g A = F h B" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
747 |
using assms unfolding simp_implies_def by (auto cong: cong) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
748 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
749 |
end |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
750 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
751 |
context comm_monoid_add begin |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
752 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
753 |
sublocale fsum: comm_monoid_fset plus 0 |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
754 |
defines fsum = fsum.F |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
755 |
rewrites "comm_monoid_set.F plus 0 = sum" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
756 |
proof - |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
757 |
show "comm_monoid_fset op + 0" by standard |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
758 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
759 |
show "comm_monoid_set.F op + 0 = sum" unfolding sum_def .. |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
760 |
qed |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
761 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
762 |
end |
66261 | 763 |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
764 |
|
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
765 |
subsubsection \<open>Semilattice operations\<close> |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
766 |
|
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
767 |
locale semilattice_fset = semilattice |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
768 |
begin |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
769 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
770 |
sublocale set: semilattice_set .. |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
771 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
772 |
lift_definition F :: "'a fset \<Rightarrow> 'a" is set.F . |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
773 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
774 |
lemma eq_fold: "F (finsert x A) = ffold f x A" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
775 |
by transfer (rule set.eq_fold) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
776 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
777 |
lemma singleton [simp]: "F {|x|} = x" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
778 |
by transfer (rule set.singleton) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
779 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
780 |
lemma insert_not_elem: "x |\<notin>| A \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> F (finsert x A) = x \<^bold>* F A" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
781 |
by transfer (rule set.insert_not_elem) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
782 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
783 |
lemma in_idem: "x |\<in>| A \<Longrightarrow> x \<^bold>* F A = F A" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
784 |
by transfer (rule set.in_idem) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
785 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
786 |
lemma insert [simp]: "A \<noteq> {||} \<Longrightarrow> F (finsert x A) = x \<^bold>* F A" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
787 |
by transfer (rule set.insert) |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
788 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
789 |
end |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
790 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
791 |
locale semilattice_order_fset = binary?: semilattice_order + semilattice_fset |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
792 |
begin |
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
793 |
|
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
794 |
end |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
795 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
796 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
797 |
context linorder begin |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
798 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
799 |
sublocale fMin: semilattice_order_fset min less_eq less |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
800 |
defines fMin = fMin.F |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
801 |
rewrites "semilattice_set.F min = Min" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
802 |
proof - |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
803 |
show "semilattice_order_fset min op \<le> op <" by standard |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
804 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
805 |
show "semilattice_set.F min = Min" unfolding Min_def .. |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
806 |
qed |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
807 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
808 |
sublocale fMax: semilattice_order_fset max greater_eq greater |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
809 |
defines fMax = fMax.F |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
810 |
rewrites "semilattice_set.F max = Max" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
811 |
proof - |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
812 |
show "semilattice_order_fset max op \<ge> op >" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
813 |
by standard |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
814 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
815 |
show "semilattice_set.F max = Max" |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
816 |
unfolding Max_def .. |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
817 |
qed |
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
818 |
|
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
819 |
end |
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
820 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
821 |
lemma mono_fMax_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMax A) = fMax (f |`| A)" |
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
822 |
by transfer (rule mono_Max_commute) |
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
823 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
824 |
lemma mono_fMin_commute: "mono f \<Longrightarrow> A \<noteq> {||} \<Longrightarrow> f (fMin A) = fMin (f |`| A)" |
66292
9930f4cf6c7a
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
Lars Hupel <lars.hupel@mytum.de>
parents:
66265
diff
changeset
|
825 |
by transfer (rule mono_Min_commute) |
66264
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
826 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
827 |
lemma fMax_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMax A |\<in>| A" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
828 |
by transfer (rule Max_in) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
829 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
830 |
lemma fMin_in[simp]: "A \<noteq> {||} \<Longrightarrow> fMin A |\<in>| A" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
831 |
by transfer (rule Min_in) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
832 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
833 |
lemma fMax_ge[simp]: "x |\<in>| A \<Longrightarrow> x \<le> fMax A" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
834 |
by transfer (rule Max_ge) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
835 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
836 |
lemma fMin_le[simp]: "x |\<in>| A \<Longrightarrow> fMin A \<le> x" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
837 |
by transfer (rule Min_le) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
838 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
839 |
lemma fMax_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> y \<le> x) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMax A = x" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
840 |
by transfer (rule Max_eqI) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
841 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
842 |
lemma fMin_eqI: "(\<And>y. y |\<in>| A \<Longrightarrow> x \<le> y) \<Longrightarrow> x |\<in>| A \<Longrightarrow> fMin A = x" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
843 |
by transfer (rule Min_eqI) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
844 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
845 |
lemma fMax_finsert[simp]: "fMax (finsert x A) = (if A = {||} then x else max x (fMax A))" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
846 |
by transfer simp |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
847 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
848 |
lemma fMin_finsert[simp]: "fMin (finsert x A) = (if A = {||} then x else min x (fMin A))" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
849 |
by transfer simp |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
850 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
851 |
context linorder begin |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
852 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
853 |
lemma fset_linorder_max_induct[case_names fempty finsert]: |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
854 |
assumes "P {||}" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
855 |
and "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y < x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
856 |
shows "P S" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
857 |
proof - |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
858 |
(* FIXME transfer and right_total vs. bi_total *) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
859 |
note Domainp_forall_transfer[transfer_rule] |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
860 |
show ?thesis |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
861 |
using assms by (transfer fixing: less) (auto intro: finite_linorder_max_induct) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
862 |
qed |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
863 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
864 |
lemma fset_linorder_min_induct[case_names fempty finsert]: |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
865 |
assumes "P {||}" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
866 |
and "\<And>x S. \<lbrakk>\<forall>y. y |\<in>| S \<longrightarrow> y > x; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
867 |
shows "P S" |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
868 |
proof - |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
869 |
(* FIXME transfer and right_total vs. bi_total *) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
870 |
note Domainp_forall_transfer[transfer_rule] |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
871 |
show ?thesis |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
872 |
using assms by (transfer fixing: less) (auto intro: finite_linorder_min_induct) |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
873 |
qed |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
874 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
875 |
end |
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
876 |
|
d516da3e7c42
material from $AFP/Formula_Derivatives/FSet_More
Lars Hupel <lars.hupel@mytum.de>
parents:
66262
diff
changeset
|
877 |
|
60500 | 878 |
subsection \<open>Choice in fsets\<close> |
53953 | 879 |
|
63331 | 880 |
lemma fset_choice: |
53953 | 881 |
assumes "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)" |
882 |
shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)" |
|
883 |
using assms by transfer metis |
|
884 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
885 |
|
60500 | 886 |
subsection \<open>Induction and Cases rules for fsets\<close> |
53953 | 887 |
|
888 |
lemma fset_exhaust [case_names empty insert, cases type: fset]: |
|
63331 | 889 |
assumes fempty_case: "S = {||} \<Longrightarrow> P" |
53953 | 890 |
and finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P" |
891 |
shows "P" |
|
892 |
using assms by transfer blast |
|
893 |
||
894 |
lemma fset_induct [case_names empty insert]: |
|
895 |
assumes fempty_case: "P {||}" |
|
896 |
and finsert_case: "\<And>x S. P S \<Longrightarrow> P (finsert x S)" |
|
897 |
shows "P S" |
|
898 |
proof - |
|
899 |
(* FIXME transfer and right_total vs. bi_total *) |
|
900 |
note Domainp_forall_transfer[transfer_rule] |
|
901 |
show ?thesis |
|
902 |
using assms by transfer (auto intro: finite_induct) |
|
903 |
qed |
|
904 |
||
905 |
lemma fset_induct_stronger [case_names empty insert, induct type: fset]: |
|
906 |
assumes empty_fset_case: "P {||}" |
|
907 |
and insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
|
908 |
shows "P S" |
|
909 |
proof - |
|
910 |
(* FIXME transfer and right_total vs. bi_total *) |
|
911 |
note Domainp_forall_transfer[transfer_rule] |
|
912 |
show ?thesis |
|
913 |
using assms by transfer (auto intro: finite_induct) |
|
914 |
qed |
|
915 |
||
916 |
lemma fset_card_induct: |
|
917 |
assumes empty_fset_case: "P {||}" |
|
918 |
and card_fset_Suc_case: "\<And>S T. Suc (fcard S) = (fcard T) \<Longrightarrow> P S \<Longrightarrow> P T" |
|
919 |
shows "P S" |
|
920 |
proof (induct S) |
|
921 |
case empty |
|
922 |
show "P {||}" by (rule empty_fset_case) |
|
923 |
next |
|
924 |
case (insert x S) |
|
925 |
have h: "P S" by fact |
|
926 |
have "x |\<notin>| S" by fact |
|
63331 | 927 |
then have "Suc (fcard S) = fcard (finsert x S)" |
53953 | 928 |
by transfer auto |
63331 | 929 |
then show "P (finsert x S)" |
53953 | 930 |
using h card_fset_Suc_case by simp |
931 |
qed |
|
932 |
||
933 |
lemma fset_strong_cases: |
|
934 |
obtains "xs = {||}" |
|
935 |
| ys x where "x |\<notin>| ys" and "xs = finsert x ys" |
|
936 |
by transfer blast |
|
937 |
||
938 |
lemma fset_induct2: |
|
939 |
"P {||} {||} \<Longrightarrow> |
|
940 |
(\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> |
|
941 |
(\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow> |
|
942 |
(\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow> |
|
943 |
P xsa ysa" |
|
944 |
apply (induct xsa arbitrary: ysa) |
|
945 |
apply (induct_tac x rule: fset_induct_stronger) |
|
946 |
apply simp_all |
|
947 |
apply (induct_tac xa rule: fset_induct_stronger) |
|
948 |
apply simp_all |
|
949 |
done |
|
950 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
951 |
|
60500 | 952 |
subsection \<open>Setup for Lifting/Transfer\<close> |
53953 | 953 |
|
60500 | 954 |
subsubsection \<open>Relator and predicator properties\<close> |
53953 | 955 |
|
55938 | 956 |
lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set |
957 |
parametric rel_set_transfer . |
|
53953 | 958 |
|
63331 | 959 |
lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) |
53953 | 960 |
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))" |
961 |
apply (rule ext)+ |
|
962 |
apply transfer' |
|
63331 | 963 |
apply (subst rel_set_def[unfolded fun_eq_iff]) |
53953 | 964 |
by blast |
965 |
||
55938 | 966 |
lemma finite_rel_set: |
53953 | 967 |
assumes fin: "finite X" "finite Z" |
55938 | 968 |
assumes R_S: "rel_set (R OO S) X Z" |
969 |
shows "\<exists>Y. finite Y \<and> rel_set R X Y \<and> rel_set S Y Z" |
|
53953 | 970 |
proof - |
971 |
obtain f where f: "\<forall>x\<in>X. R x (f x) \<and> (\<exists>z\<in>Z. S (f x) z)" |
|
972 |
apply atomize_elim |
|
973 |
apply (subst bchoice_iff[symmetric]) |
|
55938 | 974 |
using R_S[unfolded rel_set_def OO_def] by blast |
63331 | 975 |
|
56646 | 976 |
obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))" |
53953 | 977 |
apply atomize_elim |
978 |
apply (subst bchoice_iff[symmetric]) |
|
55938 | 979 |
using R_S[unfolded rel_set_def OO_def] by blast |
63331 | 980 |
|
53953 | 981 |
let ?Y = "f ` X \<union> g ` Z" |
982 |
have "finite ?Y" by (simp add: fin) |
|
55938 | 983 |
moreover have "rel_set R X ?Y" |
984 |
unfolding rel_set_def |
|
53953 | 985 |
using f g by clarsimp blast |
55938 | 986 |
moreover have "rel_set S ?Y Z" |
987 |
unfolding rel_set_def |
|
53953 | 988 |
using f g by clarsimp blast |
989 |
ultimately show ?thesis by metis |
|
990 |
qed |
|
991 |
||
60500 | 992 |
subsubsection \<open>Transfer rules for the Transfer package\<close> |
53953 | 993 |
|
60500 | 994 |
text \<open>Unconditional transfer rules\<close> |
53953 | 995 |
|
63343 | 996 |
context includes lifting_syntax |
53963 | 997 |
begin |
998 |
||
53953 | 999 |
lemmas fempty_transfer [transfer_rule] = empty_transfer[Transfer.transferred] |
1000 |
||
1001 |
lemma finsert_transfer [transfer_rule]: |
|
55933 | 1002 |
"(A ===> rel_fset A ===> rel_fset A) finsert finsert" |
55945 | 1003 |
unfolding rel_fun_def rel_fset_alt_def by blast |
53953 | 1004 |
|
1005 |
lemma funion_transfer [transfer_rule]: |
|
55933 | 1006 |
"(rel_fset A ===> rel_fset A ===> rel_fset A) funion funion" |
55945 | 1007 |
unfolding rel_fun_def rel_fset_alt_def by blast |
53953 | 1008 |
|
1009 |
lemma ffUnion_transfer [transfer_rule]: |
|
55933 | 1010 |
"(rel_fset (rel_fset A) ===> rel_fset A) ffUnion ffUnion" |
55945 | 1011 |
unfolding rel_fun_def rel_fset_alt_def by transfer (simp, fast) |
53953 | 1012 |
|
1013 |
lemma fimage_transfer [transfer_rule]: |
|
55933 | 1014 |
"((A ===> B) ===> rel_fset A ===> rel_fset B) fimage fimage" |
55945 | 1015 |
unfolding rel_fun_def rel_fset_alt_def by simp blast |
53953 | 1016 |
|
1017 |
lemma fBall_transfer [transfer_rule]: |
|
55933 | 1018 |
"(rel_fset A ===> (A ===> op =) ===> op =) fBall fBall" |
55945 | 1019 |
unfolding rel_fset_alt_def rel_fun_def by blast |
53953 | 1020 |
|
1021 |
lemma fBex_transfer [transfer_rule]: |
|
55933 | 1022 |
"(rel_fset A ===> (A ===> op =) ===> op =) fBex fBex" |
55945 | 1023 |
unfolding rel_fset_alt_def rel_fun_def by blast |
53953 | 1024 |
|
1025 |
(* FIXME transfer doesn't work here *) |
|
1026 |
lemma fPow_transfer [transfer_rule]: |
|
55933 | 1027 |
"(rel_fset A ===> rel_fset (rel_fset A)) fPow fPow" |
55945 | 1028 |
unfolding rel_fun_def |
1029 |
using Pow_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] |
|
53953 | 1030 |
by blast |
1031 |
||
55933 | 1032 |
lemma rel_fset_transfer [transfer_rule]: |
1033 |
"((A ===> B ===> op =) ===> rel_fset A ===> rel_fset B ===> op =) |
|
1034 |
rel_fset rel_fset" |
|
55945 | 1035 |
unfolding rel_fun_def |
1036 |
using rel_set_transfer[unfolded rel_fun_def,rule_format, Transfer.transferred, where A = A and B = B] |
|
53953 | 1037 |
by simp |
1038 |
||
1039 |
lemma bind_transfer [transfer_rule]: |
|
55933 | 1040 |
"(rel_fset A ===> (A ===> rel_fset B) ===> rel_fset B) fbind fbind" |
63092 | 1041 |
unfolding rel_fun_def |
55945 | 1042 |
using bind_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
53953 | 1043 |
|
60500 | 1044 |
text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close> |
53953 | 1045 |
|
1046 |
lemma fmember_transfer [transfer_rule]: |
|
1047 |
assumes "bi_unique A" |
|
55933 | 1048 |
shows "(A ===> rel_fset A ===> op =) (op |\<in>|) (op |\<in>|)" |
55945 | 1049 |
using assms unfolding rel_fun_def rel_fset_alt_def bi_unique_def by metis |
53953 | 1050 |
|
1051 |
lemma finter_transfer [transfer_rule]: |
|
1052 |
assumes "bi_unique A" |
|
55933 | 1053 |
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) finter finter" |
55945 | 1054 |
using assms unfolding rel_fun_def |
1055 |
using inter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
|
53953 | 1056 |
|
53963 | 1057 |
lemma fminus_transfer [transfer_rule]: |
53953 | 1058 |
assumes "bi_unique A" |
55933 | 1059 |
shows "(rel_fset A ===> rel_fset A ===> rel_fset A) (op |-|) (op |-|)" |
55945 | 1060 |
using assms unfolding rel_fun_def |
1061 |
using Diff_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
|
53953 | 1062 |
|
1063 |
lemma fsubset_transfer [transfer_rule]: |
|
1064 |
assumes "bi_unique A" |
|
55933 | 1065 |
shows "(rel_fset A ===> rel_fset A ===> op =) (op |\<subseteq>|) (op |\<subseteq>|)" |
55945 | 1066 |
using assms unfolding rel_fun_def |
1067 |
using subset_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
|
53953 | 1068 |
|
1069 |
lemma fSup_transfer [transfer_rule]: |
|
55938 | 1070 |
"bi_unique A \<Longrightarrow> (rel_set (rel_fset A) ===> rel_fset A) Sup Sup" |
63092 | 1071 |
unfolding rel_fun_def |
53953 | 1072 |
apply clarify |
1073 |
apply transfer' |
|
55945 | 1074 |
using Sup_fset_transfer[unfolded rel_fun_def] by blast |
53953 | 1075 |
|
1076 |
(* FIXME: add right_total_fInf_transfer *) |
|
1077 |
||
1078 |
lemma fInf_transfer [transfer_rule]: |
|
1079 |
assumes "bi_unique A" and "bi_total A" |
|
55938 | 1080 |
shows "(rel_set (rel_fset A) ===> rel_fset A) Inf Inf" |
55945 | 1081 |
using assms unfolding rel_fun_def |
53953 | 1082 |
apply clarify |
1083 |
apply transfer' |
|
55945 | 1084 |
using Inf_fset_transfer[unfolded rel_fun_def] by blast |
53953 | 1085 |
|
1086 |
lemma ffilter_transfer [transfer_rule]: |
|
1087 |
assumes "bi_unique A" |
|
55933 | 1088 |
shows "((A ===> op=) ===> rel_fset A ===> rel_fset A) ffilter ffilter" |
55945 | 1089 |
using assms unfolding rel_fun_def |
1090 |
using Lifting_Set.filter_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
|
53953 | 1091 |
|
1092 |
lemma card_transfer [transfer_rule]: |
|
55933 | 1093 |
"bi_unique A \<Longrightarrow> (rel_fset A ===> op =) fcard fcard" |
63092 | 1094 |
unfolding rel_fun_def |
55945 | 1095 |
using card_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred] by blast |
53953 | 1096 |
|
1097 |
end |
|
1098 |
||
1099 |
lifting_update fset.lifting |
|
1100 |
lifting_forget fset.lifting |
|
1101 |
||
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1102 |
|
60500 | 1103 |
subsection \<open>BNF setup\<close> |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1104 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1105 |
context |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1106 |
includes fset.lifting |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1107 |
begin |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1108 |
|
55933 | 1109 |
lemma rel_fset_alt: |
1110 |
"rel_fset R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)" |
|
55938 | 1111 |
by transfer (simp add: rel_set_def) |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1112 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1113 |
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A" |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1114 |
apply (rule f_the_inv_into_f[unfolded inj_on_def]) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1115 |
apply (simp add: fset_inject) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1116 |
apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+ |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1117 |
. |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1118 |
|
55933 | 1119 |
lemma rel_fset_aux: |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1120 |
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow> |
57398 | 1121 |
((BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO |
1122 |
BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R") |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1123 |
proof |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1124 |
assume ?L |
63040 | 1125 |
define R' where "R' = |
1126 |
the_inv fset (Collect (case_prod R) \<inter> (fset a \<times> fset b))" (is "_ = the_inv fset ?L'") |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1127 |
have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+ |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1128 |
hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1129 |
show ?R unfolding Grp_def relcompp.simps conversep.simps |
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55129
diff
changeset
|
1130 |
proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) |
60500 | 1131 |
from * show "a = fimage fst R'" using conjunct1[OF \<open>?L\<close>] |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1132 |
by (transfer, auto simp add: image_def Int_def split: prod.splits) |
60500 | 1133 |
from * show "b = fimage snd R'" using conjunct2[OF \<open>?L\<close>] |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1134 |
by (transfer, auto simp add: image_def Int_def split: prod.splits) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1135 |
qed (auto simp add: *) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1136 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1137 |
assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1138 |
apply (simp add: subset_eq Ball_def) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1139 |
apply (rule conjI) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1140 |
apply (transfer, clarsimp, metis snd_conv) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1141 |
by (transfer, clarsimp, metis fst_conv) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1142 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1143 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1144 |
bnf "'a fset" |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1145 |
map: fimage |
63331 | 1146 |
sets: fset |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1147 |
bd: natLeq |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1148 |
wits: "{||}" |
55933 | 1149 |
rel: rel_fset |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1150 |
apply - |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1151 |
apply transfer' apply simp |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1152 |
apply transfer' apply force |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1153 |
apply transfer apply force |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1154 |
apply transfer' apply force |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1155 |
apply (rule natLeq_card_order) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1156 |
apply (rule natLeq_cinfinite) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1157 |
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) |
55933 | 1158 |
apply (fastforce simp: rel_fset_alt) |
62324 | 1159 |
apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt |
63331 | 1160 |
rel_fset_aux[unfolded OO_Grp_alt]) |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1161 |
apply transfer apply simp |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1162 |
done |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1163 |
|
55938 | 1164 |
lemma rel_fset_fset: "rel_set \<chi> (fset A1) (fset A2) = rel_fset \<chi> A1 A2" |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1165 |
by transfer (rule refl) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1166 |
|
53953 | 1167 |
end |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1168 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1169 |
lemmas [simp] = fset.map_comp fset.map_id fset.set_map |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1170 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1171 |
|
60500 | 1172 |
subsection \<open>Size setup\<close> |
56646 | 1173 |
|
1174 |
context includes fset.lifting begin |
|
64267 | 1175 |
lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" . |
56646 | 1176 |
end |
1177 |
||
1178 |
instantiation fset :: (type) size begin |
|
1179 |
definition size_fset where |
|
1180 |
size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)" |
|
1181 |
instance .. |
|
1182 |
end |
|
1183 |
||
1184 |
lemmas size_fset_simps[simp] = |
|
1185 |
size_fset_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong, |
|
1186 |
unfolded map_fun_def comp_def id_apply] |
|
1187 |
||
1188 |
lemmas size_fset_overloaded_simps[simp] = |
|
1189 |
size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right, |
|
1190 |
folded size_fset_overloaded_def] |
|
1191 |
||
1192 |
lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)" |
|
60228
32dd7adba5a4
tuned proof; forget the transfer rule for size_fset
kuncar
parents:
58881
diff
changeset
|
1193 |
apply (subst fun_eq_iff) |
64267 | 1194 |
including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on) |
63331 | 1195 |
|
60500 | 1196 |
setup \<open> |
56651 | 1197 |
BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} |
62082 | 1198 |
@{thm size_fset_overloaded_def} @{thms size_fset_simps size_fset_overloaded_simps} |
1199 |
@{thms fset_size_o_map} |
|
60500 | 1200 |
\<close> |
56646 | 1201 |
|
60228
32dd7adba5a4
tuned proof; forget the transfer rule for size_fset
kuncar
parents:
58881
diff
changeset
|
1202 |
lifting_update fset.lifting |
32dd7adba5a4
tuned proof; forget the transfer rule for size_fset
kuncar
parents:
58881
diff
changeset
|
1203 |
lifting_forget fset.lifting |
56646 | 1204 |
|
60500 | 1205 |
subsection \<open>Advanced relator customization\<close> |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1206 |
|
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1207 |
(* Set vs. sum relators: *) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1208 |
|
63331 | 1209 |
lemma rel_set_rel_sum[simp]: |
1210 |
"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow> |
|
55938 | 1211 |
rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)" |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1212 |
(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr") |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1213 |
proof safe |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1214 |
assume L: "?L" |
55938 | 1215 |
show ?Rl unfolding rel_set_def Bex_def vimage_eq proof safe |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1216 |
fix l1 assume "Inl l1 \<in> A1" |
55943 | 1217 |
then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inl l1) a2" |
55938 | 1218 |
using L unfolding rel_set_def by auto |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1219 |
then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1220 |
thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1221 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1222 |
fix l2 assume "Inl l2 \<in> A2" |
55943 | 1223 |
then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inl l2)" |
55938 | 1224 |
using L unfolding rel_set_def by auto |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1225 |
then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1226 |
thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1227 |
qed |
55938 | 1228 |
show ?Rr unfolding rel_set_def Bex_def vimage_eq proof safe |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1229 |
fix r1 assume "Inr r1 \<in> A1" |
55943 | 1230 |
then obtain a2 where a2: "a2 \<in> A2" and "rel_sum \<chi> \<phi> (Inr r1) a2" |
55938 | 1231 |
using L unfolding rel_set_def by auto |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1232 |
then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1233 |
thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1234 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1235 |
fix r2 assume "Inr r2 \<in> A2" |
55943 | 1236 |
then obtain a1 where a1: "a1 \<in> A1" and "rel_sum \<chi> \<phi> a1 (Inr r2)" |
55938 | 1237 |
using L unfolding rel_set_def by auto |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1238 |
then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1239 |
thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1240 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1241 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1242 |
assume Rl: "?Rl" and Rr: "?Rr" |
55938 | 1243 |
show ?L unfolding rel_set_def Bex_def vimage_eq proof safe |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1244 |
fix a1 assume a1: "a1 \<in> A1" |
55943 | 1245 |
show "\<exists> a2. a2 \<in> A2 \<and> rel_sum \<chi> \<phi> a1 a2" |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1246 |
proof(cases a1) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1247 |
case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2" |
55938 | 1248 |
using Rl a1 unfolding rel_set_def by blast |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1249 |
thus ?thesis unfolding Inl by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1250 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1251 |
case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2" |
55938 | 1252 |
using Rr a1 unfolding rel_set_def by blast |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1253 |
thus ?thesis unfolding Inr by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1254 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1255 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1256 |
fix a2 assume a2: "a2 \<in> A2" |
55943 | 1257 |
show "\<exists> a1. a1 \<in> A1 \<and> rel_sum \<chi> \<phi> a1 a2" |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1258 |
proof(cases a2) |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1259 |
case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2" |
55938 | 1260 |
using Rl a2 unfolding rel_set_def by blast |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1261 |
thus ?thesis unfolding Inl by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1262 |
next |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1263 |
case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2" |
55938 | 1264 |
using Rr a2 unfolding rel_set_def by blast |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1265 |
thus ?thesis unfolding Inr by auto |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1266 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1267 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1268 |
qed |
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1269 |
|
60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1270 |
|
66262
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1271 |
subsubsection \<open>Countability\<close> |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1272 |
|
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1273 |
lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1274 |
including fset.lifting |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1275 |
by transfer (rule finite_list) |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1276 |
|
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1277 |
lemma fset_of_list_surj[simp, intro]: "surj fset_of_list" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1278 |
proof - |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1279 |
have "x \<in> range fset_of_list" for x :: "'a fset" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1280 |
unfolding image_iff |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1281 |
using exists_fset_of_list by fastforce |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1282 |
thus ?thesis by auto |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1283 |
qed |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1284 |
|
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1285 |
instance fset :: (countable) countable |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1286 |
proof |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1287 |
obtain to_nat :: "'a list \<Rightarrow> nat" where "inj to_nat" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1288 |
by (metis ex_inj) |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1289 |
moreover have "inj (inv fset_of_list)" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1290 |
using fset_of_list_surj by (rule surj_imp_inj_inv) |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1291 |
ultimately have "inj (to_nat \<circ> inv fset_of_list)" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1292 |
by (rule inj_comp) |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1293 |
thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat" |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1294 |
by auto |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1295 |
qed |
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1296 |
|
4a2c9d32e7aa
finite sets are countable
Lars Hupel <lars.hupel@mytum.de>
parents:
66261
diff
changeset
|
1297 |
|
60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1298 |
subsection \<open>Quickcheck setup\<close> |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1299 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1300 |
text \<open>Setup adapted from sets.\<close> |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1301 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1302 |
notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1303 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1304 |
definition (in term_syntax) [code_unfold]: |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1305 |
"valterm_femptyset = Code_Evaluation.valtermify ({||} :: ('a :: typerep) fset)" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1306 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1307 |
definition (in term_syntax) [code_unfold]: |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1308 |
"valtermify_finsert x s = Code_Evaluation.valtermify finsert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1309 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1310 |
instantiation fset :: (exhaustive) exhaustive |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1311 |
begin |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1312 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1313 |
fun exhaustive_fset where |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1314 |
"exhaustive_fset f i = (if i = 0 then None else (f {||} orelse exhaustive_fset (\<lambda>A. f A orelse Quickcheck_Exhaustive.exhaustive (\<lambda>x. if x |\<in>| A then None else f (finsert x A)) (i - 1)) (i - 1)))" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1315 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1316 |
instance .. |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1317 |
|
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54258
diff
changeset
|
1318 |
end |
60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1319 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1320 |
instantiation fset :: (full_exhaustive) full_exhaustive |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1321 |
begin |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1322 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1323 |
fun full_exhaustive_fset where |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1324 |
"full_exhaustive_fset f i = (if i = 0 then None else (f valterm_femptyset orelse full_exhaustive_fset (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive (\<lambda>x. if fst x |\<in>| fst A then None else f (valtermify_finsert x A)) (i - 1)) (i - 1)))" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1325 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1326 |
instance .. |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1327 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1328 |
end |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1329 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1330 |
no_notation Quickcheck_Exhaustive.orelse (infixr "orelse" 55) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1331 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1332 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1333 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1334 |
instantiation fset :: (random) random |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1335 |
begin |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1336 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1337 |
fun random_aux_fset :: "natural \<Rightarrow> natural \<Rightarrow> natural \<times> natural \<Rightarrow> ('a fset \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural" where |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1338 |
"random_aux_fset 0 j = Quickcheck_Random.collapse (Random.select_weight [(1, Pair valterm_femptyset)])" | |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1339 |
"random_aux_fset (Code_Numeral.Suc i) j = |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1340 |
Quickcheck_Random.collapse (Random.select_weight |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1341 |
[(1, Pair valterm_femptyset), |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1342 |
(Code_Numeral.Suc i, |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1343 |
Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>x. random_aux_fset i j \<circ>\<rightarrow> (\<lambda>s. Pair (valtermify_finsert x s))))])" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1344 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1345 |
lemma [code]: |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1346 |
"random_aux_fset i j = |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1347 |
Quickcheck_Random.collapse (Random.select_weight [(1, Pair valterm_femptyset), |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1348 |
(i, Quickcheck_Random.random j \<circ>\<rightarrow> (\<lambda>x. random_aux_fset (i - 1) j \<circ>\<rightarrow> (\<lambda>s. Pair (valtermify_finsert x s))))])" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1349 |
proof (induct i rule: natural.induct) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1350 |
case zero |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1351 |
show ?case by (subst select_weight_drop_zero[symmetric]) (simp add: less_natural_def) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1352 |
next |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1353 |
case (Suc i) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1354 |
show ?case by (simp only: random_aux_fset.simps Suc_natural_minus_one) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1355 |
qed |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1356 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1357 |
definition "random_fset i = random_aux_fset i i" |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1358 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1359 |
instance .. |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1360 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1361 |
end |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1362 |
|
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1363 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60679
diff
changeset
|
1364 |
|
66261 | 1365 |
end |