author | wenzelm |
Fri, 04 Apr 2014 22:21:46 +0200 | |
changeset 56412 | 2dd33da970ea |
parent 46963 | 67da5904300a |
child 58871 | c399ae4b836f |
permissions | -rw-r--r-- |
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 |
North-Holland, 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 set-indexed 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 113--114.*} |
|
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 well-known 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 |