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