src/HOLCF/Ssum.thy
 changeset 26962 c8b20f615d6c parent 26046 1624b3304bb9 child 27310 d0229bc6c461
```--- a/src/HOLCF/Ssum.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Ssum.thy	Mon May 19 23:49:20 2008 +0200
@@ -216,11 +216,12 @@

subsection {* Strict sum is a bifinite domain *}

-instance "++" :: (bifinite, bifinite) approx ..
+instantiation "++" :: (bifinite, bifinite) bifinite
+begin

+definition
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))"
+    "approx = (\<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
@@ -228,8 +229,7 @@
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
+instance proof
fix i :: nat and x :: "'a \<oplus> 'b"
show "chain (\<lambda>i. approx i\<cdot>x)"
unfolding approx_ssum_def by simp
@@ -248,3 +248,5 @@
qed

end
+
+end```