src/HOLCF/Ssum0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3842 b55686a7b22c
child 6382 8b0c9205da75
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Ssum0.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 sum with typedef
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Ssum0 = Cfun3 +
nipkow@243
    10
slotosch@2640
    11
constdefs
slotosch@2640
    12
  Sinl_Rep      :: ['a,'a,'b,bool]=>bool
slotosch@2640
    13
 "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
slotosch@2640
    14
  Sinr_Rep      :: ['b,'a,'b,bool]=>bool
slotosch@2640
    15
 "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
nipkow@243
    16
slotosch@2640
    17
typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
wenzelm@3842
    18
	"{f.(? a. f=Sinl_Rep(a))|(? b. f=Sinr_Rep(b))}"
nipkow@243
    19
oheimb@2394
    20
syntax (symbols)
slotosch@2640
    21
  "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
oheimb@2394
    22
nipkow@243
    23
consts
clasohm@1479
    24
  Isinl         :: "'a => ('a ++ 'b)"
clasohm@1479
    25
  Isinr         :: "'b => ('a ++ 'b)"
clasohm@1479
    26
  Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
nipkow@243
    27
regensbu@1168
    28
defs   (*defining the abstract constants*)
clasohm@1479
    29
  Isinl_def     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
clasohm@1479
    30
  Isinr_def     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
nipkow@243
    31
clasohm@1479
    32
  Iwhen_def     "Iwhen(f)(g)(s) == @z.
clasohm@1479
    33
                                    (s=Isinl(UU) --> z=UU)
clasohm@1479
    34
                        &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
clasohm@1479
    35
                        &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
nipkow@243
    36
nipkow@243
    37
end
nipkow@243
    38