src/HOLCF/Sprod.thy
changeset 39974 b525988432e9
parent 39973 c62b4ff97bfc
child 39985 310f98585107
     1.1 --- a/src/HOLCF/Sprod.thy	Tue Oct 05 17:53:00 2010 -0700
     1.2 +++ b/src/HOLCF/Sprod.thy	Wed Oct 06 10:49:27 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 Algebraic
     1.9  begin
    1.10  
    1.11  default_sort pcpo
    1.12 @@ -310,37 +310,66 @@
    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 +subsection {* Strict product is an SFP domain *}
    1.18 +
    1.19 +definition
    1.20 +  sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
    1.21 +where
    1.22 +  "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
    1.23  
    1.24 -instantiation sprod :: (bifinite, bifinite) bifinite
    1.25 +lemma sprod_approx: "approx_chain sprod_approx"
    1.26 +proof (rule approx_chain.intro)
    1.27 +  show "chain (\<lambda>i. sprod_approx i)"
    1.28 +    unfolding sprod_approx_def by simp
    1.29 +  show "(\<Squnion>i. sprod_approx i) = ID"
    1.30 +    unfolding sprod_approx_def
    1.31 +    by (simp add: lub_distribs sprod_map_ID)
    1.32 +  show "\<And>i. finite_deflation (sprod_approx i)"
    1.33 +    unfolding sprod_approx_def
    1.34 +    by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
    1.35 +qed
    1.36 +
    1.37 +definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
    1.38 +where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
    1.39 +
    1.40 +lemma cast_sprod_sfp:
    1.41 +  "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
    1.42 +    udom_emb sprod_approx oo
    1.43 +      sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
    1.44 +        udom_prj sprod_approx"
    1.45 +unfolding sprod_sfp_def
    1.46 +apply (rule cast_sfp_fun2 [OF sprod_approx])
    1.47 +apply (erule (1) finite_deflation_sprod_map)
    1.48 +done
    1.49 +
    1.50 +instantiation sprod :: (sfp, sfp) sfp
    1.51  begin
    1.52  
    1.53  definition
    1.54 -  approx_sprod_def:
    1.55 -    "approx = (\<lambda>n. sprod_map\<cdot>(approx n)\<cdot>(approx n))"
    1.56 +  "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
    1.57 +
    1.58 +definition
    1.59 +  "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
    1.60 +
    1.61 +definition
    1.62 +  "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.63  
    1.64  instance proof
    1.65 -  fix i :: nat and x :: "'a \<otimes> 'b"
    1.66 -  show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
    1.67 -    unfolding approx_sprod_def by simp
    1.68 -  show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.69 -    unfolding approx_sprod_def sprod_map_def
    1.70 -    by (simp add: lub_distribs eta_cfun)
    1.71 -  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.72 -    unfolding approx_sprod_def sprod_map_def
    1.73 -    by (simp add: ssplit_def strictify_conv_if)
    1.74 -  show "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
    1.75 -    unfolding approx_sprod_def
    1.76 -    by (intro finite_deflation.finite_fixes
    1.77 -              finite_deflation_sprod_map
    1.78 -              finite_deflation_approx)
    1.79 +  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    1.80 +    unfolding emb_sprod_def prj_sprod_def
    1.81 +    using ep_pair_udom [OF sprod_approx]
    1.82 +    by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
    1.83 +next
    1.84 +  show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
    1.85 +    unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
    1.86 +    by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
    1.87  qed
    1.88  
    1.89  end
    1.90  
    1.91 -lemma approx_spair [simp]:
    1.92 -  "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
    1.93 -unfolding approx_sprod_def sprod_map_def
    1.94 -by (simp add: ssplit_def strictify_conv_if)
    1.95 +text {* SFP of type constructor = type combinator *}
    1.96 +
    1.97 +lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
    1.98 +by (rule sfp_sprod_def)
    1.99  
   1.100  end