--- 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"
--- 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)