author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 7293  959e060f4a2f 
child 9311  ab5b24cbaa16 
permissions  rwrr 
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 

1515  9 
Sum = mono + Prod + 
923  10 

11 
(* type definition *) 

12 

1558  13 
constdefs 
1370
7361ac9b024d
removed quotes from types in consts and syntax sections
clasohm
parents:
1151
diff
changeset

14 
Inl_Rep :: ['a, 'a, 'b, bool] => bool 
1558  15 
"Inl_Rep == (%a. %x y p. x=a & p)" 
923  16 

1558  17 
Inr_Rep :: ['b, 'a, 'b, bool] => bool 
18 
"Inr_Rep == (%b. %x y p. y=b & ~p)" 

923  19 

3947  20 
global 
21 

1475  22 
typedef (Sum) 
923  23 
('a, 'b) "+" (infixr 10) 
24 
= "{f. (? a. f = Inl_Rep(a::'a))  (? b. f = Inr_Rep(b::'b))}" 

25 

26 

27 
(* abstract constants and syntax *) 

28 

29 
consts 

7254
fc7f95f293da
Renamed sum_case to basic_sum_case and removed translations for sum_case
berghofe
parents:
3947
diff
changeset

30 
Inl :: "'a => 'a + 'b" 
fc7f95f293da
Renamed sum_case to basic_sum_case and removed translations for sum_case
berghofe
parents:
3947
diff
changeset

31 
Inr :: "'b => 'a + 'b" 
923  32 

33 
(*disjoint sum for sets; the operator + is overloaded with wrong type!*) 

2212  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 

3947  37 
local 
38 

923  39 
defs 
40 
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" 

41 
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" 

42 

2212  43 
sum_def "A Plus B == (Inl``A) Un (Inr``B)" 
923  44 

45 
(*for selecting out the components of a mutually recursive definition*) 

46 
Part_def "Part A h == A Int {x. ? z. x = h(z)}" 

47 

48 
end 