src/HOLCF/Cprod.thy
changeset 17816 9942c5ed866a
parent 16916 da331e0a4a81
child 17834 28414668b43d
equal deleted inserted replaced
17815:ccf54e3cabfa 17816:9942c5ed866a
   193 
   193 
   194 translations
   194 translations
   195   "<x, y, z>" == "<x, <y, z>>"
   195   "<x, y, z>" == "<x, <y, z>>"
   196   "<x, y>"    == "cpair$x$y"
   196   "<x, y>"    == "cpair$x$y"
   197 
   197 
       
   198 syntax
       
   199   "_ctuple_pttrn" :: "[pttrn, patterns] => pttrn"  ("<_,/ _>")
       
   200 
       
   201 translations
       
   202   "LAM <x,y,zs>. t"       == "csplit$(LAM x <y,zs>. t)"
       
   203   "LAM <x,y>. t"          == "csplit$(LAM x y. t)"
       
   204 
   198 defs
   205 defs
   199   cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
   206   cpair_def:  "cpair  \<equiv> (\<Lambda> x y. (x, y))"
   200   cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
   207   cfst_def:   "cfst   \<equiv> (\<Lambda> p. fst p)"
   201   csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
   208   csnd_def:   "csnd   \<equiv> (\<Lambda> p. snd p)"      
   202   csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   209   csplit_def: "csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
   203 
   210 
   204 subsection {* Syntax *}
       
   205 
       
   206 text {* syntax for @{text "LAM <x,y,z>.e"} *}
       
   207 
       
   208 syntax
       
   209   "_LAM" :: "[patterns, 'a \<Rightarrow> 'b] \<Rightarrow> ('a \<rightarrow> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
       
   210 
       
   211 translations
       
   212   "LAM <x,y,zs>. b"       == "csplit$(LAM x. LAM <y,zs>. b)"
       
   213   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
       
   214   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
       
   215 
       
   216 syntax (xsymbols)
       
   217   "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
       
   218 
       
   219 text {* syntax for Let *}
       
   220 
       
   221 constdefs
       
   222   CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b"
       
   223   "CLet \<equiv> \<Lambda> s f. f\<cdot>s"
       
   224 
       
   225 nonterminals
       
   226   Cletbinds  Cletbind
       
   227 
       
   228 syntax
       
   229   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
       
   230   "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
       
   231   ""        :: "Cletbind => Cletbinds"               ("_")
       
   232   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
       
   233   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
       
   234 
       
   235 translations
       
   236   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
       
   237   "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
       
   238   "Let x = a in e"          == "CLet$a$(LAM x. e)"
       
   239   "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
       
   240 
       
   241 subsection {* Convert all lemmas to the continuous versions *}
   211 subsection {* Convert all lemmas to the continuous versions *}
   242 
   212 
   243 lemma cpair_eq_pair: "<x, y> = (x, y)"
   213 lemma cpair_eq_pair: "<x, y> = (x, y)"
   244 by (simp add: cpair_def cont_pair1 cont_pair2)
   214 by (simp add: cpair_def cont_pair1 cont_pair2)
   245 
   215