| author | wenzelm |
| Wed, 30 Jun 1999 12:23:46 +0200 | |
| changeset 6860 | 8dc6a1e6fa13 |
| parent 5325 | f7a5e06adea1 |
| child 13220 | 62c899c77151 |
| permissions | -rw-r--r-- |
| 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 Zermelo-Fraenkel Set Theory |
|
7 |
"Part" primitive for simultaneous recursive type definitions |
|
8 |
*) |
|
9 |
||
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
3940
diff
changeset
|
10 |
Sum = Bool + equalities + |
| 3923 | 11 |
|
12 |
global |
|
13 |
||
| 0 | 14 |
consts |
| 1478 | 15 |
"+" :: [i,i]=>i (infixr 65) |
| 1401 | 16 |
Inl,Inr :: i=>i |
17 |
case :: [i=>i, i=>i, i]=>i |
|
18 |
Part :: [i,i=>i] => i |
|
| 0 | 19 |
|
| 3940 | 20 |
local |
| 3923 | 21 |
|
| 753 | 22 |
defs |
| 0 | 23 |
sum_def "A+B == {0}*A Un {1}*B"
|
24 |
Inl_def "Inl(a) == <0,a>" |
|
25 |
Inr_def "Inr(b) == <1,b>" |
|
| 1108 | 26 |
case_def "case(c,d) == (%<y,z>. cond(y, d(z), c(z)))" |
| 0 | 27 |
|
28 |
(*operator for selecting out the various summands*) |
|
| 1478 | 29 |
Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
|
| 0 | 30 |
end |