src/HOLCF/ssum0.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
nipkow@243
     1
(*  Title: 	HOLCF/ssum0.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Strict sum
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Ssum0 = Cfun3 +
nipkow@243
    10
nipkow@243
    11
(* new type for strict sum *)
nipkow@243
    12
nipkow@243
    13
types "++" 2        (infixr 10)
nipkow@243
    14
nipkow@243
    15
arities "++" :: (pcpo,pcpo)term	
nipkow@243
    16
nipkow@243
    17
consts
nipkow@243
    18
  Ssum		:: "(['a,'b,bool]=>bool)set"
nipkow@243
    19
  Sinl_Rep	:: "['a,'a,'b,bool]=>bool"
nipkow@243
    20
  Sinr_Rep	:: "['b,'a,'b,bool]=>bool"
nipkow@243
    21
  Rep_Ssum	:: "('a ++ 'b) => (['a,'b,bool]=>bool)"
nipkow@243
    22
  Abs_Ssum	:: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
nipkow@243
    23
  Isinl		:: "'a => ('a ++ 'b)"
nipkow@243
    24
  Isinr		:: "'b => ('a ++ 'b)"
nipkow@243
    25
  Iwhen		:: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
nipkow@243
    26
nipkow@243
    27
rules
nipkow@243
    28
nipkow@243
    29
  Sinl_Rep_def		"Sinl_Rep == (%a.%x y p.\
nipkow@243
    30
\				(~a=UU --> x=a  & p))"
nipkow@243
    31
nipkow@243
    32
  Sinr_Rep_def		"Sinr_Rep == (%b.%x y p.\
nipkow@243
    33
\				(~b=UU --> y=b  & ~p))"
nipkow@243
    34
nipkow@243
    35
  Ssum_def		"Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
nipkow@243
    36
nipkow@243
    37
  (*faking a type definition... *)
nipkow@243
    38
  (* "++" is isomorphic to Ssum *)
nipkow@243
    39
nipkow@243
    40
  Rep_Ssum		"Rep_Ssum(p):Ssum"		
nipkow@243
    41
  Rep_Ssum_inverse	"Abs_Ssum(Rep_Ssum(p)) = p"	
nipkow@243
    42
  Abs_Ssum_inverse	"f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
nipkow@243
    43
nipkow@243
    44
   (*defining the abstract constants*)
nipkow@243
    45
  Isinl_def	"Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
nipkow@243
    46
  Isinr_def	"Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
nipkow@243
    47
nipkow@243
    48
  Iwhen_def	"Iwhen(f)(g)(s) == @z.\
nipkow@243
    49
\				    (s=Isinl(UU) --> z=UU)\
nipkow@243
    50
\			&(!a. ~a=UU & s=Isinl(a) --> z=f[a])\  
nipkow@243
    51
\			&(!b. ~b=UU & s=Isinr(b) --> z=g[b])"  
nipkow@243
    52
nipkow@243
    53
end
nipkow@243
    54