338 thus ?thesis using result defined by blast |
338 thus ?thesis using result defined by blast |
339 qed |
339 qed |
340 |
340 |
341 lemma admissible_image: |
341 lemma admissible_image: |
342 assumes pfun: "partial_function_definitions le lub" |
342 assumes pfun: "partial_function_definitions le lub" |
343 assumes adm: "ccpo.admissible lub le (P o g)" |
343 assumes adm: "ccpo.admissible lub le (P \<circ> g)" |
344 assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" |
344 assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" |
345 assumes inv: "\<And>x. f (g x) = x" |
345 assumes inv: "\<And>x. f (g x) = x" |
346 shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P" |
346 shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P" |
347 proof (rule ccpo.admissibleI) |
347 proof (rule ccpo.admissibleI) |
348 fix A assume "chain (img_ord f le) A" |
348 fix A assume "chain (img_ord f le) A" |
349 then have ch': "chain le (f ` A)" |
349 then have ch': "chain le (f ` A)" |
350 by (auto simp: img_ord_def intro: chainI dest: chainD) |
350 by (auto simp: img_ord_def intro: chainI dest: chainD) |
351 assume "A \<noteq> {}" |
351 assume "A \<noteq> {}" |
352 assume P_A: "\<forall>x\<in>A. P x" |
352 assume P_A: "\<forall>x\<in>A. P x" |
353 have "(P o g) (lub (f ` A))" using adm ch' |
353 have "(P \<circ> g) (lub (f ` A))" using adm ch' |
354 proof (rule ccpo.admissibleD) |
354 proof (rule ccpo.admissibleD) |
355 fix x assume "x \<in> f ` A" |
355 fix x assume "x \<in> f ` A" |
356 with P_A show "(P o g) x" by (auto simp: inj[OF inv]) |
356 with P_A show "(P \<circ> g) x" by (auto simp: inj[OF inv]) |
357 qed(simp add: \<open>A \<noteq> {}\<close>) |
357 qed(simp add: \<open>A \<noteq> {}\<close>) |
358 thus "P (img_lub f g lub A)" unfolding img_lub_def by simp |
358 thus "P (img_lub f g lub A)" unfolding img_lub_def by simp |
359 qed |
359 qed |
360 |
360 |
361 lemma admissible_fun: |
361 lemma admissible_fun: |