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