src/ZF/OrdQuant.thy
changeset 12667 7e6eaaa125f2
parent 12620 4e6626725e21
child 12763 6cecd9dfd53f
     1.1 --- a/src/ZF/OrdQuant.thy	Tue Jan 08 15:39:47 2002 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Jan 08 16:09:09 2002 +0100
     1.3 @@ -36,9 +36,9 @@
     1.4    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
     1.5  
     1.6  
     1.7 -declare Ord_Un [intro,simp]
     1.8 -declare Ord_UN [intro,simp]
     1.9 -declare Ord_Union [intro,simp]
    1.10 +declare Ord_Un [intro,simp,TC]
    1.11 +declare Ord_UN [intro,simp,TC]
    1.12 +declare Ord_Union [intro,simp,TC]
    1.13  
    1.14  (** These mostly belong to theory Ordinal **)
    1.15  
    1.16 @@ -49,6 +49,17 @@
    1.17  apply auto
    1.18  done
    1.19  
    1.20 +lemma zero_not_Limit [iff]: "~ Limit(0)"
    1.21 +by (simp add: Limit_def)
    1.22 +
    1.23 +lemma Limit_has_1: "Limit(i) \<Longrightarrow> 1 < i"
    1.24 +by (blast intro: Limit_has_0 Limit_has_succ)
    1.25 +
    1.26 +lemma Limit_Union [rule_format]: "\<lbrakk>I \<noteq> 0;  \<forall>i\<in>I. Limit(i)\<rbrakk> \<Longrightarrow> Limit(\<Union>I)"
    1.27 +apply (simp add: Limit_def lt_def)
    1.28 +apply (blast intro!: equalityI)
    1.29 +done
    1.30 +
    1.31  lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
    1.32  apply (simp add: Limit_def lt_Ord2)
    1.33  apply clarify