src/HOLCF/Sprod0.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14565 c6dc17aab88a
child 15567 60743edae74a
permissions -rw-r--r--
Merged in license change from Isabelle2004
slotosch@2640
     1
(*  Title:      HOLCF/Sprod0.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
wenzelm@6382
     5
Strict product with typedef.
nipkow@243
     6
*)
nipkow@243
     7
nipkow@243
     8
Sprod0 = Cfun3 +
nipkow@243
     9
slotosch@2640
    10
constdefs
slotosch@2640
    11
  Spair_Rep     :: ['a,'b] => ['a,'b] => bool
slotosch@2640
    12
 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
nipkow@243
    13
wenzelm@6382
    14
typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
nipkow@243
    15
wenzelm@12114
    16
syntax (xsymbols)
slotosch@2640
    17
  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
kleing@14565
    18
syntax (HTML output)
kleing@14565
    19
  "**"		:: [type, type] => type	 ("(_ \\<otimes>/ _)" [21,20] 20)
oheimb@2394
    20
nipkow@243
    21
consts
clasohm@1479
    22
  Ispair        :: "['a,'b] => ('a ** 'b)"
clasohm@1479
    23
  Isfst         :: "('a ** 'b) => 'a"
clasohm@1479
    24
  Issnd         :: "('a ** 'b) => 'b"  
nipkow@243
    25
regensbu@1168
    26
defs
nipkow@243
    27
   (*defining the abstract constants*)
nipkow@243
    28
clasohm@1479
    29
  Ispair_def    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
nipkow@243
    30
slotosch@2640
    31
  Isfst_def     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
clasohm@1479
    32
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
nipkow@243
    33
slotosch@2640
    34
  Issnd_def     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
clasohm@1479
    35
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
nipkow@243
    36
regensbu@1274
    37
nipkow@243
    38
end