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)

   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