(* Title: HOLCF/Cprod3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
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 (symbols)
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
end