equal
deleted
inserted
replaced
78 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
78 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
79 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
79 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
80 apply blast |
80 apply blast |
81 apply (drule_tac x=x in spec, blast) |
81 apply (drule_tac x=x in spec, blast) |
82 done |
82 done |
|
83 |
|
84 lemma (in M_axioms) wellfounded_on_imp_wellfounded: |
|
85 "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)" |
|
86 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff) |
83 |
87 |
84 lemma (in M_axioms) wellfounded_on_induct: |
88 lemma (in M_axioms) wellfounded_on_induct: |
85 "[| a\<in>A; wellfounded_on(M,A,r); M(A); |
89 "[| a\<in>A; wellfounded_on(M,A,r); M(A); |
86 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
90 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
87 \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |] |
91 \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |] |