|
1 (* Title: HOL/sum |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 The disjoint sum of two types |
|
7 *) |
|
8 |
|
9 Sum = Prod + |
|
10 types "+" 2 (infixl 10) |
|
11 arities "+" :: (term,term)term |
|
12 consts |
|
13 Inl_Rep :: "['a,'a,'b,bool] => bool" |
|
14 Inr_Rep :: "['b,'a,'b,bool] => bool" |
|
15 Sum :: "(['a,'b,bool] => bool)set" |
|
16 Rep_Sum :: "'a + 'b => (['a,'b,bool] => bool)" |
|
17 Abs_Sum :: "(['a,'b,bool] => bool) => 'a+'b" |
|
18 Inl :: "'a => 'a+'b" |
|
19 Inr :: "'b => 'a+'b" |
|
20 case :: "['a+'b, 'a=>'c,'b=>'c] =>'c" |
|
21 rules |
|
22 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)" |
|
24 Sum_def "Sum == {f. (? a. f = Inl_Rep(a)) | (? b. f = Inr_Rep(b))}" |
|
25 (*faking a type definition...*) |
|
26 Rep_Sum "Rep_Sum(s): Sum" |
|
27 Rep_Sum_inverse "Abs_Sum(Rep_Sum(s)) = s" |
|
28 Abs_Sum_inverse "f: Sum ==> Rep_Sum(Abs_Sum(f)) = f" |
|
29 (*defining the abstract constants*) |
|
30 Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
|
31 Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
|
32 case_def "case == (%p f g. @z. (!x. p=Inl(x) --> z=f(x))\ |
|
33 \ & (!y. p=Inr(y) --> z=g(y)))" |
|
34 end |