src/HOLCF/Cprod.thy
changeset 39985 310f98585107
parent 39974 b525988432e9
child 39986 38677db30cad
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Oct 07 13:33:06 2010 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Oct 07 13:54:43 2010 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The cpo of cartesian products *}
     1.5  
     1.6  theory Cprod
     1.7 -imports Algebraic
     1.8 +imports Bifinite
     1.9  begin
    1.10  
    1.11  default_sort cpo
    1.12 @@ -40,6 +40,63 @@
    1.13  lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    1.14  by (simp add: csplit_def)
    1.15  
    1.16 +subsection {* Map operator for product type *}
    1.17 +
    1.18 +definition
    1.19 +  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    1.20 +where
    1.21 +  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    1.22 +
    1.23 +lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    1.24 +unfolding cprod_map_def by simp
    1.25 +
    1.26 +lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    1.27 +unfolding expand_cfun_eq by auto
    1.28 +
    1.29 +lemma cprod_map_map:
    1.30 +  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    1.31 +    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    1.32 +by (induct p) simp
    1.33 +
    1.34 +lemma ep_pair_cprod_map:
    1.35 +  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    1.36 +  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    1.37 +proof
    1.38 +  interpret e1p1: ep_pair e1 p1 by fact
    1.39 +  interpret e2p2: ep_pair e2 p2 by fact
    1.40 +  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    1.41 +    by (induct x) simp
    1.42 +  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    1.43 +    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    1.44 +qed
    1.45 +
    1.46 +lemma deflation_cprod_map:
    1.47 +  assumes "deflation d1" and "deflation d2"
    1.48 +  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    1.49 +proof
    1.50 +  interpret d1: deflation d1 by fact
    1.51 +  interpret d2: deflation d2 by fact
    1.52 +  fix x
    1.53 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
    1.54 +    by (induct x) (simp add: d1.idem d2.idem)
    1.55 +  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    1.56 +    by (induct x) (simp add: d1.below d2.below)
    1.57 +qed
    1.58 +
    1.59 +lemma finite_deflation_cprod_map:
    1.60 +  assumes "finite_deflation d1" and "finite_deflation d2"
    1.61 +  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    1.62 +proof (rule finite_deflation_intro)
    1.63 +  interpret d1: finite_deflation d1 by fact
    1.64 +  interpret d2: finite_deflation d2 by fact
    1.65 +  have "deflation d1" and "deflation d2" by fact+
    1.66 +  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    1.67 +  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    1.68 +    by clarsimp
    1.69 +  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    1.70 +    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.71 +qed
    1.72 +
    1.73  subsection {* Cartesian product is an SFP domain *}
    1.74  
    1.75  definition