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