20 subsection\<open>Basic Definitions\<close> |
20 subsection\<open>Basic Definitions\<close> |
21 |
21 |
22 text\<open>First part: the cumulative hierarchy defining the class \<open>M\<close>. |
22 text\<open>First part: the cumulative hierarchy defining the class \<open>M\<close>. |
23 To avoid handling multiple arguments, we assume that \<open>Mset(l)\<close> is |
23 To avoid handling multiple arguments, we assume that \<open>Mset(l)\<close> is |
24 closed under ordered pairing provided \<open>l\<close> is limit. Possibly this |
24 closed under ordered pairing provided \<open>l\<close> is limit. Possibly this |
25 could be avoided: the induction hypothesis @{term Cl_reflects} |
25 could be avoided: the induction hypothesis \<^term>\<open>Cl_reflects\<close> |
26 (in locale \<open>ex_reflection\<close>) could be weakened to |
26 (in locale \<open>ex_reflection\<close>) 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>\<open>\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) \<longleftrightarrow> Q(a,<y,z>)\<close>, removing most |
28 uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since |
28 uses of \<^term>\<open>Pair_in_Mset\<close>. But there isn't much point in doing so, since |
29 ultimately the \<open>ex_reflection\<close> proof is packaged up using the |
29 ultimately the \<open>ex_reflection\<close> proof is packaged up using the |
30 predicate \<open>Reflects\<close>. |
30 predicate \<open>Reflects\<close>. |
31 \<close> |
31 \<close> |
32 locale reflection = |
32 locale reflection = |
33 fixes Mset and M and Reflects |
33 fixes Mset and M and Reflects |
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 \<comment> \<open>ordinal for a specific value @{term y}\<close> |
41 fixes F0 \<comment> \<open>ordinal for a specific value \<^term>\<open>y\<close>\<close> |
42 fixes FF \<comment> \<open>sup over the whole level, @{term "y\<in>Mset(a)"}\<close> |
42 fixes FF \<comment> \<open>sup over the whole level, \<^term>\<open>y\<in>Mset(a)\<close>\<close> |
43 fixes ClEx \<comment> \<open>Reflecting ordinals for the formula @{term "\<exists>z. P"}\<close> |
43 fixes ClEx \<comment> \<open>Reflecting ordinals for the formula \<^term>\<open>\<exists>z. P\<close>\<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 |
113 lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))" |
113 lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))" |
114 apply (insert Mset_cont) |
114 apply (insert Mset_cont) |
115 apply (simp add: cont_Ord_def FF_def, blast) |
115 apply (simp add: cont_Ord_def FF_def, blast) |
116 done |
116 done |
117 |
117 |
118 text\<open>Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"}, |
118 text\<open>Recall that \<^term>\<open>F0\<close> depends upon \<^term>\<open>y\<in>Mset(a)\<close>, |
119 while @{term FF} depends only upon @{term a}.\<close> |
119 while \<^term>\<open>FF\<close> depends only upon \<^term>\<open>a\<close>.\<close> |
120 lemma (in reflection) FF_works: |
120 lemma (in reflection) FF_works: |
121 "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)" |
121 "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)" |
122 apply (simp add: FF_def) |
122 apply (simp add: FF_def) |
123 apply (simp_all add: cont_Ord_Union [of concl: Mset] |
123 apply (simp_all add: cont_Ord_Union [of concl: Mset] |
124 Mset_cont Mset_mono_le not_emptyI Ord_F0) |
124 Mset_cont Mset_mono_le not_emptyI Ord_F0) |
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\<open>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>\<open>Ord(a)\<close> is redundant, |
279 though harmless.\<close> |
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)" |
326 @{goals[display,indent=0,margin=60]} |
326 @{goals[display,indent=0,margin=60]} |
327 \<close> |
327 \<close> |
328 done |
328 done |
329 |
329 |
330 text\<open>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.\<close> |
331 if \<^term>\<open>P\<close> is quantifier-free, since it is not being relativized.\<close> |
332 schematic_goal (in reflection) |
332 schematic_goal (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 |