--- a/src/ZF/ZF.thy Thu Sep 15 13:13:54 1994 +0200
+++ b/src/ZF/ZF.thy Wed Sep 21 15:39:02 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/zf.thy
+(* Title: ZF/ZF.thy
ID: $Id$
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
Copyright 1993 University of Cambridge
@@ -9,36 +9,27 @@
ZF = FOL +
types
- i is
+ i
arities
i :: term
-
consts
- "0" :: "i" ("0") (*the empty set*)
- Pow :: "i => i" (*power sets*)
- Inf :: "i" (*infinite set*)
+ "0" :: "i" ("0") (*the empty set*)
+ Pow :: "i => i" (*power sets*)
+ Inf :: "i" (*infinite set*)
(* Bounded Quantifiers *)
- "@Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10)
- "@Bex" :: "[idt, i, o] => o" ("(3EX _:_./ _)" 10)
- Ball :: "[i, i => o] => o"
- Bex :: "[i, i => o] => o"
+ Ball, Bex :: "[i, i => o] => o"
(* General Union and Intersection *)
- "@INTER" :: "[idt, i, i] => i" ("(3INT _:_./ _)" 10)
- "@UNION" :: "[idt, i, i] => i" ("(3UN _:_./ _)" 10)
Union, Inter :: "i => i"
(* Variations on Replacement *)
- "@Replace" :: "[idt, idt, i, o] => i" ("(1{_ ./ _: _, _})")
- "@RepFun" :: "[i, idt, i] => i" ("(1{_ ./ _: _})")
- "@Collect" :: "[idt, i, o] => i" ("(1{_: _ ./ _})")
PrimReplace :: "[i, [i, i] => o] => i"
Replace :: "[i, [i, i] => o] => i"
RepFun :: "[i, i => i] => i"
@@ -46,23 +37,16 @@
(* Descriptions *)
- The :: "(i => o) => i" (binder "THE " 10)
+ The :: "(i => o) => i" (binder "THE " 10)
if :: "[o, i, i] => i"
- (* Enumerations of type i *)
-
- "" :: "i => is" ("_")
- "@Enum" :: "[i, is] => is" ("_,/ _")
-
(* Finite Sets *)
- "@Finset" :: "is => i" ("{(_)}")
Upair, cons :: "[i, i] => i"
succ :: "i => i"
- (* Ordered Pairing and n-Tuples *)
+ (* Ordered Pairing *)
- "@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
Pair :: "[i, i] => i"
fst, snd :: "i => i"
split :: "[[i, i] => i, i] => i"
@@ -70,10 +54,7 @@
(* Sigma and Pi Operators *)
- "@PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10)
- "@SUM" :: "[idt, i, i] => i" ("(3SUM _:_./ _)" 10)
- "@lam" :: "[idt, i, i] => i" ("(3lam _:_./ _)" 10)
- Pi, Sigma :: "[i, i => i] => i"
+ Sigma, Pi :: "[i, i => i] => i"
(* Relations and Functions *)
@@ -86,29 +67,50 @@
(* Infixes in order of decreasing precedence *)
- "``" :: "[i, i] => i" (infixl 90) (*image*)
- "-``" :: "[i, i] => i" (infixl 90) (*inverse image*)
- "`" :: "[i, i] => i" (infixl 90) (*function application*)
-
- (*Except for their translations, * and -> are right and ~: left associative infixes*)
- "*" :: "[i, i] => i" ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
- "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
- "Un" :: "[i, i] => i" (infixl 65) (*binary union*)
- "-" :: "[i, i] => i" (infixl 65) (*set difference*)
- "->" :: "[i, i] => i" ("(_ ->/ _)" [61, 60] 60) (*function space*)
- "<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
- ":" :: "[i, i] => o" (infixl 50) (*membership relation*)
- "~:" :: "[i, i] => o" ("(_ ~:/ _)" [50, 51] 50) (*negated membership relation*)
+ "``" :: "[i, i] => i" (infixl 90) (*image*)
+ "-``" :: "[i, i] => i" (infixl 90) (*inverse image*)
+ "`" :: "[i, i] => i" (infixl 90) (*function application*)
+(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*)
+ "Int" :: "[i, i] => i" (infixl 70) (*binary intersection*)
+ "Un" :: "[i, i] => i" (infixl 65) (*binary union*)
+ "-" :: "[i, i] => i" (infixl 65) (*set difference*)
+(*"->" :: "[i, i] => i" (infixr 60) (*function space*)*)
+ "<=" :: "[i, i] => o" (infixl 50) (*subset relation*)
+ ":" :: "[i, i] => o" (infixl 50) (*membership relation*)
+(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*)
+types
+ is
+
+syntax
+ "" :: "i => is" ("_")
+ "@Enum" :: "[i, is] => is" ("_,/ _")
+ "~:" :: "[i, i] => o" (infixl 50)
+ "@Finset" :: "is => i" ("{(_)}")
+ "@Tuple" :: "[i, is] => i" ("<(_,/ _)>")
+ "@Collect" :: "[idt, i, o] => i" ("(1{_: _ ./ _})")
+ "@Replace" :: "[idt, idt, i, o] => i" ("(1{_ ./ _: _, _})")
+ "@RepFun" :: "[i, idt, i] => i" ("(1{_ ./ _: _})")
+ "@INTER" :: "[idt, i, i] => i" ("(3INT _:_./ _)" 10)
+ "@UNION" :: "[idt, i, i] => i" ("(3UN _:_./ _)" 10)
+ "@PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10)
+ "@SUM" :: "[idt, i, i] => i" ("(3SUM _:_./ _)" 10)
+ "->" :: "[i, i] => i" (infixr 60)
+ "*" :: "[i, i] => i" (infixr 80)
+ "@lam" :: "[idt, i, i] => i" ("(3lam _:_./ _)" 10)
+ "@Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10)
+ "@Bex" :: "[idt, i, o] => o" ("(3EX _:_./ _)" 10)
+
translations
+ "x ~: y" == "~ (x : y)"
"{x, xs}" == "cons(x, {xs})"
"{x}" == "cons(x, 0)"
"<x, y, z>" == "<x, <y, z>>"
"<x, y>" == "Pair(x, y)"
"{x:A. P}" == "Collect(A, %x. P)"
"{y. x:A, Q}" == "Replace(A, %x y. Q)"
- "{f. x:A}" == "RepFun(A, %x. f)"
+ "{b. x:A}" == "RepFun(A, %x. b)"
"INT x:A. B" == "Inter({B. x:A})"
"UN x:A. B" == "Union({B. x:A})"
"PROD x:A. B" => "Pi(A, %x. B)"
@@ -118,94 +120,97 @@
"lam x:A. f" == "Lambda(A, %x. f)"
"ALL x:A. P" == "Ball(A, %x. P)"
"EX x:A. P" == "Bex(A, %x. P)"
- "x ~: y" == "~ (x : y)"
rules
- (* 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"
+ (* 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"
- (* ZF axioms -- see Suppes p.238
- Axioms for Union, Pow and Replace state existence only,
- uniqueness is derivable using extensionality. *)
+ (* ZF axioms -- see Suppes p.238
+ Axioms for Union, Pow and Replace state existence only,
+ uniqueness is derivable using extensionality. *)
-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)"
+ 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)"
+ (*We may name this set, though it is not uniquely defined.*)
+ infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"
- (*This formulation facilitates case analysis on A. *)
-foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
+ (*This formulation facilitates case analysis on A.*)
+ foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
- (* Schema axiom since predicate P is a higher-order variable *)
-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))"
+ (*Schema axiom since predicate P is a higher-order variable*)
+ 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))"
+
+ (* 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. *)
- (* 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. *)
-Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
+ Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
+
+ (* Functional form of replacement -- analgous to ML's map functional *)
- (* Functional form of replacement -- analgous to ML's map functional *)
-RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}"
+ RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}"
- (* Separation and Pairing can be derived from the Replacement
- and Powerset Axioms using the following definitions. *)
+ (* Separation and Pairing can be derived from the Replacement
+ and Powerset Axioms using the following definitions. *)
-Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}"
+ Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}"
- (*Unordered pairs (Upair) express binary union/intersection and cons;
- set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...) *)
-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"
+ (*Unordered pairs (Upair) express binary union/intersection and cons;
+ set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
- (* Difference, general intersection, binary union and small intersection *)
+ 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))"
+ 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" *)
+ (* 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"
+ the_def "The(P) == Union({y . x:{0}, P(y)})"
+ if_def "if(P,a,b) == THE z. P & z=a | ~P & z=b"
- (* Ordered pairs and disjoint union of a family of sets *)
+ (* Ordered pairs and disjoint union of a family of sets *)
- (* this "symmetric" definition works better than {{a}, {a,b}} *)
-Pair_def "<a,b> == {{a,a}, {a,b}}"
-fst_def "fst == split(%x y.x)"
-snd_def "snd == split(%x y.y)"
-split_def "split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)"
-fsplit_def "fsplit(R,z) == EX x y. z=<x,y> & R(x,y)"
-Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
+ (* this "symmetric" definition works better than {{a}, {a,b}} *)
+ Pair_def "<a,b> == {{a,a}, {a,b}}"
+ fst_def "fst == split(%x y.x)"
+ snd_def "snd == split(%x y.y)"
+ split_def "split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)"
+ fsplit_def "fsplit(R,z) == EX x y. z=<x,y> & R(x,y)"
+ Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
- (* Operations on relations *)
+ (* Operations on relations *)
-(*converse of relation r, inverse of function*)
-converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
+ (*converse of relation r, inverse of function*)
+ converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
-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)"
-image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
-vimage_def "r -`` A == converse(r)``A"
+ 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)"
+ image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"
+ vimage_def "r -`` A == converse(r)``A"
- (* Abstraction, application and Cartesian product of a family of sets *)
+ (* Abstraction, application and Cartesian product of a family of sets *)
-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}"
+ 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}"
(* Restrict the function f to the domain A *)
-restrict_def "restrict(f,A) == lam x:A.f`x"
+ restrict_def "restrict(f,A) == lam x:A.f`x"
end
@@ -217,4 +222,3 @@
val print_translation =
[("Pi", dependent_tr' ("@PROD", "->")),
("Sigma", dependent_tr' ("@SUM", "*"))];
-