src/ZF/Constructible/Normal.thy
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 32960 69916a850301
child 46823 57bf0cecb366
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      ZF/Constructible/Normal.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 *)
     4 
     5 header {*Closed Unbounded Classes and Normal Functions*}
     6 
     7 theory Normal imports Main begin
     8 
     9 text{*
    10 One source is the book
    11 
    12 Frank R. Drake.
    13 \emph{Set Theory: An Introduction to Large Cardinals}.
    14 North-Holland, 1974.
    15 *}
    16 
    17 
    18 subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
    19 
    20 definition
    21   Closed :: "(i=>o) => o" where
    22     "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
    23 
    24 definition
    25   Unbounded :: "(i=>o) => o" where
    26     "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
    27 
    28 definition
    29   Closed_Unbounded :: "(i=>o) => o" where
    30     "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
    31 
    32 
    33 subsubsection{*Simple facts about c.u. classes*}
    34 
    35 lemma ClosedI:
    36      "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |] 
    37       ==> Closed(P)"
    38 by (simp add: Closed_def)
    39 
    40 lemma ClosedD:
    41      "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |] 
    42       ==> P(\<Union>(I))"
    43 by (simp add: Closed_def)
    44 
    45 lemma UnboundedD:
    46      "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
    47 by (simp add: Unbounded_def)
    48 
    49 lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
    50 by (simp add: Closed_Unbounded_def) 
    51 
    52 
    53 text{*The universal class, V, is closed and unbounded.
    54       A bit odd, since C. U. concerns only ordinals, but it's used below!*}
    55 theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
    56 by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    57 
    58 text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
    59 theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
    60 by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    61 
    62 text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
    63 theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
    64 apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
    65        clarify)
    66 apply (rule_tac x="i++nat" in exI)  
    67 apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
    68 done
    69 
    70 text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
    71 theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
    72 apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
    73 apply (blast intro: lt_csucc Card_csucc)
    74 done
    75 
    76 
    77 subsubsection{*The intersection of any set-indexed family of c.u. classes is
    78       c.u.*}
    79 
    80 text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
    81 locale cub_family =
    82   fixes P and A
    83   fixes next_greater -- "the next ordinal satisfying class @{term A}"
    84   fixes sup_greater  -- "sup of those ordinals over all @{term A}"
    85   assumes closed:    "a\<in>A ==> Closed(P(a))"
    86       and unbounded: "a\<in>A ==> Unbounded(P(a))"
    87       and A_non0: "A\<noteq>0"
    88   defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"
    89       and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
    90  
    91 
    92 text{*Trivial that the intersection is closed.*}
    93 lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
    94 by (blast intro: ClosedI ClosedD [OF closed])
    95 
    96 text{*All remaining effort goes to show that the intersection is unbounded.*}
    97 
    98 lemma (in cub_family) Ord_sup_greater:
    99      "Ord(sup_greater(x))"
   100 by (simp add: sup_greater_def next_greater_def)
   101 
   102 lemma (in cub_family) Ord_next_greater:
   103      "Ord(next_greater(a,x))"
   104 by (simp add: next_greater_def Ord_Least)
   105 
   106 text{*@{term next_greater} works as expected: it returns a larger value
   107 and one that belongs to class @{term "P(a)"}. *}
   108 lemma (in cub_family) next_greater_lemma:
   109      "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
   110 apply (simp add: next_greater_def)
   111 apply (rule exE [OF UnboundedD [OF unbounded]])
   112   apply assumption+
   113 apply (blast intro: LeastI2 lt_Ord2) 
   114 done
   115 
   116 lemma (in cub_family) next_greater_in_P:
   117      "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
   118 by (blast dest: next_greater_lemma)
   119 
   120 lemma (in cub_family) next_greater_gt:
   121      "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
   122 by (blast dest: next_greater_lemma)
   123 
   124 lemma (in cub_family) sup_greater_gt:
   125      "Ord(x) ==> x < sup_greater(x)"
   126 apply (simp add: sup_greater_def)
   127 apply (insert A_non0)
   128 apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
   129 done
   130 
   131 lemma (in cub_family) next_greater_le_sup_greater:
   132      "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
   133 apply (simp add: sup_greater_def) 
   134 apply (blast intro: UN_upper_le Ord_next_greater)
   135 done
   136 
   137 lemma (in cub_family) omega_sup_greater_eq_UN:
   138      "[| Ord(x); a\<in>A |] 
   139       ==> sup_greater^\<omega> (x) = 
   140           (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
   141 apply (simp add: iterates_omega_def)
   142 apply (rule le_anti_sym)
   143 apply (rule le_implies_UN_le_UN) 
   144 apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)  
   145 txt{*Opposite bound:
   146 @{subgoals[display,indent=0,margin=65]}
   147 *}
   148 apply (rule UN_least_le) 
   149 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   150 apply (rule_tac a="succ(n)" in UN_upper_le)
   151 apply (simp_all add: next_greater_le_sup_greater) 
   152 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   153 done
   154 
   155 lemma (in cub_family) P_omega_sup_greater:
   156      "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
   157 apply (simp add: omega_sup_greater_eq_UN)
   158 apply (rule ClosedD [OF closed]) 
   159 apply (blast intro: ltD, auto)
   160 apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
   161 apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
   162 done
   163 
   164 lemma (in cub_family) omega_sup_greater_gt:
   165      "Ord(x) ==> x < sup_greater^\<omega> (x)"
   166 apply (simp add: iterates_omega_def)
   167 apply (rule UN_upper_lt [of 1], simp_all) 
   168  apply (blast intro: sup_greater_gt) 
   169 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
   170 done
   171 
   172 lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   173 apply (unfold Unbounded_def)  
   174 apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
   175 done
   176 
   177 lemma (in cub_family) Closed_Unbounded_INT: 
   178      "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   179 by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
   180 
   181 
   182 theorem Closed_Unbounded_INT:
   183     "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
   184      ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
   185 apply (case_tac "A=0", simp)
   186 apply (rule cub_family.Closed_Unbounded_INT [OF cub_family.intro])
   187 apply (simp_all add: Closed_Unbounded_def)
   188 done
   189 
   190 lemma Int_iff_INT2:
   191      "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
   192 by auto
   193 
   194 theorem Closed_Unbounded_Int:
   195      "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] 
   196       ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
   197 apply (simp only: Int_iff_INT2)
   198 apply (rule Closed_Unbounded_INT, auto) 
   199 done
   200 
   201 
   202 subsection {*Normal Functions*} 
   203 
   204 definition
   205   mono_le_subset :: "(i=>i) => o" where
   206     "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
   207 
   208 definition
   209   mono_Ord :: "(i=>i) => o" where
   210     "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
   211 
   212 definition
   213   cont_Ord :: "(i=>i) => o" where
   214     "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
   215 
   216 definition
   217   Normal :: "(i=>i) => o" where
   218     "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
   219 
   220 
   221 subsubsection{*Immediate properties of the definitions*}
   222 
   223 lemma NormalI:
   224      "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
   225       ==> Normal(F)"
   226 by (simp add: Normal_def mono_Ord_def cont_Ord_def)
   227 
   228 lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
   229 apply (simp add: mono_Ord_def) 
   230 apply (blast intro: lt_Ord) 
   231 done
   232 
   233 lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
   234 by (simp add: mono_Ord_def)
   235 
   236 lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
   237 by (simp add: Normal_def mono_Ord_imp_Ord) 
   238 
   239 lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
   240 by (simp add: Normal_def cont_Ord_def)
   241 
   242 lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
   243 by (simp add: Normal_def mono_Ord_def)
   244 
   245 lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
   246 apply (induct i rule: trans_induct3_rule)
   247   apply (simp add: subset_imp_le)
   248  apply (subgoal_tac "F(x) < F(succ(x))")
   249   apply (force intro: lt_trans1)
   250  apply (simp add: Normal_def mono_Ord_def)
   251 apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
   252  apply (simp add: Normal_imp_cont Limit_OUN_eq) 
   253 apply (blast intro: ltD le_implies_OUN_le_OUN)
   254 done
   255 
   256 
   257 subsubsection{*The class of fixedpoints is closed and unbounded*}
   258 
   259 text{*The proof is from Drake, pages 113--114.*}
   260 
   261 lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
   262 apply (simp add: mono_le_subset_def, clarify)
   263 apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset) 
   264 apply (simp add: le_iff) 
   265 apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono) 
   266 done
   267 
   268 text{*The following equation is taken for granted in any set theory text.*}
   269 lemma cont_Ord_Union:
   270      "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |] 
   271       ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   272 apply (frule Ord_set_cases)
   273 apply (erule disjE, force) 
   274 apply (thin_tac "X=0 --> ?Q", auto)
   275  txt{*The trival case of @{term "\<Union>X \<in> X"}*}
   276  apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
   277  apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
   278  apply (blast elim: equalityE)
   279 txt{*The limit case, @{term "Limit(\<Union>X)"}:
   280 @{subgoals[display,indent=0,margin=65]}
   281 *}
   282 apply (simp add: OUN_Union_eq cont_Ord_def)
   283 apply (rule equalityI) 
   284 txt{*First inclusion:*}
   285  apply (rule UN_least [OF OUN_least])
   286  apply (simp add: mono_le_subset_def, blast intro: leI) 
   287 txt{*Second inclusion:*}
   288 apply (rule UN_least) 
   289 apply (frule Union_upper_le, blast, blast intro: Ord_Union)
   290 apply (erule leE, drule ltD, elim UnionE)
   291  apply (simp add: OUnion_def)
   292  apply blast+
   293 done
   294 
   295 lemma Normal_Union:
   296      "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   297 apply (simp add: Normal_def) 
   298 apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union) 
   299 done
   300 
   301 lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
   302 apply (simp add: Closed_def ball_conj_distrib, clarify)
   303 apply (frule Ord_set_cases)
   304 apply (auto simp add: Normal_Union)
   305 done
   306 
   307 
   308 lemma iterates_Normal_increasing:
   309      "[| n\<in>nat;  x < F(x);  Normal(F) |] 
   310       ==> F^n (x) < F^(succ(n)) (x)"  
   311 apply (induct n rule: nat_induct)
   312 apply (simp_all add: Normal_imp_mono)
   313 done
   314 
   315 lemma Ord_iterates_Normal:
   316      "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
   317 by (simp add: Ord_iterates) 
   318 
   319 text{*THIS RESULT IS UNUSED*}
   320 lemma iterates_omega_Limit:
   321      "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
   322 apply (frule lt_Ord) 
   323 apply (simp add: iterates_omega_def)
   324 apply (rule increasing_LimitI) 
   325    --"this lemma is @{thm increasing_LimitI [no_vars]}"
   326  apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
   327                      Ord_UN Ord_iterates lt_imp_0_lt
   328                      iterates_Normal_increasing, clarify)
   329 apply (rule bexI) 
   330  apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
   331 apply (rule UN_I, erule nat_succI) 
   332 apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal
   333                      ltD [OF lt_trans1, OF succ_leI, OF ltI]) 
   334 done
   335 
   336 lemma iterates_omega_fixedpoint:
   337      "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)" 
   338 apply (frule Normal_increasing, assumption)
   339 apply (erule leE) 
   340  apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)
   341 apply (simp add:  iterates_omega_def Normal_Union) 
   342 apply (rule equalityI, force simp add: nat_succI) 
   343 txt{*Opposite inclusion:
   344 @{subgoals[display,indent=0,margin=65]}
   345 *}
   346 apply clarify
   347 apply (rule UN_I, assumption) 
   348 apply (frule iterates_Normal_increasing, assumption, assumption, simp)
   349 apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F]) 
   350 done
   351 
   352 lemma iterates_omega_increasing:
   353      "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"   
   354 apply (unfold iterates_omega_def)
   355 apply (rule UN_upper_le [of 0], simp_all)
   356 done
   357 
   358 lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
   359 apply (unfold Unbounded_def, clarify)
   360 apply (rule_tac x="F^\<omega> (succ(i))" in exI)
   361 apply (simp add: iterates_omega_fixedpoint) 
   362 apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
   363 done
   364 
   365 
   366 theorem Normal_imp_fp_Closed_Unbounded: 
   367      "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
   368 by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
   369               Normal_imp_fp_Unbounded)
   370 
   371 
   372 subsubsection{*Function @{text normalize}*}
   373 
   374 text{*Function @{text normalize} maps a function @{text F} to a 
   375       normal function that bounds it above.  The result is normal if and
   376       only if @{text F} is continuous: succ is not bounded above by any 
   377       normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
   378 *}
   379 definition
   380   normalize :: "[i=>i, i] => i" where
   381     "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
   382 
   383 
   384 lemma Ord_normalize [simp, intro]:
   385      "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
   386 apply (induct a rule: trans_induct3_rule)
   387 apply (simp_all add: ltD def_transrec2 [OF normalize_def])
   388 done
   389 
   390 lemma normalize_lemma [rule_format]:
   391      "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
   392       ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
   393 apply (erule trans_induct3)
   394   apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
   395  apply clarify
   396 apply (rule Un_upper2_lt) 
   397   apply auto
   398  apply (drule spec, drule mp, assumption) 
   399  apply (erule leI) 
   400 apply (drule Limit_has_succ, assumption)
   401 apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
   402 done  
   403 
   404 lemma normalize_increasing:
   405      "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
   406       ==> normalize(F, a) < normalize(F, b)"
   407 by (blast intro!: normalize_lemma intro: lt_Ord2) 
   408 
   409 theorem Normal_normalize:
   410      "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
   411 apply (rule NormalI) 
   412 apply (blast intro!: normalize_increasing)
   413 apply (simp add: def_transrec2 [OF normalize_def])
   414 done
   415 
   416 theorem le_normalize:
   417      "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
   418       ==> F(a) \<le> normalize(F,a)"
   419 apply (erule trans_induct3) 
   420 apply (simp_all add: def_transrec2 [OF normalize_def])
   421 apply (simp add: Un_upper1_le) 
   422 apply (simp add: cont_Ord_def) 
   423 apply (blast intro: ltD le_implies_OUN_le_OUN)
   424 done
   425 
   426 
   427 subsection {*The Alephs*}
   428 text {*This is the well-known transfinite enumeration of the cardinal 
   429 numbers.*}
   430 
   431 definition
   432   Aleph :: "i => i" where
   433     "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
   434 
   435 notation (xsymbols)
   436   Aleph  ("\<aleph>_" [90] 90)
   437 
   438 lemma Card_Aleph [simp, intro]:
   439      "Ord(a) ==> Card(Aleph(a))"
   440 apply (erule trans_induct3) 
   441 apply (simp_all add: Card_csucc Card_nat Card_is_Ord
   442                      def_transrec2 [OF Aleph_def])
   443 done
   444 
   445 lemma Aleph_lemma [rule_format]:
   446      "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
   447 apply (erule trans_induct3) 
   448 apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
   449 apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
   450 apply (drule Limit_has_succ, assumption)
   451 apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
   452 done  
   453 
   454 lemma Aleph_increasing:
   455      "a < b ==> Aleph(a) < Aleph(b)"
   456 by (blast intro!: Aleph_lemma intro: lt_Ord2) 
   457 
   458 theorem Normal_Aleph: "Normal(Aleph)"
   459 apply (rule NormalI) 
   460 apply (blast intro!: Aleph_increasing)
   461 apply (simp add: def_transrec2 [OF Aleph_def])
   462 done
   463 
   464 end