src/ZF/zf.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 37 cebe01deba80
permissions -rw-r--r--
Initial revision
     1 (*  Title:      ZF/zf.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Zermelo-Fraenkel Set Theory
     7 *)
     8 
     9 ZF = FOL +
    10 
    11 types
    12   i, is, syntax 0
    13 
    14 arities
    15   i :: term
    16 
    17 
    18 consts
    19 
    20   "0"          :: "i"                          ("0") (*the empty set*)
    21   Pow          :: "i => i"                                 (*power sets*)
    22   Inf          :: "i"                                      (*infinite set*)
    23 
    24   (* Bounded Quantifiers *)
    25 
    26   "@Ball"      :: "[idt, i, o] => o"           ("(3ALL _:_./ _)" 10)
    27   "@Bex"       :: "[idt, i, o] => o"           ("(3EX _:_./ _)" 10)
    28   Ball         :: "[i, i => o] => o"
    29   Bex          :: "[i, i => o] => o"
    30 
    31   (* General Union and Intersection *)
    32 
    33   "@INTER"     :: "[idt, i, i] => i"           ("(3INT _:_./ _)" 10)
    34   "@UNION"     :: "[idt, i, i] => i"           ("(3UN _:_./ _)" 10)
    35   Union, Inter :: "i => i"
    36 
    37   (* Variations on Replacement *)
    38 
    39   "@Replace"   :: "[idt, idt, i, o] => i"      ("(1{_ ./ _: _, _})")
    40   "@RepFun"    :: "[i, idt, i] => i"           ("(1{_ ./ _: _})")
    41   "@Collect"   :: "[idt, i, o] => i"           ("(1{_: _ ./ _})")
    42   PrimReplace  :: "[i, [i, i] => o] => i"
    43   Replace      :: "[i, [i, i] => o] => i"
    44   RepFun       :: "[i, i => i] => i"
    45   Collect      :: "[i, i => o] => i"
    46 
    47   (* Descriptions *)
    48 
    49   "@THE"       :: "[idt, o] => i"              ("(3THE _./ _)" 10)
    50   The          :: "[i => o] => i"
    51   if           :: "[o, i, i] => i"
    52 
    53   (* Enumerations of type i *)
    54 
    55   ""           :: "i => is"                    ("_")
    56   "@Enum"      :: "[i, is] => is"              ("_,/ _")
    57 
    58   (* Finite Sets *)
    59 
    60   "@Finset"    :: "is => i"                    ("{(_)}")
    61   Upair, cons  :: "[i, i] => i"
    62   succ         :: "i => i"
    63 
    64   (* Ordered Pairing and n-Tuples *)
    65 
    66   "@Tuple"     :: "[i, is] => i"               ("<(_,/ _)>")
    67   PAIR         :: "syntax"
    68   Pair         :: "[i, i] => i"
    69   fst, snd     :: "i => i"
    70   split        :: "[[i,i] => i, i] => i"
    71   fsplit       :: "[[i,i] => o, i] => o"
    72 
    73   (* Sigma and Pi Operators *)
    74 
    75   "@PROD"      :: "[idt, i, i] => i"           ("(3PROD _:_./ _)" 10)
    76   "@SUM"       :: "[idt, i, i] => i"           ("(3SUM _:_./ _)" 10)
    77   "@lam"       :: "[idt, i, i] => i"           ("(3lam _:_./ _)" 10)
    78   Pi, Sigma    :: "[i, i => i] => i"
    79 
    80   (* Relations and Functions *)
    81 
    82   domain       :: "i => i"
    83   range        :: "i => i"
    84   field        :: "i => i"
    85   converse     :: "i => i"
    86   Lambda       :: "[i, i => i] => i"
    87   restrict     :: "[i, i] => i"
    88 
    89   (* Infixes in order of decreasing precedence *)
    90 
    91   "``"  :: "[i, i] => i"         (infixl 90) (*image*)
    92   "-``" :: "[i, i] => i"         (infixl 90) (*inverse image*)
    93   "`"   :: "[i, i] => i"         (infixl 90) (*function application*)
    94 
    95   (*Except for their translations, * and -> are right-associating infixes*)
    96   " *"  :: "[i, i] => i"         ("(_ */ _)" [81, 80] 80) (*Cartesian product*)
    97   "Int" :: "[i, i] => i"         (infixl 70) (*binary intersection*)
    98   "Un"  :: "[i, i] => i"         (infixl 65) (*binary union*)
    99   "-"   :: "[i, i] => i"         (infixl 65) (*set difference*)
   100   " ->" :: "[i, i] => i"         ("(_ ->/ _)" [61, 60] 60) (*function space*)
   101   "<="  :: "[i, i] => o"         (infixl 50) (*subset relation*)
   102   ":"   :: "[i, i] => o"         (infixl 50) (*membership relation*)
   103 
   104 
   105 translations
   106   "{x, xs}"     == "cons(x, {xs})"
   107   "{x}"         == "cons(x, 0)"
   108 
   109   "PAIR(x, Pair(y, z))" <= "Pair(x, Pair(y, z))"
   110   "PAIR(x, PAIR(y, z))" <= "Pair(x, PAIR(y, z))"
   111   "<x, y, z>"           <= "PAIR(x, <y, z>)"
   112   "<x, y, z>"           == "Pair(x, <y, z>)"
   113   "<x, y>"              == "Pair(x, y)"
   114 
   115   "{x:A. P}"    == "Collect(A, %x. P)"
   116   "{y. x:A, Q}" == "Replace(A, %x y. Q)"
   117   "{f. x:A}"    == "RepFun(A, %x. f)"
   118   "INT x:A. B"  == "Inter({B. x:A})"
   119   "UN x:A. B"   == "Union({B. x:A})"
   120   "PROD x:A. B" => "Pi(A, %x. B)"
   121   "SUM x:A. B"  => "Sigma(A, %x. B)"
   122   "THE x. P"    == "The(%x. P)"
   123   "lam x:A. f"  == "Lambda(A, %x. f)"
   124   "ALL x:A. P"  == "Ball(A, %x. P)"
   125   "EX x:A. P"   == "Bex(A, %x. P)"
   126 
   127 
   128 rules
   129 
   130  (* Bounded Quantifiers *)
   131 Ball_def        "Ball(A,P) == ALL x. x:A --> P(x)"
   132 Bex_def         "Bex(A,P) == EX x. x:A & P(x)"
   133 subset_def      "A <= B == ALL x:A. x:B"
   134 
   135  (* ZF axioms -- see Suppes p.238
   136     Axioms for Union, Pow and Replace state existence only,
   137         uniqueness is derivable using extensionality.  *)
   138 
   139 extension       "A = B <-> A <= B & B <= A"
   140 union_iff       "A : Union(C) <-> (EX B:C. A:B)"
   141 power_set       "A : Pow(B) <-> A <= B"
   142 succ_def        "succ(i) == cons(i,i)"
   143 
   144  (*We may name this set, though it is not uniquely defined. *)
   145 infinity        "0:Inf & (ALL y:Inf. succ(y): Inf)"
   146 
   147  (*This formulation facilitates case analysis on A. *)
   148 foundation      "A=0 | (EX x:A. ALL y:x. ~ y:A)"
   149 
   150  (* Schema axiom since predicate P is a higher-order variable *)
   151 replacement     "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
   152 \                        b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
   153 
   154  (* Derived form of replacement, restricting P to its functional part.
   155     The resulting set (for functional P) is the same as with
   156     PrimReplace, but the rules are simpler. *)
   157 Replace_def     "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
   158 
   159  (* Functional form of replacement -- analgous to ML's map functional *)
   160 RepFun_def      "RepFun(A,f) == {y . x:A, y=f(x)}"
   161 
   162  (* Separation and Pairing can be derived from the Replacement
   163     and Powerset Axioms using the following definitions.  *)
   164 
   165 Collect_def     "Collect(A,P) == {y . x:A, x=y & P(x)}"
   166 
   167  (*Unordered pairs (Upair) express binary union/intersection and cons;
   168    set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)  *)
   169 Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
   170 cons_def    "cons(a,A) == Upair(a,a) Un A"
   171 
   172  (* Difference, general intersection, binary union and small intersection *)
   173 
   174 Diff_def        "A - B    == { x:A . ~(x:B) }"
   175 Inter_def       "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
   176 Un_def          "A Un  B  == Union(Upair(A,B))"
   177 Int_def         "A Int B  == Inter(Upair(A,B))"
   178 
   179  (* Definite descriptions -- via Replace over the set "1" *)
   180 
   181 the_def         "The(P)    == Union({y . x:{0}, P(y)})"
   182 if_def          "if(P,a,b) == THE z. P & z=a | ~P & z=b"
   183 
   184  (* Ordered pairs and disjoint union of a family of sets *)
   185 
   186  (* this "symmetric" definition works better than {{a}, {a,b}} *)
   187 Pair_def        "<a,b>  == {{a,a}, {a,b}}"
   188 fst_def         "fst == split(%x y.x)"
   189 snd_def         "snd == split(%x y.y)"
   190 split_def       "split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)"
   191 fsplit_def      "fsplit(R,z) == EX x y. z=<x,y> & R(x,y)"
   192 Sigma_def       "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
   193 
   194  (* Operations on relations *)
   195 
   196 (*converse of relation r, inverse of function*)
   197 converse_def    "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
   198 
   199 domain_def      "domain(r) == {x. w:r, EX y. w=<x,y>}"
   200 range_def       "range(r) == domain(converse(r))"
   201 field_def       "field(r) == domain(r) Un range(r)"
   202 image_def       "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   203 vimage_def      "r -`` A == converse(r)``A"
   204 
   205  (* Abstraction, application and Cartesian product of a family of sets *)
   206 
   207 lam_def         "Lambda(A,b) == {<x,b(x)> . x:A}"
   208 apply_def       "f`a == THE y. <a,y> : f"
   209 Pi_def          "Pi(A,B)  == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}"
   210 
   211   (* Restrict the function f to the domain A *)
   212 restrict_def    "restrict(f,A) == lam x:A.f`x"
   213 
   214 end
   215 
   216 
   217 ML
   218 
   219 (* 'Dependent' type operators *)
   220 
   221 val parse_translation =
   222   [(" ->", ndependent_tr "Pi"),
   223    (" *", ndependent_tr "Sigma")];
   224 
   225 val print_translation =
   226   [("Pi", dependent_tr' ("@PROD", " ->")),
   227    ("Sigma", dependent_tr' ("@SUM", " *"))];