author | wenzelm |
Fri, 06 May 2011 17:52:08 +0200 | |
changeset 42711 | 159c4d1d4c42 |
parent 35762 | af3ff2ba4c54 |
child 46820 | c656222c4dc1 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Ordinal.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
435 | 3 |
Copyright 1994 University of Cambridge |
4 |
*) |
|
5 |
||
13356 | 6 |
header{*Transitive Sets and Ordinals*} |
7 |
||
16417 | 8 |
theory Ordinal imports WF Bool equalities begin |
13155 | 9 |
|
24893 | 10 |
definition |
11 |
Memrel :: "i=>i" where |
|
13155 | 12 |
"Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }" |
13 |
||
24893 | 14 |
definition |
15 |
Transset :: "i=>o" where |
|
13155 | 16 |
"Transset(i) == ALL x:i. x<=i" |
17 |
||
24893 | 18 |
definition |
19 |
Ord :: "i=>o" where |
|
13155 | 20 |
"Ord(i) == Transset(i) & (ALL x:i. Transset(x))" |
21 |
||
24893 | 22 |
definition |
23 |
lt :: "[i,i] => o" (infixl "<" 50) (*less-than on ordinals*) where |
|
13155 | 24 |
"i<j == i:j & Ord(j)" |
25 |
||
24893 | 26 |
definition |
27 |
Limit :: "i=>o" where |
|
13155 | 28 |
"Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)" |
2539 | 29 |
|
22808 | 30 |
abbreviation |
31 |
le (infixl "le" 50) where |
|
32 |
"x le y == x < succ(y)" |
|
435 | 33 |
|
22808 | 34 |
notation (xsymbols) |
35 |
le (infixl "\<le>" 50) |
|
435 | 36 |
|
22808 | 37 |
notation (HTML output) |
38 |
le (infixl "\<le>" 50) |
|
13155 | 39 |
|
40 |
||
13356 | 41 |
subsection{*Rules for Transset*} |
13155 | 42 |
|
13356 | 43 |
subsubsection{*Three Neat Characterisations of Transset*} |
13155 | 44 |
|
45 |
lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" |
|
46 |
by (unfold Transset_def, blast) |
|
47 |
||
48 |
lemma Transset_iff_Union_succ: "Transset(A) <-> Union(succ(A)) = A" |
|
49 |
apply (unfold Transset_def) |
|
50 |
apply (blast elim!: equalityE) |
|
51 |
done |
|
52 |
||
53 |
lemma Transset_iff_Union_subset: "Transset(A) <-> Union(A) <= A" |
|
54 |
by (unfold Transset_def, blast) |
|
55 |
||
13356 | 56 |
subsubsection{*Consequences of Downwards Closure*} |
13155 | 57 |
|
58 |
lemma Transset_doubleton_D: |
|
59 |
"[| Transset(C); {a,b}: C |] ==> a:C & b: C" |
|
60 |
by (unfold Transset_def, blast) |
|
61 |
||
62 |
lemma Transset_Pair_D: |
|
63 |
"[| Transset(C); <a,b>: C |] ==> a:C & b: C" |
|
64 |
apply (simp add: Pair_def) |
|
65 |
apply (blast dest: Transset_doubleton_D) |
|
66 |
done |
|
67 |
||
68 |
lemma Transset_includes_domain: |
|
69 |
"[| Transset(C); A*B <= C; b: B |] ==> A <= C" |
|
70 |
by (blast dest: Transset_Pair_D) |
|
71 |
||
72 |
lemma Transset_includes_range: |
|
73 |
"[| Transset(C); A*B <= C; a: A |] ==> B <= C" |
|
74 |
by (blast dest: Transset_Pair_D) |
|
75 |
||
13356 | 76 |
subsubsection{*Closure Properties*} |
13155 | 77 |
|
78 |
lemma Transset_0: "Transset(0)" |
|
79 |
by (unfold Transset_def, blast) |
|
80 |
||
81 |
lemma Transset_Un: |
|
82 |
"[| Transset(i); Transset(j) |] ==> Transset(i Un j)" |
|
83 |
by (unfold Transset_def, blast) |
|
84 |
||
85 |
lemma Transset_Int: |
|
86 |
"[| Transset(i); Transset(j) |] ==> Transset(i Int j)" |
|
87 |
by (unfold Transset_def, blast) |
|
88 |
||
89 |
lemma Transset_succ: "Transset(i) ==> Transset(succ(i))" |
|
90 |
by (unfold Transset_def, blast) |
|
91 |
||
92 |
lemma Transset_Pow: "Transset(i) ==> Transset(Pow(i))" |
|
93 |
by (unfold Transset_def, blast) |
|
94 |
||
95 |
lemma Transset_Union: "Transset(A) ==> Transset(Union(A))" |
|
96 |
by (unfold Transset_def, blast) |
|
97 |
||
98 |
lemma Transset_Union_family: |
|
99 |
"[| !!i. i:A ==> Transset(i) |] ==> Transset(Union(A))" |
|
100 |
by (unfold Transset_def, blast) |
|
101 |
||
102 |
lemma Transset_Inter_family: |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
103 |
"[| !!i. i:A ==> Transset(i) |] ==> Transset(Inter(A))" |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
104 |
by (unfold Inter_def Transset_def, blast) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
105 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
106 |
lemma Transset_UN: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
107 |
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
108 |
by (rule Transset_Union_family, auto) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
109 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
110 |
lemma Transset_INT: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
111 |
"(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
112 |
by (rule Transset_Inter_family, auto) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
113 |
|
13155 | 114 |
|
13356 | 115 |
subsection{*Lemmas for Ordinals*} |
13155 | 116 |
|
117 |
lemma OrdI: |
|
118 |
"[| Transset(i); !!x. x:i ==> Transset(x) |] ==> Ord(i)" |
|
119 |
by (simp add: Ord_def) |
|
120 |
||
121 |
lemma Ord_is_Transset: "Ord(i) ==> Transset(i)" |
|
122 |
by (simp add: Ord_def) |
|
123 |
||
124 |
lemma Ord_contains_Transset: |
|
125 |
"[| Ord(i); j:i |] ==> Transset(j) " |
|
126 |
by (unfold Ord_def, blast) |
|
127 |
||
128 |
||
129 |
lemma Ord_in_Ord: "[| Ord(i); j:i |] ==> Ord(j)" |
|
130 |
by (unfold Ord_def Transset_def, blast) |
|
131 |
||
13243 | 132 |
(*suitable for rewriting PROVIDED i has been fixed*) |
133 |
lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)" |
|
134 |
by (blast intro: Ord_in_Ord) |
|
135 |
||
13155 | 136 |
(* Ord(succ(j)) ==> Ord(j) *) |
137 |
lemmas Ord_succD = Ord_in_Ord [OF _ succI1] |
|
138 |
||
139 |
lemma Ord_subset_Ord: "[| Ord(i); Transset(j); j<=i |] ==> Ord(j)" |
|
140 |
by (simp add: Ord_def Transset_def, blast) |
|
141 |
||
142 |
lemma OrdmemD: "[| j:i; Ord(i) |] ==> j<=i" |
|
143 |
by (unfold Ord_def Transset_def, blast) |
|
144 |
||
145 |
lemma Ord_trans: "[| i:j; j:k; Ord(k) |] ==> i:k" |
|
146 |
by (blast dest: OrdmemD) |
|
147 |
||
148 |
lemma Ord_succ_subsetI: "[| i:j; Ord(j) |] ==> succ(i) <= j" |
|
149 |
by (blast dest: OrdmemD) |
|
150 |
||
151 |
||
13356 | 152 |
subsection{*The Construction of Ordinals: 0, succ, Union*} |
13155 | 153 |
|
154 |
lemma Ord_0 [iff,TC]: "Ord(0)" |
|
155 |
by (blast intro: OrdI Transset_0) |
|
156 |
||
157 |
lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" |
|
158 |
by (blast intro: OrdI Transset_succ Ord_is_Transset Ord_contains_Transset) |
|
159 |
||
160 |
lemmas Ord_1 = Ord_0 [THEN Ord_succ] |
|
161 |
||
162 |
lemma Ord_succ_iff [iff]: "Ord(succ(i)) <-> Ord(i)" |
|
163 |
by (blast intro: Ord_succ dest!: Ord_succD) |
|
164 |
||
13172 | 165 |
lemma Ord_Un [intro,simp,TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Un j)" |
13155 | 166 |
apply (unfold Ord_def) |
167 |
apply (blast intro!: Transset_Un) |
|
168 |
done |
|
169 |
||
170 |
lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i Int j)" |
|
171 |
apply (unfold Ord_def) |
|
172 |
apply (blast intro!: Transset_Int) |
|
173 |
done |
|
174 |
||
175 |
(*There is no set of all ordinals, for then it would contain itself*) |
|
176 |
lemma ON_class: "~ (ALL i. i:X <-> Ord(i))" |
|
177 |
apply (rule notI) |
|
13784 | 178 |
apply (frule_tac x = X in spec) |
13155 | 179 |
apply (safe elim!: mem_irrefl) |
180 |
apply (erule swap, rule OrdI [OF _ Ord_is_Transset]) |
|
181 |
apply (simp add: Transset_def) |
|
182 |
apply (blast intro: Ord_in_Ord)+ |
|
183 |
done |
|
184 |
||
13356 | 185 |
subsection{*< is 'less Than' for Ordinals*} |
13155 | 186 |
|
187 |
lemma ltI: "[| i:j; Ord(j) |] ==> i<j" |
|
188 |
by (unfold lt_def, blast) |
|
189 |
||
190 |
lemma ltE: |
|
191 |
"[| i<j; [| i:j; Ord(i); Ord(j) |] ==> P |] ==> P" |
|
192 |
apply (unfold lt_def) |
|
193 |
apply (blast intro: Ord_in_Ord) |
|
194 |
done |
|
195 |
||
196 |
lemma ltD: "i<j ==> i:j" |
|
197 |
by (erule ltE, assumption) |
|
198 |
||
199 |
lemma not_lt0 [simp]: "~ i<0" |
|
200 |
by (unfold lt_def, blast) |
|
201 |
||
202 |
lemma lt_Ord: "j<i ==> Ord(j)" |
|
203 |
by (erule ltE, assumption) |
|
204 |
||
205 |
lemma lt_Ord2: "j<i ==> Ord(i)" |
|
206 |
by (erule ltE, assumption) |
|
207 |
||
208 |
(* "ja le j ==> Ord(j)" *) |
|
209 |
lemmas le_Ord2 = lt_Ord2 [THEN Ord_succD] |
|
210 |
||
211 |
(* i<0 ==> R *) |
|
212 |
lemmas lt0E = not_lt0 [THEN notE, elim!] |
|
213 |
||
214 |
lemma lt_trans: "[| i<j; j<k |] ==> i<k" |
|
215 |
by (blast intro!: ltI elim!: ltE intro: Ord_trans) |
|
216 |
||
217 |
lemma lt_not_sym: "i<j ==> ~ (j<i)" |
|
218 |
apply (unfold lt_def) |
|
219 |
apply (blast elim: mem_asym) |
|
220 |
done |
|
221 |
||
222 |
(* [| i<j; ~P ==> j<i |] ==> P *) |
|
223 |
lemmas lt_asym = lt_not_sym [THEN swap] |
|
224 |
||
225 |
lemma lt_irrefl [elim!]: "i<i ==> P" |
|
226 |
by (blast intro: lt_asym) |
|
227 |
||
228 |
lemma lt_not_refl: "~ i<i" |
|
229 |
apply (rule notI) |
|
230 |
apply (erule lt_irrefl) |
|
231 |
done |
|
232 |
||
233 |
||
234 |
(** le is less than or equals; recall i le j abbrevs i<succ(j) !! **) |
|
235 |
||
236 |
lemma le_iff: "i le j <-> i<j | (i=j & Ord(j))" |
|
237 |
by (unfold lt_def, blast) |
|
238 |
||
239 |
(*Equivalently, i<j ==> i < succ(j)*) |
|
240 |
lemma leI: "i<j ==> i le j" |
|
241 |
by (simp (no_asm_simp) add: le_iff) |
|
242 |
||
243 |
lemma le_eqI: "[| i=j; Ord(j) |] ==> i le j" |
|
244 |
by (simp (no_asm_simp) add: le_iff) |
|
245 |
||
246 |
lemmas le_refl = refl [THEN le_eqI] |
|
247 |
||
248 |
lemma le_refl_iff [iff]: "i le i <-> Ord(i)" |
|
249 |
by (simp (no_asm_simp) add: lt_not_refl le_iff) |
|
250 |
||
251 |
lemma leCI: "(~ (i=j & Ord(j)) ==> i<j) ==> i le j" |
|
252 |
by (simp add: le_iff, blast) |
|
253 |
||
254 |
lemma leE: |
|
255 |
"[| i le j; i<j ==> P; [| i=j; Ord(j) |] ==> P |] ==> P" |
|
256 |
by (simp add: le_iff, blast) |
|
257 |
||
258 |
lemma le_anti_sym: "[| i le j; j le i |] ==> i=j" |
|
259 |
apply (simp add: le_iff) |
|
260 |
apply (blast elim: lt_asym) |
|
261 |
done |
|
262 |
||
263 |
lemma le0_iff [simp]: "i le 0 <-> i=0" |
|
264 |
by (blast elim!: leE) |
|
265 |
||
266 |
lemmas le0D = le0_iff [THEN iffD1, dest!] |
|
267 |
||
13356 | 268 |
subsection{*Natural Deduction Rules for Memrel*} |
13155 | 269 |
|
270 |
(*The lemmas MemrelI/E give better speed than [iff] here*) |
|
271 |
lemma Memrel_iff [simp]: "<a,b> : Memrel(A) <-> a:b & a:A & b:A" |
|
272 |
by (unfold Memrel_def, blast) |
|
273 |
||
274 |
lemma MemrelI [intro!]: "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)" |
|
275 |
by auto |
|
276 |
||
277 |
lemma MemrelE [elim!]: |
|
278 |
"[| <a,b> : Memrel(A); |
|
279 |
[| a: A; b: A; a:b |] ==> P |] |
|
280 |
==> P" |
|
281 |
by auto |
|
282 |
||
283 |
lemma Memrel_type: "Memrel(A) <= A*A" |
|
284 |
by (unfold Memrel_def, blast) |
|
285 |
||
286 |
lemma Memrel_mono: "A<=B ==> Memrel(A) <= Memrel(B)" |
|
287 |
by (unfold Memrel_def, blast) |
|
288 |
||
289 |
lemma Memrel_0 [simp]: "Memrel(0) = 0" |
|
290 |
by (unfold Memrel_def, blast) |
|
291 |
||
292 |
lemma Memrel_1 [simp]: "Memrel(1) = 0" |
|
293 |
by (unfold Memrel_def, blast) |
|
294 |
||
13269 | 295 |
lemma relation_Memrel: "relation(Memrel(A))" |
14864 | 296 |
by (simp add: relation_def Memrel_def) |
13269 | 297 |
|
13155 | 298 |
(*The membership relation (as a set) is well-founded. |
299 |
Proof idea: show A<=B by applying the foundation axiom to A-B *) |
|
300 |
lemma wf_Memrel: "wf(Memrel(A))" |
|
301 |
apply (unfold wf_def) |
|
302 |
apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) |
|
303 |
done |
|
304 |
||
13396 | 305 |
text{*The premise @{term "Ord(i)"} does not suffice.*} |
13155 | 306 |
lemma trans_Memrel: |
307 |
"Ord(i) ==> trans(Memrel(i))" |
|
308 |
by (unfold Ord_def Transset_def trans_def, blast) |
|
309 |
||
13396 | 310 |
text{*However, the following premise is strong enough.*} |
311 |
lemma Transset_trans_Memrel: |
|
312 |
"\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))" |
|
313 |
by (unfold Transset_def trans_def, blast) |
|
314 |
||
13155 | 315 |
(*If Transset(A) then Memrel(A) internalizes the membership relation below A*) |
316 |
lemma Transset_Memrel_iff: |
|
317 |
"Transset(A) ==> <a,b> : Memrel(A) <-> a:b & b:A" |
|
318 |
by (unfold Transset_def, blast) |
|
319 |
||
320 |
||
13356 | 321 |
subsection{*Transfinite Induction*} |
13155 | 322 |
|
323 |
(*Epsilon induction over a transitive set*) |
|
324 |
lemma Transset_induct: |
|
325 |
"[| i: k; Transset(k); |
|
326 |
!!x.[| x: k; ALL y:x. P(y) |] ==> P(x) |] |
|
327 |
==> P(i)" |
|
328 |
apply (simp add: Transset_def) |
|
13269 | 329 |
apply (erule wf_Memrel [THEN wf_induct2], blast+) |
13155 | 330 |
done |
331 |
||
332 |
(*Induction over an ordinal*) |
|
13534 | 333 |
lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset] |
334 |
lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2] |
|
13155 | 335 |
|
336 |
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*) |
|
337 |
||
13534 | 338 |
lemma trans_induct [consumes 1]: |
13155 | 339 |
"[| Ord(i); |
340 |
!!x.[| Ord(x); ALL y:x. P(y) |] ==> P(x) |] |
|
341 |
==> P(i)" |
|
342 |
apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) |
|
343 |
apply (blast intro: Ord_succ [THEN Ord_in_Ord]) |
|
344 |
done |
|
345 |
||
13534 | 346 |
lemmas trans_induct_rule = trans_induct [rule_format, consumes 1] |
347 |
||
13155 | 348 |
|
349 |
(*** Fundamental properties of the epsilon ordering (< on ordinals) ***) |
|
350 |
||
351 |
||
13356 | 352 |
subsubsection{*Proving That < is a Linear Ordering on the Ordinals*} |
13155 | 353 |
|
354 |
lemma Ord_linear [rule_format]: |
|
355 |
"Ord(i) ==> (ALL j. Ord(j) --> i:j | i=j | j:i)" |
|
356 |
apply (erule trans_induct) |
|
357 |
apply (rule impI [THEN allI]) |
|
358 |
apply (erule_tac i=j in trans_induct) |
|
359 |
apply (blast dest: Ord_trans) |
|
360 |
done |
|
361 |
||
362 |
(*The trichotomy law for ordinals!*) |
|
363 |
lemma Ord_linear_lt: |
|
364 |
"[| Ord(i); Ord(j); i<j ==> P; i=j ==> P; j<i ==> P |] ==> P" |
|
365 |
apply (simp add: lt_def) |
|
366 |
apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+) |
|
367 |
done |
|
368 |
||
369 |
lemma Ord_linear2: |
|
370 |
"[| Ord(i); Ord(j); i<j ==> P; j le i ==> P |] ==> P" |
|
13784 | 371 |
apply (rule_tac i = i and j = j in Ord_linear_lt) |
13155 | 372 |
apply (blast intro: leI le_eqI sym ) + |
373 |
done |
|
374 |
||
375 |
lemma Ord_linear_le: |
|
376 |
"[| Ord(i); Ord(j); i le j ==> P; j le i ==> P |] ==> P" |
|
13784 | 377 |
apply (rule_tac i = i and j = j in Ord_linear_lt) |
13155 | 378 |
apply (blast intro: leI le_eqI ) + |
379 |
done |
|
380 |
||
381 |
lemma le_imp_not_lt: "j le i ==> ~ i<j" |
|
382 |
by (blast elim!: leE elim: lt_asym) |
|
383 |
||
384 |
lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j le i" |
|
13784 | 385 |
by (rule_tac i = i and j = j in Ord_linear2, auto) |
13155 | 386 |
|
13356 | 387 |
subsubsection{*Some Rewrite Rules for <, le*} |
13155 | 388 |
|
389 |
lemma Ord_mem_iff_lt: "Ord(j) ==> i:j <-> i<j" |
|
390 |
by (unfold lt_def, blast) |
|
391 |
||
392 |
lemma not_lt_iff_le: "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j le i" |
|
393 |
by (blast dest: le_imp_not_lt not_lt_imp_le) |
|
2540 | 394 |
|
13155 | 395 |
lemma not_le_iff_lt: "[| Ord(i); Ord(j) |] ==> ~ i le j <-> j<i" |
396 |
by (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
|
397 |
||
398 |
(*This is identical to 0<succ(i) *) |
|
399 |
lemma Ord_0_le: "Ord(i) ==> 0 le i" |
|
400 |
by (erule not_lt_iff_le [THEN iffD1], auto) |
|
401 |
||
402 |
lemma Ord_0_lt: "[| Ord(i); i~=0 |] ==> 0<i" |
|
403 |
apply (erule not_le_iff_lt [THEN iffD1]) |
|
404 |
apply (rule Ord_0, blast) |
|
405 |
done |
|
406 |
||
407 |
lemma Ord_0_lt_iff: "Ord(i) ==> i~=0 <-> 0<i" |
|
408 |
by (blast intro: Ord_0_lt) |
|
409 |
||
410 |
||
13356 | 411 |
subsection{*Results about Less-Than or Equals*} |
13155 | 412 |
|
413 |
(** For ordinals, j<=i (subset) implies j le i (less-than or equals) **) |
|
414 |
||
415 |
lemma zero_le_succ_iff [iff]: "0 le succ(x) <-> Ord(x)" |
|
416 |
by (blast intro: Ord_0_le elim: ltE) |
|
417 |
||
418 |
lemma subset_imp_le: "[| j<=i; Ord(i); Ord(j) |] ==> j le i" |
|
13269 | 419 |
apply (rule not_lt_iff_le [THEN iffD1], assumption+) |
13155 | 420 |
apply (blast elim: ltE mem_irrefl) |
421 |
done |
|
422 |
||
423 |
lemma le_imp_subset: "i le j ==> i<=j" |
|
424 |
by (blast dest: OrdmemD elim: ltE leE) |
|
425 |
||
426 |
lemma le_subset_iff: "j le i <-> j<=i & Ord(i) & Ord(j)" |
|
427 |
by (blast dest: subset_imp_le le_imp_subset elim: ltE) |
|
428 |
||
429 |
lemma le_succ_iff: "i le succ(j) <-> i le j | i=succ(j) & Ord(i)" |
|
430 |
apply (simp (no_asm) add: le_iff) |
|
431 |
apply blast |
|
432 |
done |
|
433 |
||
434 |
(*Just a variant of subset_imp_le*) |
|
435 |
lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j le i" |
|
436 |
by (blast intro: not_lt_imp_le dest: lt_irrefl) |
|
437 |
||
13356 | 438 |
subsubsection{*Transitivity Laws*} |
13155 | 439 |
|
440 |
lemma lt_trans1: "[| i le j; j<k |] ==> i<k" |
|
441 |
by (blast elim!: leE intro: lt_trans) |
|
442 |
||
443 |
lemma lt_trans2: "[| i<j; j le k |] ==> i<k" |
|
444 |
by (blast elim!: leE intro: lt_trans) |
|
445 |
||
446 |
lemma le_trans: "[| i le j; j le k |] ==> i le k" |
|
447 |
by (blast intro: lt_trans1) |
|
448 |
||
449 |
lemma succ_leI: "i<j ==> succ(i) le j" |
|
450 |
apply (rule not_lt_iff_le [THEN iffD1]) |
|
451 |
apply (blast elim: ltE leE lt_asym)+ |
|
452 |
done |
|
453 |
||
454 |
(*Identical to succ(i) < succ(j) ==> i<j *) |
|
455 |
lemma succ_leE: "succ(i) le j ==> i<j" |
|
456 |
apply (rule not_le_iff_lt [THEN iffD1]) |
|
457 |
apply (blast elim: ltE leE lt_asym)+ |
|
458 |
done |
|
459 |
||
460 |
lemma succ_le_iff [iff]: "succ(i) le j <-> i<j" |
|
461 |
by (blast intro: succ_leI succ_leE) |
|
462 |
||
463 |
lemma succ_le_imp_le: "succ(i) le succ(j) ==> i le j" |
|
464 |
by (blast dest!: succ_leE) |
|
465 |
||
466 |
lemma lt_subset_trans: "[| i <= j; j<k; Ord(i) |] ==> i<k" |
|
467 |
apply (rule subset_imp_le [THEN lt_trans1]) |
|
468 |
apply (blast intro: elim: ltE) + |
|
469 |
done |
|
470 |
||
13172 | 471 |
lemma lt_imp_0_lt: "j<i ==> 0<i" |
472 |
by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) |
|
473 |
||
13243 | 474 |
lemma succ_lt_iff: "succ(i) < j <-> i<j & succ(i) \<noteq> j" |
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
475 |
apply auto |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
476 |
apply (blast intro: lt_trans le_refl dest: lt_Ord) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
477 |
apply (frule lt_Ord) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
478 |
apply (rule not_le_iff_lt [THEN iffD1]) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
479 |
apply (blast intro: lt_Ord2) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
480 |
apply blast |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
481 |
apply (simp add: lt_Ord lt_Ord2 le_iff) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
482 |
apply (blast dest: lt_asym) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
483 |
done |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
484 |
|
13243 | 485 |
lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j" |
486 |
apply (insert succ_le_iff [of i j]) |
|
487 |
apply (simp add: lt_def) |
|
488 |
done |
|
489 |
||
13356 | 490 |
subsubsection{*Union and Intersection*} |
13155 | 491 |
|
492 |
lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j" |
|
493 |
by (rule Un_upper1 [THEN subset_imp_le], auto) |
|
494 |
||
495 |
lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j le i Un j" |
|
496 |
by (rule Un_upper2 [THEN subset_imp_le], auto) |
|
497 |
||
498 |
(*Replacing k by succ(k') yields the similar rule for le!*) |
|
499 |
lemma Un_least_lt: "[| i<k; j<k |] ==> i Un j < k" |
|
13784 | 500 |
apply (rule_tac i = i and j = j in Ord_linear_le) |
13155 | 501 |
apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) |
502 |
done |
|
503 |
||
504 |
lemma Un_least_lt_iff: "[| Ord(i); Ord(j) |] ==> i Un j < k <-> i<k & j<k" |
|
505 |
apply (safe intro!: Un_least_lt) |
|
506 |
apply (rule_tac [2] Un_upper2_le [THEN lt_trans1]) |
|
507 |
apply (rule Un_upper1_le [THEN lt_trans1], auto) |
|
508 |
done |
|
509 |
||
510 |
lemma Un_least_mem_iff: |
|
511 |
"[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k <-> i:k & j:k" |
|
512 |
apply (insert Un_least_lt_iff [of i j k]) |
|
513 |
apply (simp add: lt_def) |
|
514 |
done |
|
515 |
||
516 |
(*Replacing k by succ(k') yields the similar rule for le!*) |
|
517 |
lemma Int_greatest_lt: "[| i<k; j<k |] ==> i Int j < k" |
|
13784 | 518 |
apply (rule_tac i = i and j = j in Ord_linear_le) |
13155 | 519 |
apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) |
520 |
done |
|
521 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
522 |
lemma Ord_Un_if: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
523 |
"[| Ord(i); Ord(j) |] ==> i \<union> j = (if j<i then i else j)" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
524 |
by (simp add: not_lt_iff_le le_imp_subset leI |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
525 |
subset_Un_iff [symmetric] subset_Un_iff2 [symmetric]) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
526 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
527 |
lemma succ_Un_distrib: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
528 |
"[| Ord(i); Ord(j) |] ==> succ(i \<union> j) = succ(i) \<union> succ(j)" |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
529 |
by (simp add: Ord_Un_if lt_Ord le_Ord2) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
530 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
531 |
lemma lt_Un_iff: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
532 |
"[| Ord(i); Ord(j) |] ==> k < i \<union> j <-> k < i | k < j"; |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
533 |
apply (simp add: Ord_Un_if not_lt_iff_le) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
534 |
apply (blast intro: leI lt_trans2)+ |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
535 |
done |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
536 |
|
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
537 |
lemma le_Un_iff: |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
538 |
"[| Ord(i); Ord(j) |] ==> k \<le> i \<union> j <-> k \<le> i | k \<le> j"; |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
539 |
by (simp add: succ_Un_distrib lt_Un_iff [symmetric]) |
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
540 |
|
13172 | 541 |
lemma Un_upper1_lt: "[|k < i; Ord(j)|] ==> k < i Un j" |
542 |
by (simp add: lt_Un_iff lt_Ord2) |
|
543 |
||
544 |
lemma Un_upper2_lt: "[|k < j; Ord(i)|] ==> k < i Un j" |
|
545 |
by (simp add: lt_Un_iff lt_Ord2) |
|
546 |
||
547 |
(*See also Transset_iff_Union_succ*) |
|
548 |
lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" |
|
549 |
by (blast intro: Ord_trans) |
|
550 |
||
13162
660a71e712af
New theorems from Constructible, and moving some Isar material from Main
paulson
parents:
13155
diff
changeset
|
551 |
|
13356 | 552 |
subsection{*Results about Limits*} |
13155 | 553 |
|
13172 | 554 |
lemma Ord_Union [intro,simp,TC]: "[| !!i. i:A ==> Ord(i) |] ==> Ord(Union(A))" |
13155 | 555 |
apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
556 |
apply (blast intro: Ord_contains_Transset)+ |
|
557 |
done |
|
558 |
||
13172 | 559 |
lemma Ord_UN [intro,simp,TC]: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
560 |
"[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))" |
13155 | 561 |
by (rule Ord_Union, blast) |
562 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
563 |
lemma Ord_Inter [intro,simp,TC]: |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
564 |
"[| !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))" |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
565 |
apply (rule Transset_Inter_family [THEN OrdI]) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
566 |
apply (blast intro: Ord_is_Transset) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
567 |
apply (simp add: Inter_def) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
568 |
apply (blast intro: Ord_contains_Transset) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
569 |
done |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
570 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
571 |
lemma Ord_INT [intro,simp,TC]: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
572 |
"[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))" |
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
573 |
by (rule Ord_Inter, blast) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
574 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13172
diff
changeset
|
575 |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
576 |
(* No < version; consider (\<Union>i\<in>nat.i)=nat *) |
13155 | 577 |
lemma UN_least_le: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
578 |
"[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (\<Union>x\<in>A. b(x)) le i" |
13155 | 579 |
apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le]) |
580 |
apply (blast intro: Ord_UN elim: ltE)+ |
|
581 |
done |
|
582 |
||
583 |
lemma UN_succ_least_lt: |
|
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
584 |
"[| j<i; !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i" |
13155 | 585 |
apply (rule ltE, assumption) |
586 |
apply (rule UN_least_le [THEN lt_trans2]) |
|
587 |
apply (blast intro: succ_leI)+ |
|
588 |
done |
|
589 |
||
13172 | 590 |
lemma UN_upper_lt: |
591 |
"[| a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i < (\<Union>x\<in>A. b(x))" |
|
592 |
by (unfold lt_def, blast) |
|
593 |
||
13155 | 594 |
lemma UN_upper_le: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
595 |
"[| a: A; i le b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i le (\<Union>x\<in>A. b(x))" |
13155 | 596 |
apply (frule ltD) |
597 |
apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le]) |
|
598 |
apply (blast intro: lt_Ord UN_upper)+ |
|
599 |
done |
|
600 |
||
13172 | 601 |
lemma lt_Union_iff: "\<forall>i\<in>A. Ord(i) ==> (j < \<Union>(A)) <-> (\<exists>i\<in>A. j<i)" |
602 |
by (auto simp: lt_def Ord_Union) |
|
603 |
||
604 |
lemma Union_upper_le: |
|
605 |
"[| j: J; i\<le>j; Ord(\<Union>(J)) |] ==> i \<le> \<Union>J" |
|
606 |
apply (subst Union_eq_UN) |
|
607 |
apply (rule UN_upper_le, auto) |
|
608 |
done |
|
609 |
||
13155 | 610 |
lemma le_implies_UN_le_UN: |
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
611 |
"[| !!x. x:A ==> c(x) le d(x) |] ==> (\<Union>x\<in>A. c(x)) le (\<Union>x\<in>A. d(x))" |
13155 | 612 |
apply (rule UN_least_le) |
613 |
apply (rule_tac [2] UN_upper_le) |
|
614 |
apply (blast intro: Ord_UN le_Ord2)+ |
|
615 |
done |
|
616 |
||
13615
449a70d88b38
Numerous cosmetic changes, prompted by the new simplifier
paulson
parents:
13544
diff
changeset
|
617 |
lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i" |
13155 | 618 |
by (blast intro: Ord_trans) |
619 |
||
620 |
(*Holds for all transitive sets, not just ordinals*) |
|
621 |
lemma Ord_Union_subset: "Ord(i) ==> Union(i) <= i" |
|
622 |
by (blast intro: Ord_trans) |
|
623 |
||
624 |
||
13356 | 625 |
subsection{*Limit Ordinals -- General Properties*} |
13155 | 626 |
|
627 |
lemma Limit_Union_eq: "Limit(i) ==> Union(i) = i" |
|
628 |
apply (unfold Limit_def) |
|
629 |
apply (fast intro!: ltI elim!: ltE elim: Ord_trans) |
|
630 |
done |
|
631 |
||
632 |
lemma Limit_is_Ord: "Limit(i) ==> Ord(i)" |
|
633 |
apply (unfold Limit_def) |
|
634 |
apply (erule conjunct1) |
|
635 |
done |
|
636 |
||
637 |
lemma Limit_has_0: "Limit(i) ==> 0 < i" |
|
638 |
apply (unfold Limit_def) |
|
639 |
apply (erule conjunct2 [THEN conjunct1]) |
|
640 |
done |
|
641 |
||
13544 | 642 |
lemma Limit_nonzero: "Limit(i) ==> i ~= 0" |
643 |
by (drule Limit_has_0, blast) |
|
644 |
||
13155 | 645 |
lemma Limit_has_succ: "[| Limit(i); j<i |] ==> succ(j) < i" |
646 |
by (unfold Limit_def, blast) |
|
647 |
||
13544 | 648 |
lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)" |
649 |
apply (safe intro!: Limit_has_succ) |
|
650 |
apply (frule lt_Ord) |
|
651 |
apply (blast intro: lt_trans) |
|
652 |
done |
|
653 |
||
13172 | 654 |
lemma zero_not_Limit [iff]: "~ Limit(0)" |
655 |
by (simp add: Limit_def) |
|
656 |
||
657 |
lemma Limit_has_1: "Limit(i) ==> 1 < i" |
|
658 |
by (blast intro: Limit_has_0 Limit_has_succ) |
|
659 |
||
660 |
lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)" |
|
13544 | 661 |
apply (unfold Limit_def, simp add: lt_Ord2, clarify) |
13172 | 662 |
apply (drule_tac i=y in ltD) |
663 |
apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2) |
|
664 |
done |
|
665 |
||
13155 | 666 |
lemma non_succ_LimitI: |
667 |
"[| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)" |
|
668 |
apply (unfold Limit_def) |
|
669 |
apply (safe del: subsetI) |
|
670 |
apply (rule_tac [2] not_le_iff_lt [THEN iffD1]) |
|
671 |
apply (simp_all add: lt_Ord lt_Ord2) |
|
672 |
apply (blast elim: leE lt_asym) |
|
673 |
done |
|
674 |
||
675 |
lemma succ_LimitE [elim!]: "Limit(succ(i)) ==> P" |
|
676 |
apply (rule lt_irrefl) |
|
677 |
apply (rule Limit_has_succ, assumption) |
|
678 |
apply (erule Limit_is_Ord [THEN Ord_succD, THEN le_refl]) |
|
679 |
done |
|
680 |
||
681 |
lemma not_succ_Limit [simp]: "~ Limit(succ(i))" |
|
682 |
by blast |
|
683 |
||
684 |
lemma Limit_le_succD: "[| Limit(i); i le succ(j) |] ==> i le j" |
|
685 |
by (blast elim!: leE) |
|
686 |
||
13172 | 687 |
|
13356 | 688 |
subsubsection{*Traditional 3-Way Case Analysis on Ordinals*} |
13155 | 689 |
|
690 |
lemma Ord_cases_disj: "Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)" |
|
691 |
by (blast intro!: non_succ_LimitI Ord_0_lt) |
|
692 |
||
693 |
lemma Ord_cases: |
|
694 |
"[| Ord(i); |
|
695 |
i=0 ==> P; |
|
696 |
!!j. [| Ord(j); i=succ(j) |] ==> P; |
|
697 |
Limit(i) ==> P |
|
698 |
|] ==> P" |
|
699 |
by (drule Ord_cases_disj, blast) |
|
700 |
||
13534 | 701 |
lemma trans_induct3 [case_names 0 succ limit, consumes 1]: |
13155 | 702 |
"[| Ord(i); |
703 |
P(0); |
|
704 |
!!x. [| Ord(x); P(x) |] ==> P(succ(x)); |
|
705 |
!!x. [| Limit(x); ALL y:x. P(y) |] ==> P(x) |
|
706 |
|] ==> P(i)" |
|
707 |
apply (erule trans_induct) |
|
708 |
apply (erule Ord_cases, blast+) |
|
709 |
done |
|
710 |
||
13534 | 711 |
lemmas trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1] |
712 |
||
13172 | 713 |
text{*A set of ordinals is either empty, contains its own union, or its |
714 |
union is a limit ordinal.*} |
|
715 |
lemma Ord_set_cases: |
|
716 |
"\<forall>i\<in>I. Ord(i) ==> I=0 \<or> \<Union>(I) \<in> I \<or> (\<Union>(I) \<notin> I \<and> Limit(\<Union>(I)))" |
|
717 |
apply (clarify elim!: not_emptyE) |
|
718 |
apply (cases "\<Union>(I)" rule: Ord_cases) |
|
719 |
apply (blast intro: Ord_Union) |
|
720 |
apply (blast intro: subst_elem) |
|
721 |
apply auto |
|
722 |
apply (clarify elim!: equalityE succ_subsetE) |
|
723 |
apply (simp add: Union_subset_iff) |
|
724 |
apply (subgoal_tac "B = succ(j)", blast) |
|
725 |
apply (rule le_anti_sym) |
|
726 |
apply (simp add: le_subset_iff) |
|
727 |
apply (simp add: ltI) |
|
728 |
done |
|
729 |
||
730 |
text{*If the union of a set of ordinals is a successor, then it is |
|
731 |
an element of that set.*} |
|
732 |
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
|
733 |
by (drule Ord_set_cases, auto) |
|
734 |
||
735 |
lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)" |
|
736 |
apply (simp add: Limit_def lt_def) |
|
737 |
apply (blast intro!: equalityI) |
|
738 |
done |
|
739 |
||
435 | 740 |
end |