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 {*Wellfounded relations*} 
79 subsubsection {*Wellfounded 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) ] 