src/HOLCF/Sprod0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 2640 ee4dfce170a0
child 6382 8b0c9205da75
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Sprod0.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     6
Strict product with typedef
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Sprod0 = Cfun3 +
nipkow@243
    10
slotosch@2640
    11
constdefs
slotosch@2640
    12
  Spair_Rep     :: ['a,'b] => ['a,'b] => bool
slotosch@2640
    13
 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
nipkow@243
    14
slotosch@2640
    15
typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep a b}"
nipkow@243
    16
oheimb@2394
    17
syntax (symbols)
slotosch@2640
    18
  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
oheimb@2394
    19
nipkow@243
    20
consts
clasohm@1479
    21
  Ispair        :: "['a,'b] => ('a ** 'b)"
clasohm@1479
    22
  Isfst         :: "('a ** 'b) => 'a"
clasohm@1479
    23
  Issnd         :: "('a ** 'b) => 'b"  
nipkow@243
    24
regensbu@1168
    25
defs
nipkow@243
    26
   (*defining the abstract constants*)
nipkow@243
    27
clasohm@1479
    28
  Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
nipkow@243
    29
slotosch@2640
    30
  Isfst_def     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
clasohm@1479
    31
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
nipkow@243
    32
slotosch@2640
    33
  Issnd_def     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
clasohm@1479
    34
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
nipkow@243
    35
regensbu@1274
    36
nipkow@243
    37
end
nipkow@243
    38