src/HOLCF/Sprod3.thy
changeset 243 c22b85994e17
child 442 13ac1fd0a14d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Sprod3.thy	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title: 	HOLCF/sprod3.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright   1993 Technische Universitaet Muenchen
     1.8 +
     1.9 +Class instance of  ** for class pcpo
    1.10 +*)
    1.11 +
    1.12 +Sprod3 = Sprod2 +
    1.13 +
    1.14 +arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
    1.15 +
    1.16 +consts  
    1.17 +	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
    1.18 +	"cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair")
    1.19 +					(* continuous strict pairing *)
    1.20 +	sfst         :: "('a**'b)->'a"
    1.21 +	ssnd         :: "('a**'b)->'b"
    1.22 +	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
    1.23 +
    1.24 +rules 
    1.25 +
    1.26 +inst_sprod_pcpo	"UU::'a**'b = Ispair(UU,UU)"
    1.27 +spair_def	"spair  == (LAM x y.Ispair(x,y))"
    1.28 +sfst_def	"sfst   == (LAM p.Isfst(p))"
    1.29 +ssnd_def	"ssnd   == (LAM p.Issnd(p))"	
    1.30 +ssplit_def	"ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])"
    1.31 +
    1.32 +end
    1.33 +
    1.34 +ML
    1.35 +
    1.36 +(* ----------------------------------------------------------------------*)
    1.37 +(* parse translations for the above mixfix                               *)
    1.38 +(* ----------------------------------------------------------------------*)
    1.39 +
    1.40 +val parse_translation = [("@spair",mk_cinfixtr "@spair")];
    1.41 +
    1.42 +