1 (* Title: ZF/Ordinal.thy |
1 (* Title: ZF/Ordinal.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section{*Transitive Sets and Ordinals*} |
6 section\<open>Transitive Sets and Ordinals\<close> |
7 |
7 |
8 theory Ordinal imports WF Bool equalities begin |
8 theory Ordinal imports WF Bool equalities begin |
9 |
9 |
10 definition |
10 definition |
11 Memrel :: "i=>i" where |
11 Memrel :: "i=>i" where |
36 |
36 |
37 notation (HTML output) |
37 notation (HTML output) |
38 le (infixl "\<le>" 50) |
38 le (infixl "\<le>" 50) |
39 |
39 |
40 |
40 |
41 subsection{*Rules for Transset*} |
41 subsection\<open>Rules for Transset\<close> |
42 |
42 |
43 subsubsection{*Three Neat Characterisations of Transset*} |
43 subsubsection\<open>Three Neat Characterisations of Transset\<close> |
44 |
44 |
45 lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" |
45 lemma Transset_iff_Pow: "Transset(A) <-> A<=Pow(A)" |
46 by (unfold Transset_def, blast) |
46 by (unfold Transset_def, blast) |
47 |
47 |
48 lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A" |
48 lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A" |
51 done |
51 done |
52 |
52 |
53 lemma Transset_iff_Union_subset: "Transset(A) <-> \<Union>(A) \<subseteq> A" |
53 lemma Transset_iff_Union_subset: "Transset(A) <-> \<Union>(A) \<subseteq> A" |
54 by (unfold Transset_def, blast) |
54 by (unfold Transset_def, blast) |
55 |
55 |
56 subsubsection{*Consequences of Downwards Closure*} |
56 subsubsection\<open>Consequences of Downwards Closure\<close> |
57 |
57 |
58 lemma Transset_doubleton_D: |
58 lemma Transset_doubleton_D: |
59 "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C" |
59 "[| Transset(C); {a,b}: C |] ==> a\<in>C & b\<in>C" |
60 by (unfold Transset_def, blast) |
60 by (unfold Transset_def, blast) |
61 |
61 |
71 |
71 |
72 lemma Transset_includes_range: |
72 lemma Transset_includes_range: |
73 "[| Transset(C); A*B \<subseteq> C; a \<in> A |] ==> B \<subseteq> C" |
73 "[| Transset(C); A*B \<subseteq> C; a \<in> A |] ==> B \<subseteq> C" |
74 by (blast dest: Transset_Pair_D) |
74 by (blast dest: Transset_Pair_D) |
75 |
75 |
76 subsubsection{*Closure Properties*} |
76 subsubsection\<open>Closure Properties\<close> |
77 |
77 |
78 lemma Transset_0: "Transset(0)" |
78 lemma Transset_0: "Transset(0)" |
79 by (unfold Transset_def, blast) |
79 by (unfold Transset_def, blast) |
80 |
80 |
81 lemma Transset_Un: |
81 lemma Transset_Un: |
110 lemma Transset_INT: |
110 lemma Transset_INT: |
111 "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))" |
111 "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))" |
112 by (rule Transset_Inter_family, auto) |
112 by (rule Transset_Inter_family, auto) |
113 |
113 |
114 |
114 |
115 subsection{*Lemmas for Ordinals*} |
115 subsection\<open>Lemmas for Ordinals\<close> |
116 |
116 |
117 lemma OrdI: |
117 lemma OrdI: |
118 "[| Transset(i); !!x. x\<in>i ==> Transset(x) |] ==> Ord(i)" |
118 "[| Transset(i); !!x. x\<in>i ==> Transset(x) |] ==> Ord(i)" |
119 by (simp add: Ord_def) |
119 by (simp add: Ord_def) |
120 |
120 |
147 |
147 |
148 lemma Ord_succ_subsetI: "[| i\<in>j; Ord(j) |] ==> succ(i) \<subseteq> j" |
148 lemma Ord_succ_subsetI: "[| i\<in>j; Ord(j) |] ==> succ(i) \<subseteq> j" |
149 by (blast dest: OrdmemD) |
149 by (blast dest: OrdmemD) |
150 |
150 |
151 |
151 |
152 subsection{*The Construction of Ordinals: 0, succ, Union*} |
152 subsection\<open>The Construction of Ordinals: 0, succ, Union\<close> |
153 |
153 |
154 lemma Ord_0 [iff,TC]: "Ord(0)" |
154 lemma Ord_0 [iff,TC]: "Ord(0)" |
155 by (blast intro: OrdI Transset_0) |
155 by (blast intro: OrdI Transset_0) |
156 |
156 |
157 lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" |
157 lemma Ord_succ [TC]: "Ord(i) ==> Ord(succ(i))" |
170 lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<inter> j)" |
170 lemma Ord_Int [TC]: "[| Ord(i); Ord(j) |] ==> Ord(i \<inter> j)" |
171 apply (unfold Ord_def) |
171 apply (unfold Ord_def) |
172 apply (blast intro!: Transset_Int) |
172 apply (blast intro!: Transset_Int) |
173 done |
173 done |
174 |
174 |
175 text{*There is no set of all ordinals, for then it would contain itself*} |
175 text\<open>There is no set of all ordinals, for then it would contain itself\<close> |
176 lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))" |
176 lemma ON_class: "~ (\<forall>i. i\<in>X <-> Ord(i))" |
177 proof (rule notI) |
177 proof (rule notI) |
178 assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)" |
178 assume X: "\<forall>i. i \<in> X \<longleftrightarrow> Ord(i)" |
179 have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X" |
179 have "\<forall>x y. x\<in>X \<longrightarrow> y\<in>x \<longrightarrow> y\<in>X" |
180 by (simp add: X, blast intro: Ord_in_Ord) |
180 by (simp add: X, blast intro: Ord_in_Ord) |
185 ultimately have "Ord(X)" by (rule OrdI) |
185 ultimately have "Ord(X)" by (rule OrdI) |
186 hence "X \<in> X" by (simp add: X) |
186 hence "X \<in> X" by (simp add: X) |
187 thus "False" by (rule mem_irrefl) |
187 thus "False" by (rule mem_irrefl) |
188 qed |
188 qed |
189 |
189 |
190 subsection{*< is 'less Than' for Ordinals*} |
190 subsection\<open>< is 'less Than' for Ordinals\<close> |
191 |
191 |
192 lemma ltI: "[| i\<in>j; Ord(j) |] ==> i<j" |
192 lemma ltI: "[| i\<in>j; Ord(j) |] ==> i<j" |
193 by (unfold lt_def, blast) |
193 by (unfold lt_def, blast) |
194 |
194 |
195 lemma ltE: |
195 lemma ltE: |
234 apply (rule notI) |
234 apply (rule notI) |
235 apply (erule lt_irrefl) |
235 apply (erule lt_irrefl) |
236 done |
236 done |
237 |
237 |
238 |
238 |
239 text{* Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !! *} |
239 text\<open>Recall that @{term"i \<le> j"} abbreviates @{term"i<succ(j)"} !!\<close> |
240 |
240 |
241 lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))" |
241 lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))" |
242 by (unfold lt_def, blast) |
242 by (unfold lt_def, blast) |
243 |
243 |
244 (*Equivalently, i<j ==> i < succ(j)*) |
244 (*Equivalently, i<j ==> i < succ(j)*) |
268 lemma le0_iff [simp]: "i \<le> 0 <-> i=0" |
268 lemma le0_iff [simp]: "i \<le> 0 <-> i=0" |
269 by (blast elim!: leE) |
269 by (blast elim!: leE) |
270 |
270 |
271 lemmas le0D = le0_iff [THEN iffD1, dest!] |
271 lemmas le0D = le0_iff [THEN iffD1, dest!] |
272 |
272 |
273 subsection{*Natural Deduction Rules for Memrel*} |
273 subsection\<open>Natural Deduction Rules for Memrel\<close> |
274 |
274 |
275 (*The lemmas MemrelI/E give better speed than [iff] here*) |
275 (*The lemmas MemrelI/E give better speed than [iff] here*) |
276 lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A" |
276 lemma Memrel_iff [simp]: "<a,b> \<in> Memrel(A) <-> a\<in>b & a\<in>A & b\<in>A" |
277 by (unfold Memrel_def, blast) |
277 by (unfold Memrel_def, blast) |
278 |
278 |
305 lemma wf_Memrel: "wf(Memrel(A))" |
305 lemma wf_Memrel: "wf(Memrel(A))" |
306 apply (unfold wf_def) |
306 apply (unfold wf_def) |
307 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) |
307 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast) |
308 done |
308 done |
309 |
309 |
310 text{*The premise @{term "Ord(i)"} does not suffice.*} |
310 text\<open>The premise @{term "Ord(i)"} does not suffice.\<close> |
311 lemma trans_Memrel: |
311 lemma trans_Memrel: |
312 "Ord(i) ==> trans(Memrel(i))" |
312 "Ord(i) ==> trans(Memrel(i))" |
313 by (unfold Ord_def Transset_def trans_def, blast) |
313 by (unfold Ord_def Transset_def trans_def, blast) |
314 |
314 |
315 text{*However, the following premise is strong enough.*} |
315 text\<open>However, the following premise is strong enough.\<close> |
316 lemma Transset_trans_Memrel: |
316 lemma Transset_trans_Memrel: |
317 "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))" |
317 "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))" |
318 by (unfold Transset_def trans_def, blast) |
318 by (unfold Transset_def trans_def, blast) |
319 |
319 |
320 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*) |
320 (*If Transset(A) then Memrel(A) internalizes the membership relation below A*) |
321 lemma Transset_Memrel_iff: |
321 lemma Transset_Memrel_iff: |
322 "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A" |
322 "Transset(A) ==> <a,b> \<in> Memrel(A) <-> a\<in>b & b\<in>A" |
323 by (unfold Transset_def, blast) |
323 by (unfold Transset_def, blast) |
324 |
324 |
325 |
325 |
326 subsection{*Transfinite Induction*} |
326 subsection\<open>Transfinite Induction\<close> |
327 |
327 |
328 (*Epsilon induction over a transitive set*) |
328 (*Epsilon induction over a transitive set*) |
329 lemma Transset_induct: |
329 lemma Transset_induct: |
330 "[| i \<in> k; Transset(k); |
330 "[| i \<in> k; Transset(k); |
331 !!x.[| x \<in> k; \<forall>y\<in>x. P(y) |] ==> P(x) |] |
331 !!x.[| x \<in> k; \<forall>y\<in>x. P(y) |] ==> P(x) |] |
346 apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) |
346 apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption) |
347 apply (blast intro: Ord_succ [THEN Ord_in_Ord]) |
347 apply (blast intro: Ord_succ [THEN Ord_in_Ord]) |
348 done |
348 done |
349 |
349 |
350 |
350 |
351 section{*Fundamental properties of the epsilon ordering (< on ordinals)*} |
351 section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close> |
352 |
352 |
353 |
353 |
354 subsubsection{*Proving That < is a Linear Ordering on the Ordinals*} |
354 subsubsection\<open>Proving That < is a Linear Ordering on the Ordinals\<close> |
355 |
355 |
356 lemma Ord_linear: |
356 lemma Ord_linear: |
357 "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i" |
357 "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i" |
358 proof (induct i arbitrary: j rule: trans_induct) |
358 proof (induct i arbitrary: j rule: trans_induct) |
359 case (step i) |
359 case (step i) |
360 note step_i = step |
360 note step_i = step |
361 show ?case using `Ord(j)` |
361 show ?case using \<open>Ord(j)\<close> |
362 proof (induct j rule: trans_induct) |
362 proof (induct j rule: trans_induct) |
363 case (step j) |
363 case (step j) |
364 thus ?case using step_i |
364 thus ?case using step_i |
365 by (blast dest: Ord_trans) |
365 by (blast dest: Ord_trans) |
366 qed |
366 qed |
367 qed |
367 qed |
368 |
368 |
369 text{*The trichotomy law for ordinals*} |
369 text\<open>The trichotomy law for ordinals\<close> |
370 lemma Ord_linear_lt: |
370 lemma Ord_linear_lt: |
371 assumes o: "Ord(i)" "Ord(j)" |
371 assumes o: "Ord(i)" "Ord(j)" |
372 obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i" |
372 obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i" |
373 apply (simp add: lt_def) |
373 apply (simp add: lt_def) |
374 apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE]) |
374 apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE]) |
393 by (blast elim!: leE elim: lt_asym) |
393 by (blast elim!: leE elim: lt_asym) |
394 |
394 |
395 lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j \<le> i" |
395 lemma not_lt_imp_le: "[| ~ i<j; Ord(i); Ord(j) |] ==> j \<le> i" |
396 by (rule_tac i = i and j = j in Ord_linear2, auto) |
396 by (rule_tac i = i and j = j in Ord_linear2, auto) |
397 |
397 |
398 subsubsection{*Some Rewrite Rules for <, le*} |
398 subsubsection\<open>Some Rewrite Rules for <, le\<close> |
399 |
399 |
400 lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j" |
400 lemma Ord_mem_iff_lt: "Ord(j) ==> i\<in>j <-> i<j" |
401 by (unfold lt_def, blast) |
401 by (unfold lt_def, blast) |
402 |
402 |
403 lemma not_lt_iff_le: "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j \<le> i" |
403 lemma not_lt_iff_le: "[| Ord(i); Ord(j) |] ==> ~ i<j <-> j \<le> i" |
417 |
417 |
418 lemma Ord_0_lt_iff: "Ord(i) ==> i\<noteq>0 <-> 0<i" |
418 lemma Ord_0_lt_iff: "Ord(i) ==> i\<noteq>0 <-> 0<i" |
419 by (blast intro: Ord_0_lt) |
419 by (blast intro: Ord_0_lt) |
420 |
420 |
421 |
421 |
422 subsection{*Results about Less-Than or Equals*} |
422 subsection\<open>Results about Less-Than or Equals\<close> |
423 |
423 |
424 (** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (less-than or equals) **) |
424 (** For ordinals, @{term"j\<subseteq>i"} implies @{term"j \<le> i"} (less-than or equals) **) |
425 |
425 |
426 lemma zero_le_succ_iff [iff]: "0 \<le> succ(x) <-> Ord(x)" |
426 lemma zero_le_succ_iff [iff]: "0 \<le> succ(x) <-> Ord(x)" |
427 by (blast intro: Ord_0_le elim: ltE) |
427 by (blast intro: Ord_0_le elim: ltE) |
444 |
444 |
445 (*Just a variant of subset_imp_le*) |
445 (*Just a variant of subset_imp_le*) |
446 lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j \<le> i" |
446 lemma all_lt_imp_le: "[| Ord(i); Ord(j); !!x. x<j ==> x<i |] ==> j \<le> i" |
447 by (blast intro: not_lt_imp_le dest: lt_irrefl) |
447 by (blast intro: not_lt_imp_le dest: lt_irrefl) |
448 |
448 |
449 subsubsection{*Transitivity Laws*} |
449 subsubsection\<open>Transitivity Laws\<close> |
450 |
450 |
451 lemma lt_trans1: "[| i \<le> j; j<k |] ==> i<k" |
451 lemma lt_trans1: "[| i \<le> j; j<k |] ==> i<k" |
452 by (blast elim!: leE intro: lt_trans) |
452 by (blast elim!: leE intro: lt_trans) |
453 |
453 |
454 lemma lt_trans2: "[| i<j; j \<le> k |] ==> i<k" |
454 lemma lt_trans2: "[| i<j; j \<le> k |] ==> i<k" |
496 lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j" |
496 lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j" |
497 apply (insert succ_le_iff [of i j]) |
497 apply (insert succ_le_iff [of i j]) |
498 apply (simp add: lt_def) |
498 apply (simp add: lt_def) |
499 done |
499 done |
500 |
500 |
501 subsubsection{*Union and Intersection*} |
501 subsubsection\<open>Union and Intersection\<close> |
502 |
502 |
503 lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i \<le> i \<union> j" |
503 lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i \<le> i \<union> j" |
504 by (rule Un_upper1 [THEN subset_imp_le], auto) |
504 by (rule Un_upper1 [THEN subset_imp_le], auto) |
505 |
505 |
506 lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j \<le> i \<union> j" |
506 lemma Un_upper2_le: "[| Ord(i); Ord(j) |] ==> j \<le> i \<union> j" |
558 (*See also Transset_iff_Union_succ*) |
558 (*See also Transset_iff_Union_succ*) |
559 lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" |
559 lemma Ord_Union_succ_eq: "Ord(i) ==> \<Union>(succ(i)) = i" |
560 by (blast intro: Ord_trans) |
560 by (blast intro: Ord_trans) |
561 |
561 |
562 |
562 |
563 subsection{*Results about Limits*} |
563 subsection\<open>Results about Limits\<close> |
564 |
564 |
565 lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))" |
565 lemma Ord_Union [intro,simp,TC]: "[| !!i. i\<in>A ==> Ord(i) |] ==> Ord(\<Union>(A))" |
566 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
566 apply (rule Ord_is_Transset [THEN Transset_Union_family, THEN OrdI]) |
567 apply (blast intro: Ord_contains_Transset)+ |
567 apply (blast intro: Ord_contains_Transset)+ |
568 done |
568 done |
631 (*Holds for all transitive sets, not just ordinals*) |
631 (*Holds for all transitive sets, not just ordinals*) |
632 lemma Ord_Union_subset: "Ord(i) ==> \<Union>(i) \<subseteq> i" |
632 lemma Ord_Union_subset: "Ord(i) ==> \<Union>(i) \<subseteq> i" |
633 by (blast intro: Ord_trans) |
633 by (blast intro: Ord_trans) |
634 |
634 |
635 |
635 |
636 subsection{*Limit Ordinals -- General Properties*} |
636 subsection\<open>Limit Ordinals -- General Properties\<close> |
637 |
637 |
638 lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i" |
638 lemma Limit_Union_eq: "Limit(i) ==> \<Union>(i) = i" |
639 apply (unfold Limit_def) |
639 apply (unfold Limit_def) |
640 apply (fast intro!: ltI elim!: ltE elim: Ord_trans) |
640 apply (fast intro!: ltI elim!: ltE elim: Ord_trans) |
641 done |
641 done |
699 |
699 |
700 lemma Limit_le_succD: "[| Limit(i); i \<le> succ(j) |] ==> i \<le> j" |
700 lemma Limit_le_succD: "[| Limit(i); i \<le> succ(j) |] ==> i \<le> j" |
701 by (blast elim!: leE) |
701 by (blast elim!: leE) |
702 |
702 |
703 |
703 |
704 subsubsection{*Traditional 3-Way Case Analysis on Ordinals*} |
704 subsubsection\<open>Traditional 3-Way Case Analysis on Ordinals\<close> |
705 |
705 |
706 lemma Ord_cases_disj: "Ord(i) ==> i=0 | (\<exists>j. Ord(j) & i=succ(j)) | Limit(i)" |
706 lemma Ord_cases_disj: "Ord(i) ==> i=0 | (\<exists>j. Ord(j) & i=succ(j)) | Limit(i)" |
707 by (blast intro!: non_succ_LimitI Ord_0_lt) |
707 by (blast intro!: non_succ_LimitI Ord_0_lt) |
708 |
708 |
709 lemma Ord_cases: |
709 lemma Ord_cases: |
721 apply (erule Ord_cases, blast+) |
721 apply (erule Ord_cases, blast+) |
722 done |
722 done |
723 |
723 |
724 lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1] |
724 lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1] |
725 |
725 |
726 text{*A set of ordinals is either empty, contains its own union, or its |
726 text\<open>A set of ordinals is either empty, contains its own union, or its |
727 union is a limit ordinal.*} |
727 union is a limit ordinal.\<close> |
728 |
728 |
729 lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j" |
729 lemma Union_le: "[| !!x. x\<in>I ==> x\<le>j; Ord(j) |] ==> \<Union>(I) \<le> j" |
730 by (auto simp add: le_subset_iff Union_least) |
730 by (auto simp add: le_subset_iff Union_least) |
731 |
731 |
732 lemma Ord_set_cases: |
732 lemma Ord_set_cases: |
755 thus ?thesis by (simp add: UIj) |
755 thus ?thesis by (simp add: UIj) |
756 next |
756 next |
757 assume "Limit(\<Union>I)" thus ?thesis by auto |
757 assume "Limit(\<Union>I)" thus ?thesis by auto |
758 qed |
758 qed |
759 |
759 |
760 text{*If the union of a set of ordinals is a successor, then it is an element of that set.*} |
760 text\<open>If the union of a set of ordinals is a successor, then it is an element of that set.\<close> |
761 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
761 lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X" |
762 by (drule Ord_set_cases, auto) |
762 by (drule Ord_set_cases, auto) |
763 |
763 |
764 lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)" |
764 lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)" |
765 apply (simp add: Limit_def lt_def) |
765 apply (simp add: Limit_def lt_def) |