slotosch@2640: (*  Title:      HOLCF/Cprod3.thy
nipkow@243:     ID:         $Id$
clasohm@1479:     Author:     Franz Regensburger
wenzelm@12030:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243: 
wenzelm@3693: Class instance of * for class pcpo and cpo.
nipkow@243: *)
nipkow@243: 
nipkow@243: Cprod3 = Cprod2 +
nipkow@243: 
slotosch@2840: instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
slotosch@2840: instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)
nipkow@243: 
wenzelm@3693: consts
wenzelm@3693:         cpair        :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
clasohm@1479:         cfst         :: "('a*'b)->'a"
clasohm@1479:         csnd         :: "('a*'b)->'b"
clasohm@1479:         csplit       :: "('a->'b->'c)->('a*'b)->'c"
nipkow@243: 
wenzelm@3693: syntax
clasohm@1479:         "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
regensbu@1168: 
wenzelm@3693: translations
clasohm@1479:         "<x, y, z>"   == "<x, <y, z>>"
nipkow@10834:         "<x, y>"      == "cpair$x$y"
nipkow@625: 
regensbu@1168: defs
clasohm@1479: cpair_def       "cpair  == (LAM x y.(x,y))"
wenzelm@3842: cfst_def        "cfst   == (LAM p. fst(p))"
wenzelm@3842: csnd_def        "csnd   == (LAM p. snd(p))"      
nipkow@10834: csplit_def      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
nipkow@243: 
regensbu@1274: 
regensbu@1274: 
regensbu@1274: (* introduce syntax for
regensbu@1274: 
regensbu@1274:    Let <x,y> = e1; z = E2 in E3
regensbu@1274: 
regensbu@1274:    and
regensbu@1274: 
oheimb@2394:    LAM <x,y,z>.e
regensbu@1274: *)
regensbu@1274: 
wenzelm@3693: constdefs
wenzelm@3693:   CLet           :: "'a -> ('a -> 'b) -> 'b"
nipkow@10834:   "CLet == LAM s f. f$s"
wenzelm@3693: 
regensbu@1274: 
wenzelm@3693: (* syntax for Let *)
wenzelm@3693: 
wenzelm@3693: types
wenzelm@3693:   Cletbinds  Cletbind
regensbu@1274: 
regensbu@1274: syntax
regensbu@1274:   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
regensbu@1274:   ""        :: "Cletbind => Cletbinds"               ("_")
regensbu@1274:   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
wenzelm@3693:   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
regensbu@1274: 
regensbu@1274: translations
regensbu@1274:   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
nipkow@10834:   "Let x = a in e"          == "CLet$a$(LAM x. e)"
regensbu@1274: 
wenzelm@3693: 
wenzelm@3693: (* syntax for LAM <x,y,z>.e *)
regensbu@1274: 
regensbu@1274: syntax
wenzelm@3693:   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
regensbu@1274: 
regensbu@1274: translations
nipkow@10834:   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
nipkow@10834:   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
nipkow@10834:   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
wenzelm@3693: 
wenzelm@3693: syntax (symbols)
wenzelm@4191:   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
regensbu@1274: 
nipkow@243: end