(* Title: HOLCF/ssum0.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Strict sum
*)
Ssum0 = Cfun3 +
(* new type for strict sum *)
types "++" 2 (infixr 10)
arities "++" :: (pcpo,pcpo)term
consts
Ssum :: "(['a,'b,bool]=>bool)set"
Sinl_Rep :: "['a,'a,'b,bool]=>bool"
Sinr_Rep :: "['b,'a,'b,bool]=>bool"
Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)"
Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)"
Isinl :: "'a => ('a ++ 'b)"
Isinr :: "'b => ('a ++ 'b)"
Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c"
rules
Sinl_Rep_def "Sinl_Rep == (%a.%x y p.\
\ (~a=UU --> x=a & p))"
Sinr_Rep_def "Sinr_Rep == (%b.%x y p.\
\ (~b=UU --> y=b & ~p))"
Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
(*faking a type definition... *)
(* "++" is isomorphic to Ssum *)
Rep_Ssum "Rep_Ssum(p):Ssum"
Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p"
Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f"
(*defining the abstract constants*)
Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))"
Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))"
Iwhen_def "Iwhen(f)(g)(s) == @z.\
\ (s=Isinl(UU) --> z=UU)\
\ &(!a. ~a=UU & s=Isinl(a) --> z=f[a])\
\ &(!b. ~b=UU & s=Isinr(b) --> z=g[b])"
end