src/HOLCF/cprod3.thy

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.

(*  Title: 	HOLCF/cprod3.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen


Class instance of  * for class pcpo

*)

Cprod3 = Cprod2 +

arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)

consts  
	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
	"cop @cpair" :: "'a -> 'b -> ('a*'b)" ("cpair")
					(* continuous  pairing *)
	cfst         :: "('a*'b)->'a"
	csnd         :: "('a*'b)->'b"
	csplit       :: "('a->'b->'c)->('a*'b)->'c"

rules 

inst_cprod_pcpo	"UU::'a*'b = <UU,UU>"

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]])"

end

ML

(* ----------------------------------------------------------------------*)
(* parse translations for the above mixfix                               *)
(* ----------------------------------------------------------------------*)

val parse_translation = [("@cpair",mk_cinfixtr "@cpair")];