src/HOLCF/Ssum0.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/Ssum0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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::'a))|(? b. f=Sinr_Rep(b::'b))}"
    19 
    20 syntax (xsymbols)
    21   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    22 syntax (HTML output)
    23   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
    24 
    25 consts
    26   Isinl         :: "'a => ('a ++ 'b)"
    27   Isinr         :: "'b => ('a ++ 'b)"
    28   Iwhen         :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
    29 
    30 defs   (*defining the abstract constants*)
    31   Isinl_def     "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
    32   Isinr_def     "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
    33 
    34   Iwhen_def     "Iwhen(f)(g)(s) == @z.
    35                                     (s=Isinl(UU) --> z=UU)
    36                         &(!a. a~=UU & s=Isinl(a) --> z=f$a)  
    37                         &(!b. b~=UU & s=Isinr(b) --> z=g$b)"  
    38 
    39 end