equal
deleted
inserted
replaced
1 (* Title: ZF/upair.thy |
1 (* Title: ZF/upair.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
3 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Definitions involving unordered pairing |
6 Dummy theory, but holds the standard ZF simpset. |
|
7 (This is why the +end is present.) |
7 *) |
8 *) |
8 |
9 |
9 upair = ZF + |
10 upair = ZF + |
10 |
11 |
11 defs |
|
12 (* Definite descriptions -- via Replace over the set "1" *) |
|
13 the_def "The(P) == Union({y . x:{0}, P(y)})" |
|
14 if_def "if(P,a,b) == THE z. P & z=a | ~P & z=b" |
|
15 |
|
16 (*Set difference; binary union and intersection*) |
|
17 Diff_def "A - B == { x:A . ~(x:B) }" |
|
18 Un_def "A Un B == Union(Upair(A,B))" |
|
19 Int_def "A Int B == Inter(Upair(A,B))" |
|
20 |
|
21 end |
12 end |