src/ZF/Constructible/Reflection.thy
changeset 69593 3dda49e08b9d
parent 67443 3abf6a722518
child 71417 89d05db6dd1f
equal deleted inserted replaced
69592:a80d8ec6c998 69593:3dda49e08b9d
    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