src/ZF/Constructible/Normal.thy
changeset 13223 45be08fbdcff
child 13268 240509babf00
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/Normal.thy	Wed Jun 19 11:48:01 2002 +0200
     1.3 @@ -0,0 +1,457 @@
     1.4 +header {*Closed Unbounded Classes and Normal Functions*}
     1.5 +
     1.6 +theory Normal = Main:
     1.7 +
     1.8 +text{*
     1.9 +One source is the book
    1.10 +
    1.11 +Frank R. Drake.
    1.12 +\emph{Set Theory: An Introduction to Large Cardinals}.
    1.13 +North-Holland, 1974.
    1.14 +*}
    1.15 +
    1.16 +
    1.17 +subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
    1.18 +
    1.19 +constdefs
    1.20 +  Closed :: "(i=>o) => o"
    1.21 +    "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
    1.22 +
    1.23 +  Unbounded :: "(i=>o) => o"
    1.24 +    "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
    1.25 +
    1.26 +  Closed_Unbounded :: "(i=>o) => o"
    1.27 +    "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
    1.28 +
    1.29 +
    1.30 +subsubsection{*Simple facts about c.u. classes*}
    1.31 +
    1.32 +lemma ClosedI:
    1.33 +     "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |] 
    1.34 +      ==> Closed(P)"
    1.35 +by (simp add: Closed_def)
    1.36 +
    1.37 +lemma ClosedD:
    1.38 +     "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |] 
    1.39 +      ==> P(\<Union>(I))"
    1.40 +by (simp add: Closed_def)
    1.41 +
    1.42 +lemma UnboundedD:
    1.43 +     "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
    1.44 +by (simp add: Unbounded_def)
    1.45 +
    1.46 +lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
    1.47 +by (simp add: Closed_Unbounded_def) 
    1.48 +
    1.49 +
    1.50 +text{*The universal class, V, is closed and unbounded.
    1.51 +      A bit odd, since C. U. concerns only ordinals, but it's used below!*}
    1.52 +theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
    1.53 +by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    1.54 +
    1.55 +text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
    1.56 +theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
    1.57 +by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    1.58 +
    1.59 +text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
    1.60 +theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
    1.61 +apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
    1.62 +       clarify)
    1.63 +apply (rule_tac x="i++nat" in exI)  
    1.64 +apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
    1.65 +done
    1.66 +
    1.67 +text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
    1.68 +theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
    1.69 +apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
    1.70 +apply (blast intro: lt_csucc Card_csucc)
    1.71 +done
    1.72 +
    1.73 +
    1.74 +subsubsection{*The intersection of any set-indexed family of c.u. classes is
    1.75 +      c.u.*}
    1.76 +
    1.77 +text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
    1.78 +locale cub_family =
    1.79 +  fixes P and A
    1.80 +  fixes next_greater -- "the next ordinal satisfying class @{term A}"
    1.81 +  fixes sup_greater  -- "sup of those ordinals over all @{term A}"
    1.82 +  assumes closed:    "a\<in>A ==> Closed(P(a))"
    1.83 +      and unbounded: "a\<in>A ==> Unbounded(P(a))"
    1.84 +      and A_non0: "A\<noteq>0"
    1.85 +  defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
    1.86 +      and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
    1.87 + 
    1.88 +
    1.89 +text{*Trivial that the intersection is closed.*}
    1.90 +lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
    1.91 +by (blast intro: ClosedI ClosedD [OF closed])
    1.92 +
    1.93 +text{*All remaining effort goes to show that the intersection is unbounded.*}
    1.94 +
    1.95 +lemma (in cub_family) Ord_sup_greater:
    1.96 +     "Ord(sup_greater(x))"
    1.97 +by (simp add: sup_greater_def next_greater_def)
    1.98 +
    1.99 +lemma (in cub_family) Ord_next_greater:
   1.100 +     "Ord(next_greater(a,x))"
   1.101 +by (simp add: next_greater_def Ord_Least)
   1.102 +
   1.103 +text{*@{term next_greater} works as expected: it returns a larger value
   1.104 +and one that belongs to class @{term "P(a)"}. *}
   1.105 +lemma (in cub_family) next_greater_lemma:
   1.106 +     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
   1.107 +apply (simp add: next_greater_def)
   1.108 +apply (rule exE [OF UnboundedD [OF unbounded]])
   1.109 +  apply assumption+
   1.110 +apply (blast intro: LeastI2 lt_Ord2) 
   1.111 +done
   1.112 +
   1.113 +lemma (in cub_family) next_greater_in_P:
   1.114 +     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
   1.115 +by (blast dest: next_greater_lemma)
   1.116 +
   1.117 +lemma (in cub_family) next_greater_gt:
   1.118 +     "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
   1.119 +by (blast dest: next_greater_lemma)
   1.120 +
   1.121 +lemma (in cub_family) sup_greater_gt:
   1.122 +     "Ord(x) ==> x < sup_greater(x)"
   1.123 +apply (simp add: sup_greater_def)
   1.124 +apply (insert A_non0)
   1.125 +apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
   1.126 +done
   1.127 +
   1.128 +lemma (in cub_family) next_greater_le_sup_greater:
   1.129 +     "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
   1.130 +apply (simp add: sup_greater_def) 
   1.131 +apply (blast intro: UN_upper_le Ord_next_greater)
   1.132 +done
   1.133 +
   1.134 +lemma (in cub_family) omega_sup_greater_eq_UN:
   1.135 +     "[| Ord(x); a\<in>A |] 
   1.136 +      ==> sup_greater^\<omega> (x) = 
   1.137 +          (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
   1.138 +apply (simp add: iterates_omega_def)
   1.139 +apply (rule le_anti_sym)
   1.140 +apply (rule le_implies_UN_le_UN) 
   1.141 +apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)  
   1.142 +txt{*Opposite bound:
   1.143 +@{subgoals[display,indent=0,margin=65]}
   1.144 +*}
   1.145 +apply (rule UN_least_le) 
   1.146 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   1.147 +apply (rule_tac a="succ(n)" in UN_upper_le)
   1.148 +apply (simp_all add: next_greater_le_sup_greater) 
   1.149 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   1.150 +done
   1.151 +
   1.152 +lemma (in cub_family) P_omega_sup_greater:
   1.153 +     "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
   1.154 +apply (simp add: omega_sup_greater_eq_UN)
   1.155 +apply (rule ClosedD [OF closed]) 
   1.156 +apply (blast intro: ltD, auto)
   1.157 +apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
   1.158 +apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
   1.159 +done
   1.160 +
   1.161 +lemma (in cub_family) omega_sup_greater_gt:
   1.162 +     "Ord(x) ==> x < sup_greater^\<omega> (x)"
   1.163 +apply (simp add: iterates_omega_def)
   1.164 +apply (rule UN_upper_lt [of 1], simp_all) 
   1.165 + apply (blast intro: sup_greater_gt) 
   1.166 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
   1.167 +done
   1.168 +
   1.169 +lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   1.170 +apply (unfold Unbounded_def)  
   1.171 +apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
   1.172 +done
   1.173 +
   1.174 +lemma (in cub_family) Closed_Unbounded_INT: 
   1.175 +     "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   1.176 +by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
   1.177 +
   1.178 +
   1.179 +theorem Closed_Unbounded_INT:
   1.180 +    "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
   1.181 +     ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
   1.182 +apply (case_tac "A=0", simp)
   1.183 +apply (rule cub_family.Closed_Unbounded_INT)
   1.184 +apply (simp_all add: Closed_Unbounded_def)
   1.185 +done
   1.186 +
   1.187 +lemma Int_iff_INT2:
   1.188 +     "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
   1.189 +by auto
   1.190 +
   1.191 +theorem Closed_Unbounded_Int:
   1.192 +     "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] 
   1.193 +      ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
   1.194 +apply (simp only: Int_iff_INT2)
   1.195 +apply (rule Closed_Unbounded_INT, auto) 
   1.196 +done
   1.197 +
   1.198 +
   1.199 +subsection {*Normal Functions*} 
   1.200 +
   1.201 +constdefs
   1.202 +  mono_le_subset :: "(i=>i) => o"
   1.203 +    "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
   1.204 +
   1.205 +  mono_Ord :: "(i=>i) => o"
   1.206 +    "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
   1.207 +
   1.208 +  cont_Ord :: "(i=>i) => o"
   1.209 +    "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
   1.210 +
   1.211 +  Normal :: "(i=>i) => o"
   1.212 +    "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
   1.213 +
   1.214 +
   1.215 +subsubsection{*Immediate properties of the definitions*}
   1.216 +
   1.217 +lemma NormalI:
   1.218 +     "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
   1.219 +      ==> Normal(F)"
   1.220 +by (simp add: Normal_def mono_Ord_def cont_Ord_def)
   1.221 +
   1.222 +lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
   1.223 +apply (simp add: mono_Ord_def) 
   1.224 +apply (blast intro: lt_Ord) 
   1.225 +done
   1.226 +
   1.227 +lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
   1.228 +by (simp add: mono_Ord_def)
   1.229 +
   1.230 +lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
   1.231 +by (simp add: Normal_def mono_Ord_imp_Ord) 
   1.232 +
   1.233 +lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
   1.234 +by (simp add: Normal_def cont_Ord_def)
   1.235 +
   1.236 +lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
   1.237 +by (simp add: Normal_def mono_Ord_def)
   1.238 +
   1.239 +lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
   1.240 +apply (induct i rule: trans_induct3_rule)
   1.241 +  apply (simp add: subset_imp_le)
   1.242 + apply (subgoal_tac "F(x) < F(succ(x))")
   1.243 +  apply (force intro: lt_trans1)
   1.244 + apply (simp add: Normal_def mono_Ord_def)
   1.245 +apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
   1.246 + apply (simp add: Normal_imp_cont Limit_OUN_eq) 
   1.247 +apply (blast intro: ltD le_implies_OUN_le_OUN)
   1.248 +done
   1.249 +
   1.250 +
   1.251 +subsubsection{*The class of fixedpoints is closed and unbounded*}
   1.252 +
   1.253 +text{*The proof is from Drake, pages 113--114.*}
   1.254 +
   1.255 +lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
   1.256 +apply (simp add: mono_le_subset_def, clarify)
   1.257 +apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset) 
   1.258 +apply (simp add: le_iff) 
   1.259 +apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono) 
   1.260 +done
   1.261 +
   1.262 +text{*The following equation is taken for granted in any set theory text.*}
   1.263 +lemma cont_Ord_Union:
   1.264 +     "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |] 
   1.265 +      ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   1.266 +apply (frule Ord_set_cases)
   1.267 +apply (erule disjE, force) 
   1.268 +apply (thin_tac "X=0 --> ?Q", auto)
   1.269 + txt{*The trival case of @{term "\<Union>X \<in> X"}*}
   1.270 + apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
   1.271 + apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
   1.272 + apply (blast elim: equalityE)
   1.273 +txt{*The limit case, @{term "Limit(\<Union>X)"}:
   1.274 +@{subgoals[display,indent=0,margin=65]}
   1.275 +*}
   1.276 +apply (simp add: OUN_Union_eq cont_Ord_def)
   1.277 +apply (rule equalityI) 
   1.278 +txt{*First inclusion:*}
   1.279 + apply (rule UN_least [OF OUN_least])
   1.280 + apply (simp add: mono_le_subset_def, blast intro: leI) 
   1.281 +txt{*Second inclusion:*}
   1.282 +apply (rule UN_least) 
   1.283 +apply (frule Union_upper_le, blast, blast intro: Ord_Union)
   1.284 +apply (erule leE, drule ltD, elim UnionE)
   1.285 + apply (simp add: OUnion_def)
   1.286 + apply blast+
   1.287 +done
   1.288 +
   1.289 +lemma Normal_Union:
   1.290 +     "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   1.291 +apply (simp add: Normal_def) 
   1.292 +apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union) 
   1.293 +done
   1.294 +
   1.295 +lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
   1.296 +apply (simp add: Closed_def ball_conj_distrib, clarify)
   1.297 +apply (frule Ord_set_cases)
   1.298 +apply (auto simp add: Normal_Union)
   1.299 +done
   1.300 +
   1.301 +
   1.302 +lemma iterates_Normal_increasing:
   1.303 +     "[| n\<in>nat;  x < F(x);  Normal(F) |] 
   1.304 +      ==> F^n (x) < F^(succ(n)) (x)"  
   1.305 +apply (induct n rule: nat_induct)
   1.306 +apply (simp_all add: Normal_imp_mono)
   1.307 +done
   1.308 +
   1.309 +lemma Ord_iterates_Normal:
   1.310 +     "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
   1.311 +by (simp add: Ord_iterates) 
   1.312 +
   1.313 +text{*THIS RESULT IS UNUSED*}
   1.314 +lemma iterates_omega_Limit:
   1.315 +     "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
   1.316 +apply (frule lt_Ord) 
   1.317 +apply (simp add: iterates_omega_def)
   1.318 +apply (rule increasing_LimitI) 
   1.319 +   --"this lemma is @{thm increasing_LimitI [no_vars]}"
   1.320 + apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
   1.321 +                     Ord_UN Ord_iterates lt_imp_0_lt
   1.322 +                     iterates_Normal_increasing)
   1.323 +apply clarify
   1.324 +apply (rule bexI) 
   1.325 + apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
   1.326 +apply (rule UN_I, erule nat_succI) 
   1.327 +apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal
   1.328 +                     ltD [OF lt_trans1, OF succ_leI, OF ltI]) 
   1.329 +done
   1.330 +
   1.331 +lemma iterates_omega_fixedpoint:
   1.332 +     "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)" 
   1.333 +apply (frule Normal_increasing, assumption)
   1.334 +apply (erule leE) 
   1.335 + apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)
   1.336 +apply (simp add:  iterates_omega_def Normal_Union) 
   1.337 +apply (rule equalityI, force simp add: nat_succI) 
   1.338 +txt{*Opposite inclusion:
   1.339 +@{subgoals[display,indent=0,margin=65]}
   1.340 +*}
   1.341 +apply clarify
   1.342 +apply (rule UN_I, assumption) 
   1.343 +apply (frule iterates_Normal_increasing, assumption, assumption, simp)
   1.344 +apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F]) 
   1.345 +done
   1.346 +
   1.347 +lemma iterates_omega_increasing:
   1.348 +     "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"   
   1.349 +apply (unfold iterates_omega_def)
   1.350 +apply (rule UN_upper_le [of 0], simp_all)
   1.351 +done
   1.352 +
   1.353 +lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
   1.354 +apply (unfold Unbounded_def, clarify)
   1.355 +apply (rule_tac x="F^\<omega> (succ(i))" in exI)
   1.356 +apply (simp add: iterates_omega_fixedpoint) 
   1.357 +apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
   1.358 +done
   1.359 +
   1.360 +
   1.361 +theorem Normal_imp_fp_Closed_Unbounded: 
   1.362 +     "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
   1.363 +by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
   1.364 +              Normal_imp_fp_Unbounded)
   1.365 +
   1.366 +
   1.367 +subsubsection{*Function @{text normalize}*}
   1.368 +
   1.369 +text{*Function @{text normalize} maps a function @{text F} to a 
   1.370 +      normal function that bounds it above.  The result is normal if and
   1.371 +      only if @{text F} is continuous: succ is not bounded above by any 
   1.372 +      normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
   1.373 +*}
   1.374 +constdefs
   1.375 +  normalize :: "[i=>i, i] => i"
   1.376 +    "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
   1.377 +
   1.378 +
   1.379 +lemma Ord_normalize [simp, intro]:
   1.380 +     "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
   1.381 +apply (induct a rule: trans_induct3_rule)
   1.382 +apply (simp_all add: ltD def_transrec2 [OF normalize_def])
   1.383 +done
   1.384 +
   1.385 +lemma normalize_lemma [rule_format]:
   1.386 +     "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
   1.387 +      ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
   1.388 +apply (erule trans_induct3)
   1.389 +  apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
   1.390 + apply clarify
   1.391 +apply (rule Un_upper2_lt) 
   1.392 +  apply auto
   1.393 + apply (drule spec, drule mp, assumption) 
   1.394 + apply (erule leI) 
   1.395 +apply (drule Limit_has_succ, assumption)
   1.396 +apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
   1.397 +done  
   1.398 +
   1.399 +lemma normalize_increasing:
   1.400 +     "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
   1.401 +      ==> normalize(F, a) < normalize(F, b)"
   1.402 +by (blast intro!: normalize_lemma intro: lt_Ord2) 
   1.403 +
   1.404 +theorem Normal_normalize:
   1.405 +     "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
   1.406 +apply (rule NormalI) 
   1.407 +apply (blast intro!: normalize_increasing)
   1.408 +apply (simp add: def_transrec2 [OF normalize_def])
   1.409 +done
   1.410 +
   1.411 +theorem le_normalize:
   1.412 +     "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
   1.413 +      ==> F(a) \<le> normalize(F,a)"
   1.414 +apply (erule trans_induct3) 
   1.415 +apply (simp_all add: def_transrec2 [OF normalize_def])
   1.416 +apply (simp add: Un_upper1_le) 
   1.417 +apply (simp add: cont_Ord_def) 
   1.418 +apply (blast intro: ltD le_implies_OUN_le_OUN)
   1.419 +done
   1.420 +
   1.421 +
   1.422 +subsection {*The Alephs*}
   1.423 +text {*This is the well-known transfinite enumeration of the cardinal 
   1.424 +numbers.*}
   1.425 +
   1.426 +constdefs
   1.427 +  Aleph :: "i => i"
   1.428 +    "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
   1.429 +
   1.430 +syntax (xsymbols)
   1.431 +  Aleph :: "i => i"   ("\<aleph>_" [90] 90)
   1.432 +
   1.433 +lemma Card_Aleph [simp, intro]:
   1.434 +     "Ord(a) ==> Card(Aleph(a))"
   1.435 +apply (erule trans_induct3) 
   1.436 +apply (simp_all add: Card_csucc Card_nat Card_is_Ord
   1.437 +                     def_transrec2 [OF Aleph_def])
   1.438 +done
   1.439 +
   1.440 +lemma Aleph_lemma [rule_format]:
   1.441 +     "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
   1.442 +apply (erule trans_induct3) 
   1.443 +apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
   1.444 +apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
   1.445 +apply (drule Limit_has_succ, assumption)
   1.446 +apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
   1.447 +done  
   1.448 +
   1.449 +lemma Aleph_increasing:
   1.450 +     "a < b ==> Aleph(a) < Aleph(b)"
   1.451 +by (blast intro!: Aleph_lemma intro: lt_Ord2) 
   1.452 +
   1.453 +theorem Normal_Aleph: "Normal(Aleph)"
   1.454 +apply (rule NormalI) 
   1.455 +apply (blast intro!: Aleph_increasing)
   1.456 +apply (simp add: def_transrec2 [OF Aleph_def])
   1.457 +done
   1.458 +
   1.459 +end
   1.460 +