src/ZF/Constructible/Wellorderings.thy
changeset 13269 3ba9be497c33
parent 13251 74cb2af8811e
child 13293 09276ee04361
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -71,6 +71,10 @@
     1.4      "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
     1.5  by (auto simp add: wellfounded_def wellfounded_on_def)
     1.6  
     1.7 +lemma (in M_axioms) wellfounded_on_subset_A:
     1.8 +     "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
     1.9 +by (simp add: wellfounded_on_def, blast)
    1.10 +
    1.11  
    1.12  subsubsection {*Well-founded relations*}
    1.13  
    1.14 @@ -85,6 +89,15 @@
    1.15       "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
    1.16  by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
    1.17  
    1.18 +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
    1.19 +     "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
    1.20 +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
    1.21 +
    1.22 +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
    1.23 +     "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
    1.24 +by (blast intro: wellfounded_imp_wellfounded_on
    1.25 +                 wellfounded_on_field_imp_wellfounded)
    1.26 +
    1.27  (*Consider the least z in domain(r) such that P(z) does not hold...*)
    1.28  lemma (in M_axioms) wellfounded_induct: 
    1.29       "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));