src/ZF/Constructible/Wellorderings.thy
changeset 13269 3ba9be497c33
parent 13251 74cb2af8811e
child 13293 09276ee04361
equal deleted inserted replaced
13268:240509babf00 13269:3ba9be497c33
    69 
    69 
    70 lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
    70 lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
    71     "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    71     "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    72 by (auto simp add: wellfounded_def wellfounded_on_def)
    72 by (auto simp add: wellfounded_def wellfounded_on_def)
    73 
    73 
       
    74 lemma (in M_axioms) wellfounded_on_subset_A:
       
    75      "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
       
    76 by (simp add: wellfounded_on_def, blast)
       
    77 
    74 
    78 
    75 subsubsection {*Well-founded relations*}
    79 subsubsection {*Well-founded relations*}
    76 
    80 
    77 lemma  (in M_axioms) wellfounded_on_iff_wellfounded:
    81 lemma  (in M_axioms) wellfounded_on_iff_wellfounded:
    78      "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
    82      "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
    82 done
    86 done
    83 
    87 
    84 lemma (in M_axioms) wellfounded_on_imp_wellfounded:
    88 lemma (in M_axioms) wellfounded_on_imp_wellfounded:
    85      "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
    89      "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
    86 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
    90 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
       
    91 
       
    92 lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
       
    93      "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
       
    94 by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
       
    95 
       
    96 lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
       
    97      "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
       
    98 by (blast intro: wellfounded_imp_wellfounded_on
       
    99                  wellfounded_on_field_imp_wellfounded)
    87 
   100 
    88 (*Consider the least z in domain(r) such that P(z) does not hold...*)
   101 (*Consider the least z in domain(r) such that P(z) does not hold...*)
    89 lemma (in M_axioms) wellfounded_induct: 
   102 lemma (in M_axioms) wellfounded_induct: 
    90      "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
   103      "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));  
    91          \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
   104          \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]