src/HOLCF/Cprod.thy
changeset 18078 20e5a6440790
parent 18077 f1f4f951ec8d
child 18289 56ddf617d6e8
equal deleted inserted replaced
18077:f1f4f951ec8d 18078:20e5a6440790
   200 
   200 
   201 syntax (xsymbols)
   201 syntax (xsymbols)
   202   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   202   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
   203 
   203 
   204 translations
   204 translations
   205   "<x, y, z>" == "<x, <y, z>>"
   205   "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   206   "<x, y>"    == "cpair$x$y"
   206   "\<langle>x, y\<rangle>"    == "cpair\<cdot>x\<cdot>y"
   207 
       
   208 text {* syntax for @{text "LAM <x,y,z>.e"} *}
       
   209 
       
   210 syntax
       
   211   "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
       
   212 
       
   213 syntax (xsymbols)
       
   214   "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("\<langle>_,/ _\<rangle>")
       
   215 
   207 
   216 translations
   208 translations
   217   "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
   209   "\<Lambda>(cpair\<cdot>x\<cdot>y). t" == "csplit\<cdot>(\<Lambda> x y. t)"
   218   "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
       
   219 
   210 
   220 
   211 
   221 subsection {* Convert all lemmas to the continuous versions *}
   212 subsection {* Convert all lemmas to the continuous versions *}
   222 
   213 
   223 lemma cpair_eq_pair: "<x, y> = (x, y)"
   214 lemma cpair_eq_pair: "<x, y> = (x, y)"