src/ZF/Constructible/Normal.thy
 author ballarin Thu Dec 11 18:30:26 2008 +0100 (2008-12-11) changeset 29223 e09c53289830 parent 21404 eb85850d3eb7 child 32960 69916a850301 permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/Normal.thy

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4 *)

     5

     6 header {*Closed Unbounded Classes and Normal Functions*}

     7

     8 theory Normal imports Main begin

     9

    10 text{*

    11 One source is the book

    12

    13 Frank R. Drake.

    14 \emph{Set Theory: An Introduction to Large Cardinals}.

    15 North-Holland, 1974.

    16 *}

    17

    18

    19 subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}

    20

    21 definition

    22   Closed :: "(i=>o) => o" where

    23     "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"

    24

    25 definition

    26   Unbounded :: "(i=>o) => o" where

    27     "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"

    28

    29 definition

    30   Closed_Unbounded :: "(i=>o) => o" where

    31     "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"

    32

    33

    34 subsubsection{*Simple facts about c.u. classes*}

    35

    36 lemma ClosedI:

    37      "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |]

    38       ==> Closed(P)"

    39 by (simp add: Closed_def)

    40

    41 lemma ClosedD:

    42      "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |]

    43       ==> P(\<Union>(I))"

    44 by (simp add: Closed_def)

    45

    46 lemma UnboundedD:

    47      "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"

    48 by (simp add: Unbounded_def)

    49

    50 lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"

    51 by (simp add: Closed_Unbounded_def)

    52

    53

    54 text{*The universal class, V, is closed and unbounded.

    55       A bit odd, since C. U. concerns only ordinals, but it's used below!*}

    56 theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"

    57 by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)

    58

    59 text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}

    60 theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"

    61 by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)

    62

    63 text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}

    64 theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"

    65 apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union,

    66        clarify)

    67 apply (rule_tac x="i++nat" in exI)

    68 apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0)

    69 done

    70

    71 text{*The class of cardinals, @{term Card}, is closed and unbounded.*}

    72 theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"

    73 apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)

    74 apply (blast intro: lt_csucc Card_csucc)

    75 done

    76

    77

    78 subsubsection{*The intersection of any set-indexed family of c.u. classes is

    79       c.u.*}

    80

    81 text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}

    82 locale cub_family =

    83   fixes P and A

    84   fixes next_greater -- "the next ordinal satisfying class @{term A}"

    85   fixes sup_greater  -- "sup of those ordinals over all @{term A}"

    86   assumes closed:    "a\<in>A ==> Closed(P(a))"

    87       and unbounded: "a\<in>A ==> Unbounded(P(a))"

    88       and A_non0: "A\<noteq>0"

    89   defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)"

    90       and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"

    91

    92

    93 text{*Trivial that the intersection is closed.*}

    94 lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"

    95 by (blast intro: ClosedI ClosedD [OF closed])

    96

    97 text{*All remaining effort goes to show that the intersection is unbounded.*}

    98

    99 lemma (in cub_family) Ord_sup_greater:

   100      "Ord(sup_greater(x))"

   101 by (simp add: sup_greater_def next_greater_def)

   102

   103 lemma (in cub_family) Ord_next_greater:

   104      "Ord(next_greater(a,x))"

   105 by (simp add: next_greater_def Ord_Least)

   106

   107 text{*@{term next_greater} works as expected: it returns a larger value

   108 and one that belongs to class @{term "P(a)"}. *}

   109 lemma (in cub_family) next_greater_lemma:

   110      "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"

   111 apply (simp add: next_greater_def)

   112 apply (rule exE [OF UnboundedD [OF unbounded]])

   113   apply assumption+

   114 apply (blast intro: LeastI2 lt_Ord2)

   115 done

   116

   117 lemma (in cub_family) next_greater_in_P:

   118      "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"

   119 by (blast dest: next_greater_lemma)

   120

   121 lemma (in cub_family) next_greater_gt:

   122      "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"

   123 by (blast dest: next_greater_lemma)

   124

   125 lemma (in cub_family) sup_greater_gt:

   126      "Ord(x) ==> x < sup_greater(x)"

   127 apply (simp add: sup_greater_def)

   128 apply (insert A_non0)

   129 apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)

   130 done

   131

   132 lemma (in cub_family) next_greater_le_sup_greater:

   133      "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"

   134 apply (simp add: sup_greater_def)

   135 apply (blast intro: UN_upper_le Ord_next_greater)

   136 done

   137

   138 lemma (in cub_family) omega_sup_greater_eq_UN:

   139      "[| Ord(x); a\<in>A |]

   140       ==> sup_greater^\<omega> (x) =

   141           (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"

   142 apply (simp add: iterates_omega_def)

   143 apply (rule le_anti_sym)

   144 apply (rule le_implies_UN_le_UN)

   145 apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)

   146 txt{*Opposite bound:

   147 @{subgoals[display,indent=0,margin=65]}

   148 *}

   149 apply (rule UN_least_le)

   150 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)

   151 apply (rule_tac a="succ(n)" in UN_upper_le)

   152 apply (simp_all add: next_greater_le_sup_greater)

   153 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)

   154 done

   155

   156 lemma (in cub_family) P_omega_sup_greater:

   157      "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"

   158 apply (simp add: omega_sup_greater_eq_UN)

   159 apply (rule ClosedD [OF closed])

   160 apply (blast intro: ltD, auto)

   161 apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)

   162 apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)

   163 done

   164

   165 lemma (in cub_family) omega_sup_greater_gt:

   166      "Ord(x) ==> x < sup_greater^\<omega> (x)"

   167 apply (simp add: iterates_omega_def)

   168 apply (rule UN_upper_lt [of 1], simp_all)

   169  apply (blast intro: sup_greater_gt)

   170 apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)

   171 done

   172

   173 lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"

   174 apply (unfold Unbounded_def)

   175 apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater)

   176 done

   177

   178 lemma (in cub_family) Closed_Unbounded_INT:

   179      "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"

   180 by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)

   181

   182

   183 theorem Closed_Unbounded_INT:

   184     "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))

   185      ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"

   186 apply (case_tac "A=0", simp)

   187 apply (rule cub_family.Closed_Unbounded_INT [OF cub_family.intro])

   188 apply (simp_all add: Closed_Unbounded_def)

   189 done

   190

   191 lemma Int_iff_INT2:

   192      "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"

   193 by auto

   194

   195 theorem Closed_Unbounded_Int:

   196      "[| Closed_Unbounded(P); Closed_Unbounded(Q) |]

   197       ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"

   198 apply (simp only: Int_iff_INT2)

   199 apply (rule Closed_Unbounded_INT, auto)

   200 done

   201

   202

   203 subsection {*Normal Functions*}

   204

   205 definition

   206   mono_le_subset :: "(i=>i) => o" where

   207     "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"

   208

   209 definition

   210   mono_Ord :: "(i=>i) => o" where

   211     "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"

   212

   213 definition

   214   cont_Ord :: "(i=>i) => o" where

   215     "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"

   216

   217 definition

   218   Normal :: "(i=>i) => o" where

   219     "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"

   220

   221

   222 subsubsection{*Immediate properties of the definitions*}

   223

   224 lemma NormalI:

   225      "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]

   226       ==> Normal(F)"

   227 by (simp add: Normal_def mono_Ord_def cont_Ord_def)

   228

   229 lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"

   230 apply (simp add: mono_Ord_def)

   231 apply (blast intro: lt_Ord)

   232 done

   233

   234 lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"

   235 by (simp add: mono_Ord_def)

   236

   237 lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"

   238 by (simp add: Normal_def mono_Ord_imp_Ord)

   239

   240 lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"

   241 by (simp add: Normal_def cont_Ord_def)

   242

   243 lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"

   244 by (simp add: Normal_def mono_Ord_def)

   245

   246 lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"

   247 apply (induct i rule: trans_induct3_rule)

   248   apply (simp add: subset_imp_le)

   249  apply (subgoal_tac "F(x) < F(succ(x))")

   250   apply (force intro: lt_trans1)

   251  apply (simp add: Normal_def mono_Ord_def)

   252 apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")

   253  apply (simp add: Normal_imp_cont Limit_OUN_eq)

   254 apply (blast intro: ltD le_implies_OUN_le_OUN)

   255 done

   256

   257

   258 subsubsection{*The class of fixedpoints is closed and unbounded*}

   259

   260 text{*The proof is from Drake, pages 113--114.*}

   261

   262 lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"

   263 apply (simp add: mono_le_subset_def, clarify)

   264 apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset)

   265 apply (simp add: le_iff)

   266 apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono)

   267 done

   268

   269 text{*The following equation is taken for granted in any set theory text.*}

   270 lemma cont_Ord_Union:

   271      "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |]

   272       ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"

   273 apply (frule Ord_set_cases)

   274 apply (erule disjE, force)

   275 apply (thin_tac "X=0 --> ?Q", auto)

   276  txt{*The trival case of @{term "\<Union>X \<in> X"}*}

   277  apply (rule equalityI, blast intro: Ord_Union_eq_succD)

   278  apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)

   279  apply (blast elim: equalityE)

   280 txt{*The limit case, @{term "Limit(\<Union>X)"}:

   281 @{subgoals[display,indent=0,margin=65]}

   282 *}

   283 apply (simp add: OUN_Union_eq cont_Ord_def)

   284 apply (rule equalityI)

   285 txt{*First inclusion:*}

   286  apply (rule UN_least [OF OUN_least])

   287  apply (simp add: mono_le_subset_def, blast intro: leI)

   288 txt{*Second inclusion:*}

   289 apply (rule UN_least)

   290 apply (frule Union_upper_le, blast, blast intro: Ord_Union)

   291 apply (erule leE, drule ltD, elim UnionE)

   292  apply (simp add: OUnion_def)

   293  apply blast+

   294 done

   295

   296 lemma Normal_Union:

   297      "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"

   298 apply (simp add: Normal_def)

   299 apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union)

   300 done

   301

   302 lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"

   303 apply (simp add: Closed_def ball_conj_distrib, clarify)

   304 apply (frule Ord_set_cases)

   305 apply (auto simp add: Normal_Union)

   306 done

   307

   308

   309 lemma iterates_Normal_increasing:

   310      "[| n\<in>nat;  x < F(x);  Normal(F) |]

   311       ==> F^n (x) < F^(succ(n)) (x)"

   312 apply (induct n rule: nat_induct)

   313 apply (simp_all add: Normal_imp_mono)

   314 done

   315

   316 lemma Ord_iterates_Normal:

   317      "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"

   318 by (simp add: Ord_iterates)

   319

   320 text{*THIS RESULT IS UNUSED*}

   321 lemma iterates_omega_Limit:

   322      "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"

   323 apply (frule lt_Ord)

   324 apply (simp add: iterates_omega_def)

   325 apply (rule increasing_LimitI)

   326    --"this lemma is @{thm increasing_LimitI [no_vars]}"

   327  apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord

   328                      Ord_UN Ord_iterates lt_imp_0_lt

   329                      iterates_Normal_increasing, clarify)

   330 apply (rule bexI)

   331  apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])

   332 apply (rule UN_I, erule nat_succI)

   333 apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal

   334                      ltD [OF lt_trans1, OF succ_leI, OF ltI])

   335 done

   336

   337 lemma iterates_omega_fixedpoint:

   338      "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)"

   339 apply (frule Normal_increasing, assumption)

   340 apply (erule leE)

   341  apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)

   342 apply (simp add:  iterates_omega_def Normal_Union)

   343 apply (rule equalityI, force simp add: nat_succI)

   344 txt{*Opposite inclusion:

   345 @{subgoals[display,indent=0,margin=65]}

   346 *}

   347 apply clarify

   348 apply (rule UN_I, assumption)

   349 apply (frule iterates_Normal_increasing, assumption, assumption, simp)

   350 apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F])

   351 done

   352

   353 lemma iterates_omega_increasing:

   354      "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"

   355 apply (unfold iterates_omega_def)

   356 apply (rule UN_upper_le [of 0], simp_all)

   357 done

   358

   359 lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"

   360 apply (unfold Unbounded_def, clarify)

   361 apply (rule_tac x="F^\<omega> (succ(i))" in exI)

   362 apply (simp add: iterates_omega_fixedpoint)

   363 apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])

   364 done

   365

   366

   367 theorem Normal_imp_fp_Closed_Unbounded:

   368      "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"

   369 by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed

   370               Normal_imp_fp_Unbounded)

   371

   372

   373 subsubsection{*Function @{text normalize}*}

   374

   375 text{*Function @{text normalize} maps a function @{text F} to a

   376       normal function that bounds it above.  The result is normal if and

   377       only if @{text F} is continuous: succ is not bounded above by any

   378       normal function, by @{thm [source] Normal_imp_fp_Unbounded}.

   379 *}

   380 definition

   381   normalize :: "[i=>i, i] => i" where

   382     "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"

   383

   384

   385 lemma Ord_normalize [simp, intro]:

   386      "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"

   387 apply (induct a rule: trans_induct3_rule)

   388 apply (simp_all add: ltD def_transrec2 [OF normalize_def])

   389 done

   390

   391 lemma normalize_lemma [rule_format]:

   392      "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |]

   393       ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"

   394 apply (erule trans_induct3)

   395   apply (simp_all add: le_iff def_transrec2 [OF normalize_def])

   396  apply clarify

   397 apply (rule Un_upper2_lt)

   398   apply auto

   399  apply (drule spec, drule mp, assumption)

   400  apply (erule leI)

   401 apply (drule Limit_has_succ, assumption)

   402 apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)

   403 done

   404

   405 lemma normalize_increasing:

   406      "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |]

   407       ==> normalize(F, a) < normalize(F, b)"

   408 by (blast intro!: normalize_lemma intro: lt_Ord2)

   409

   410 theorem Normal_normalize:

   411      "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"

   412 apply (rule NormalI)

   413 apply (blast intro!: normalize_increasing)

   414 apply (simp add: def_transrec2 [OF normalize_def])

   415 done

   416

   417 theorem le_normalize:

   418      "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |]

   419       ==> F(a) \<le> normalize(F,a)"

   420 apply (erule trans_induct3)

   421 apply (simp_all add: def_transrec2 [OF normalize_def])

   422 apply (simp add: Un_upper1_le)

   423 apply (simp add: cont_Ord_def)

   424 apply (blast intro: ltD le_implies_OUN_le_OUN)

   425 done

   426

   427

   428 subsection {*The Alephs*}

   429 text {*This is the well-known transfinite enumeration of the cardinal

   430 numbers.*}

   431

   432 definition

   433   Aleph :: "i => i" where

   434     "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"

   435

   436 notation (xsymbols)

   437   Aleph  ("\<aleph>_"  90)

   438

   439 lemma Card_Aleph [simp, intro]:

   440      "Ord(a) ==> Card(Aleph(a))"

   441 apply (erule trans_induct3)

   442 apply (simp_all add: Card_csucc Card_nat Card_is_Ord

   443                      def_transrec2 [OF Aleph_def])

   444 done

   445

   446 lemma Aleph_lemma [rule_format]:

   447      "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"

   448 apply (erule trans_induct3)

   449 apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])

   450 apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)

   451 apply (drule Limit_has_succ, assumption)

   452 apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)

   453 done

   454

   455 lemma Aleph_increasing:

   456      "a < b ==> Aleph(a) < Aleph(b)"

   457 by (blast intro!: Aleph_lemma intro: lt_Ord2)

   458

   459 theorem Normal_Aleph: "Normal(Aleph)"

   460 apply (rule NormalI)

   461 apply (blast intro!: Aleph_increasing)

   462 apply (simp add: def_transrec2 [OF Aleph_def])

   463 done

   464

   465 end