|
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 Zermelo-Fraenkel Set Theory
|
|
|
7 |
"Part" primitive for simultaneous recursive type definitions
|
|
|
8 |
*)
|
|
|
9 |
|
|
124
|
10 |
Sum = Bool + "simpdata" +
|
|
0
|
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
|