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"

     2.1 --- a/src/ZF/Trancl.thy	Mon Jun 24 11:57:23 2002 +0200
     2.2 +++ b/src/ZF/Trancl.thy	Mon Jun 24 11:58:21 2002 +0200
     2.3 @@ -79,8 +79,10 @@
     2.4  
     2.5  lemma trans_onD: 
     2.6      "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
     2.7 -apply (unfold trans_on_def, blast)
     2.8 -done
     2.9 +by (unfold trans_on_def, blast)
    2.10 +
    2.11 +lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    2.12 +by (unfold trans_def trans_on_def, blast)
    2.13  
    2.14  subsection{*Transitive closure of a relation*}
    2.15  
    2.16 @@ -187,6 +189,8 @@
    2.17                      trans_rtrancl [THEN transD, THEN compI])
    2.18  done
    2.19  
    2.20 +lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
    2.21 +
    2.22  lemmas trancl_trans = trans_trancl [THEN transD, standard]
    2.23  
    2.24  (** Conversions between trancl and rtrancl **)
    2.25 @@ -253,6 +257,9 @@
    2.26  apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
    2.27  done
    2.28  
    2.29 +lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A"
    2.30 +by (insert trancl_type [of r], blast)
    2.31 +
    2.32  lemma trancl_mono: "r<=s ==> r^+ <= s^+"
    2.33  by (unfold trancl_def, intro comp_mono rtrancl_mono)
    2.34