src/HOLCF/Sprod3.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5033 06f03dc5a1dc
child 10834 a7897aebbffc
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 instance "**" :: (pcpo,pcpo)pcpo  (least_sprod,cpo_sprod)
    12 
    13 consts  
    14   spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
    15   sfst		:: "('a**'b)->'a"
    16   ssnd		:: "('a**'b)->'b"
    17   ssplit	:: "('a->'b->'c)->('a**'b)->'c"
    18 
    19 syntax  
    20   "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
    21 
    22 translations
    23         "(:x, y, z:)"   == "(:x, (:y, z:):)"
    24         "(:x, y:)"      == "spair`x`y"
    25 
    26 defs
    27 spair_def       "spair  == (LAM x y. Ispair x y)"
    28 sfst_def        "sfst   == (LAM p. Isfst p)"
    29 ssnd_def        "ssnd   == (LAM p. Issnd p)"     
    30 ssplit_def      "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
    31 
    32 end