src/HOLCF/Cprod3.thy
author wenzelm
Mon Sep 22 17:35:52 1997 +0200 (1997-09-22)
changeset 3693 37aa547fb564
parent 2840 7e03e61612b0
child 3842 b55686a7b22c
permissions -rw-r--r--
fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
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))"
clasohm@1479
    29
cfst_def        "cfst   == (LAM p.fst(p))"
clasohm@1479
    30
csnd_def        "csnd   == (LAM p.snd(p))"      
clasohm@1479
    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@3693
    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)"
regensbu@1274
    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@3693
    76
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda><_>./ _)" [0, 10] 10)
regensbu@1274
    77
nipkow@243
    78
end