src/ZF/ZF.thy
 changeset 615 84ac5f101bd1 parent 516 1957113f0d7d child 632 f9a3f77f71e8
equal 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 `
`    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 `
`    35   Union, Inter  :: "i => i"`
`    29   Union, Inter  :: "i => i"`
`    36 `
`    30 `
`    37   (* Variations on Replacement *)`
`    31   (* Variations on Replacement *)`
`    38 `
`    32 `
`    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 `
`    57   (* Finite Sets *)`
`    43   (* Finite Sets *)`
`    58 `
`    44 `
`    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)"`
`   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", "*"))];`