--- a/src/HOLCF/Bifinite.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Bifinite.thy Sat Oct 09 07:24:49 2010 -0700
@@ -5,7 +5,7 @@
header {* Bifinite domains *}
theory Bifinite
-imports Algebraic
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr
begin
subsection {* Class of bifinite domains *}
@@ -144,7 +144,7 @@
Abs_fin_defl_inverse [unfolded mem_Collect_eq, OF 1])
qed
-subsection {* Instance for universal domain type *}
+subsection {* The universal domain is bifinite *}
instantiation udom :: bifinite
begin
@@ -178,7 +178,7 @@
end
-subsection {* Instance for continuous function space *}
+subsection {* Continuous function space is a bifinite domain *}
definition
cfun_approx :: "nat \<Rightarrow> (udom \<rightarrow> udom) \<rightarrow> (udom \<rightarrow> udom)"
@@ -237,4 +237,324 @@
"SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_cfun_def)
+subsection {* Cartesian product is a bifinite domain *}
+
+definition
+ prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
+where
+ "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma prod_approx: "approx_chain prod_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. prod_approx i)"
+ unfolding prod_approx_def by simp
+ show "(\<Squnion>i. prod_approx i) = ID"
+ unfolding prod_approx_def
+ by (simp add: lub_distribs cprod_map_ID)
+ show "\<And>i. finite_deflation (prod_approx i)"
+ unfolding prod_approx_def
+ by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
+qed
+
+definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "prod_sfp = sfp_fun2 prod_approx cprod_map"
+
+lemma cast_prod_sfp:
+ "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
+ cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
+unfolding prod_sfp_def
+apply (rule cast_sfp_fun2 [OF prod_approx])
+apply (erule (1) finite_deflation_cprod_map)
+done
+
+instantiation prod :: (bifinite, bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
+
+definition
+ "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def
+ using ep_pair_udom [OF prod_approx]
+ by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
+ unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
+qed
+
end
+
+lemma SFP_prod:
+ "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_prod_def)
+
+subsection {* Strict product is a bifinite domain *}
+
+definition
+ sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
+where
+ "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma sprod_approx: "approx_chain sprod_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. sprod_approx i)"
+ unfolding sprod_approx_def by simp
+ show "(\<Squnion>i. sprod_approx i) = ID"
+ unfolding sprod_approx_def
+ by (simp add: lub_distribs sprod_map_ID)
+ show "\<And>i. finite_deflation (sprod_approx i)"
+ unfolding sprod_approx_def
+ by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
+qed
+
+definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
+
+lemma cast_sprod_sfp:
+ "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
+ udom_emb sprod_approx oo
+ sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
+ udom_prj sprod_approx"
+unfolding sprod_sfp_def
+apply (rule cast_sfp_fun2 [OF sprod_approx])
+apply (erule (1) finite_deflation_sprod_map)
+done
+
+instantiation sprod :: (bifinite, bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
+
+definition
+ "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def
+ using ep_pair_udom [OF sprod_approx]
+ by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
+ unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
+qed
+
+end
+
+lemma SFP_sprod:
+ "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_sprod_def)
+
+subsection {* Lifted cpo is a bifinite domain *}
+
+definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
+where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
+
+lemma u_approx: "approx_chain u_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. u_approx i)"
+ unfolding u_approx_def by simp
+ show "(\<Squnion>i. u_approx i) = ID"
+ unfolding u_approx_def
+ by (simp add: lub_distribs u_map_ID)
+ show "\<And>i. finite_deflation (u_approx i)"
+ unfolding u_approx_def
+ by (intro finite_deflation_u_map finite_deflation_udom_approx)
+qed
+
+definition u_sfp :: "sfp \<rightarrow> sfp"
+where "u_sfp = sfp_fun1 u_approx u_map"
+
+lemma cast_u_sfp:
+ "cast\<cdot>(u_sfp\<cdot>A) =
+ udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
+unfolding u_sfp_def
+apply (rule cast_sfp_fun1 [OF u_approx])
+apply (erule finite_deflation_u_map)
+done
+
+instantiation u :: (bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb u_approx oo u_map\<cdot>emb"
+
+definition
+ "prj = u_map\<cdot>prj oo udom_prj u_approx"
+
+definition
+ "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def
+ using ep_pair_udom [OF u_approx]
+ by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
+ unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
+qed
+
+end
+
+lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
+by (rule sfp_u_def)
+
+subsection {* Lifted countable types are bifinite domains *}
+
+definition
+ lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
+where
+ "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
+
+lemma chain_lift_approx [simp]: "chain lift_approx"
+ unfolding lift_approx_def
+ by (rule chainI, simp add: FLIFT_mono)
+
+lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
+apply (rule ext_cfun)
+apply (simp add: contlub_cfun_fun)
+apply (simp add: lift_approx_def)
+apply (case_tac x, simp)
+apply (rule thelubI)
+apply (rule is_lubI)
+apply (rule ub_rangeI, simp)
+apply (drule ub_rangeD)
+apply (erule rev_below_trans)
+apply simp
+apply (rule lessI)
+done
+
+lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
+proof
+ fix x
+ show "lift_approx i\<cdot>x \<sqsubseteq> x"
+ unfolding lift_approx_def
+ by (cases x, simp, simp)
+ show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
+ unfolding lift_approx_def
+ by (cases x, simp, simp)
+ show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
+ proof (rule finite_subset)
+ let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
+ show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
+ unfolding lift_approx_def
+ by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
+ show "finite ?S"
+ by (simp add: finite_vimageI)
+ qed
+qed
+
+lemma lift_approx: "approx_chain lift_approx"
+using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
+by (rule approx_chain.intro)
+
+instantiation lift :: (countable) bifinite
+begin
+
+definition
+ "emb = udom_emb lift_approx"
+
+definition
+ "prj = udom_prj lift_approx"
+
+definition
+ "sfp (t::'a lift itself) =
+ (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
+
+instance proof
+ show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
+ unfolding emb_lift_def prj_lift_def
+ by (rule ep_pair_udom [OF lift_approx])
+ show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
+ unfolding sfp_lift_def
+ apply (subst contlub_cfun_arg)
+ apply (rule chainI)
+ apply (rule sfp.principal_mono)
+ apply (simp add: below_fin_defl_def)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
+ ep_pair.finite_deflation_e_d_p [OF ep])
+ apply (intro monofun_cfun below_refl)
+ apply (rule chainE)
+ apply (rule chain_lift_approx)
+ apply (subst cast_sfp_principal)
+ apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
+ ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
+ done
+qed
+
+end
+
+subsection {* Strict sum is a bifinite domain *}
+
+definition
+ ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
+where
+ "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
+
+lemma ssum_approx: "approx_chain ssum_approx"
+proof (rule approx_chain.intro)
+ show "chain (\<lambda>i. ssum_approx i)"
+ unfolding ssum_approx_def by simp
+ show "(\<Squnion>i. ssum_approx i) = ID"
+ unfolding ssum_approx_def
+ by (simp add: lub_distribs ssum_map_ID)
+ show "\<And>i. finite_deflation (ssum_approx i)"
+ unfolding ssum_approx_def
+ by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
+qed
+
+definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
+where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
+
+lemma cast_ssum_sfp:
+ "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
+ udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
+unfolding ssum_sfp_def
+apply (rule cast_sfp_fun2 [OF ssum_approx])
+apply (erule (1) finite_deflation_ssum_map)
+done
+
+instantiation ssum :: (bifinite, bifinite) bifinite
+begin
+
+definition
+ "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
+
+definition
+ "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
+
+definition
+ "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+
+instance proof
+ show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def
+ using ep_pair_udom [OF ssum_approx]
+ by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
+next
+ show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
+ unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
+ by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
+qed
+
+end
+
+lemma SFP_ssum:
+ "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+by (rule sfp_ssum_def)
+
+end
--- a/src/HOLCF/Cprod.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Cprod.thy Sat Oct 09 07:24:49 2010 -0700
@@ -5,7 +5,7 @@
header {* The cpo of cartesian products *}
theory Cprod
-imports Bifinite
+imports Deflation
begin
default_sort cpo
@@ -97,63 +97,4 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Cartesian product is a bifinite domain *}
-
-definition
- prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
-where
- "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma prod_approx: "approx_chain prod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. prod_approx i)"
- unfolding prod_approx_def by simp
- show "(\<Squnion>i. prod_approx i) = ID"
- unfolding prod_approx_def
- by (simp add: lub_distribs cprod_map_ID)
- show "\<And>i. finite_deflation (prod_approx i)"
- unfolding prod_approx_def
- by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
-qed
-
-definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "prod_sfp = sfp_fun2 prod_approx cprod_map"
-
-lemma cast_prod_sfp:
- "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
- cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
-unfolding prod_sfp_def
-apply (rule cast_sfp_fun2 [OF prod_approx])
-apply (erule (1) finite_deflation_cprod_map)
-done
-
-instantiation prod :: (bifinite, bifinite) bifinite
-begin
-
-definition
- "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
-
-definition
- "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def
- using ep_pair_udom [OF prod_approx]
- by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
- unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
-qed
-
end
-
-lemma SFP_prod:
- "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_prod_def)
-
-end
--- a/src/HOLCF/Lift.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Lift.thy Sat Oct 09 07:24:49 2010 -0700
@@ -170,90 +170,4 @@
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cases x, simp_all)
-
-subsection {* Lifted countable types are bifinite domains *}
-
-definition
- lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
-where
- "lift_approx = (\<lambda>i. FLIFT x. if to_nat x < i then Def x else \<bottom>)"
-
-lemma chain_lift_approx [simp]: "chain lift_approx"
- unfolding lift_approx_def
- by (rule chainI, simp add: FLIFT_mono)
-
-lemma lub_lift_approx [simp]: "(\<Squnion>i. lift_approx i) = ID"
-apply (rule ext_cfun)
-apply (simp add: contlub_cfun_fun)
-apply (simp add: lift_approx_def)
-apply (case_tac x, simp)
-apply (rule thelubI)
-apply (rule is_lubI)
-apply (rule ub_rangeI, simp)
-apply (drule ub_rangeD)
-apply (erule rev_below_trans)
-apply simp
-apply (rule lessI)
-done
-
-lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
-proof
- fix x
- show "lift_approx i\<cdot>x \<sqsubseteq> x"
- unfolding lift_approx_def
- by (cases x, simp, simp)
- show "lift_approx i\<cdot>(lift_approx i\<cdot>x) = lift_approx i\<cdot>x"
- unfolding lift_approx_def
- by (cases x, simp, simp)
- show "finite {x::'a lift. lift_approx i\<cdot>x = x}"
- proof (rule finite_subset)
- let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
- show "{x::'a lift. lift_approx i\<cdot>x = x} \<subseteq> ?S"
- unfolding lift_approx_def
- by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
- show "finite ?S"
- by (simp add: finite_vimageI)
- qed
-qed
-
-lemma lift_approx: "approx_chain lift_approx"
-using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
-by (rule approx_chain.intro)
-
-instantiation lift :: (countable) bifinite
-begin
-
-definition
- "emb = udom_emb lift_approx"
-
-definition
- "prj = udom_prj lift_approx"
-
-definition
- "sfp (t::'a lift itself) =
- (\<Squnion>i. sfp_principal (Abs_fin_defl (emb oo lift_approx i oo prj)))"
-
-instance proof
- show ep: "ep_pair emb (prj :: udom \<rightarrow> 'a lift)"
- unfolding emb_lift_def prj_lift_def
- by (rule ep_pair_udom [OF lift_approx])
- show "cast\<cdot>SFP('a lift) = emb oo (prj :: udom \<rightarrow> 'a lift)"
- unfolding sfp_lift_def
- apply (subst contlub_cfun_arg)
- apply (rule chainI)
- apply (rule sfp.principal_mono)
- apply (simp add: below_fin_defl_def)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep])
- apply (intro monofun_cfun below_refl)
- apply (rule chainE)
- apply (rule chain_lift_approx)
- apply (subst cast_sfp_principal)
- apply (simp add: Abs_fin_defl_inverse finite_deflation_lift_approx
- ep_pair.finite_deflation_e_d_p [OF ep] lub_distribs)
- done
-qed
-
end
-
-end
--- a/src/HOLCF/Representable.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Representable.thy Sat Oct 09 07:24:49 2010 -0700
@@ -5,7 +5,7 @@
header {* Representable Types *}
theory Representable
-imports Algebraic Universal Ssum One Fixrec Domain_Aux
+imports Algebraic Bifinite Universal Ssum One Fixrec Domain_Aux
uses
("Tools/repdef.ML")
("Tools/Domain/domain_isomorphism.ML")
--- a/src/HOLCF/Sprod.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Sprod.thy Sat Oct 09 07:24:49 2010 -0700
@@ -5,7 +5,7 @@
header {* The type of strict products *}
theory Sprod
-imports Bifinite
+imports Deflation
begin
default_sort pcpo
@@ -310,65 +310,4 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict product is a bifinite domain *}
-
-definition
- sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
-where
- "sprod_approx = (\<lambda>i. sprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma sprod_approx: "approx_chain sprod_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. sprod_approx i)"
- unfolding sprod_approx_def by simp
- show "(\<Squnion>i. sprod_approx i) = ID"
- unfolding sprod_approx_def
- by (simp add: lub_distribs sprod_map_ID)
- show "\<And>i. finite_deflation (sprod_approx i)"
- unfolding sprod_approx_def
- by (intro finite_deflation_sprod_map finite_deflation_udom_approx)
-qed
-
-definition sprod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "sprod_sfp = sfp_fun2 sprod_approx sprod_map"
-
-lemma cast_sprod_sfp:
- "cast\<cdot>(sprod_sfp\<cdot>A\<cdot>B) =
- udom_emb sprod_approx oo
- sprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo
- udom_prj sprod_approx"
-unfolding sprod_sfp_def
-apply (rule cast_sfp_fun2 [OF sprod_approx])
-apply (erule (1) finite_deflation_sprod_map)
-done
-
-instantiation sprod :: (bifinite, bifinite) bifinite
-begin
-
-definition
- "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj sprod_approx"
-
-definition
- "sfp (t::('a \<otimes> 'b) itself) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
- unfolding emb_sprod_def prj_sprod_def
- using ep_pair_udom [OF sprod_approx]
- by (intro ep_pair_comp ep_pair_sprod_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a \<otimes> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<otimes> 'b)"
- unfolding emb_sprod_def prj_sprod_def sfp_sprod_def cast_sprod_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq sprod_map_map)
-qed
-
end
-
-lemma SFP_sprod:
- "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_sprod_def)
-
-end
--- a/src/HOLCF/Ssum.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Ssum.thy Sat Oct 09 07:24:49 2010 -0700
@@ -295,63 +295,4 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict sum is a bifinite domain *}
-
-definition
- ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
-where
- "ssum_approx = (\<lambda>i. ssum_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
-
-lemma ssum_approx: "approx_chain ssum_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. ssum_approx i)"
- unfolding ssum_approx_def by simp
- show "(\<Squnion>i. ssum_approx i) = ID"
- unfolding ssum_approx_def
- by (simp add: lub_distribs ssum_map_ID)
- show "\<And>i. finite_deflation (ssum_approx i)"
- unfolding ssum_approx_def
- by (intro finite_deflation_ssum_map finite_deflation_udom_approx)
-qed
-
-definition ssum_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
-where "ssum_sfp = sfp_fun2 ssum_approx ssum_map"
-
-lemma cast_ssum_sfp:
- "cast\<cdot>(ssum_sfp\<cdot>A\<cdot>B) =
- udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx"
-unfolding ssum_sfp_def
-apply (rule cast_sfp_fun2 [OF ssum_approx])
-apply (erule (1) finite_deflation_ssum_map)
-done
-
-instantiation ssum :: (bifinite, bifinite) bifinite
-begin
-
-definition
- "emb = udom_emb ssum_approx oo ssum_map\<cdot>emb\<cdot>emb"
-
-definition
- "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj ssum_approx"
-
-definition
- "sfp (t::('a \<oplus> 'b) itself) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def
- using ep_pair_udom [OF ssum_approx]
- by (intro ep_pair_comp ep_pair_ssum_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a \<oplus> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<oplus> 'b)"
- unfolding emb_ssum_def prj_ssum_def sfp_ssum_def cast_ssum_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq ssum_map_map)
-qed
-
end
-
-lemma SFP_ssum:
- "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
-by (rule sfp_ssum_def)
-
-end
--- a/src/HOLCF/Up.thy Fri Oct 08 07:39:50 2010 -0700
+++ b/src/HOLCF/Up.thy Sat Oct 09 07:24:49 2010 -0700
@@ -5,7 +5,7 @@
header {* The type of lifted values *}
theory Up
-imports Bifinite
+imports Deflation
begin
default_sort cpo
@@ -332,60 +332,4 @@
by (rule finite_subset, simp add: d.finite_fixes)
qed
-subsection {* Lifted cpo is a bifinite domain *}
-
-definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
-where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
-
-lemma u_approx: "approx_chain u_approx"
-proof (rule approx_chain.intro)
- show "chain (\<lambda>i. u_approx i)"
- unfolding u_approx_def by simp
- show "(\<Squnion>i. u_approx i) = ID"
- unfolding u_approx_def
- by (simp add: lub_distribs u_map_ID)
- show "\<And>i. finite_deflation (u_approx i)"
- unfolding u_approx_def
- by (intro finite_deflation_u_map finite_deflation_udom_approx)
-qed
-
-definition u_sfp :: "sfp \<rightarrow> sfp"
-where "u_sfp = sfp_fun1 u_approx u_map"
-
-lemma cast_u_sfp:
- "cast\<cdot>(u_sfp\<cdot>A) =
- udom_emb u_approx oo u_map\<cdot>(cast\<cdot>A) oo udom_prj u_approx"
-unfolding u_sfp_def
-apply (rule cast_sfp_fun1 [OF u_approx])
-apply (erule finite_deflation_u_map)
-done
-
-instantiation u :: (bifinite) bifinite
-begin
-
-definition
- "emb = udom_emb u_approx oo u_map\<cdot>emb"
-
-definition
- "prj = u_map\<cdot>prj oo udom_prj u_approx"
-
-definition
- "sfp (t::'a u itself) = u_sfp\<cdot>SFP('a)"
-
-instance proof
- show "ep_pair emb (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def
- using ep_pair_udom [OF u_approx]
- by (intro ep_pair_comp ep_pair_u_map ep_pair_emb_prj)
-next
- show "cast\<cdot>SFP('a u) = emb oo (prj :: udom \<rightarrow> 'a u)"
- unfolding emb_u_def prj_u_def sfp_u_def cast_u_sfp
- by (simp add: cast_SFP oo_def expand_cfun_eq u_map_map)
-qed
-
end
-
-lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
-by (rule sfp_u_def)
-
-end