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