src/HOLCF/Ssum.thy
 changeset 25915 f1bce5261dec parent 25882 c58e380d9f7d child 26046 1624b3304bb9
```--- a/src/HOLCF/Ssum.thy	Tue Jan 15 02:20:47 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Tue Jan 15 02:38:13 2008 +0100
@@ -99,10 +99,10 @@
text {* Strictness *}

lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)

lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)

lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
@@ -214,4 +214,37 @@
apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
done

+subsection {* Strict sum is a bifinite domain *}
+
+instance "++" :: (bifinite, bifinite) approx ..
+
+  approx_ssum_def:
+    "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
+
+lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
+unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
+
+lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
+unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
+
+instance "++" :: (bifinite, bifinite) bifinite
+proof
+  fix i :: nat and x :: "'a \<oplus> 'b"
+  show "chain (\<lambda>i. approx i\<cdot>x)"
+    unfolding approx_ssum_def by simp
+  show "(\<Squnion>i. approx i\<cdot>x) = x"
+    unfolding approx_ssum_def
+    by (simp add: lub_distribs eta_cfun)
+  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+    by (cases x, simp add: approx_ssum_def, simp, simp)
+  have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
+        (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
+        (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
+    by (rule subsetI, rule_tac p=x in ssumE2, simp, simp)
+  thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
+    by (rule finite_subset,
+        intro finite_UnI finite_imageI finite_fixes_approx)
+qed
+
end```