src/ZF/Constructible/Wellorderings.thy
changeset 13269 3ba9be497c33
parent 13251 74cb2af8811e
child 13293 09276ee04361
--- 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 \<subseteq> 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, \<lambda>x. ~P(x));