10 |
10 |
11 (* new type for strict sum *) |
11 (* new type for strict sum *) |
12 |
12 |
13 types "++" 2 (infixr 10) |
13 types "++" 2 (infixr 10) |
14 |
14 |
15 arities "++" :: (pcpo,pcpo)term |
15 arities "++" :: (pcpo,pcpo)term |
16 |
16 |
17 consts |
17 consts |
18 Ssum :: "(['a,'b,bool]=>bool)set" |
18 Ssum :: "(['a,'b,bool]=>bool)set" |
19 Sinl_Rep :: "['a,'a,'b,bool]=>bool" |
19 Sinl_Rep :: "['a,'a,'b,bool]=>bool" |
20 Sinr_Rep :: "['b,'a,'b,bool]=>bool" |
20 Sinr_Rep :: "['b,'a,'b,bool]=>bool" |
21 Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)" |
21 Rep_Ssum :: "('a ++ 'b) => (['a,'b,bool]=>bool)" |
22 Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)" |
22 Abs_Ssum :: "(['a,'b,bool]=>bool) => ('a ++ 'b)" |
23 Isinl :: "'a => ('a ++ 'b)" |
23 Isinl :: "'a => ('a ++ 'b)" |
24 Isinr :: "'b => ('a ++ 'b)" |
24 Isinr :: "'b => ('a ++ 'b)" |
25 Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" |
25 Iwhen :: "('a->'c)=>('b->'c)=>('a ++ 'b)=> 'c" |
26 |
26 |
27 defs |
27 defs |
28 |
28 |
29 Sinl_Rep_def "Sinl_Rep == (%a.%x y p. |
29 Sinl_Rep_def "Sinl_Rep == (%a.%x y p. |
30 (a~=UU --> x=a & p))" |
30 (a~=UU --> x=a & p))" |
31 |
31 |
32 Sinr_Rep_def "Sinr_Rep == (%b.%x y p. |
32 Sinr_Rep_def "Sinr_Rep == (%b.%x y p. |
33 (b~=UU --> y=b & ~p))" |
33 (b~=UU --> y=b & ~p))" |
34 |
34 |
35 Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}" |
35 Ssum_def "Ssum =={f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}" |
36 |
36 |
37 rules |
37 rules |
38 (*faking a type definition... *) |
38 (*faking a type definition... *) |
39 (* "++" is isomorphic to Ssum *) |
39 (* "++" is isomorphic to Ssum *) |
40 |
40 |
41 Rep_Ssum "Rep_Ssum(p):Ssum" |
41 Rep_Ssum "Rep_Ssum(p):Ssum" |
42 Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p" |
42 Rep_Ssum_inverse "Abs_Ssum(Rep_Ssum(p)) = p" |
43 Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f" |
43 Abs_Ssum_inverse "f:Ssum ==> Rep_Ssum(Abs_Ssum(f)) = f" |
44 |
44 |
45 defs (*defining the abstract constants*) |
45 defs (*defining the abstract constants*) |
46 Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))" |
46 Isinl_def "Isinl(a) == Abs_Ssum(Sinl_Rep(a))" |
47 Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))" |
47 Isinr_def "Isinr(b) == Abs_Ssum(Sinr_Rep(b))" |
48 |
48 |
49 Iwhen_def "Iwhen(f)(g)(s) == @z. |
49 Iwhen_def "Iwhen(f)(g)(s) == @z. |
50 (s=Isinl(UU) --> z=UU) |
50 (s=Isinl(UU) --> z=UU) |
51 &(!a. a~=UU & s=Isinl(a) --> z=f`a) |
51 &(!a. a~=UU & s=Isinl(a) --> z=f`a) |
52 &(!b. b~=UU & s=Isinr(b) --> z=g`b)" |
52 &(!b. b~=UU & s=Isinr(b) --> z=g`b)" |
53 |
53 |
54 (* start 8bit 1 *) |
54 (* start 8bit 1 *) |
55 (* end 8bit 1 *) |
55 (* end 8bit 1 *) |
56 end |
56 end |
57 |
57 |