src/ZF/Constructible/Wellorderings.thy
changeset 13251 74cb2af8811e
parent 13247 e3c289f0724b
child 13269 3ba9be497c33
--- a/src/ZF/Constructible/Wellorderings.thy	Wed Jun 26 12:17:21 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jun 26 18:31:20 2002 +0200
@@ -85,6 +85,16 @@
      "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
 
+(*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));  
+         \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
+      ==> P(a)";
+apply (simp (no_asm_use) add: wellfounded_def)
+apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in spec)
+apply (blast dest: transM)
+done
+
 lemma (in M_axioms) wellfounded_on_induct: 
      "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
        separation(M, \<lambda>x. x\<in>A --> ~P(x));