211 done |
211 done |
212 |
212 |
213 lemma apply_recfun: |
213 lemma apply_recfun: |
214 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))" |
214 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))" |
215 apply (unfold is_recfun_def) |
215 apply (unfold is_recfun_def) |
216 apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst) |
216 txt{*replace f only on the left-hand side*} |
217 apply (erule underI [THEN beta]) |
217 apply (erule_tac P = "%x.?t(x) = ?u" in ssubst) |
|
218 apply (simp add: underI); |
218 done |
219 done |
219 |
220 |
220 lemma is_recfun_equal [rule_format]: |
221 lemma is_recfun_equal [rule_format]: |
221 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] |
222 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] |
222 ==> <x,a>:r --> <x,b>:r --> f`x=g`x" |
223 ==> <x,a>:r --> <x,b>:r --> f`x=g`x" |
278 apply blast |
279 apply blast |
279 apply (blast dest: transD) |
280 apply (blast dest: transD) |
280 apply (frule spec [THEN mp], assumption) |
281 apply (frule spec [THEN mp], assumption) |
281 apply (subgoal_tac "<xa,a1> : r") |
282 apply (subgoal_tac "<xa,a1> : r") |
282 apply (drule_tac x1 = "xa" in spec [THEN mp], assumption) |
283 apply (drule_tac x1 = "xa" in spec [THEN mp], assumption) |
283 apply (simp add: vimage_singleton_iff underI [THEN beta] |
284 apply (simp add: vimage_singleton_iff |
284 apply_recfun is_recfun_cut) |
285 apply_recfun is_recfun_cut) |
285 apply (blast dest: transD) |
286 apply (blast dest: transD) |
286 done |
287 done |
287 |
288 |
288 |
289 |