author lcp Thu, 03 Nov 1994 12:35:41 +0100 changeset 690 b2bd1d5a3d16 parent 689 bf95dada47ac child 691 b9fc536792bb
ZF: NEW DEFINITION OF PI(A,B) Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f} Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y') Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" This simplifies many proofs, since (a) the top-level definition has fewer bound variables (b) the "total" and "function" properties are separated (c) the awkward EX! quantifier is eliminated. ZF/ZF.thy/function: new definition
 src/ZF/ZF.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/ZF.thy	Thu Nov 03 12:30:55 1994 +0100
+++ b/src/ZF/ZF.thy	Thu Nov 03 12:35:41 1994 +0100
@@ -62,6 +62,7 @@
range       :: "i => i"
field       :: "i => i"
converse    :: "i => i"
+  function    :: "i => o"	    	(*is a relation a function?*)
Lambda      :: "[i, i => i] => i"
restrict    :: "[i, i] => i"

@@ -122,13 +123,16 @@
"EX x:A. P"   == "Bex(A, %x. P)"

-rules
+defs

(* Bounded Quantifiers *)
-
Ball_def      "Ball(A, P) == ALL x. x:A --> P(x)"
Bex_def       "Bex(A, P) == EX x. x:A & P(x)"
+
subset_def    "A <= B == ALL x:A. x:B"
+  succ_def      "succ(i) == cons(i, i)"
+
+rules

(* ZF axioms -- see Suppes p.238
Axioms for Union, Pow and Replace state existence only,
@@ -137,7 +141,6 @@
extension     "A = B <-> A <= B & B <= A"
Union_iff     "A : Union(C) <-> (EX B:C. A:B)"
Pow_iff       "A : Pow(B) <-> A <= B"
-  succ_def      "succ(i) == cons(i, i)"

(*We may name this set, though it is not uniquely defined.*)
infinity      "0:Inf & (ALL y:Inf. succ(y): Inf)"
@@ -149,6 +152,8 @@
replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
\        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"

+defs
+
(* Derived form of replacement, restricting P to its functional part.
The resulting set (for functional P) is the same as with
PrimReplace, but the rules are simpler. *)
@@ -200,6 +205,8 @@
domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
range_def     "range(r) == domain(converse(r))"
field_def     "field(r) == domain(r) Un range(r)"
+  function_def	"function(r) == ALL x y. <x,y>:r -->   \
+\		                (ALL y'. <x,y'>:r --> y=y')"
image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
vimage_def    "r -`` A == converse(r)``A"

@@ -207,7 +214,7 @@

lam_def       "Lambda(A,b) == {<x,b(x)> . x:A}"
apply_def     "f`a == THE y. <a,y> : f"
-  Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}"
+  Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"

(* Restrict the function f to the domain A *)
restrict_def  "restrict(f,A) == lam x:A.f`x"```