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