--- a/src/HOLCF/ssum0.thy Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* 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
-