--- 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