# HG changeset patch
# User paulson
# Date 1024912701 -7200
# Node ID ba53d07d32d53359c3661aaeadc7bb1c71525d8d
# Parent  f96bd927dd37ef5f320872e302214c00d73e395d
new lemmas

diff -r f96bd927dd37 -r ba53d07d32d5 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Mon Jun 24 11:57:23 2002 +0200
+++ b/src/ZF/Ordinal.thy	Mon Jun 24 11:58:21 2002 +0200
@@ -127,6 +127,10 @@
 lemma Ord_in_Ord: "[| Ord(i);  j:i |] ==> Ord(j)"
 by (unfold Ord_def Transset_def, blast)
 
+(*suitable for rewriting PROVIDED i has been fixed*)
+lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
+by (blast intro: Ord_in_Ord)
+
 (* Ord(succ(j)) ==> Ord(j) *)
 lemmas Ord_succD = Ord_in_Ord [OF _ succI1]
 
@@ -456,7 +460,7 @@
 lemma lt_imp_0_lt: "j<i ==> 0<i"
 by (blast intro: lt_trans1 Ord_0_le [OF lt_Ord]) 
 
-lemma succ_lt_iff: "succ(i) < j \<longleftrightarrow> i<j & succ(i) \<noteq> j"
+lemma succ_lt_iff: "succ(i) < j <-> i<j & succ(i) \<noteq> j"
 apply auto 
 apply (blast intro: lt_trans le_refl dest: lt_Ord) 
 apply (frule lt_Ord) 
@@ -467,6 +471,11 @@
 apply (blast dest: lt_asym) 
 done
 
+lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
+apply (insert succ_le_iff [of i j]) 
+apply (simp add: lt_def) 
+done
+
 (** Union and Intersection **)
 
 lemma Un_upper1_le: "[| Ord(i); Ord(j) |] ==> i le i Un j"
diff -r f96bd927dd37 -r ba53d07d32d5 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Mon Jun 24 11:57:23 2002 +0200
+++ b/src/ZF/Trancl.thy	Mon Jun 24 11:58:21 2002 +0200
@@ -79,8 +79,10 @@
 
 lemma trans_onD: 
     "[| trans[A](r);  <a,b>:r;  <b,c>:r;  a:A;  b:A;  c:A |] ==> <a,c>:r"
-apply (unfold trans_on_def, blast)
-done
+by (unfold trans_on_def, blast)
+
+lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
+by (unfold trans_def trans_on_def, blast)
 
 subsection{*Transitive closure of a relation*}
 
@@ -187,6 +189,8 @@
                     trans_rtrancl [THEN transD, THEN compI])
 done
 
+lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
+
 lemmas trancl_trans = trans_trancl [THEN transD, standard]
 
 (** Conversions between trancl and rtrancl **)
@@ -253,6 +257,9 @@
 apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
 done
 
+lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A"
+by (insert trancl_type [of r], blast)
+
 lemma trancl_mono: "r<=s ==> r^+ <= s^+"
 by (unfold trancl_def, intro comp_mono rtrancl_mono)