src/HOLCF/Cprod3.thy
author regensbu
Fri Oct 06 17:25:24 1995 +0100 (1995-10-06)
changeset 1274 ea0668a1c0ba
parent 1168 74be52691d62
child 1479 21eb5e156d91
permissions -rw-r--r--
added 8bit pragmas
added directory ax_ops for sections axioms and ops
added directory domain for sections domain and generated
this is the type definition package of David Oheimb
nipkow@243
     1
(*  Title: 	HOLCF/cprod3.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     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
nipkow@243
    13
arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)
nipkow@243
    14
nipkow@243
    15
consts  
regensbu@752
    16
	cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
nipkow@243
    17
	cfst         :: "('a*'b)->'a"
nipkow@243
    18
	csnd         :: "('a*'b)->'b"
nipkow@243
    19
	csplit       :: "('a->'b->'c)->('a*'b)->'c"
nipkow@243
    20
regensbu@1168
    21
syntax	
regensbu@1168
    22
	"@ctuple"    :: "['a, args] => 'a * 'b"		("(1<_,/ _>)")
regensbu@1168
    23
regensbu@752
    24
regensbu@1168
    25
translations 
regensbu@1168
    26
	"<x, y, z>"   == "<x, <y, z>>"
regensbu@1168
    27
	"<x, y>"      == "cpair`x`y"
nipkow@625
    28
nipkow@243
    29
rules 
nipkow@243
    30
regensbu@1168
    31
inst_cprod_pcpo	"(UU::'a*'b) = (UU,UU)"
nipkow@243
    32
regensbu@1168
    33
defs
regensbu@1168
    34
cpair_def	"cpair  == (LAM x y.(x,y))"
nipkow@243
    35
cfst_def	"cfst   == (LAM p.fst(p))"
nipkow@243
    36
csnd_def	"csnd   == (LAM p.snd(p))"	
regensbu@1168
    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