author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46963  67da5904300a 
child 58871  c399ae4b836f 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/Normal.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
*) 

4 

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

16417  7 
theory Normal imports Main begin 
13223  8 

9 
text{* 

10 
One source is the book 

11 

12 
Frank R. Drake. 

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

14 
NorthHolland, 1974. 

15 
*} 

16 

17 

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

19 

21233  20 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

21 
Closed :: "(i=>o) => o" where 
46823  22 
"Closed(P) == \<forall>I. I \<noteq> 0 \<longrightarrow> (\<forall>i\<in>I. Ord(i) \<and> P(i)) \<longrightarrow> P(\<Union>(I))" 
13223  23 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

24 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

25 
Unbounded :: "(i=>o) => o" where 
46823  26 
"Unbounded(P) == \<forall>i. Ord(i) \<longrightarrow> (\<exists>j. i<j \<and> P(j))" 
13223  27 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

28 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

29 
Closed_Unbounded :: "(i=>o) => o" where 
13223  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 setindexed family of c.u. classes is 

78 
c.u.*} 

79 

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

13428  81 
locale cub_family = 
13223  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" 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13634
diff
changeset

88 
defines "next_greater(a,x) == \<mu> y. x<y \<and> P(a,y)" 
13223  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) 

13428  186 
apply (rule cub_family.Closed_Unbounded_INT [OF cub_family.intro]) 
13223  187 
apply (simp_all add: Closed_Unbounded_def) 
188 
done 

189 

190 
lemma Int_iff_INT2: 

46823  191 
"P(x) \<and> Q(x) \<longleftrightarrow> (\<forall>i\<in>2. (i=0 \<longrightarrow> P(x)) \<and> (i=1 \<longrightarrow> Q(x)))" 
13223  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 

21233  204 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

205 
mono_le_subset :: "(i=>i) => o" where 
46823  206 
"mono_le_subset(M) == \<forall>i j. i\<le>j \<longrightarrow> M(i) \<subseteq> M(j)" 
13223  207 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

208 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

209 
mono_Ord :: "(i=>i) => o" where 
46823  210 
"mono_Ord(F) == \<forall>i j. i<j \<longrightarrow> F(i) < F(j)" 
13223  211 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

212 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

213 
cont_Ord :: "(i=>i) => o" where 
46823  214 
"cont_Ord(F) == \<forall>l. Limit(l) \<longrightarrow> F(l) = (\<Union>i<l. F(i))" 
13223  215 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

216 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

217 
Normal :: "(i=>i) => o" where 
13223  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))" 

46963  229 
apply (auto simp add: mono_Ord_def) 
13223  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 

46963  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 

13223  268 

269 

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

271 

272 
text{*The proof is from Drake, pages 113114.*} 

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{*The following equation is taken for granted in any set theory text.*} 

282 
lemma cont_Ord_Union: 

46823  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))" 

13223  285 
apply (frule Ord_set_cases) 
286 
apply (erule disjE, force) 

46823  287 
apply (thin_tac "X=0 \<longrightarrow> ?Q", auto) 
13223  288 
txt{*The trival case of @{term "\<Union>X \<in> X"}*} 
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{*The limit case, @{term "Limit(\<Union>X)"}: 

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

294 
*} 

295 
apply (simp add: OUN_Union_eq cont_Ord_def) 

296 
apply (rule equalityI) 

297 
txt{*First inclusion:*} 

298 
apply (rule UN_least [OF OUN_least]) 

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

300 
txt{*Second inclusion:*} 

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: 

46823  309 
"[ X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) ] ==> F(\<Union>(X)) = (\<Union>y\<in>X. F(y))" 
13223  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{*THIS RESULT IS UNUSED*} 

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 
"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 

13268  341 
iterates_Normal_increasing, clarify) 
13223  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{*Opposite inclusion: 

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

358 
*} 

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{*Function @{text normalize}*} 

386 

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

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

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

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

391 
*} 

21233  392 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

393 
normalize :: "[i=>i, i] => i" where 
46823  394 
"normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) \<union> succ(r))" 
13223  395 

396 

397 
lemma Ord_normalize [simp, intro]: 

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

46927  399 
apply (induct a rule: trans_induct3) 
13223  400 
apply (simp_all add: ltD def_transrec2 [OF normalize_def]) 
401 
done 

402 

403 
lemma normalize_increasing: 

46963  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 

13223  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: 

46963  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 

13223  452 

453 

454 
subsection {*The Alephs*} 

455 
text {*This is the wellknown transfinite enumeration of the cardinal 

456 
numbers.*} 

457 

21233  458 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset

459 
Aleph :: "i => i" where 
13223  460 
"Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))" 
461 

21233  462 
notation (xsymbols) 
463 
Aleph ("\<aleph>_" [90] 90) 

13223  464 

465 
lemma Card_Aleph [simp, intro]: 

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

467 
apply (erule trans_induct3) 

468 
apply (simp_all add: Card_csucc Card_nat Card_is_Ord 

469 
def_transrec2 [OF Aleph_def]) 

470 
done 

471 

472 
lemma Aleph_increasing: 

46963  473 
assumes ab: "a < b" shows "Aleph(a) < Aleph(b)" 
474 
proof  

475 
{ fix x 

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

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

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

479 
case 0 thus ?case by simp 

480 
next 

481 
case (succ b) 

482 
thus ?case 

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

484 
intro: lt_trans lt_csucc Card_is_Ord) 

485 
next 

486 
case (limit l) 

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

488 
by (blast intro: Limit_has_succ) 

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

490 
by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord) 

491 
thus ?case using limit 

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

493 
qed 

494 
} thus ?thesis using ab . 

495 
qed 

13223  496 

497 
theorem Normal_Aleph: "Normal(Aleph)" 

498 
apply (rule NormalI) 

499 
apply (blast intro!: Aleph_increasing) 

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

501 
done 

502 

503 
end 