21 Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)" |
21 Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)" |
22 Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b" |
22 Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b" |
23 Inl :: "'a => 'a+'b" |
23 Inl :: "'a => 'a+'b" |
24 Inr :: "'b => 'a+'b" |
24 Inr :: "'b => 'a+'b" |
25 sum_case :: "['a=>'c,'b=>'c, 'a+'b] =>'c" |
25 sum_case :: "['a=>'c,'b=>'c, 'a+'b] =>'c" |
|
26 |
|
27 (*disjoint sum for sets; the operator + is overloaded with wrong type!*) |
|
28 "plus" :: "['a set, 'b set] => ('a+'b)set" (infixr 65) |
26 Part :: "['a set, 'a=>'a] => 'a set" |
29 Part :: "['a set, 'a=>'a] => 'a set" |
27 |
30 |
28 translations |
31 translations |
29 "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)" |
32 "case p of Inl(x) => a | Inr(y) => b" == "sum_case(%x.a, %y.b, p)" |
30 |
33 |
31 rules |
34 rules |
32 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
35 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
33 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
36 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
34 |
37 |
35 Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}" |
38 Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}" |
36 (*faking a type definition...*) |
39 (*faking a type definition...*) |
37 Rep_Sum "Rep_Sum(s): Sum" |
40 Rep_Sum "Rep_Sum(s): Sum" |
38 Rep_Sum_inverse "Abs_Sum(Rep_Sum(s)) = s" |
41 Rep_Sum_inverse "Abs_Sum(Rep_Sum(s)) = s" |
39 Abs_Sum_inverse "f: Sum ==> Rep_Sum(Abs_Sum(f)) = f" |
42 Abs_Sum_inverse "f: Sum ==> Rep_Sum(Abs_Sum(f)) = f" |
40 |
43 |
41 (*defining the abstract constants*) |
44 (*defining the abstract constants*) |
42 Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
45 Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
43 Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
46 Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
44 sum_case_def "sum_case(f,g,p) == @z. (!x. p=Inl(x) --> z=f(x)) \ |
47 sum_case_def "sum_case(f,g,p) == @z. (!x. p=Inl(x) --> z=f(x)) \ |
45 \ & (!y. p=Inr(y) --> z=g(y))" |
48 \ & (!y. p=Inr(y) --> z=g(y))" |
|
49 |
|
50 sum_def "A plus B == (Inl``A) Un (Inr``B)" |
46 |
51 |
47 (*for selecting out the components of a mutually recursive definition*) |
52 (*for selecting out the components of a mutually recursive definition*) |
48 Part_def "Part(A,h) == A Int {x. ? z. x = h(z)}" |
53 Part_def "Part(A,h) == A Int {x. ? z. x = h(z)}" |
49 |
54 |
50 end |
55 end |