src/HOLCF/sprod3.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/sprod3.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Class instance of  ** for class pcpo
     7 *)
     8 
     9 Sprod3 = Sprod2 +
    10 
    11 arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
    12 
    13 consts  
    14 	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
    15 	"cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair")
    16 					(* continuous strict pairing *)
    17 	sfst         :: "('a**'b)->'a"
    18 	ssnd         :: "('a**'b)->'b"
    19 	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
    20 
    21 rules 
    22 
    23 inst_sprod_pcpo	"UU::'a**'b = Ispair(UU,UU)"
    24 spair_def	"spair  == (LAM x y.Ispair(x,y))"
    25 sfst_def	"sfst   == (LAM p.Isfst(p))"
    26 ssnd_def	"ssnd   == (LAM p.Issnd(p))"	
    27 ssplit_def	"ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])"
    28 
    29 end
    30 
    31 ML
    32 
    33 (* ----------------------------------------------------------------------*)
    34 (* parse translations for the above mixfix                               *)
    35 (* ----------------------------------------------------------------------*)
    36 
    37 val parse_translation = [("@spair",mk_cinfixtr "@spair")];
    38 
    39