src/HOLCF/Sprod.thy
changeset 26962 c8b20f615d6c
parent 25914 ff835e25ae87
child 27310 d0229bc6c461
     1.1 --- a/src/HOLCF/Sprod.thy	Sun May 18 17:04:48 2008 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Mon May 19 23:49:20 2008 +0200
     1.3 @@ -230,14 +230,14 @@
     1.4  
     1.5  subsection {* Strict product is a bifinite domain *}
     1.6  
     1.7 -instance "**" :: (bifinite, bifinite) approx ..
     1.8 +instantiation "**" :: (bifinite, bifinite) bifinite
     1.9 +begin
    1.10  
    1.11 -defs (overloaded)
    1.12 +definition
    1.13    approx_sprod_def:
    1.14 -    "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
    1.15 +    "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
    1.16  
    1.17 -instance "**" :: (bifinite, bifinite) bifinite
    1.18 -proof
    1.19 +instance proof
    1.20    fix i :: nat and x :: "'a \<otimes> 'b"
    1.21    show "chain (\<lambda>i. approx i\<cdot>x)"
    1.22      unfolding approx_sprod_def by simp
    1.23 @@ -259,6 +259,8 @@
    1.24      by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
    1.25  qed
    1.26  
    1.27 +end
    1.28 +
    1.29  lemma approx_spair [simp]:
    1.30    "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
    1.31  unfolding approx_sprod_def