src/ZF/Constructible/Reflection.thy
changeset 13223 45be08fbdcff
child 13268 240509babf00
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/Reflection.thy	Wed Jun 19 11:48:01 2002 +0200
     1.3 @@ -0,0 +1,321 @@
     1.4 +header {* The Reflection Theorem*}
     1.5 +
     1.6 +theory Reflection = Normal:
     1.7 +
     1.8 +lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
     1.9 +by blast
    1.10 +
    1.11 +lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) <-> (~ (\<exists>x\<in>A. ~ P(x)))";
    1.12 +by blast
    1.13 +
    1.14 +text{*From the notes of A. S. Kechris, page 6, and from 
    1.15 +      Andrzej Mostowski, \emph{Constructible Sets with Applications},
    1.16 +      North-Holland, 1969, page 23.*}
    1.17 +
    1.18 +
    1.19 +subsection{*Basic Definitions*}
    1.20 +
    1.21 +text{*First part: the cumulative hierarchy defining the class @{text M}.  
    1.22 +To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
    1.23 +closed under ordered pairing provided @{text l} is limit.  Possibly this
    1.24 +could be avoided: the induction hypothesis @{term Cl_reflects} 
    1.25 +(in locale @{text ex_reflection}) could be weakened to
    1.26 +@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
    1.27 +uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since 
    1.28 +ultimately the @{text ex_reflection} proof is packaged up using the
    1.29 +predicate @{text Reflects}.
    1.30 +*}
    1.31 +locale reflection =
    1.32 +  fixes Mset and M and Reflects
    1.33 +  assumes Mset_mono_le : "mono_le_subset(Mset)"
    1.34 +      and Mset_cont    : "cont_Ord(Mset)"
    1.35 +      and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] 
    1.36 +                          ==> <x,y> \<in> Mset(a)"
    1.37 +  defines "M(x) == \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
    1.38 +      and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \<and>
    1.39 +                              (\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
    1.40 +  fixes F0 --{*ordinal for a specific value @{term y}*}
    1.41 +  fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
    1.42 +  fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
    1.43 +  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) \<and> P(<y,z>)) --> 
    1.44 +                               (\<exists>z\<in>Mset(b). P(<y,z>))"
    1.45 +      and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
    1.46 +      and "ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
    1.47 +
    1.48 +lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
    1.49 +apply (insert Mset_mono_le) 
    1.50 +apply (simp add: mono_le_subset_def leI) 
    1.51 +done
    1.52 +
    1.53 +subsection{*Easy Cases of the Reflection Theorem*}
    1.54 +
    1.55 +theorem (in reflection) Triv_reflection [intro]:
    1.56 +     "Reflects(Ord, P, \<lambda>a x. P(x))"
    1.57 +by (simp add: Reflects_def)
    1.58 +
    1.59 +theorem (in reflection) Not_reflection [intro]:
    1.60 +     "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
    1.61 +by (simp add: Reflects_def); 
    1.62 +
    1.63 +theorem (in reflection) And_reflection [intro]:
    1.64 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    1.65 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
    1.66 +                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
    1.67 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    1.68 +
    1.69 +theorem (in reflection) Or_reflection [intro]:
    1.70 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    1.71 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
    1.72 +                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
    1.73 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    1.74 +
    1.75 +theorem (in reflection) Imp_reflection [intro]:
    1.76 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    1.77 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    1.78 +                   \<lambda>x. P(x) --> P'(x), 
    1.79 +                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
    1.80 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    1.81 +
    1.82 +theorem (in reflection) Iff_reflection [intro]:
    1.83 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    1.84 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    1.85 +                   \<lambda>x. P(x) <-> P'(x), 
    1.86 +                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
    1.87 +by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
    1.88 +
    1.89 +subsection{*Reflection for Existential Quantifiers*}
    1.90 +
    1.91 +lemma (in reflection) F0_works:
    1.92 +     "[| y\<in>Mset(a); Ord(a); M(z); P(<y,z>) |] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
    1.93 +apply (unfold F0_def M_def, clarify)
    1.94 +apply (rule LeastI2)
    1.95 +  apply (blast intro: Mset_mono [THEN subsetD])
    1.96 + apply (blast intro: lt_Ord2, blast)
    1.97 +done
    1.98 +
    1.99 +lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))"
   1.100 +by (simp add: F0_def)
   1.101 +
   1.102 +lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))"
   1.103 +by (simp add: FF_def)
   1.104 +
   1.105 +lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
   1.106 +apply (insert Mset_cont)
   1.107 +apply (simp add: cont_Ord_def FF_def, blast)
   1.108 +done
   1.109 +
   1.110 +text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"}, 
   1.111 +while @{term FF} depends only upon @{term a}. *}
   1.112 +lemma (in reflection) FF_works:
   1.113 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
   1.114 +apply (simp add: FF_def)
   1.115 +apply (simp_all add: cont_Ord_Union [of concl: Mset] 
   1.116 +                     Mset_cont Mset_mono_le not_emptyI Ord_F0)
   1.117 +apply (blast intro: F0_works)  
   1.118 +done
   1.119 +
   1.120 +lemma (in reflection) FFN_works:
   1.121 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] 
   1.122 +      ==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
   1.123 +apply (drule FF_works [of concl: P], assumption+) 
   1.124 +apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
   1.125 +done
   1.126 +
   1.127 +
   1.128 +text{*Locale for the induction hypothesis*}
   1.129 +
   1.130 +locale ex_reflection = reflection +
   1.131 +  fixes P  --"the original formula"
   1.132 +  fixes Q  --"the reflected formula"
   1.133 +  fixes Cl --"the class of reflecting ordinals"
   1.134 +  assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
   1.135 +
   1.136 +lemma (in ex_reflection) ClEx_downward:
   1.137 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |] 
   1.138 +      ==> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
   1.139 +apply (simp add: ClEx_def, clarify) 
   1.140 +apply (frule Limit_is_Ord) 
   1.141 +apply (frule FFN_works [of concl: P], assumption+) 
   1.142 +apply (drule Cl_reflects, assumption+) 
   1.143 +apply (auto simp add: Limit_is_Ord Pair_in_Mset)
   1.144 +done
   1.145 +
   1.146 +lemma (in ex_reflection) ClEx_upward:
   1.147 +     "[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |] 
   1.148 +      ==> \<exists>z. M(z) \<and> P(<y,z>)"
   1.149 +apply (simp add: ClEx_def M_def)
   1.150 +apply (blast dest: Cl_reflects
   1.151 +	     intro: Limit_is_Ord Pair_in_Mset)
   1.152 +done
   1.153 +
   1.154 +text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
   1.155 +lemma (in ex_reflection) ZF_ClEx_iff:
   1.156 +     "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] 
   1.157 +      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
   1.158 +by (blast intro: dest: ClEx_downward ClEx_upward) 
   1.159 +
   1.160 +text{*...and it is closed and unbounded*}
   1.161 +lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx:
   1.162 +     "Closed_Unbounded(ClEx(P))"
   1.163 +apply (simp add: ClEx_def)
   1.164 +apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
   1.165 +                   Closed_Unbounded_Limit Normal_normalize)
   1.166 +done
   1.167 +
   1.168 +text{*The same two theorems, exported to locale @{text reflection}.*}
   1.169 +
   1.170 +text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
   1.171 +lemma (in reflection) ClEx_iff:
   1.172 +     "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
   1.173 +        !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |] 
   1.174 +      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
   1.175 +apply (unfold ClEx_def FF_def F0_def M_def)
   1.176 +apply (rule Reflection.ZF_ClEx_iff [of Mset Cl], 
   1.177 +       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
   1.178 +done
   1.179 +
   1.180 +lemma (in reflection) Closed_Unbounded_ClEx:
   1.181 +     "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
   1.182 +      ==> Closed_Unbounded(ClEx(P))"
   1.183 +apply (unfold ClEx_def FF_def F0_def M_def)
   1.184 +apply (rule Reflection.ZF_Closed_Unbounded_ClEx, 
   1.185 +       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
   1.186 +done
   1.187 +
   1.188 +lemma (in reflection) Ex_reflection_0:
   1.189 +     "Reflects(Cl,P0,Q0) 
   1.190 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a), 
   1.191 +                   \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>), 
   1.192 +                   \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 
   1.193 +apply (simp add: Reflects_def) 
   1.194 +apply (intro conjI Closed_Unbounded_Int)
   1.195 +  apply blast 
   1.196 + apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 
   1.197 +apply (rule_tac Cl=Cl in  ClEx_iff, assumption+, blast) 
   1.198 +done
   1.199 +
   1.200 +lemma (in reflection) All_reflection_0:
   1.201 +     "Reflects(Cl,P0,Q0) 
   1.202 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.~P0(x), a), 
   1.203 +                   \<lambda>x. \<forall>z. M(z) --> P0(<x,z>), 
   1.204 +                   \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))" 
   1.205 +apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) 
   1.206 +apply (rule Not_reflection, drule Not_reflection, simp) 
   1.207 +apply (erule Ex_reflection_0)
   1.208 +done
   1.209 +
   1.210 +theorem (in reflection) Ex_reflection [intro]:
   1.211 +     "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   1.212 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   1.213 +                   \<lambda>x. \<exists>z. M(z) \<and> P(x,z), 
   1.214 +                   \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
   1.215 +by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))" 
   1.216 +                               "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
   1.217 +
   1.218 +theorem (in reflection) All_reflection [intro]:
   1.219 +     "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   1.220 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   1.221 +                   \<lambda>x. \<forall>z. M(z) --> P(x,z), 
   1.222 +                   \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
   1.223 +by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 
   1.224 +                                "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
   1.225 +
   1.226 +text{*No point considering bounded quantifiers, where reflection is trivial.*}
   1.227 +
   1.228 +
   1.229 +subsection{*Simple Examples of Reflection*}
   1.230 +
   1.231 +text{*Example 1: reflecting a simple formula.  The reflecting class is first
   1.232 +given as the variable @{text ?Cl} and later retrieved from the final 
   1.233 +proof state.*}
   1.234 +lemma (in reflection) 
   1.235 +     "Reflects(?Cl,
   1.236 +               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   1.237 +               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
   1.238 +by fast
   1.239 +
   1.240 +text{*Problem here: there needs to be a conjunction (class intersection)
   1.241 +in the class of reflecting ordinals.  The @{term "Ord(a)"} is redundant,
   1.242 +though harmless.*}
   1.243 +lemma (in reflection) 
   1.244 +     "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),   
   1.245 +               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   1.246 +               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 
   1.247 +by fast
   1.248 +
   1.249 +
   1.250 +text{*Example 2*}
   1.251 +lemma (in reflection) 
   1.252 +     "Reflects(?Cl,
   1.253 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   1.254 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   1.255 +by fast
   1.256 +
   1.257 +text{*Example 2'.  We give the reflecting class explicitly. *}
   1.258 +lemma (in reflection) 
   1.259 +  "Reflects
   1.260 +    (\<lambda>a. (Ord(a) \<and>
   1.261 +          ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) \<and>
   1.262 +          ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
   1.263 +	    \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   1.264 +	    \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   1.265 +by fast
   1.266 +
   1.267 +text{*Example 2''.  We expand the subset relation.*}
   1.268 +lemma (in reflection) 
   1.269 +  "Reflects(?Cl,
   1.270 +        \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
   1.271 +        \<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)"
   1.272 +by fast
   1.273 +
   1.274 +text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
   1.275 +lemma (in reflection) 
   1.276 +     "Reflects(?Cl,
   1.277 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   1.278 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   1.279 +apply (rule Ex_reflection) 
   1.280 +txt{*
   1.281 +@{goals[display,indent=0,margin=60]}
   1.282 +*}
   1.283 +apply (rule All_reflection) 
   1.284 +txt{*
   1.285 +@{goals[display,indent=0,margin=60]}
   1.286 +*}
   1.287 +apply (rule Triv_reflection) 
   1.288 +txt{*
   1.289 +@{goals[display,indent=0,margin=60]}
   1.290 +*}
   1.291 +done
   1.292 +
   1.293 +text{*Example 3.  Warning: the following examples make sense only
   1.294 +if @{term P} is quantifier-free, since it is not being relativized.*}
   1.295 +lemma (in reflection) 
   1.296 +     "Reflects(?Cl,
   1.297 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<in> y <-> z \<in> x \<and> P(z)), 
   1.298 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x \<and> P(z))"
   1.299 +by fast
   1.300 +
   1.301 +text{*Example 3'*}
   1.302 +lemma (in reflection) 
   1.303 +     "Reflects(?Cl,
   1.304 +               \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
   1.305 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
   1.306 +by fast
   1.307 +
   1.308 +text{*Example 3''*}
   1.309 +lemma (in reflection) 
   1.310 +     "Reflects(?Cl,
   1.311 +               \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
   1.312 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
   1.313 +by fast
   1.314 +
   1.315 +text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
   1.316 +to be relativized.*}
   1.317 +lemma (in reflection) 
   1.318 +     "Reflects(?Cl,
   1.319 +               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) \<and> f \<in> (\<Pi>X \<in> A. X)),
   1.320 +               \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
   1.321 +by fast
   1.322 +
   1.323 +end
   1.324 +