src/HOLCF/Cprod.thy
changeset 39974 b525988432e9
parent 36452 d37c6eed8117
child 39985 310f98585107
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Oct 05 17:53:00 2010 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Oct 06 10:49:27 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 Bifinite
     1.8 +imports Algebraic
     1.9  begin
    1.10  
    1.11  default_sort cpo
    1.12 @@ -40,4 +40,62 @@
    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 {* Cartesian product is an SFP domain *}
    1.17 +
    1.18 +definition
    1.19 +  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
    1.20 +where
    1.21 +  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.22 +
    1.23 +lemma prod_approx: "approx_chain prod_approx"
    1.24 +proof (rule approx_chain.intro)
    1.25 +  show "chain (\<lambda>i. prod_approx i)"
    1.26 +    unfolding prod_approx_def by simp
    1.27 +  show "(\<Squnion>i. prod_approx i) = ID"
    1.28 +    unfolding prod_approx_def
    1.29 +    by (simp add: lub_distribs cprod_map_ID)
    1.30 +  show "\<And>i. finite_deflation (prod_approx i)"
    1.31 +    unfolding prod_approx_def
    1.32 +    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
    1.33 +qed
    1.34 +
    1.35 +definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    1.36 +where "prod_sfp = sfp_fun2 prod_approx cprod_map"
    1.37 +
    1.38 +lemma cast_prod_sfp:
    1.39 +  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
    1.40 +    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
    1.41 +unfolding prod_sfp_def
    1.42 +apply (rule cast_sfp_fun2 [OF prod_approx])
    1.43 +apply (erule (1) finite_deflation_cprod_map)
    1.44 +done
    1.45 +
    1.46 +instantiation prod :: (sfp, sfp) sfp
    1.47 +begin
    1.48 +
    1.49 +definition
    1.50 +  "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
    1.51 +
    1.52 +definition
    1.53 +  "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
    1.54 +
    1.55 +definition
    1.56 +  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.57 +
    1.58 +instance proof
    1.59 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
    1.60 +    unfolding emb_prod_def prj_prod_def
    1.61 +    using ep_pair_udom [OF prod_approx]
    1.62 +    by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
    1.63 +next
    1.64 +  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
    1.65 +    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
    1.66 +    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
    1.67 +qed
    1.68 +
    1.69  end
    1.70 +
    1.71 +lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.72 +by (rule sfp_prod_def)
    1.73 +
    1.74 +end