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) |] |