author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
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 |