src/HOLCF/Cprod3.thy
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 10834 a7897aebbffc
child 12114 a8e860c86252
permissions -rw-r--r--
GPLed;
slotosch@2640
     1
(*  Title:      HOLCF/Cprod3.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
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>>"
nipkow@10834
    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))"      
nipkow@10834
    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"
nipkow@10834
    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)"
nipkow@10834
    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
nipkow@10834
    71
  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
nipkow@10834
    72
  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
nipkow@10834
    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