equal
deleted
inserted
replaced
367 apply blast |
367 apply blast |
368 apply blast |
368 apply blast |
369 done |
369 done |
370 |
370 |
371 text{*But note that the combination of @{text wf_imp_wf_on} and |
371 text{*But note that the combination of @{text wf_imp_wf_on} and |
372 @{text wf_rvimage} gives @{term "wf(r) ==> wf[C](rvimage(A,f,r))"}*} |
372 @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}*} |
373 lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))" |
373 lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))" |
374 apply (rule wf_onI2) |
374 apply (rule wf_onI2) |
375 apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba") |
375 apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba") |
376 apply blast |
376 apply blast |
377 apply (erule_tac a = "f`y" in wf_on_induct) |
377 apply (erule_tac a = "f`y" in wf_on_induct) |