--- a/src/HOLCF/ConvexPD.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOLCF/ConvexPD.thy Mon Nov 09 12:40:47 2009 -0800
@@ -515,6 +515,18 @@
lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
by (induct xs rule: convex_pd_induct, simp_all)
+lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: convex_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
subsection {* Conversions to other powerdomains *}
--- a/src/HOLCF/LowerPD.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOLCF/LowerPD.thy Mon Nov 09 12:40:47 2009 -0800
@@ -491,4 +491,16 @@
lemma lower_map_approx: "lower_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
by (induct xs rule: lower_pd_induct, simp_all)
+lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: lower_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
end
--- a/src/HOLCF/UpperPD.thy Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOLCF/UpperPD.thy Mon Nov 09 12:40:47 2009 -0800
@@ -486,4 +486,16 @@
lemma upper_map_approx: "upper_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
by (induct xs rule: upper_pd_induct, simp_all)
+lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
+apply default
+apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
+apply (induct_tac y rule: upper_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+done
+
+lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
+apply default
+apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
+apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.below monofun_cfun)
+done
+
end