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