src/ZF/Ordinal.thy
changeset 13544 895994073bdf
parent 13534 ca6debb89d77
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Ordinal.thy	Wed Aug 28 13:08:34 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Wed Aug 28 13:08:50 2002 +0200
     1.3 @@ -637,9 +637,18 @@
     1.4  apply (erule conjunct2 [THEN conjunct1])
     1.5  done
     1.6  
     1.7 +lemma Limit_nonzero: "Limit(i) ==> i ~= 0"
     1.8 +by (drule Limit_has_0, blast)
     1.9 +
    1.10  lemma Limit_has_succ: "[| Limit(i);  j<i |] ==> succ(j) < i"
    1.11  by (unfold Limit_def, blast)
    1.12  
    1.13 +lemma Limit_succ_lt_iff [simp]: "Limit(i) ==> succ(j) < i <-> (j<i)"
    1.14 +apply (safe intro!: Limit_has_succ)
    1.15 +apply (frule lt_Ord)
    1.16 +apply (blast intro: lt_trans)   
    1.17 +done
    1.18 +
    1.19  lemma zero_not_Limit [iff]: "~ Limit(0)"
    1.20  by (simp add: Limit_def)
    1.21  
    1.22 @@ -647,7 +656,7 @@
    1.23  by (blast intro: Limit_has_0 Limit_has_succ)
    1.24  
    1.25  lemma increasing_LimitI: "[| 0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y |] ==> Limit(l)"
    1.26 -apply (simp add: Limit_def lt_Ord2, clarify)
    1.27 +apply (unfold Limit_def, simp add: lt_Ord2, clarify)
    1.28  apply (drule_tac i=y in ltD) 
    1.29  apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
    1.30  done