src/HOLCF/Ssum0.thy

Simplification of definition of synth

(*  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"

defs

  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))}"

rules
  (*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"

defs   (*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)"  

(* start 8bit 1 *)
(* end 8bit 1 *)
end