diff -r 240509babf00 -r 3ba9be497c33 src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Jul 02 13:28:08 2002 +0200
@@ -71,6 +71,10 @@
"[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
by (auto simp add: wellfounded_def wellfounded_on_def)
+lemma (in M_axioms) wellfounded_on_subset_A:
+ "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
+by (simp add: wellfounded_on_def, blast)
+
subsubsection {*Well-founded relations*}
@@ -85,6 +89,15 @@
"[|wellfounded_on(M,A,r); r \ A*A|] ==> wellfounded(M,r)"
by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
+lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
+ "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
+by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
+
+lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
+ "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
+by (blast intro: wellfounded_imp_wellfounded_on
+ wellfounded_on_field_imp_wellfounded)
+
(*Consider the least z in domain(r) such that P(z) does not hold...*)
lemma (in M_axioms) wellfounded_induct:
"[| wellfounded(M,r); M(a); M(r); separation(M, \x. ~P(x));