13505
|
1 |
(* Title: ZF/Constructible/Reflection.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
*)
|
|
5 |
|
13223
|
6 |
header {* The Reflection Theorem*}
|
|
7 |
|
|
8 |
theory Reflection = Normal:
|
|
9 |
|
|
10 |
lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
|
|
11 |
by blast
|
|
12 |
|
|
13 |
lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) <-> (~ (\<exists>x\<in>A. ~ P(x)))";
|
|
14 |
by blast
|
|
15 |
|
|
16 |
text{*From the notes of A. S. Kechris, page 6, and from
|
|
17 |
Andrzej Mostowski, \emph{Constructible Sets with Applications},
|
|
18 |
North-Holland, 1969, page 23.*}
|
|
19 |
|
|
20 |
|
|
21 |
subsection{*Basic Definitions*}
|
|
22 |
|
|
23 |
text{*First part: the cumulative hierarchy defining the class @{text M}.
|
|
24 |
To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
|
|
25 |
closed under ordered pairing provided @{text l} is limit. Possibly this
|
|
26 |
could be avoided: the induction hypothesis @{term Cl_reflects}
|
|
27 |
(in locale @{text ex_reflection}) could be weakened to
|
|
28 |
@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
|
|
29 |
uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since
|
|
30 |
ultimately the @{text ex_reflection} proof is packaged up using the
|
|
31 |
predicate @{text Reflects}.
|
|
32 |
*}
|
13428
|
33 |
locale reflection =
|
13223
|
34 |
fixes Mset and M and Reflects
|
|
35 |
assumes Mset_mono_le : "mono_le_subset(Mset)"
|
|
36 |
and Mset_cont : "cont_Ord(Mset)"
|
|
37 |
and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |]
|
|
38 |
==> <x,y> \<in> Mset(a)"
|
13563
|
39 |
defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)"
|
|
40 |
and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
|
13223
|
41 |
(\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
|
|
42 |
fixes F0 --{*ordinal for a specific value @{term y}*}
|
|
43 |
fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
|
|
44 |
fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
|
13563
|
45 |
defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) & P(<y,z>)) -->
|
13223
|
46 |
(\<exists>z\<in>Mset(b). P(<y,z>))"
|
|
47 |
and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
|
13563
|
48 |
and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a"
|
13223
|
49 |
|
|
50 |
lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
|
|
51 |
apply (insert Mset_mono_le)
|
|
52 |
apply (simp add: mono_le_subset_def leI)
|
|
53 |
done
|
|
54 |
|
13434
|
55 |
text{*Awkward: we need a version of @{text ClEx_def} as an equality
|
|
56 |
at the level of classes, which do not really exist*}
|
|
57 |
lemma (in reflection) ClEx_eq:
|
13563
|
58 |
"ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a"
|
13434
|
59 |
by (simp add: ClEx_def [symmetric])
|
|
60 |
|
|
61 |
|
13223
|
62 |
subsection{*Easy Cases of the Reflection Theorem*}
|
|
63 |
|
|
64 |
theorem (in reflection) Triv_reflection [intro]:
|
|
65 |
"Reflects(Ord, P, \<lambda>a x. P(x))"
|
|
66 |
by (simp add: Reflects_def)
|
|
67 |
|
|
68 |
theorem (in reflection) Not_reflection [intro]:
|
|
69 |
"Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
|
13268
|
70 |
by (simp add: Reflects_def)
|
13223
|
71 |
|
|
72 |
theorem (in reflection) And_reflection [intro]:
|
|
73 |
"[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
|
13563
|
74 |
==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) & P'(x),
|
|
75 |
\<lambda>a x. Q(a,x) & Q'(a,x))"
|
13223
|
76 |
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
|
|
77 |
|
|
78 |
theorem (in reflection) Or_reflection [intro]:
|
|
79 |
"[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
|
13563
|
80 |
==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) | P'(x),
|
|
81 |
\<lambda>a x. Q(a,x) | Q'(a,x))"
|
13223
|
82 |
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
|
|
83 |
|
|
84 |
theorem (in reflection) Imp_reflection [intro]:
|
|
85 |
"[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
|
13563
|
86 |
==> Reflects(\<lambda>a. Cl(a) & C'(a),
|
13223
|
87 |
\<lambda>x. P(x) --> P'(x),
|
|
88 |
\<lambda>a x. Q(a,x) --> Q'(a,x))"
|
|
89 |
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
|
|
90 |
|
|
91 |
theorem (in reflection) Iff_reflection [intro]:
|
|
92 |
"[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
|
13563
|
93 |
==> Reflects(\<lambda>a. Cl(a) & C'(a),
|
13223
|
94 |
\<lambda>x. P(x) <-> P'(x),
|
|
95 |
\<lambda>a x. Q(a,x) <-> Q'(a,x))"
|
|
96 |
by (simp add: Reflects_def Closed_Unbounded_Int, blast)
|
|
97 |
|
|
98 |
subsection{*Reflection for Existential Quantifiers*}
|
|
99 |
|
|
100 |
lemma (in reflection) F0_works:
|
|
101 |
"[| y\<in>Mset(a); Ord(a); M(z); P(<y,z>) |] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
|
|
102 |
apply (unfold F0_def M_def, clarify)
|
|
103 |
apply (rule LeastI2)
|
|
104 |
apply (blast intro: Mset_mono [THEN subsetD])
|
|
105 |
apply (blast intro: lt_Ord2, blast)
|
|
106 |
done
|
|
107 |
|
|
108 |
lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))"
|
|
109 |
by (simp add: F0_def)
|
|
110 |
|
|
111 |
lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))"
|
|
112 |
by (simp add: FF_def)
|
|
113 |
|
|
114 |
lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
|
|
115 |
apply (insert Mset_cont)
|
|
116 |
apply (simp add: cont_Ord_def FF_def, blast)
|
|
117 |
done
|
|
118 |
|
|
119 |
text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"},
|
|
120 |
while @{term FF} depends only upon @{term a}. *}
|
|
121 |
lemma (in reflection) FF_works:
|
|
122 |
"[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
|
|
123 |
apply (simp add: FF_def)
|
|
124 |
apply (simp_all add: cont_Ord_Union [of concl: Mset]
|
|
125 |
Mset_cont Mset_mono_le not_emptyI Ord_F0)
|
|
126 |
apply (blast intro: F0_works)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma (in reflection) FFN_works:
|
|
130 |
"[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |]
|
|
131 |
==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
|
|
132 |
apply (drule FF_works [of concl: P], assumption+)
|
|
133 |
apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
|
|
134 |
done
|
|
135 |
|
|
136 |
|
|
137 |
text{*Locale for the induction hypothesis*}
|
|
138 |
|
13428
|
139 |
locale ex_reflection = reflection +
|
13223
|
140 |
fixes P --"the original formula"
|
|
141 |
fixes Q --"the reflected formula"
|
|
142 |
fixes Cl --"the class of reflecting ordinals"
|
|
143 |
assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
|
|
144 |
|
|
145 |
lemma (in ex_reflection) ClEx_downward:
|
|
146 |
"[| M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |]
|
|
147 |
==> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
|
|
148 |
apply (simp add: ClEx_def, clarify)
|
|
149 |
apply (frule Limit_is_Ord)
|
|
150 |
apply (frule FFN_works [of concl: P], assumption+)
|
|
151 |
apply (drule Cl_reflects, assumption+)
|
|
152 |
apply (auto simp add: Limit_is_Ord Pair_in_Mset)
|
|
153 |
done
|
|
154 |
|
|
155 |
lemma (in ex_reflection) ClEx_upward:
|
|
156 |
"[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |]
|
13563
|
157 |
==> \<exists>z. M(z) & P(<y,z>)"
|
13223
|
158 |
apply (simp add: ClEx_def M_def)
|
|
159 |
apply (blast dest: Cl_reflects
|
|
160 |
intro: Limit_is_Ord Pair_in_Mset)
|
|
161 |
done
|
|
162 |
|
|
163 |
text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
|
|
164 |
lemma (in ex_reflection) ZF_ClEx_iff:
|
|
165 |
"[| y\<in>Mset(a); Cl(a); ClEx(P,a) |]
|
13563
|
166 |
==> (\<exists>z. M(z) & P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
|
13223
|
167 |
by (blast intro: dest: ClEx_downward ClEx_upward)
|
|
168 |
|
|
169 |
text{*...and it is closed and unbounded*}
|
|
170 |
lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx:
|
|
171 |
"Closed_Unbounded(ClEx(P))"
|
13434
|
172 |
apply (simp add: ClEx_eq)
|
13223
|
173 |
apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
|
|
174 |
Closed_Unbounded_Limit Normal_normalize)
|
|
175 |
done
|
|
176 |
|
|
177 |
text{*The same two theorems, exported to locale @{text reflection}.*}
|
|
178 |
|
|
179 |
text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
|
|
180 |
lemma (in reflection) ClEx_iff:
|
|
181 |
"[| y\<in>Mset(a); Cl(a); ClEx(P,a);
|
|
182 |
!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |]
|
13563
|
183 |
==> (\<exists>z. M(z) & P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
|
13223
|
184 |
apply (unfold ClEx_def FF_def F0_def M_def)
|
13428
|
185 |
apply (rule ex_reflection.ZF_ClEx_iff
|
|
186 |
[OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
|
|
187 |
of Mset Cl])
|
|
188 |
apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
|
13223
|
189 |
done
|
|
190 |
|
13434
|
191 |
(*Alternative proof, less unfolding:
|
|
192 |
apply (rule Reflection.ZF_ClEx_iff [of Mset _ _ Cl, folded M_def])
|
|
193 |
apply (fold ClEx_def FF_def F0_def)
|
|
194 |
apply (rule ex_reflection.intro, assumption)
|
|
195 |
apply (simp add: ex_reflection_axioms.intro, assumption+)
|
|
196 |
*)
|
|
197 |
|
13223
|
198 |
lemma (in reflection) Closed_Unbounded_ClEx:
|
|
199 |
"(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
|
|
200 |
==> Closed_Unbounded(ClEx(P))"
|
13434
|
201 |
apply (unfold ClEx_eq FF_def F0_def M_def)
|
|
202 |
apply (rule Reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl])
|
|
203 |
apply (rule ex_reflection.intro, assumption)
|
|
204 |
apply (blast intro: ex_reflection_axioms.intro)
|
13223
|
205 |
done
|
|
206 |
|
13292
|
207 |
subsection{*Packaging the Quantifier Reflection Rules*}
|
|
208 |
|
13223
|
209 |
lemma (in reflection) Ex_reflection_0:
|
|
210 |
"Reflects(Cl,P0,Q0)
|
13563
|
211 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(P0,a),
|
|
212 |
\<lambda>x. \<exists>z. M(z) & P0(<x,z>),
|
13223
|
213 |
\<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))"
|
|
214 |
apply (simp add: Reflects_def)
|
|
215 |
apply (intro conjI Closed_Unbounded_Int)
|
|
216 |
apply blast
|
13382
|
217 |
apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify)
|
13223
|
218 |
apply (rule_tac Cl=Cl in ClEx_iff, assumption+, blast)
|
|
219 |
done
|
|
220 |
|
|
221 |
lemma (in reflection) All_reflection_0:
|
|
222 |
"Reflects(Cl,P0,Q0)
|
13563
|
223 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x.~P0(x), a),
|
13223
|
224 |
\<lambda>x. \<forall>z. M(z) --> P0(<x,z>),
|
|
225 |
\<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))"
|
|
226 |
apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not)
|
|
227 |
apply (rule Not_reflection, drule Not_reflection, simp)
|
|
228 |
apply (erule Ex_reflection_0)
|
|
229 |
done
|
|
230 |
|
|
231 |
theorem (in reflection) Ex_reflection [intro]:
|
|
232 |
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
|
13563
|
233 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a),
|
|
234 |
\<lambda>x. \<exists>z. M(z) & P(x,z),
|
13223
|
235 |
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
|
|
236 |
by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))"
|
|
237 |
"\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
|
|
238 |
|
|
239 |
theorem (in reflection) All_reflection [intro]:
|
|
240 |
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
|
13563
|
241 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),
|
13223
|
242 |
\<lambda>x. \<forall>z. M(z) --> P(x,z),
|
|
243 |
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))"
|
|
244 |
by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))"
|
|
245 |
"\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
|
|
246 |
|
13292
|
247 |
text{*And again, this time using class-bounded quantifiers*}
|
|
248 |
|
|
249 |
theorem (in reflection) Rex_reflection [intro]:
|
|
250 |
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
|
13563
|
251 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a),
|
13292
|
252 |
\<lambda>x. \<exists>z[M]. P(x,z),
|
|
253 |
\<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
|
|
254 |
by (unfold rex_def, blast)
|
|
255 |
|
|
256 |
theorem (in reflection) Rall_reflection [intro]:
|
|
257 |
"Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
|
13563
|
258 |
==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),
|
13292
|
259 |
\<lambda>x. \<forall>z[M]. P(x,z),
|
|
260 |
\<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))"
|
|
261 |
by (unfold rall_def, blast)
|
|
262 |
|
|
263 |
|
13223
|
264 |
text{*No point considering bounded quantifiers, where reflection is trivial.*}
|
|
265 |
|
|
266 |
|
|
267 |
subsection{*Simple Examples of Reflection*}
|
|
268 |
|
|
269 |
text{*Example 1: reflecting a simple formula. The reflecting class is first
|
|
270 |
given as the variable @{text ?Cl} and later retrieved from the final
|
|
271 |
proof state.*}
|
|
272 |
lemma (in reflection)
|
|
273 |
"Reflects(?Cl,
|
13563
|
274 |
\<lambda>x. \<exists>y. M(y) & x \<in> y,
|
13223
|
275 |
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
|
|
276 |
by fast
|
|
277 |
|
|
278 |
text{*Problem here: there needs to be a conjunction (class intersection)
|
|
279 |
in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant,
|
|
280 |
though harmless.*}
|
|
281 |
lemma (in reflection)
|
13563
|
282 |
"Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a),
|
|
283 |
\<lambda>x. \<exists>y. M(y) & x \<in> y,
|
13223
|
284 |
\<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
|
|
285 |
by fast
|
|
286 |
|
|
287 |
|
|
288 |
text{*Example 2*}
|
|
289 |
lemma (in reflection)
|
|
290 |
"Reflects(?Cl,
|
13563
|
291 |
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
|
13223
|
292 |
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
|
|
293 |
by fast
|
|
294 |
|
|
295 |
text{*Example 2'. We give the reflecting class explicitly. *}
|
|
296 |
lemma (in reflection)
|
|
297 |
"Reflects
|
13563
|
298 |
(\<lambda>a. (Ord(a) &
|
|
299 |
ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) &
|
13223
|
300 |
ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
|
13563
|
301 |
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
|
13223
|
302 |
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
|
|
303 |
by fast
|
|
304 |
|
|
305 |
text{*Example 2''. We expand the subset relation.*}
|
|
306 |
lemma (in reflection)
|
|
307 |
"Reflects(?Cl,
|
13563
|
308 |
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
|
13223
|
309 |
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
|
|
310 |
by fast
|
|
311 |
|
|
312 |
text{*Example 2'''. Single-step version, to reveal the reflecting class.*}
|
|
313 |
lemma (in reflection)
|
|
314 |
"Reflects(?Cl,
|
13563
|
315 |
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
|
13223
|
316 |
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
|
|
317 |
apply (rule Ex_reflection)
|
|
318 |
txt{*
|
|
319 |
@{goals[display,indent=0,margin=60]}
|
|
320 |
*}
|
|
321 |
apply (rule All_reflection)
|
|
322 |
txt{*
|
|
323 |
@{goals[display,indent=0,margin=60]}
|
|
324 |
*}
|
|
325 |
apply (rule Triv_reflection)
|
|
326 |
txt{*
|
|
327 |
@{goals[display,indent=0,margin=60]}
|
|
328 |
*}
|
|
329 |
done
|
|
330 |
|
|
331 |
text{*Example 3. Warning: the following examples make sense only
|
|
332 |
if @{term P} is quantifier-free, since it is not being relativized.*}
|
|
333 |
lemma (in reflection)
|
|
334 |
"Reflects(?Cl,
|
13563
|
335 |
\<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)),
|
|
336 |
\<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
|
13223
|
337 |
by fast
|
|
338 |
|
|
339 |
text{*Example 3'*}
|
|
340 |
lemma (in reflection)
|
|
341 |
"Reflects(?Cl,
|
13563
|
342 |
\<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
|
13223
|
343 |
\<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
|
|
344 |
by fast
|
|
345 |
|
|
346 |
text{*Example 3''*}
|
|
347 |
lemma (in reflection)
|
|
348 |
"Reflects(?Cl,
|
13563
|
349 |
\<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
|
13223
|
350 |
\<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
|
|
351 |
by fast
|
|
352 |
|
|
353 |
text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
|
|
354 |
to be relativized.*}
|
|
355 |
lemma (in reflection)
|
|
356 |
"Reflects(?Cl,
|
13563
|
357 |
\<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi>X \<in> A. X)),
|
13223
|
358 |
\<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
|
|
359 |
by fast
|
|
360 |
|
|
361 |
end
|
|
362 |
|