equal
deleted
inserted
replaced
238 apply (fast intro: converse_rtrancl_into_rtrancl) |
238 apply (fast intro: converse_rtrancl_into_rtrancl) |
239 done |
239 done |
240 |
240 |
241 text{*Well-foundedness of image*} |
241 text{*Well-foundedness of image*} |
242 |
242 |
243 lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)" |
243 lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)" |
244 apply (simp only: wf_eq_minimal, clarify) |
244 apply (simp only: wf_eq_minimal, clarify) |
245 apply (case_tac "EX p. f p : Q") |
245 apply (case_tac "EX p. f p : Q") |
246 apply (erule_tac x = "{p. f p : Q}" in allE) |
246 apply (erule_tac x = "{p. f p : Q}" in allE) |
247 apply (fast dest: inj_onD, blast) |
247 apply (fast dest: inj_onD, blast) |
248 done |
248 done |