author | clasohm |
Mon, 05 Feb 1996 21:29:06 +0100 | |
changeset 1476 | 608483c2122a |
parent 1475 | 7f5a4cd08209 |
child 1515 | 4ed79ebab64d |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Sum.thy |
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 |
||
11 |
(* type definition *) |
|
12 |
||
13 |
consts |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset
|
14 |
Inl_Rep :: ['a, 'a, 'b, bool] => bool |
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset
|
15 |
Inr_Rep :: ['b, 'a, 'b, bool] => bool |
923 | 16 |
|
17 |
defs |
|
18 |
Inl_Rep_def "Inl_Rep == (%a. %x y p. x=a & p)" |
|
19 |
Inr_Rep_def "Inr_Rep == (%b. %x y p. y=b & ~p)" |
|
20 |
||
1475 | 21 |
typedef (Sum) |
923 | 22 |
('a, 'b) "+" (infixr 10) |
23 |
= "{f. (? a. f = Inl_Rep(a::'a)) | (? b. f = Inr_Rep(b::'b))}" |
|
24 |
||
25 |
||
26 |
(* abstract constants and syntax *) |
|
27 |
||
28 |
consts |
|
29 |
Inl :: "'a => 'a + 'b" |
|
30 |
Inr :: "'b => 'a + 'b" |
|
31 |
sum_case :: "['a => 'c, 'b => 'c, 'a + 'b] => 'c" |
|
32 |
||
33 |
(*disjoint sum for sets; the operator + is overloaded with wrong type!*) |
|
34 |
"plus" :: "['a set, 'b set] => ('a + 'b) set" (infixr 65) |
|
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset
|
35 |
Part :: ['a set, 'b => 'a] => 'a set |
923 | 36 |
|
37 |
translations |
|
38 |
"case p of Inl(x) => a | Inr(y) => b" == "sum_case (%x.a) (%y.b) p" |
|
39 |
||
40 |
defs |
|
41 |
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
|
42 |
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
|
1151 | 43 |
sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) |
1423 | 44 |
& (!y. p=Inr(y) --> z=g(y))" |
923 | 45 |
|
46 |
sum_def "A plus B == (Inl``A) Un (Inr``B)" |
|
47 |
||
48 |
(*for selecting out the components of a mutually recursive definition*) |
|
49 |
Part_def "Part A h == A Int {x. ? z. x = h(z)}" |
|
50 |
||
51 |
end |