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