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