add (LAM (x, y). t) syntax and lemma csplit_Pair
authorhuffman
Mon Nov 02 17:19:49 2009 -0800 (2009-11-02)
changeset 33399768b2bb9e66a
parent 33397 609389f3ea1e
child 33400 7c4ab69a15c3
add (LAM (x, y). t) syntax and lemma csplit_Pair
src/HOLCF/Cprod.thy
     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 *}