1 (* Title: ZF/Constructible/Reflection.thy |
1 (* Title: ZF/Constructible/Reflection.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 section {* The Reflection Theorem*} |
5 section \<open>The Reflection Theorem\<close> |
6 |
6 |
7 theory Reflection imports Normal begin |
7 theory Reflection imports Normal begin |
8 |
8 |
9 lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))" |
9 lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))" |
10 by blast |
10 by blast |
11 |
11 |
12 lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))" |
12 lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))" |
13 by blast |
13 by blast |
14 |
14 |
15 text{*From the notes of A. S. Kechris, page 6, and from |
15 text\<open>From the notes of A. S. Kechris, page 6, and from |
16 Andrzej Mostowski, \emph{Constructible Sets with Applications}, |
16 Andrzej Mostowski, \emph{Constructible Sets with Applications}, |
17 North-Holland, 1969, page 23.*} |
17 North-Holland, 1969, page 23.\<close> |
18 |
18 |
19 |
19 |
20 subsection{*Basic Definitions*} |
20 subsection\<open>Basic Definitions\<close> |
21 |
21 |
22 text{*First part: the cumulative hierarchy defining the class @{text M}. |
22 text\<open>First part: the cumulative hierarchy defining the class @{text M}. |
23 To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is |
23 To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is |
24 closed under ordered pairing provided @{text l} is limit. Possibly this |
24 closed under ordered pairing provided @{text l} is limit. Possibly this |
25 could be avoided: the induction hypothesis @{term Cl_reflects} |
25 could be avoided: the induction hypothesis @{term Cl_reflects} |
26 (in locale @{text ex_reflection}) could be weakened to |
26 (in locale @{text ex_reflection}) could be weakened to |
27 @{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)"}, removing most |
27 @{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)"}, removing most |
28 uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since |
28 uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since |
29 ultimately the @{text ex_reflection} proof is packaged up using the |
29 ultimately the @{text ex_reflection} proof is packaged up using the |
30 predicate @{text Reflects}. |
30 predicate @{text Reflects}. |
31 *} |
31 \<close> |
32 locale reflection = |
32 locale reflection = |
33 fixes Mset and M and Reflects |
33 fixes Mset and M and Reflects |
34 assumes Mset_mono_le : "mono_le_subset(Mset)" |
34 assumes Mset_mono_le : "mono_le_subset(Mset)" |
35 and Mset_cont : "cont_Ord(Mset)" |
35 and Mset_cont : "cont_Ord(Mset)" |
36 and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] |
36 and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] |
37 ==> <x,y> \<in> Mset(a)" |
37 ==> <x,y> \<in> Mset(a)" |
38 defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)" |
38 defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)" |
39 and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) & |
39 and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) & |
40 (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))" |
40 (\<forall>a. Cl(a) \<longrightarrow> (\<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)))" |
41 fixes F0 --{*ordinal for a specific value @{term y}*} |
41 fixes F0 --\<open>ordinal for a specific value @{term y}\<close> |
42 fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*} |
42 fixes FF --\<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close> |
43 fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*} |
43 fixes ClEx --\<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close> |
44 defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) \<longrightarrow> |
44 defines "F0(P,y) == \<mu> b. (\<exists>z. M(z) & P(<y,z>)) \<longrightarrow> |
45 (\<exists>z\<in>Mset(b). P(<y,z>))" |
45 (\<exists>z\<in>Mset(b). P(<y,z>))" |
46 and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)" |
46 and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)" |
47 and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a" |
47 and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a" |
48 |
48 |
49 lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) \<subseteq> Mset(j)" |
49 lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) \<subseteq> Mset(j)" |
50 apply (insert Mset_mono_le) |
50 apply (insert Mset_mono_le) |
51 apply (simp add: mono_le_subset_def leI) |
51 apply (simp add: mono_le_subset_def leI) |
52 done |
52 done |
53 |
53 |
54 text{*Awkward: we need a version of @{text ClEx_def} as an equality |
54 text\<open>Awkward: we need a version of @{text ClEx_def} as an equality |
55 at the level of classes, which do not really exist*} |
55 at the level of classes, which do not really exist\<close> |
56 lemma (in reflection) ClEx_eq: |
56 lemma (in reflection) ClEx_eq: |
57 "ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a" |
57 "ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a" |
58 by (simp add: ClEx_def [symmetric]) |
58 by (simp add: ClEx_def [symmetric]) |
59 |
59 |
60 |
60 |
61 subsection{*Easy Cases of the Reflection Theorem*} |
61 subsection\<open>Easy Cases of the Reflection Theorem\<close> |
62 |
62 |
63 theorem (in reflection) Triv_reflection [intro]: |
63 theorem (in reflection) Triv_reflection [intro]: |
64 "Reflects(Ord, P, \<lambda>a x. P(x))" |
64 "Reflects(Ord, P, \<lambda>a x. P(x))" |
65 by (simp add: Reflects_def) |
65 by (simp add: Reflects_def) |
66 |
66 |
157 apply (simp add: ClEx_def M_def) |
157 apply (simp add: ClEx_def M_def) |
158 apply (blast dest: Cl_reflects |
158 apply (blast dest: Cl_reflects |
159 intro: Limit_is_Ord Pair_in_Mset) |
159 intro: Limit_is_Ord Pair_in_Mset) |
160 done |
160 done |
161 |
161 |
162 text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} |
162 text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close> |
163 lemma (in ex_reflection) ZF_ClEx_iff: |
163 lemma (in ex_reflection) ZF_ClEx_iff: |
164 "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] |
164 "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] |
165 ==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" |
165 ==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" |
166 by (blast intro: dest: ClEx_downward ClEx_upward) |
166 by (blast intro: dest: ClEx_downward ClEx_upward) |
167 |
167 |
168 text{*...and it is closed and unbounded*} |
168 text\<open>...and it is closed and unbounded\<close> |
169 lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx: |
169 lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx: |
170 "Closed_Unbounded(ClEx(P))" |
170 "Closed_Unbounded(ClEx(P))" |
171 apply (simp add: ClEx_eq) |
171 apply (simp add: ClEx_eq) |
172 apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded |
172 apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded |
173 Closed_Unbounded_Limit Normal_normalize) |
173 Closed_Unbounded_Limit Normal_normalize) |
174 done |
174 done |
175 |
175 |
176 text{*The same two theorems, exported to locale @{text reflection}.*} |
176 text\<open>The same two theorems, exported to locale @{text reflection}.\<close> |
177 |
177 |
178 text{*Class @{text ClEx} indeed consists of reflecting ordinals...*} |
178 text\<open>Class @{text ClEx} indeed consists of reflecting ordinals...\<close> |
179 lemma (in reflection) ClEx_iff: |
179 lemma (in reflection) ClEx_iff: |
180 "[| y\<in>Mset(a); Cl(a); ClEx(P,a); |
180 "[| y\<in>Mset(a); Cl(a); ClEx(P,a); |
181 !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x) |] |
181 !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x) |] |
182 ==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" |
182 ==> (\<exists>z. M(z) & P(<y,z>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,<y,z>))" |
183 apply (unfold ClEx_def FF_def F0_def M_def) |
183 apply (unfold ClEx_def FF_def F0_def M_def) |
241 \<lambda>x. \<forall>z. M(z) \<longrightarrow> P(x,z), |
241 \<lambda>x. \<forall>z. M(z) \<longrightarrow> P(x,z), |
242 \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" |
242 \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" |
243 by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" |
243 by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" |
244 "\<lambda>a x. Q(a,fst(x),snd(x))", simplified]) |
244 "\<lambda>a x. Q(a,fst(x),snd(x))", simplified]) |
245 |
245 |
246 text{*And again, this time using class-bounded quantifiers*} |
246 text\<open>And again, this time using class-bounded quantifiers\<close> |
247 |
247 |
248 theorem (in reflection) Rex_reflection [intro]: |
248 theorem (in reflection) Rex_reflection [intro]: |
249 "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) |
249 "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) |
250 ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), |
250 ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), |
251 \<lambda>x. \<exists>z[M]. P(x,z), |
251 \<lambda>x. \<exists>z[M]. P(x,z), |
258 \<lambda>x. \<forall>z[M]. P(x,z), |
258 \<lambda>x. \<forall>z[M]. P(x,z), |
259 \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" |
259 \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" |
260 by (unfold rall_def, blast) |
260 by (unfold rall_def, blast) |
261 |
261 |
262 |
262 |
263 text{*No point considering bounded quantifiers, where reflection is trivial.*} |
263 text\<open>No point considering bounded quantifiers, where reflection is trivial.\<close> |
264 |
264 |
265 |
265 |
266 subsection{*Simple Examples of Reflection*} |
266 subsection\<open>Simple Examples of Reflection\<close> |
267 |
267 |
268 text{*Example 1: reflecting a simple formula. The reflecting class is first |
268 text\<open>Example 1: reflecting a simple formula. The reflecting class is first |
269 given as the variable @{text ?Cl} and later retrieved from the final |
269 given as the variable @{text ?Cl} and later retrieved from the final |
270 proof state.*} |
270 proof state.\<close> |
271 schematic_lemma (in reflection) |
271 schematic_lemma (in reflection) |
272 "Reflects(?Cl, |
272 "Reflects(?Cl, |
273 \<lambda>x. \<exists>y. M(y) & x \<in> y, |
273 \<lambda>x. \<exists>y. M(y) & x \<in> y, |
274 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" |
274 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" |
275 by fast |
275 by fast |
276 |
276 |
277 text{*Problem here: there needs to be a conjunction (class intersection) |
277 text\<open>Problem here: there needs to be a conjunction (class intersection) |
278 in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant, |
278 in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant, |
279 though harmless.*} |
279 though harmless.\<close> |
280 lemma (in reflection) |
280 lemma (in reflection) |
281 "Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a), |
281 "Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a), |
282 \<lambda>x. \<exists>y. M(y) & x \<in> y, |
282 \<lambda>x. \<exists>y. M(y) & x \<in> y, |
283 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" |
283 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" |
284 by fast |
284 by fast |
285 |
285 |
286 |
286 |
287 text{*Example 2*} |
287 text\<open>Example 2\<close> |
288 schematic_lemma (in reflection) |
288 schematic_lemma (in reflection) |
289 "Reflects(?Cl, |
289 "Reflects(?Cl, |
290 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
290 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
291 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
291 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
292 by fast |
292 by fast |
293 |
293 |
294 text{*Example 2'. We give the reflecting class explicitly. *} |
294 text\<open>Example 2'. We give the reflecting class explicitly.\<close> |
295 lemma (in reflection) |
295 lemma (in reflection) |
296 "Reflects |
296 "Reflects |
297 (\<lambda>a. (Ord(a) & |
297 (\<lambda>a. (Ord(a) & |
298 ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) \<longrightarrow> snd(x) \<in> snd(fst(x))), a)) & |
298 ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) \<longrightarrow> snd(x) \<in> snd(fst(x))), a)) & |
299 ClEx(\<lambda>x. \<forall>z. M(z) \<longrightarrow> z \<subseteq> fst(x) \<longrightarrow> z \<in> snd(x), a), |
299 ClEx(\<lambda>x. \<forall>z. M(z) \<longrightarrow> z \<subseteq> fst(x) \<longrightarrow> z \<in> snd(x), a), |
300 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
300 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
301 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
301 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
302 by fast |
302 by fast |
303 |
303 |
304 text{*Example 2''. We expand the subset relation.*} |
304 text\<open>Example 2''. We expand the subset relation.\<close> |
305 schematic_lemma (in reflection) |
305 schematic_lemma (in reflection) |
306 "Reflects(?Cl, |
306 "Reflects(?Cl, |
307 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y), |
307 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> (\<forall>w. M(w) \<longrightarrow> w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y), |
308 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y)" |
308 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z \<longrightarrow> w\<in>x) \<longrightarrow> z\<in>y)" |
309 by fast |
309 by fast |
310 |
310 |
311 text{*Example 2'''. Single-step version, to reveal the reflecting class.*} |
311 text\<open>Example 2'''. Single-step version, to reveal the reflecting class.\<close> |
312 schematic_lemma (in reflection) |
312 schematic_lemma (in reflection) |
313 "Reflects(?Cl, |
313 "Reflects(?Cl, |
314 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
314 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<subseteq> x \<longrightarrow> z \<in> y), |
315 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
315 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x \<longrightarrow> z \<in> y)" |
316 apply (rule Ex_reflection) |
316 apply (rule Ex_reflection) |
317 txt{* |
317 txt\<open> |
318 @{goals[display,indent=0,margin=60]} |
318 @{goals[display,indent=0,margin=60]} |
319 *} |
319 \<close> |
320 apply (rule All_reflection) |
320 apply (rule All_reflection) |
321 txt{* |
321 txt\<open> |
322 @{goals[display,indent=0,margin=60]} |
322 @{goals[display,indent=0,margin=60]} |
323 *} |
323 \<close> |
324 apply (rule Triv_reflection) |
324 apply (rule Triv_reflection) |
325 txt{* |
325 txt\<open> |
326 @{goals[display,indent=0,margin=60]} |
326 @{goals[display,indent=0,margin=60]} |
327 *} |
327 \<close> |
328 done |
328 done |
329 |
329 |
330 text{*Example 3. Warning: the following examples make sense only |
330 text\<open>Example 3. Warning: the following examples make sense only |
331 if @{term P} is quantifier-free, since it is not being relativized.*} |
331 if @{term P} is quantifier-free, since it is not being relativized.\<close> |
332 schematic_lemma (in reflection) |
332 schematic_lemma (in reflection) |
333 "Reflects(?Cl, |
333 "Reflects(?Cl, |
334 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)), |
334 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) \<longrightarrow> z \<in> y \<longleftrightarrow> z \<in> x & P(z)), |
335 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))" |
335 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y \<longleftrightarrow> z \<in> x & P(z))" |
336 by fast |
336 by fast |
337 |
337 |
338 text{*Example 3'*} |
338 text\<open>Example 3'\<close> |
339 schematic_lemma (in reflection) |
339 schematic_lemma (in reflection) |
340 "Reflects(?Cl, |
340 "Reflects(?Cl, |
341 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P), |
341 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P), |
342 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))" |
342 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))" |
343 by fast |
343 by fast |
344 |
344 |
345 text{*Example 3''*} |
345 text\<open>Example 3''\<close> |
346 schematic_lemma (in reflection) |
346 schematic_lemma (in reflection) |
347 "Reflects(?Cl, |
347 "Reflects(?Cl, |
348 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P), |
348 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P), |
349 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))" |
349 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))" |
350 by fast |
350 by fast |
351 |
351 |
352 text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs |
352 text\<open>Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs |
353 to be relativized.*} |
353 to be relativized.\<close> |
354 schematic_lemma (in reflection) |
354 schematic_lemma (in reflection) |
355 "Reflects(?Cl, |
355 "Reflects(?Cl, |
356 \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)), |
356 \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)), |
357 \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))" |
357 \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))" |
358 by fast |
358 by fast |