src/HOLCF/Cprod3.thy

clarified multi statements;

(*  Title:      HOLCF/Cprod3.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Class instance of * for class pcpo and cpo.
*)

Cprod3 = Cprod2 +

instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)

consts
        cpair        :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
        cfst         :: "('a*'b)->'a"
        csnd         :: "('a*'b)->'b"
        csplit       :: "('a->'b->'c)->('a*'b)->'c"

syntax
        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")

translations
        "<x, y, z>"   == "<x, <y, z>>"
        "<x, y>"      == "cpair$x$y"

defs
cpair_def       "cpair  == (LAM x y.(x,y))"
cfst_def        "cfst   == (LAM p. fst(p))"
csnd_def        "csnd   == (LAM p. snd(p))"      
csplit_def      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"



(* introduce syntax for

   Let <x,y> = e1; z = E2 in E3

   and

   LAM <x,y,z>.e
*)

constdefs
  CLet           :: "'a -> ('a -> 'b) -> 'b"
  "CLet == LAM s f. f$s"


(* syntax for Let *)

types
  Cletbinds  Cletbind

syntax
  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
  ""        :: "Cletbind => Cletbinds"               ("_")
  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)

translations
  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
  "Let x = a in e"          == "CLet$a$(LAM x. e)"


(* syntax for LAM <x,y,z>.e *)

syntax
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)

translations
  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"

syntax (xsymbols)
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)

end