src/HOLCF/Cprod3.thy
author clasohm
Tue Feb 06 12:42:31 1996 +0100 (1996-02-06)
changeset 1479 21eb5e156d91
parent 1274 ea0668a1c0ba
child 2278 d63ffafce255
permissions -rw-r--r--
expanded tabs
clasohm@1479
     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
nipkow@243
     6
nipkow@243
     7
Class instance of  * for class pcpo
nipkow@243
     8
nipkow@243
     9
*)
nipkow@243
    10
nipkow@243
    11
Cprod3 = Cprod2 +
nipkow@243
    12
clasohm@1479
    13
arities "*" :: (pcpo,pcpo)pcpo                  (* Witness cprod2.ML *)
nipkow@243
    14
nipkow@243
    15
consts  
clasohm@1479
    16
        cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
clasohm@1479
    17
        cfst         :: "('a*'b)->'a"
clasohm@1479
    18
        csnd         :: "('a*'b)->'b"
clasohm@1479
    19
        csplit       :: "('a->'b->'c)->('a*'b)->'c"
nipkow@243
    20
clasohm@1479
    21
syntax  
clasohm@1479
    22
        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
regensbu@1168
    23
regensbu@752
    24
regensbu@1168
    25
translations 
clasohm@1479
    26
        "<x, y, z>"   == "<x, <y, z>>"
clasohm@1479
    27
        "<x, y>"      == "cpair`x`y"
nipkow@625
    28
nipkow@243
    29
rules 
nipkow@243
    30
clasohm@1479
    31
inst_cprod_pcpo "(UU::'a*'b) = (UU,UU)"
nipkow@243
    32
regensbu@1168
    33
defs
clasohm@1479
    34
cpair_def       "cpair  == (LAM x y.(x,y))"
clasohm@1479
    35
cfst_def        "cfst   == (LAM p.fst(p))"
clasohm@1479
    36
csnd_def        "csnd   == (LAM p.snd(p))"      
clasohm@1479
    37
csplit_def      "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
nipkow@243
    38
regensbu@1274
    39
regensbu@1274
    40
regensbu@1274
    41
(* introduce syntax for
regensbu@1274
    42
regensbu@1274
    43
   Let <x,y> = e1; z = E2 in E3
regensbu@1274
    44
regensbu@1274
    45
   and
regensbu@1274
    46
regensbu@1274
    47
   <x,y,z>.e
regensbu@1274
    48
*)
regensbu@1274
    49
regensbu@1274
    50
types
regensbu@1274
    51
  Cletbinds  Cletbind 
regensbu@1274
    52
regensbu@1274
    53
consts
regensbu@1274
    54
  CLet           :: "'a -> ('a -> 'b) -> 'b"
regensbu@1274
    55
regensbu@1274
    56
syntax
regensbu@1274
    57
  (* syntax for Let *) 
regensbu@1274
    58
regensbu@1274
    59
  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
regensbu@1274
    60
  ""        :: "Cletbind => Cletbinds"               ("_")
regensbu@1274
    61
  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
regensbu@1274
    62
  "_CLet"   :: "[Cletbinds, 'a] => 'a"                ("(Let (_)/ in (_))" 10)
regensbu@1274
    63
regensbu@1274
    64
translations
regensbu@1274
    65
  (* translation for Let *)
regensbu@1274
    66
  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
regensbu@1274
    67
  "Let x = a in e"          == "CLet`a`(LAM x.e)"
regensbu@1274
    68
regensbu@1274
    69
defs
regensbu@1274
    70
  (* Misc Definitions *)
regensbu@1274
    71
  CLet_def       "CLet == LAM s. LAM f.f`s"
regensbu@1274
    72
regensbu@1274
    73
regensbu@1274
    74
syntax
regensbu@1274
    75
  (* syntax for LAM <x,y,z>.E *)
regensbu@1274
    76
  "@Cpttrn"  :: "[pttrn,pttrns] => pttrn"              ("<_,/_>")
regensbu@1274
    77
regensbu@1274
    78
translations
regensbu@1274
    79
  (* translations for LAM <x,y,z>.E *)
regensbu@1274
    80
  "LAM <x,y,zs>.b"   == "csplit`(LAM x.LAM <y,zs>.b)"
regensbu@1274
    81
  "LAM <x,y>.b"      == "csplit`(LAM x.LAM y.b)"
regensbu@1274
    82
  (* reverse translation <= does not work yet !! *)
regensbu@1274
    83
regensbu@1274
    84
(* start 8bit 1 *)
regensbu@1274
    85
(* end 8bit 1 *)
nipkow@243
    86
end
nipkow@243
    87
nipkow@243
    88
nipkow@243
    89
nipkow@243
    90