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;
clasohm@1479
     1
(*  Title:      HOLCF/sprod3.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Class instance of  ** for class pcpo
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Sprod3 = Sprod2 +
nipkow@243
    10
slotosch@2640
    11
instance "**" :: (pcpo,pcpo)pcpo  (least_sprod,cpo_sprod)
nipkow@243
    12
regensbu@752
    13
consts  
oheimb@2394
    14
  spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
oheimb@2394
    15
  sfst		:: "('a**'b)->'a"
oheimb@2394
    16
  ssnd		:: "('a**'b)->'b"
oheimb@2394
    17
  ssplit	:: "('a->'b->'c)->('a**'b)->'c"
nipkow@243
    18
regensbu@1168
    19
syntax  
wenzelm@5033
    20
  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
regensbu@752
    21
regensbu@1168
    22
translations
wenzelm@5033
    23
        "(:x, y, z:)"   == "(:x, (:y, z:):)"
wenzelm@5033
    24
        "(:x, y:)"      == "spair`x`y"
nipkow@625
    25
regensbu@1168
    26
defs
wenzelm@3842
    27
spair_def       "spair  == (LAM x y. Ispair x y)"
wenzelm@3842
    28
sfst_def        "sfst   == (LAM p. Isfst p)"
wenzelm@3842
    29
ssnd_def        "ssnd   == (LAM p. Issnd p)"     
wenzelm@3842
    30
ssplit_def      "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
nipkow@243
    31
nipkow@243
    32
end