src/HOLCF/Sprod0.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 12114 a8e860c86252
child 14981 e73f8140af78
permissions -rw-r--r--
use more symbols in HTML output
     1 (*  Title:      HOLCF/Sprod0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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::'a) (b::'b)}"
    16 
    17 syntax (xsymbols)
    18   "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
    19 syntax (HTML output)
    20   "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
    21 
    22 consts
    23   Ispair        :: "['a,'b] => ('a ** 'b)"
    24   Isfst         :: "('a ** 'b) => 'a"
    25   Issnd         :: "('a ** 'b) => 'b"  
    26 
    27 defs
    28    (*defining the abstract constants*)
    29 
    30   Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
    31 
    32   Isfst_def     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
    33                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
    34 
    35   Issnd_def     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
    36                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
    37 
    38 
    39 end