src/HOLCF/Cprod.thy
changeset 39987 8c2f449af35a
parent 39986 38677db30cad
child 40002 c5b5f7a3a3b1
     1.1 --- a/src/HOLCF/Cprod.thy	Fri Oct 08 07:39:50 2010 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Sat Oct 09 07:24:49 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 Deflation
     1.9  begin
    1.10  
    1.11  default_sort cpo
    1.12 @@ -97,63 +97,4 @@
    1.13      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.14  qed
    1.15  
    1.16 -subsection {* Cartesian product is a bifinite 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 :: (bifinite, bifinite) bifinite
    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:
    1.72 -  "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.73 -by (rule sfp_prod_def)
    1.74 -
    1.75 -end