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;
     1 (*  Title:      HOLCF/Ssum0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Strict sum with typedef
     7 *)
     8 
     9 Ssum0 = Cfun3 +
    10 
    11 constdefs
    12   Sinl_Rep      :: ['a,'a,'b,bool]=>bool
    13  "Sinl_Rep == (%a.%x y p. (a~=UU --> x=a & p))"
    14   Sinr_Rep      :: ['b,'a,'b,bool]=>bool
    15  "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
    16 
    17 typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
    18 	"{f.(? a. f=Sinl_Rep(a))|(? b. f=Sinr_Rep(b))}"
    19 
    20 syntax (symbols)
    21   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    22 
    23 consts
    24   Isinl         :: "'a => ('a ++ 'b)"
    25   Isinr         :: "'b => ('a ++ 'b)"
    26   Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
    27 
    28 defs   (*defining the abstract constants*)
    29   Isinl_def     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
    30   Isinr_def     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
    31 
    32   Iwhen_def     "Iwhen(f)(g)(s) == @z.
    33                                     (s=Isinl(UU) --> z=UU)
    34                         &(!a. a~=UU & s=Isinl(a) --> z=f`a)  
    35                         &(!b. b~=UU & s=Isinr(b) --> z=g`b)"  
    36 
    37 end
    38