equal
deleted
inserted
replaced
128 |] ==> P(a)" |
128 |] ==> P(a)" |
129 apply (unfold wf_on_def) |
129 apply (unfold wf_on_def) |
130 apply (erule wf_induct2, assumption) |
130 apply (erule wf_induct2, assumption) |
131 apply (rule field_Int_square, blast) |
131 apply (rule field_Int_square, blast) |
132 done |
132 done |
|
133 |
|
134 text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction |
|
135 hypothesis by removing the restriction to @{term A}.*} |
|
136 lemma wf_on_induct2: |
|
137 "[| wf[A](r); a:A; r \<subseteq> A*A; |
|
138 !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) |
|
139 |] ==> P(a)" |
|
140 by (rule wf_on_induct, assumption+, blast) |
133 |
141 |
134 (*fixed up for induct method*) |
142 (*fixed up for induct method*) |
135 lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on] |
143 lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on] |
136 and wf_on_induct_rule = |
144 and wf_on_induct_rule = |
137 wf_on_induct [rule_format, consumes 2, induct set: wf_on] |
145 wf_on_induct [rule_format, consumes 2, induct set: wf_on] |