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