1478

1 
(* Title: ZF/sum.thy

0

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 


6 
Disjoint sums in ZermeloFraenkel Set Theory


7 
"Part" primitive for simultaneous recursive type definitions


8 
*)


9 

124

10 
Sum = Bool + "simpdata" +

0

11 
consts

1478

12 
"+" :: [i,i]=>i (infixr 65)

1401

13 
Inl,Inr :: i=>i


14 
case :: [i=>i, i=>i, i]=>i


15 
Part :: [i,i=>i] => i

0

16 

753

17 
defs

0

18 
sum_def "A+B == {0}*A Un {1}*B"


19 
Inl_def "Inl(a) == <0,a>"


20 
Inr_def "Inr(b) == <1,b>"

1108

21 
case_def "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))"

0

22 


23 
(*operator for selecting out the various summands*)

1478

24 
Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"

0

25 
end
