src/HOLCF/Cprod.thy
changeset 33399 768b2bb9e66a
parent 31113 15cf300a742f
child 35900 aa5dfb03eb1e
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Nov 02 13:43:50 2009 -0800
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Nov 02 17:19:49 2009 -0800
     1.3 @@ -52,6 +52,7 @@
     1.4  
     1.5  translations
     1.6    "\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
     1.7 +  "\<Lambda>(CONST Pair x y). t" => "CONST csplit\<cdot>(\<Lambda> x y. t)"
     1.8  
     1.9  
    1.10  subsection {* Convert all lemmas to the continuous versions *}
    1.11 @@ -150,6 +151,9 @@
    1.12  lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
    1.13  by (simp add: csplit_def cpair_cfst_csnd)
    1.14  
    1.15 +lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    1.16 +by (simp add: csplit_def cfst_def csnd_def)
    1.17 +
    1.18  lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
    1.19  
    1.20  subsection {* Product type is a bifinite domain *}