src/ZF/ZF.thy
changeset 0 a5a9c433f639
child 37 cebe01deba80
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ZF.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,227 @@
     1.4 +(*  Title:      ZF/zf.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Zermelo-Fraenkel Set Theory
    1.10 +*)
    1.11 +
    1.12 +ZF = FOL +
    1.13 +
    1.14 +types
    1.15 +  i, is, syntax 0
    1.16 +
    1.17 +arities
    1.18 +  i :: term
    1.19 +
    1.20 +
    1.21 +consts
    1.22 +
    1.23 +  "0"          :: "i"                          ("0") (*the empty set*)
    1.24 +  Pow          :: "i => i"                                 (*power sets*)
    1.25 +  Inf          :: "i"                                      (*infinite set*)
    1.26 +
    1.27 +  (* Bounded Quantifiers *)
    1.28 +
    1.29 +  "@Ball"      :: "[idt, i, o] => o"           ("(3ALL _:_./ _)" 10)
    1.30 +  "@Bex"       :: "[idt, i, o] => o"           ("(3EX _:_./ _)" 10)
    1.31 +  Ball         :: "[i, i => o] => o"
    1.32 +  Bex          :: "[i, i => o] => o"
    1.33 +
    1.34 +  (* General Union and Intersection *)
    1.35 +
    1.36 +  "@INTER"     :: "[idt, i, i] => i"           ("(3INT _:_./ _)" 10)
    1.37 +  "@UNION"     :: "[idt, i, i] => i"           ("(3UN _:_./ _)" 10)
    1.38 +  Union, Inter :: "i => i"
    1.39 +
    1.40 +  (* Variations on Replacement *)
    1.41 +
    1.42 +  "@Replace"   :: "[idt, idt, i, o] => i"      ("(1{_ ./ _: _, _})")
    1.43 +  "@RepFun"    :: "[i, idt, i] => i"           ("(1{_ ./ _: _})")
    1.44 +  "@Collect"   :: "[idt, i, o] => i"           ("(1{_: _ ./ _})")
    1.45 +  PrimReplace  :: "[i, [i, i] => o] => i"
    1.46 +  Replace      :: "[i, [i, i] => o] => i"
    1.47 +  RepFun       :: "[i, i => i] => i"
    1.48 +  Collect      :: "[i, i => o] => i"
    1.49 +
    1.50 +  (* Descriptions *)
    1.51 +
    1.52 +  "@THE"       :: "[idt, o] => i"              ("(3THE _./ _)" 10)
    1.53 +  The          :: "[i => o] => i"
    1.54 +  if           :: "[o, i, i] => i"
    1.55 +
    1.56 +  (* Enumerations of type i *)
    1.57 +
    1.58 +  ""           :: "i => is"                    ("_")
    1.59 +  "@Enum"      :: "[i, is] => is"              ("_,/ _")
    1.60 +
    1.61 +  (* Finite Sets *)
    1.62 +
    1.63 +  "@Finset"    :: "is => i"                    ("{(_)}")
    1.64 +  Upair, cons  :: "[i, i] => i"
    1.65 +  succ         :: "i => i"
    1.66 +
    1.67 +  (* Ordered Pairing and n-Tuples *)
    1.68 +
    1.69 +  "@Tuple"     :: "[i, is] => i"               ("<(_,/ _)>")
    1.70 +  PAIR         :: "syntax"
    1.71 +  Pair         :: "[i, i] => i"
    1.72 +  fst, snd     :: "i => i"
    1.73 +  split        :: "[[i,i] => i, i] => i"
    1.74 +  fsplit       :: "[[i,i] => o, i] => o"
    1.75 +
    1.76 +  (* Sigma and Pi Operators *)
    1.77 +
    1.78 +  "@PROD"      :: "[idt, i, i] => i"           ("(3PROD _:_./ _)" 10)
    1.79 +  "@SUM"       :: "[idt, i, i] => i"           ("(3SUM _:_./ _)" 10)
    1.80 +  "@lam"       :: "[idt, i, i] => i"           ("(3lam _:_./ _)" 10)
    1.81 +  Pi, Sigma    :: "[i, i => i] => i"
    1.82 +
    1.83 +  (* Relations and Functions *)
    1.84 +
    1.85 +  domain       :: "i => i"
    1.86 +  range        :: "i => i"
    1.87 +  field        :: "i => i"
    1.88 +  converse     :: "i => i"
    1.89 +  Lambda       :: "[i, i => i] => i"
    1.90 +  restrict     :: "[i, i] => i"
    1.91 +
    1.92 +  (* Infixes in order of decreasing precedence *)
    1.93 +
    1.94 +  "``"  :: "[i, i] => i"         (infixl 90) (*image*)
    1.95 +  "-``" :: "[i, i] => i"         (infixl 90) (*inverse image*)
    1.96 +  "`"   :: "[i, i] => i"         (infixl 90) (*function application*)
    1.97 +
    1.98 +  (*Except for their translations, * and -> are right-associating infixes*)
    1.99 +  " *"  :: "[i, i] => i"         ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
   1.100 +  "Int" :: "[i, i] => i"         (infixl 70) (*binary intersection*)
   1.101 +  "Un"  :: "[i, i] => i"         (infixl 65) (*binary union*)
   1.102 +  "-"   :: "[i, i] => i"         (infixl 65) (*set difference*)
   1.103 +  " ->" :: "[i, i] => i"         ("(_ ->/ _)" [61, 60] 60) (*function space*)
   1.104 +  "<="  :: "[i, i] => o"         (infixl 50) (*subset relation*)
   1.105 +  ":"   :: "[i, i] => o"         (infixl 50) (*membership relation*)
   1.106 +
   1.107 +
   1.108 +translations
   1.109 +  "{x, xs}"     == "cons(x, {xs})"
   1.110 +  "{x}"         == "cons(x, 0)"
   1.111 +
   1.112 +  "PAIR(x, Pair(y, z))" <= "Pair(x, Pair(y, z))"
   1.113 +  "PAIR(x, PAIR(y, z))" <= "Pair(x, PAIR(y, z))"
   1.114 +  "<x, y, z>"           <= "PAIR(x, <y, z>)"
   1.115 +  "<x, y, z>"           == "Pair(x, <y, z>)"
   1.116 +  "<x, y>"              == "Pair(x, y)"
   1.117 +
   1.118 +  "{x:A. P}"    == "Collect(A, %x. P)"
   1.119 +  "{y. x:A, Q}" == "Replace(A, %x y. Q)"
   1.120 +  "{f. x:A}"    == "RepFun(A, %x. f)"
   1.121 +  "INT x:A. B"  == "Inter({B. x:A})"
   1.122 +  "UN x:A. B"   == "Union({B. x:A})"
   1.123 +  "PROD x:A. B" => "Pi(A, %x. B)"
   1.124 +  "SUM x:A. B"  => "Sigma(A, %x. B)"
   1.125 +  "THE x. P"    == "The(%x. P)"
   1.126 +  "lam x:A. f"  == "Lambda(A, %x. f)"
   1.127 +  "ALL x:A. P"  == "Ball(A, %x. P)"
   1.128 +  "EX x:A. P"   == "Bex(A, %x. P)"
   1.129 +
   1.130 +
   1.131 +rules
   1.132 +
   1.133 + (* Bounded Quantifiers *)
   1.134 +Ball_def        "Ball(A,P) == ALL x. x:A --> P(x)"
   1.135 +Bex_def         "Bex(A,P) == EX x. x:A & P(x)"
   1.136 +subset_def      "A <= B == ALL x:A. x:B"
   1.137 +
   1.138 + (* ZF axioms -- see Suppes p.238
   1.139 +    Axioms for Union, Pow and Replace state existence only,
   1.140 +        uniqueness is derivable using extensionality.  *)
   1.141 +
   1.142 +extension       "A = B <-> A <= B & B <= A"
   1.143 +union_iff       "A : Union(C) <-> (EX B:C. A:B)"
   1.144 +power_set       "A : Pow(B) <-> A <= B"
   1.145 +succ_def        "succ(i) == cons(i,i)"
   1.146 +
   1.147 + (*We may name this set, though it is not uniquely defined. *)
   1.148 +infinity        "0:Inf & (ALL y:Inf. succ(y): Inf)"
   1.149 +
   1.150 + (*This formulation facilitates case analysis on A. *)
   1.151 +foundation      "A=0 | (EX x:A. ALL y:x. ~ y:A)"
   1.152 +
   1.153 + (* Schema axiom since predicate P is a higher-order variable *)
   1.154 +replacement     "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
   1.155 +\                        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
   1.156 +
   1.157 + (* Derived form of replacement, restricting P to its functional part.
   1.158 +    The resulting set (for functional P) is the same as with
   1.159 +    PrimReplace, but the rules are simpler. *)
   1.160 +Replace_def     "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
   1.161 +
   1.162 + (* Functional form of replacement -- analgous to ML's map functional *)
   1.163 +RepFun_def      "RepFun(A,f) == {y . x:A, y=f(x)}"
   1.164 +
   1.165 + (* Separation and Pairing can be derived from the Replacement
   1.166 +    and Powerset Axioms using the following definitions.  *)
   1.167 +
   1.168 +Collect_def     "Collect(A,P) == {y . x:A, x=y & P(x)}"
   1.169 +
   1.170 + (*Unordered pairs (Upair) express binary union/intersection and cons;
   1.171 +   set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)  *)
   1.172 +Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
   1.173 +cons_def    "cons(a,A) == Upair(a,a) Un A"
   1.174 +
   1.175 + (* Difference, general intersection, binary union and small intersection *)
   1.176 +
   1.177 +Diff_def        "A - B    == { x:A . ~(x:B) }"
   1.178 +Inter_def       "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
   1.179 +Un_def          "A Un  B  == Union(Upair(A,B))"
   1.180 +Int_def         "A Int B  == Inter(Upair(A,B))"
   1.181 +
   1.182 + (* Definite descriptions -- via Replace over the set "1" *)
   1.183 +
   1.184 +the_def         "The(P)    == Union({y . x:{0}, P(y)})"
   1.185 +if_def          "if(P,a,b) == THE z. P & z=a | ~P & z=b"
   1.186 +
   1.187 + (* Ordered pairs and disjoint union of a family of sets *)
   1.188 +
   1.189 + (* this "symmetric" definition works better than {{a}, {a,b}} *)
   1.190 +Pair_def        "<a,b>  == {{a,a}, {a,b}}"
   1.191 +fst_def         "fst == split(%x y.x)"
   1.192 +snd_def         "snd == split(%x y.y)"
   1.193 +split_def       "split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)"
   1.194 +fsplit_def      "fsplit(R,z) == EX x y. z=<x,y> & R(x,y)"
   1.195 +Sigma_def       "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
   1.196 +
   1.197 + (* Operations on relations *)
   1.198 +
   1.199 +(*converse of relation r, inverse of function*)
   1.200 +converse_def    "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
   1.201 +
   1.202 +domain_def      "domain(r) == {x. w:r, EX y. w=<x,y>}"
   1.203 +range_def       "range(r) == domain(converse(r))"
   1.204 +field_def       "field(r) == domain(r) Un range(r)"
   1.205 +image_def       "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   1.206 +vimage_def      "r -`` A == converse(r)``A"
   1.207 +
   1.208 + (* Abstraction, application and Cartesian product of a family of sets *)
   1.209 +
   1.210 +lam_def         "Lambda(A,b) == {<x,b(x)> . x:A}"
   1.211 +apply_def       "f`a == THE y. <a,y> : f"
   1.212 +Pi_def          "Pi(A,B)  == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}"
   1.213 +
   1.214 +  (* Restrict the function f to the domain A *)
   1.215 +restrict_def    "restrict(f,A) == lam x:A.f`x"
   1.216 +
   1.217 +end
   1.218 +
   1.219 +
   1.220 +ML
   1.221 +
   1.222 +(* 'Dependent' type operators *)
   1.223 +
   1.224 +val parse_translation =
   1.225 +  [(" ->", ndependent_tr "Pi"),
   1.226 +   (" *", ndependent_tr "Sigma")];
   1.227 +
   1.228 +val print_translation =
   1.229 +  [("Pi", dependent_tr' ("@PROD", " ->")),
   1.230 +   ("Sigma", dependent_tr' ("@SUM", " *"))];