src/ZF/Constructible/Normal.thy
 author wenzelm Mon Dec 04 22:54:31 2017 +0100 (21 months ago) changeset 67131 85d10959c2e4 parent 65449 c82e63b11b8b child 67443 3abf6a722518 permissions -rw-r--r--
tuned signature;
     1 (*  Title:      ZF/Constructible/Normal.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3 *)

     4

     5 section \<open>Closed Unbounded Classes and Normal Functions\<close>

     6

     7 theory Normal imports ZF begin

     8

     9 text\<open>

    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 \<close>

    16

    17

    18 subsection \<open>Closed and Unbounded (c.u.) Classes of Ordinals\<close>

    19

    20 definition

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

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

    23

    24 definition

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

    26     "Unbounded(P) == \<forall>i. Ord(i) \<longrightarrow> (\<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\<open>Simple facts about c.u. classes\<close>

    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\<open>The universal class, V, is closed and unbounded.

    54       A bit odd, since C. U. concerns only ordinals, but it's used below!\<close>

    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\<open>The class of ordinals, @{term Ord}, is closed and unbounded.\<close>

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

    60 by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)

    61

    62 text\<open>The class of limit ordinals, @{term Limit}, is closed and unbounded.\<close>

    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\<open>The class of cardinals, @{term Card}, is closed and unbounded.\<close>

    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\<open>The intersection of any set-indexed family of c.u. classes is

    78       c.u.\<close>

    79

    80 text\<open>The constructions below come from Kunen, \emph{Set Theory}, page 78.\<close>

    81 locale cub_family =

    82   fixes P and A

    83   fixes next_greater \<comment> "the next ordinal satisfying class @{term A}"

    84   fixes sup_greater  \<comment> "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\<open>Trivial that the intersection is closed.\<close>

    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\<open>All remaining effort goes to show that the intersection is unbounded.\<close>

    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\<open>@{term next_greater} works as expected: it returns a larger value

   107 and one that belongs to class @{term "P(a)"}.\<close>

   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\<open>Opposite bound:

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

   147 \<close>

   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)  \<longleftrightarrow>  (\<forall>i\<in>2. (i=0 \<longrightarrow> P(x)) \<and> (i=1 \<longrightarrow> 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 \<open>Normal Functions\<close>

   203

   204 definition

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

   206     "mono_le_subset(M) == \<forall>i j. i\<le>j \<longrightarrow> M(i) \<subseteq> M(j)"

   207

   208 definition

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

   210     "mono_Ord(F) == \<forall>i j. i<j \<longrightarrow> F(i) < F(j)"

   211

   212 definition

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

   214     "cont_Ord(F) == \<forall>l. Limit(l) \<longrightarrow> 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\<open>Immediate properties of the definitions\<close>

   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 (auto 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:

   246   assumes i: "Ord(i)" and F: "Normal(F)" shows"i \<le> F(i)"

   247 using i

   248 proof (induct i rule: trans_induct3)

   249   case 0 thus ?case by (simp add: subset_imp_le F)

   250 next

   251   case (succ i)

   252   hence "F(i) < F(succ(i))" using F

   253     by (simp add: Normal_def mono_Ord_def)

   254   thus ?case using succ.hyps

   255     by (blast intro: lt_trans1)

   256 next

   257   case (limit l)

   258   hence "l = (\<Union>y<l. y)"

   259     by (simp add: Limit_OUN_eq)

   260   also have "... \<le> (\<Union>y<l. F(y))" using limit

   261     by (blast intro: ltD le_implies_OUN_le_OUN)

   262   finally have "l \<le> (\<Union>y<l. F(y))" .

   263   moreover have "(\<Union>y<l. F(y)) \<le> F(l)" using limit F

   264     by (simp add: Normal_imp_cont lt_Ord)

   265   ultimately show ?case

   266     by (blast intro: le_trans)

   267 qed

   268

   269

   270 subsubsection\<open>The class of fixedpoints is closed and unbounded\<close>

   271

   272 text\<open>The proof is from Drake, pages 113--114.\<close>

   273

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

   275 apply (simp add: mono_le_subset_def, clarify)

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

   277 apply (simp add: le_iff)

   278 apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono)

   279 done

   280

   281 text\<open>The following equation is taken for granted in any set theory text.\<close>

   282 lemma cont_Ord_Union:

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

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

   285 apply (frule Ord_set_cases)

   286 apply (erule disjE, force)

   287 apply (thin_tac "X=0 \<longrightarrow> Q" for Q, auto)

   288  txt\<open>The trival case of @{term "\<Union>X \<in> X"}\<close>

   289  apply (rule equalityI, blast intro: Ord_Union_eq_succD)

   290  apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)

   291  apply (blast elim: equalityE)

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

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

   294 \<close>

   295 apply (simp add: OUN_Union_eq cont_Ord_def)

   296 apply (rule equalityI)

   297 txt\<open>First inclusion:\<close>

   298  apply (rule UN_least [OF OUN_least])

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

   300 txt\<open>Second inclusion:\<close>

   301 apply (rule UN_least)

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

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

   304  apply (simp add: OUnion_def)

   305  apply blast+

   306 done

   307

   308 lemma Normal_Union:

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

   310 apply (simp add: Normal_def)

   311 apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union)

   312 done

   313

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

   315 apply (simp add: Closed_def ball_conj_distrib, clarify)

   316 apply (frule Ord_set_cases)

   317 apply (auto simp add: Normal_Union)

   318 done

   319

   320

   321 lemma iterates_Normal_increasing:

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

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

   324 apply (induct n rule: nat_induct)

   325 apply (simp_all add: Normal_imp_mono)

   326 done

   327

   328 lemma Ord_iterates_Normal:

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

   330 by (simp add: Ord_iterates)

   331

   332 text\<open>THIS RESULT IS UNUSED\<close>

   333 lemma iterates_omega_Limit:

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

   335 apply (frule lt_Ord)

   336 apply (simp add: iterates_omega_def)

   337 apply (rule increasing_LimitI)

   338    \<comment>"this lemma is @{thm increasing_LimitI [no_vars]}"

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

   340                      Ord_UN Ord_iterates lt_imp_0_lt

   341                      iterates_Normal_increasing, clarify)

   342 apply (rule bexI)

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

   344 apply (rule UN_I, erule nat_succI)

   345 apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal

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

   347 done

   348

   349 lemma iterates_omega_fixedpoint:

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

   351 apply (frule Normal_increasing, assumption)

   352 apply (erule leE)

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

   354 apply (simp add:  iterates_omega_def Normal_Union)

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

   356 txt\<open>Opposite inclusion:

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

   358 \<close>

   359 apply clarify

   360 apply (rule UN_I, assumption)

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

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

   363 done

   364

   365 lemma iterates_omega_increasing:

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

   367 apply (unfold iterates_omega_def)

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

   369 done

   370

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

   372 apply (unfold Unbounded_def, clarify)

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

   374 apply (simp add: iterates_omega_fixedpoint)

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

   376 done

   377

   378

   379 theorem Normal_imp_fp_Closed_Unbounded:

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

   381 by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed

   382               Normal_imp_fp_Unbounded)

   383

   384

   385 subsubsection\<open>Function \<open>normalize\<close>\<close>

   386

   387 text\<open>Function \<open>normalize\<close> maps a function \<open>F\<close> to a

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

   389       only if \<open>F\<close> is continuous: succ is not bounded above by any

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

   391 \<close>

   392 definition

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

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

   395

   396

   397 lemma Ord_normalize [simp, intro]:

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

   399 apply (induct a rule: trans_induct3)

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

   401 done

   402

   403 lemma normalize_increasing:

   404   assumes ab: "a < b" and F: "!!x. Ord(x) ==> Ord(F(x))"

   405   shows "normalize(F,a) < normalize(F,b)"

   406 proof -

   407   { fix x

   408     have "Ord(b)" using ab by (blast intro: lt_Ord2)

   409     hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)"

   410     proof (induct b arbitrary: x rule: trans_induct3)

   411       case 0 thus ?case by simp

   412     next

   413       case (succ b)

   414       thus ?case

   415         by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)

   416     next

   417       case (limit l)

   418       hence sc: "succ(x) < l"

   419         by (blast intro: Limit_has_succ)

   420       hence "normalize(F,x) < normalize(F,succ(x))"

   421         by (blast intro: limit elim: ltE)

   422       hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"

   423         by (blast intro: OUN_upper_lt lt_Ord F sc)

   424       thus ?case using limit

   425         by (simp add: def_transrec2 [OF normalize_def])

   426     qed

   427   } thus ?thesis using ab .

   428 qed

   429

   430 theorem Normal_normalize:

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

   432 apply (rule NormalI)

   433 apply (blast intro!: normalize_increasing)

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

   435 done

   436

   437 theorem le_normalize:

   438   assumes a: "Ord(a)" and coF: "cont_Ord(F)" and F: "!!x. Ord(x) ==> Ord(F(x))"

   439   shows "F(a) \<le> normalize(F,a)"

   440 using a

   441 proof (induct a rule: trans_induct3)

   442   case 0 thus ?case by (simp add: F def_transrec2 [OF normalize_def])

   443 next

   444   case (succ a)

   445   thus ?case

   446     by (simp add: def_transrec2 [OF normalize_def] Un_upper1_le F )

   447 next

   448   case (limit l)

   449   thus ?case using F coF [unfolded cont_Ord_def]

   450     by (simp add: def_transrec2 [OF normalize_def] le_implies_OUN_le_OUN ltD)

   451 qed

   452

   453

   454 subsection \<open>The Alephs\<close>

   455 text \<open>This is the well-known transfinite enumeration of the cardinal

   456 numbers.\<close>

   457

   458 definition

   459   Aleph :: "i => i"  ("\<aleph>_"  90) where

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

   461

   462 lemma Card_Aleph [simp, intro]:

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

   464 apply (erule trans_induct3)

   465 apply (simp_all add: Card_csucc Card_nat Card_is_Ord

   466                      def_transrec2 [OF Aleph_def])

   467 done

   468

   469 lemma Aleph_increasing:

   470   assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"

   471 proof -

   472   { fix x

   473     have "Ord(b)" using ab by (blast intro: lt_Ord2)

   474     hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)"

   475     proof (induct b arbitrary: x rule: trans_induct3)

   476       case 0 thus ?case by simp

   477     next

   478       case (succ b)

   479       thus ?case

   480         by (force simp add: le_iff def_transrec2 [OF Aleph_def]

   481                   intro: lt_trans lt_csucc Card_is_Ord)

   482     next

   483       case (limit l)

   484       hence sc: "succ(x) < l"

   485         by (blast intro: Limit_has_succ)

   486       hence "\<aleph> x < (\<Union>j<l. \<aleph>j)" using limit

   487         by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)

   488       thus ?case using limit

   489         by (simp add: def_transrec2 [OF Aleph_def])

   490     qed

   491   } thus ?thesis using ab .

   492 qed

   493

   494 theorem Normal_Aleph: "Normal(Aleph)"

   495 apply (rule NormalI)

   496 apply (blast intro!: Aleph_increasing)

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

   498 done

   499

   500 end