src/ZF/Ordinal.thy
changeset 13243 ba53d07d32d5
parent 13203 fac77a839aa2
child 13269 3ba9be497c33
     1.1 --- a/src/ZF/Ordinal.thy	Mon Jun 24 11:57:23 2002 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Mon Jun 24 11:58:21 2002 +0200
     1.3 @@ -127,6 +127,10 @@
     1.4  lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
     1.5  by (unfold Ord_def Transset_def, blast)
     1.6  
     1.7 +(*suitable for rewriting PROVIDED i has been fixed*)
     1.8 +lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
     1.9 +by (blast intro: Ord_in_Ord)
    1.10 +
    1.11  (* Ord(succ(j)) ==> Ord(j) *)
    1.12  lemmas Ord_succD = Ord_in_Ord [OF _ succI1]
    1.13  
    1.14 @@ -456,7 +460,7 @@
    1.15  lemma lt_imp_0_lt: "j<i ==> 0<i"
    1.16  by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) 
    1.17  
    1.18 -lemma succ_lt_iff: "succ(i) < j \<longleftrightarrow> i<j & succ(i) \<noteq> j"
    1.19 +lemma succ_lt_iff: "succ(i) < j <-> i<j & succ(i) \<noteq> j"
    1.20  apply auto 
    1.21  apply (blast intro: lt_trans le_refl dest: lt_Ord) 
    1.22  apply (frule lt_Ord) 
    1.23 @@ -467,6 +471,11 @@
    1.24  apply (blast dest: lt_asym) 
    1.25  done
    1.26  
    1.27 +lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
    1.28 +apply (insert succ_le_iff [of i j]) 
    1.29 +apply (simp add: lt_def) 
    1.30 +done
    1.31 +
    1.32  (** Union and Intersection **)
    1.33  
    1.34  lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j"