5 |
5 |
6 The disjoint sum of two types |
6 The disjoint sum of two types |
7 *) |
7 *) |
8 |
8 |
9 Sum = Prod + |
9 Sum = Prod + |
10 types "+" 2 (infixl 10) |
10 |
11 arities "+" :: (term,term)term |
11 types |
|
12 ('a,'b) "+" (infixl 10) |
|
13 |
|
14 arities |
|
15 "+" :: (term,term)term |
|
16 |
12 consts |
17 consts |
13 Inl_Rep :: "['a,'a,'b,bool] => bool" |
18 Inl_Rep :: "['a,'a,'b,bool] => bool" |
14 Inr_Rep :: "['b,'a,'b,bool] => bool" |
19 Inr_Rep :: "['b,'a,'b,bool] => bool" |
15 Sum :: "(['a,'b,bool] => bool)set" |
20 Sum :: "(['a,'b,bool] => bool)set" |
16 Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)" |
21 Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)" |
17 Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b" |
22 Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b" |
18 Inl :: "'a => 'a+'b" |
23 Inl :: "'a => 'a+'b" |
19 Inr :: "'b => 'a+'b" |
24 Inr :: "'b => 'a+'b" |
20 sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c" |
25 sum_case :: "['a+'b, 'a=>'c,'b=>'c] =>'c" |
|
26 |
21 rules |
27 rules |
22 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
28 Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
23 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
29 Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
24 Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}" |
30 Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}" |
25 (*faking a type definition...*) |
31 (*faking a type definition...*) |