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