# 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 0 i j" +lemma succ_lt_iff: "succ(i) < j <-> i 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) \ succ(j) <-> i\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); :r; :r; a:A; b:A; c:A |] ==> :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 \ A * A ==> r^+ \ 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)