34 "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10) |
34 "@oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10) |
35 "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10) |
35 "@oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10) |
36 "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10) |
36 "@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10) |
37 |
37 |
38 |
38 |
39 declare Ord_Un [intro,simp] |
39 declare Ord_Un [intro,simp,TC] |
40 declare Ord_UN [intro,simp] |
40 declare Ord_UN [intro,simp,TC] |
41 declare Ord_Union [intro,simp] |
41 declare Ord_Union [intro,simp,TC] |
42 |
42 |
43 (** These mostly belong to theory Ordinal **) |
43 (** These mostly belong to theory Ordinal **) |
44 |
44 |
45 lemma Union_upper_le: |
45 lemma Union_upper_le: |
46 "\<lbrakk>j: J; i\<le>j; Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J" |
46 "\<lbrakk>j: J; i\<le>j; Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J" |
47 apply (subst Union_eq_UN) |
47 apply (subst Union_eq_UN) |
48 apply (rule UN_upper_le) |
48 apply (rule UN_upper_le) |
49 apply auto |
49 apply auto |
|
50 done |
|
51 |
|
52 lemma zero_not_Limit [iff]: "~ Limit(0)" |
|
53 by (simp add: Limit_def) |
|
54 |
|
55 lemma Limit_has_1: "Limit(i) \<Longrightarrow> 1 < i" |
|
56 by (blast intro: Limit_has_0 Limit_has_succ) |
|
57 |
|
58 lemma Limit_Union [rule_format]: "\<lbrakk>I \<noteq> 0; \<forall>i\<in>I. Limit(i)\<rbrakk> \<Longrightarrow> Limit(\<Union>I)" |
|
59 apply (simp add: Limit_def lt_def) |
|
60 apply (blast intro!: equalityI) |
50 done |
61 done |
51 |
62 |
52 lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)" |
63 lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)" |
53 apply (simp add: Limit_def lt_Ord2) |
64 apply (simp add: Limit_def lt_Ord2) |
54 apply clarify |
65 apply clarify |