equal
deleted
inserted
replaced
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 |
|
10 Sum = Bool + "simpdata" + |
|
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 |
|