|
2469
|
1 |
(* Title: ZF/upair.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Definitions involving unordered pairing
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
upair = ZF +
|
|
124
|
10 |
|
|
2469
|
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
|