src/HOLCF/Cprod3.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4191 f967419250d1
child 10834 a7897aebbffc
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Cprod3.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
wenzelm@3693
     6
Class instance of * for class pcpo and cpo.
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Cprod3 = Cprod2 +
nipkow@243
    10
slotosch@2840
    11
instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
slotosch@2840
    12
instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)
nipkow@243
    13
wenzelm@3693
    14
consts
wenzelm@3693
    15
        cpair        :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
clasohm@1479
    16
        cfst         :: "('a*'b)->'a"
clasohm@1479
    17
        csnd         :: "('a*'b)->'b"
clasohm@1479
    18
        csplit       :: "('a->'b->'c)->('a*'b)->'c"
nipkow@243
    19
wenzelm@3693
    20
syntax
clasohm@1479
    21
        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
regensbu@1168
    22
wenzelm@3693
    23
translations
clasohm@1479
    24
        "<x, y, z>"   == "<x, <y, z>>"
clasohm@1479
    25
        "<x, y>"      == "cpair`x`y"
nipkow@625
    26
regensbu@1168
    27
defs
clasohm@1479
    28
cpair_def       "cpair  == (LAM x y.(x,y))"
wenzelm@3842
    29
cfst_def        "cfst   == (LAM p. fst(p))"
wenzelm@3842
    30
csnd_def        "csnd   == (LAM p. snd(p))"      
wenzelm@3842
    31
csplit_def      "csplit == (LAM f p. f`(cfst`p)`(csnd`p))"
nipkow@243
    32
regensbu@1274
    33
regensbu@1274
    34
regensbu@1274
    35
(* introduce syntax for
regensbu@1274
    36
regensbu@1274
    37
   Let <x,y> = e1; z = E2 in E3
regensbu@1274
    38
regensbu@1274
    39
   and
regensbu@1274
    40
oheimb@2394
    41
   LAM <x,y,z>.e
regensbu@1274
    42
*)
regensbu@1274
    43
wenzelm@3693
    44
constdefs
wenzelm@3693
    45
  CLet           :: "'a -> ('a -> 'b) -> 'b"
wenzelm@3842
    46
  "CLet == LAM s f. f`s"
wenzelm@3693
    47
regensbu@1274
    48
wenzelm@3693
    49
(* syntax for Let *)
wenzelm@3693
    50
wenzelm@3693
    51
types
wenzelm@3693
    52
  Cletbinds  Cletbind
regensbu@1274
    53
regensbu@1274
    54
syntax
regensbu@1274
    55
  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
regensbu@1274
    56
  ""        :: "Cletbind => Cletbinds"               ("_")
regensbu@1274
    57
  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
wenzelm@3693
    58
  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
regensbu@1274
    59
regensbu@1274
    60
translations
regensbu@1274
    61
  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
wenzelm@3842
    62
  "Let x = a in e"          == "CLet`a`(LAM x. e)"
regensbu@1274
    63
wenzelm@3693
    64
wenzelm@3693
    65
(* syntax for LAM <x,y,z>.e *)
regensbu@1274
    66
regensbu@1274
    67
syntax
wenzelm@3693
    68
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
regensbu@1274
    69
regensbu@1274
    70
translations
wenzelm@3693
    71
  "LAM <x,y,zs>.b"        == "csplit`(LAM x. LAM <y,zs>.b)"
wenzelm@3693
    72
  "LAM <x,y>. LAM zs. b"  <= "csplit`(LAM x y zs. b)"
wenzelm@3693
    73
  "LAM <x,y>.b"           == "csplit`(LAM x y. b)"
wenzelm@3693
    74
wenzelm@3693
    75
syntax (symbols)
wenzelm@4191
    76
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
regensbu@1274
    77
nipkow@243
    78
end