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