# HG changeset patch
# User huffman
# Date 1257799247 28800
# Node ID 8d39394fe5cfa47630c8c2b767055fc54ff8274d
# Parent  b233f48a4d3d8865a79fc813d0ceebc7f9a51427
ep_pair and deflation lemmas for powerdomain map functions

diff -r b233f48a4d3d -r 8d39394fe5cf src/HOLCF/ConvexPD.thy
--- 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 *}
 
diff -r b233f48a4d3d -r 8d39394fe5cf src/HOLCF/LowerPD.thy
--- 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
diff -r b233f48a4d3d -r 8d39394fe5cf src/HOLCF/UpperPD.thy
--- 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