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