0

1 
(* Title: ZF/sum.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Disjoint sums in ZermeloFraenkel Set Theory


7 
"Part" primitive for simultaneous recursive type definitions


8 
*)


9 


10 
Sum = Bool +


11 
consts


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


13 
Inl,Inr :: "i=>i"


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


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


16 


17 
rules


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


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


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


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


22 


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


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


25 
end
