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
slotosch@2640
     1
(*  Title:      HOLCF/Sprod0.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243
     5
wenzelm@6382
     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
wenzelm@6382
    15
typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
nipkow@243
    16
wenzelm@12114
    17
syntax (xsymbols)
slotosch@2640
    18
  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
kleing@14565
    19
syntax (HTML output)
kleing@14565
    20
  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
oheimb@2394
    21
nipkow@243
    22
consts
clasohm@1479
    23
  Ispair        :: "['a,'b] => ('a ** 'b)"
clasohm@1479
    24
  Isfst         :: "('a ** 'b) => 'a"
clasohm@1479
    25
  Issnd         :: "('a ** 'b) => 'b"  
nipkow@243
    26
regensbu@1168
    27
defs
nipkow@243
    28
   (*defining the abstract constants*)
nipkow@243
    29
clasohm@1479
    30
  Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
nipkow@243
    31
slotosch@2640
    32
  Isfst_def     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
clasohm@1479
    33
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
nipkow@243
    34
slotosch@2640
    35
  Issnd_def     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
clasohm@1479
    36
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
nipkow@243
    37
regensbu@1274
    38
nipkow@243
    39
end