src/HOLCF/Cprod.thy
changeset 17834 28414668b43d
parent 17816 9942c5ed866a
child 17837 2922be3544f8
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Oct 11 23:23:39 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Tue Oct 11 23:27:14 2005 +0200
     1.3 @@ -182,31 +182,41 @@
     1.4  
     1.5  subsection {* Continuous versions of constants *}
     1.6  
     1.7 -consts
     1.8 -  cpair  :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
     1.9 -  cfst   :: "('a * 'b) \<rightarrow> 'a"
    1.10 -  csnd   :: "('a * 'b) \<rightarrow> 'b"
    1.11 +constdefs
    1.12 +  cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *)
    1.13 +  "cpair \<equiv> (\<Lambda> x y. (x, y))"
    1.14 +
    1.15 +  cfst :: "('a * 'b) \<rightarrow> 'a"
    1.16 +  "cfst \<equiv> (\<Lambda> p. fst p)"
    1.17 +
    1.18 +  csnd :: "('a * 'b) \<rightarrow> 'b"
    1.19 +  "csnd \<equiv> (\<Lambda> p. snd p)"      
    1.20 +
    1.21    csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c"
    1.22 +  "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
    1.23  
    1.24  syntax
    1.25 -  "@ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
    1.26 +  "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
    1.27 +
    1.28 +syntax (xsymbols)
    1.29 +  "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1\<langle>_,/ _\<rangle>)")
    1.30  
    1.31  translations
    1.32    "<x, y, z>" == "<x, <y, z>>"
    1.33    "<x, y>"    == "cpair$x$y"
    1.34  
    1.35 +text {* syntax for @{text "LAM <x,y,z>.e"} *}
    1.36 +
    1.37  syntax
    1.38    "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
    1.39  
    1.40 +syntax (xsymbols)
    1.41 +  "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("\<langle>_,/ _\<rangle>")
    1.42 +
    1.43  translations
    1.44    "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
    1.45    "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
    1.46  
    1.47 -defs
    1.48 -  cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
    1.49 -  cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
    1.50 -  csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
    1.51 -  csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
    1.52  
    1.53  subsection {* Convert all lemmas to the continuous versions *}
    1.54