diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Ssum.thy --- 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 -defs (overloaded) +definition approx_ssum_def: - "approx \ \n. sscase\(\ x. sinl\(approx n\x))\(\ y. sinr\(approx n\y))" + "approx = (\n. sscase\(\ x. sinl\(approx n\x))\(\ y. sinr\(approx n\y)))" lemma approx_sinl [simp]: "approx i\(sinl\x) = sinl\(approx i\x)" unfolding approx_ssum_def by (cases "x = \") simp_all @@ -228,8 +229,7 @@ lemma approx_sinr [simp]: "approx i\(sinr\x) = sinr\(approx i\x)" unfolding approx_ssum_def by (cases "x = \") simp_all -instance "++" :: (bifinite, bifinite) bifinite -proof +instance proof fix i :: nat and x :: "'a \ 'b" show "chain (\i. approx i\x)" unfolding approx_ssum_def by simp @@ -248,3 +248,5 @@ qed end + +end