author paulson Wed, 02 Apr 1997 15:28:42 +0200 changeset 2872 ac81a17f86f8 parent 2871 ba585d52ea4e child 2873 5f0599e15448
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
 src/ZF/ZF.thy file | annotate | diff | comparison | revisions src/ZF/upair.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/ZF.thy	Wed Apr 02 15:26:52 1997 +0200
+++ b/src/ZF/ZF.thy	Wed Apr 02 15:28:42 1997 +0200
@@ -196,7 +196,6 @@
and Powerset Axioms using the following definitions. *)

Collect_def   "Collect(A,P) == {y . x:A, x=y & P(x)}"
-  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"

(*Unordered pairs (Upair) express binary union/intersection and cons;
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
@@ -204,6 +203,17 @@
Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
cons_def    "cons(a,A) == Upair(a,a) Un A"

+  (* Difference, general intersection, binary union and small intersection *)
+
+  Diff_def      "A - B    == { x:A . ~(x:B) }"
+  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
+  Un_def        "A Un  B  == Union(Upair(A,B))"
+  Int_def       "A Int B  == Inter(Upair(A,B))"
+
+  (* Definite descriptions -- via Replace over the set "1" *)
+
+  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
+  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"

(* this "symmetric" definition works better than {{a}, {a,b}} *)
Pair_def      "<a,b>  == {{a,a}, {a,b}}"```
```--- a/src/ZF/upair.thy	Wed Apr 02 15:26:52 1997 +0200
+++ b/src/ZF/upair.thy	Wed Apr 02 15:28:42 1997 +0200
@@ -3,19 +3,10 @@
Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory

-Definitions involving unordered pairing
+Dummy theory, but holds the standard ZF simpset.
+	(This is why the +end is present.)
*)

upair = ZF +

-defs
-  (* Definite descriptions -- via Replace over the set "1" *)
-  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
-  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
-
-  (*Set difference; binary union and intersection*)
-  Diff_def      "A - B    == { x:A . ~(x:B) }"
-  Un_def        "A Un  B  == Union(Upair(A,B))"
-  Int_def       "A Int B  == Inter(Upair(A,B))"
-
end```