src/ZF/ZF.thy
author paulson
Mon May 13 13:22:15 2002 +0200 (2002-05-13 ago)
changeset 13144 c5ae1522fb82
parent 13121 4888694b2829
child 13175 81082cfa5618
permissions -rw-r--r--
quotes around types
wenzelm@615
     1
(*  Title:      ZF/ZF.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Zermelo-Fraenkel Set Theory
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@13108
     9
ZF = Let +
clasohm@0
    10
wenzelm@3906
    11
global
wenzelm@3906
    12
clasohm@0
    13
types
wenzelm@615
    14
  i
clasohm@0
    15
clasohm@0
    16
arities
paulson@13144
    17
  i :: "term"
clasohm@0
    18
clasohm@0
    19
consts
clasohm@0
    20
paulson@13144
    21
  "0"         :: "i"                  ("0")   (*the empty set*)
paulson@13144
    22
  Pow         :: "i => i"                     (*power sets*)
paulson@13144
    23
  Inf         :: "i"                          (*infinite set*)
clasohm@0
    24
clasohm@0
    25
  (* Bounded Quantifiers *)
clasohm@0
    26
paulson@13144
    27
  Ball, Bex   :: "[i, i => o] => o"
clasohm@0
    28
clasohm@0
    29
  (* General Union and Intersection *)
clasohm@0
    30
paulson@13144
    31
  Union,Inter :: "i => i"
clasohm@0
    32
clasohm@0
    33
  (* Variations on Replacement *)
clasohm@0
    34
paulson@13144
    35
  PrimReplace :: "[i, [i, i] => o] => i"
paulson@13144
    36
  Replace     :: "[i, [i, i] => o] => i"
paulson@13144
    37
  RepFun      :: "[i, i => i] => i"
paulson@13144
    38
  Collect     :: "[i, i => o] => i"
clasohm@0
    39
clasohm@0
    40
  (* Descriptions *)
clasohm@0
    41
clasohm@1401
    42
  The         :: (i => o) => i      (binder "THE " 10)
paulson@13144
    43
  If          :: "[o, i, i] => i"     ("(if (_)/ then (_)/ else (_))" [10] 10)
paulson@6068
    44
paulson@6068
    45
syntax
paulson@13144
    46
  old_if      :: "[o, i, i] => i"   ("if '(_,_,_')")
clasohm@0
    47
paulson@6068
    48
translations
paulson@6068
    49
  "if(P,a,b)" => "If(P,a,b)"
paulson@6068
    50
paulson@6068
    51
paulson@6068
    52
consts
clasohm@0
    53
  (* Finite Sets *)
clasohm@0
    54
paulson@13144
    55
  Upair, cons :: "[i, i] => i"
paulson@13144
    56
  succ        :: "i => i"
clasohm@0
    57
wenzelm@615
    58
  (* Ordered Pairing *)
clasohm@0
    59
paulson@13144
    60
  Pair        :: "[i, i] => i"
paulson@13144
    61
  fst, snd    :: "i => i"
paulson@13144
    62
  split       :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
clasohm@0
    63
clasohm@0
    64
  (* Sigma and Pi Operators *)
clasohm@0
    65
paulson@13144
    66
  Sigma, Pi   :: "[i, i => i] => i"
clasohm@0
    67
clasohm@0
    68
  (* Relations and Functions *)
clasohm@0
    69
paulson@13144
    70
  domain      :: "i => i"
paulson@13144
    71
  range       :: "i => i"
paulson@13144
    72
  field       :: "i => i"
paulson@13144
    73
  converse    :: "i => i"
paulson@13144
    74
  relation    :: "i => o"         (*recognizes sets of pairs*)
paulson@13144
    75
  function    :: "i => o"         (*recognizes functions; can have non-pairs*)
paulson@13144
    76
  Lambda      :: "[i, i => i] => i"
paulson@13144
    77
  restrict    :: "[i, i] => i"
clasohm@0
    78
clasohm@0
    79
  (* Infixes in order of decreasing precedence *)
clasohm@0
    80
paulson@13144
    81
  "``"        :: "[i, i] => i"    (infixl 90) (*image*)
paulson@13144
    82
  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
paulson@13144
    83
  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
paulson@13144
    84
(*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
paulson@13144
    85
  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
paulson@13144
    86
  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
paulson@13144
    87
  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
paulson@13144
    88
(*"->"        :: "[i, i] => i"    (infixr 60) (*function space*)*)
paulson@13144
    89
  "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
paulson@13144
    90
  ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
paulson@13144
    91
(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
clasohm@0
    92
clasohm@0
    93
wenzelm@615
    94
types
wenzelm@615
    95
  is
wenzelm@3692
    96
  patterns
wenzelm@615
    97
wenzelm@615
    98
syntax
paulson@13144
    99
  ""          :: "i => is"                   ("_")
paulson@13144
   100
  "@Enum"     :: "[i, is] => is"             ("_,/ _")
paulson@13144
   101
  "~:"        :: "[i, i] => o"               (infixl 50)
paulson@13144
   102
  "@Finset"   :: "is => i"                   ("{(_)}")
paulson@13144
   103
  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
paulson@13144
   104
  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
paulson@13144
   105
  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
paulson@13144
   106
  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
paulson@13144
   107
  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
paulson@13144
   108
  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
paulson@13144
   109
  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
paulson@13144
   110
  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
paulson@13144
   111
  "->"        :: "[i, i] => i"               (infixr 60)
paulson@13144
   112
  "*"         :: "[i, i] => i"               (infixr 80)
paulson@13144
   113
  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
paulson@13144
   114
  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
paulson@13144
   115
  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
lcp@1106
   116
lcp@1106
   117
  (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
lcp@1106
   118
paulson@13144
   119
  "@pattern"  :: "patterns => pttrn"         ("<_>")
paulson@13144
   120
  ""          :: "pttrn => patterns"         ("_")
paulson@13144
   121
  "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
wenzelm@615
   122
clasohm@0
   123
translations
wenzelm@615
   124
  "x ~: y"      == "~ (x : y)"
clasohm@0
   125
  "{x, xs}"     == "cons(x, {xs})"
clasohm@0
   126
  "{x}"         == "cons(x, 0)"
clasohm@0
   127
  "{x:A. P}"    == "Collect(A, %x. P)"
clasohm@0
   128
  "{y. x:A, Q}" == "Replace(A, %x y. Q)"
wenzelm@615
   129
  "{b. x:A}"    == "RepFun(A, %x. b)"
clasohm@0
   130
  "INT x:A. B"  == "Inter({B. x:A})"
clasohm@0
   131
  "UN x:A. B"   == "Union({B. x:A})"
clasohm@0
   132
  "PROD x:A. B" => "Pi(A, %x. B)"
clasohm@0
   133
  "SUM x:A. B"  => "Sigma(A, %x. B)"
wenzelm@49
   134
  "A -> B"      => "Pi(A, _K(B))"
wenzelm@49
   135
  "A * B"       => "Sigma(A, _K(B))"
clasohm@0
   136
  "lam x:A. f"  == "Lambda(A, %x. f)"
clasohm@0
   137
  "ALL x:A. P"  == "Ball(A, %x. P)"
clasohm@0
   138
  "EX x:A. P"   == "Bex(A, %x. P)"
lcp@37
   139
lcp@1106
   140
  "<x, y, z>"   == "<x, <y, z>>"
lcp@1106
   141
  "<x, y>"      == "Pair(x, y)"
wenzelm@2286
   142
  "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
wenzelm@3840
   143
  "%<x,y>.b"    == "split(%x y. b)"
wenzelm@2286
   144
clasohm@0
   145
wenzelm@12114
   146
syntax (xsymbols)
paulson@13144
   147
  "op *"      :: "[i, i] => i"               (infixr "\\<times>" 80)
paulson@13144
   148
  "op Int"    :: "[i, i] => i"    	   (infixl "\\<inter>" 70)
paulson@13144
   149
  "op Un"     :: "[i, i] => i"    	   (infixl "\\<union>" 65)
paulson@13144
   150
  "op ->"     :: "[i, i] => i"               (infixr "\\<rightarrow>" 60)
paulson@13144
   151
  "op <="     :: "[i, i] => o"    	   (infixl "\\<subseteq>" 50)
paulson@13144
   152
  "op :"      :: "[i, i] => o"    	   (infixl "\\<in>" 50)
paulson@13144
   153
  "op ~:"     :: "[i, i] => o"               (infixl "\\<notin>" 50)
paulson@13144
   154
  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \\<in> _ ./ _})")
paulson@13144
   155
  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \\<in> _, _})")
paulson@13144
   156
  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \\<in> _})" [51,0,51])
paulson@13144
   157
  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\\<Union>_\\<in>_./ _)" 10)
paulson@13144
   158
  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\\<Inter>_\\<in>_./ _)" 10)
paulson@13144
   159
  Union       :: "i =>i"                     ("\\<Union>_" [90] 90)
paulson@13144
   160
  Inter       :: "i =>i"                     ("\\<Inter>_" [90] 90)
paulson@13144
   161
  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\\<Pi>_\\<in>_./ _)" 10)
paulson@13144
   162
  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\\<Sigma>_\\<in>_./ _)" 10)
paulson@13144
   163
  "@lam"      :: "[pttrn, i, i] => i"        ("(3\\<lambda>_\\<in>_./ _)" 10)
paulson@13144
   164
  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\\<forall>_\\<in>_./ _)" 10)
paulson@13144
   165
  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\\<exists>_\\<in>_./ _)" 10)
paulson@13144
   166
  "@Tuple"    :: "[i, is] => i"              ("\\<langle>(_,/ _)\\<rangle>")
paulson@13144
   167
  "@pattern"  :: "patterns => pttrn"         ("\\<langle>_\\<rangle>")
wenzelm@2540
   168
wenzelm@6340
   169
syntax (HTML output)
paulson@13144
   170
  "op *"      :: "[i, i] => i"               (infixr "\\<times>" 80)
wenzelm@6340
   171
wenzelm@2540
   172
lcp@690
   173
defs
clasohm@0
   174
wenzelm@615
   175
  (* Bounded Quantifiers *)
wenzelm@615
   176
  Ball_def      "Ball(A, P) == ALL x. x:A --> P(x)"
wenzelm@615
   177
  Bex_def       "Bex(A, P) == EX x. x:A & P(x)"
lcp@690
   178
wenzelm@615
   179
  subset_def    "A <= B == ALL x:A. x:B"
lcp@690
   180
  succ_def      "succ(i) == cons(i, i)"
lcp@690
   181
wenzelm@3906
   182
wenzelm@3940
   183
local
wenzelm@3906
   184
lcp@690
   185
rules
clasohm@0
   186
wenzelm@615
   187
  (* ZF axioms -- see Suppes p.238
wenzelm@615
   188
     Axioms for Union, Pow and Replace state existence only,
wenzelm@615
   189
     uniqueness is derivable using extensionality. *)
clasohm@0
   190
wenzelm@615
   191
  extension     "A = B <-> A <= B & B <= A"
wenzelm@615
   192
  Union_iff     "A : Union(C) <-> (EX B:C. A:B)"
wenzelm@615
   193
  Pow_iff       "A : Pow(B) <-> A <= B"
clasohm@0
   194
wenzelm@615
   195
  (*We may name this set, though it is not uniquely defined.*)
wenzelm@615
   196
  infinity      "0:Inf & (ALL y:Inf. succ(y): Inf)"
clasohm@0
   197
wenzelm@615
   198
  (*This formulation facilitates case analysis on A.*)
wenzelm@615
   199
  foundation    "A=0 | (EX x:A. ALL y:x. y~:A)"
clasohm@0
   200
wenzelm@615
   201
  (*Schema axiom since predicate P is a higher-order variable*)
paulson@12762
   202
  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
clasohm@1155
   203
                         b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
wenzelm@615
   204
lcp@690
   205
defs
lcp@690
   206
wenzelm@615
   207
  (* Derived form of replacement, restricting P to its functional part.
wenzelm@615
   208
     The resulting set (for functional P) is the same as with
wenzelm@615
   209
     PrimReplace, but the rules are simpler. *)
clasohm@0
   210
wenzelm@3840
   211
  Replace_def   "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
wenzelm@615
   212
wenzelm@615
   213
  (* Functional form of replacement -- analgous to ML's map functional *)
clasohm@0
   214
wenzelm@615
   215
  RepFun_def    "RepFun(A,f) == {y . x:A, y=f(x)}"
clasohm@0
   216
wenzelm@615
   217
  (* Separation and Pairing can be derived from the Replacement
wenzelm@615
   218
     and Powerset Axioms using the following definitions. *)
clasohm@0
   219
wenzelm@615
   220
  Collect_def   "Collect(A,P) == {y . x:A, x=y & P(x)}"
clasohm@0
   221
wenzelm@615
   222
  (*Unordered pairs (Upair) express binary union/intersection and cons;
wenzelm@615
   223
    set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
clasohm@0
   224
wenzelm@615
   225
  Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
wenzelm@615
   226
  cons_def    "cons(a,A) == Upair(a,a) Un A"
wenzelm@615
   227
paulson@2872
   228
  (* Difference, general intersection, binary union and small intersection *)
paulson@2872
   229
paulson@2872
   230
  Diff_def      "A - B    == { x:A . ~(x:B) }"
paulson@2872
   231
  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
paulson@2872
   232
  Un_def        "A Un  B  == Union(Upair(A,B))"
paulson@2872
   233
  Int_def       "A Int B  == Inter(Upair(A,B))"
paulson@2872
   234
paulson@2872
   235
  (* Definite descriptions -- via Replace over the set "1" *)
paulson@2872
   236
paulson@2872
   237
  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
paulson@2872
   238
  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
clasohm@0
   239
wenzelm@615
   240
  (* this "symmetric" definition works better than {{a}, {a,b}} *)
wenzelm@615
   241
  Pair_def      "<a,b>  == {{a,a}, {a,b}}"
lcp@1106
   242
  fst_def       "fst(p) == THE a. EX b. p=<a,b>"
lcp@1106
   243
  snd_def       "snd(p) == THE b. EX a. p=<a,b>"
paulson@12762
   244
  split_def     "split(c) == %p. c(fst(p), snd(p))"
wenzelm@615
   245
  Sigma_def     "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
clasohm@0
   246
wenzelm@615
   247
  (* Operations on relations *)
clasohm@0
   248
wenzelm@615
   249
  (*converse of relation r, inverse of function*)
wenzelm@615
   250
  converse_def  "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
clasohm@0
   251
wenzelm@615
   252
  domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
wenzelm@615
   253
  range_def     "range(r) == domain(converse(r))"
wenzelm@615
   254
  field_def     "field(r) == domain(r) Un range(r)"
paulson@13121
   255
  relation_def  "relation(r) == ALL z:r. EX x y. z = <x,y>"
paulson@13121
   256
  function_def  "function(r) ==
paulson@13121
   257
		    ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')"
wenzelm@615
   258
  image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
wenzelm@615
   259
  vimage_def    "r -`` A == converse(r)``A"
clasohm@0
   260
wenzelm@615
   261
  (* Abstraction, application and Cartesian product of a family of sets *)
clasohm@0
   262
wenzelm@615
   263
  lam_def       "Lambda(A,b) == {<x,b(x)> . x:A}"
wenzelm@615
   264
  apply_def     "f`a == THE y. <a,y> : f"
lcp@690
   265
  Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
clasohm@0
   266
paulson@12891
   267
  (* Restrict the relation r to the domain A *)
paulson@12891
   268
  restrict_def  "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}"
clasohm@0
   269
clasohm@0
   270
end
clasohm@0
   271
clasohm@0
   272
clasohm@0
   273
ML
clasohm@0
   274
lcp@1106
   275
(* Pattern-matching and 'Dependent' type operators *)
lcp@1106
   276
paulson@12762
   277
val print_translation =
nipkow@1116
   278
  [(*("split", split_tr'),*)
lcp@1106
   279
   ("Pi",    dependent_tr' ("@PROD", "op ->")),
wenzelm@632
   280
   ("Sigma", dependent_tr' ("@SUM", "op *"))];