src/HOLCF/Sprod.thy
changeset 39987 8c2f449af35a
parent 39986 38677db30cad
child 40002 c5b5f7a3a3b1
     1.1 --- a/src/HOLCF/Sprod.thy	Fri Oct 08 07:39:50 2010 -0700
     1.2 +++ b/src/HOLCF/Sprod.thy	Sat Oct 09 07:24:49 2010 -0700
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The type of strict products *}
     1.5  
     1.6  theory Sprod
     1.7 -imports Bifinite
     1.8 +imports Deflation
     1.9  begin
    1.10  
    1.11  default_sort pcpo
    1.12 @@ -310,65 +310,4 @@
    1.13      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.14  qed
    1.15  
    1.16 -subsection {* Strict product is a bifinite domain *}
    1.17 -
    1.18 -definition
    1.19 -  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    1.20 -where
    1.21 -  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.22 -
    1.23 -lemma sprod_approx: "approx_chain sprod_approx"
    1.24 -proof (rule approx_chain.intro)
    1.25 -  show "chain (\<lambda>i. sprod_approx i)"
    1.26 -    unfolding sprod_approx_def by simp
    1.27 -  show "(\<Squnion>i. sprod_approx i) = ID"
    1.28 -    unfolding sprod_approx_def
    1.29 -    by (simp add: lub_distribs sprod_map_ID)
    1.30 -  show "\<And>i. finite_deflation (sprod_approx i)"
    1.31 -    unfolding sprod_approx_def
    1.32 -    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
    1.33 -qed
    1.34 -
    1.35 -definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    1.36 -where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
    1.37 -
    1.38 -lemma cast_sprod_sfp:
    1.39 -  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
    1.40 -    udom_emb sprod_approx oo
    1.41 -      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
    1.42 -        udom_prj sprod_approx"
    1.43 -unfolding sprod_sfp_def
    1.44 -apply (rule cast_sfp_fun2 [OF sprod_approx])
    1.45 -apply (erule (1) finite_deflation_sprod_map)
    1.46 -done
    1.47 -
    1.48 -instantiation sprod :: (bifinite, bifinite) bifinite
    1.49 -begin
    1.50 -
    1.51 -definition
    1.52 -  "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
    1.53 -
    1.54 -definition
    1.55 -  "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
    1.56 -
    1.57 -definition
    1.58 -  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.59 -
    1.60 -instance proof
    1.61 -  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    1.62 -    unfolding emb_sprod_def prj_sprod_def
    1.63 -    using ep_pair_udom [OF sprod_approx]
    1.64 -    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
    1.65 -next
    1.66 -  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    1.67 -    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
    1.68 -    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
    1.69 -qed
    1.70 -
    1.71  end
    1.72 -
    1.73 -lemma SFP_sprod:
    1.74 -  "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.75 -by (rule sfp_sprod_def)
    1.76 -
    1.77 -end