src/ZF/ZF.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 2286 c2f76a5bad65
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
     1
(*  Title:      ZF/ZF.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
     9
ZF = FOL + Let + 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
types
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    12
  i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
arities
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  i :: term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    19
  "0"         :: i                  ("0")   (*the empty set*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    20
  Pow         :: i => i                     (*power sets*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    21
  Inf         :: i                          (*infinite set*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  (* Bounded Quantifiers *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    25
  Ball, Bex   :: [i, i => o] => o
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  (* General Union and Intersection *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    29
  Union,Inter :: i => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  (* Variations on Replacement *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    33
  PrimReplace :: [i, [i, i] => o] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    34
  Replace     :: [i, [i, i] => o] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    35
  RepFun      :: [i, i => i] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    36
  Collect     :: [i, i => o] => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  (* Descriptions *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    40
  The         :: (i => o) => i      (binder "THE " 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    41
  if          :: [o, i, i] => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  (* Finite Sets *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    45
  Upair, cons :: [i, i] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    46
  succ        :: i => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    48
  (* Ordered Pairing *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    50
  Pair        :: [i, i] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    51
  fst, snd    :: i => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    52
  split       :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  (* Sigma and Pi Operators *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    56
  Sigma, Pi   :: [i, i => i] => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  (* Relations and Functions *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    60
  domain      :: i => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    61
  range       :: i => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    62
  field       :: i => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    63
  converse    :: i => i
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    64
  function    :: i => o         (*is a relation a function?*)
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    65
  Lambda      :: [i, i => i] => i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    66
  restrict    :: [i, i] => i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  (* Infixes in order of decreasing precedence *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    70
  "``"        :: [i, i] => i    (infixl 90) (*image*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    71
  "-``"       :: [i, i] => i    (infixl 90) (*inverse image*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    72
  "`"         :: [i, i] => i    (infixl 90) (*function application*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    73
(*"*"         :: [i, i] => i    (infixr 80) (*Cartesian product*)*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    74
  "Int"       :: [i, i] => i    (infixl 70) (*binary intersection*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    75
  "Un"        :: [i, i] => i    (infixl 65) (*binary union*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    76
  "-"         :: [i, i] => i    (infixl 65) (*set difference*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    77
(*"->"        :: [i, i] => i    (infixr 60) (*function space*)*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    78
  "<="        :: [i, i] => o    (infixl 50) (*subset relation*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    79
  ":"         :: [i, i] => o    (infixl 50) (*membership relation*)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    80
(*"~:"        :: [i, i] => o    (infixl 50) (*negated membership relation*)*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    83
types
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    84
  is
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
    85
  pttrns
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    86
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
    87
syntax
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    88
  ""          :: i => is                   ("_")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    89
  "@Enum"     :: [i, is] => is             ("_,/ _")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    90
  "~:"        :: [i, i] => o               (infixl 50)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    91
  "@Finset"   :: is => i                   ("{(_)}")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    92
  "@Tuple"    :: [i, is] => i              ("<(_,/ _)>")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    93
  "@Collect"  :: [pttrn, i, o] => i        ("(1{_: _ ./ _})")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    94
  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    95
  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _: _})" [51,0,51])
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    96
  "@INTER"    :: [pttrn, i, i] => i        ("(3INT _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    97
  "@UNION"    :: [pttrn, i, i] => i        ("(3UN _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    98
  "@PROD"     :: [pttrn, i, i] => i        ("(3PROD _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    99
  "@SUM"      :: [pttrn, i, i] => i        ("(3SUM _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   100
  "->"        :: [i, i] => i               (infixr 60)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   101
  "*"         :: [i, i] => i               (infixr 80)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   102
  "@lam"      :: [pttrn, i, i] => i        ("(3lam _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   103
  "@Ball"     :: [pttrn, i, o] => o        ("(3ALL _:_./ _)" 10)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   104
  "@Bex"      :: [pttrn, i, o] => o        ("(3EX _:_./ _)" 10)
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   105
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   106
  (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   107
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   108
  "@pttrn"  :: pttrns => pttrn            ("<_>")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   109
  ""        ::  pttrn           => pttrns ("_")
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
   110
  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   111
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
translations
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   113
  "x ~: y"      == "~ (x : y)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  "{x, xs}"     == "cons(x, {xs})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
  "{x}"         == "cons(x, 0)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  "{x:A. P}"    == "Collect(A, %x. P)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
  "{y. x:A, Q}" == "Replace(A, %x y. Q)"
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   118
  "{b. x:A}"    == "RepFun(A, %x. b)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
  "INT x:A. B"  == "Inter({B. x:A})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
  "UN x:A. B"   == "Union({B. x:A})"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
  "PROD x:A. B" => "Pi(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
  "SUM x:A. B"  => "Sigma(A, %x. B)"
49
c78503b345c4 "The" now a binder, removed translation;
wenzelm
parents: 37
diff changeset
   123
  "A -> B"      => "Pi(A, _K(B))"
c78503b345c4 "The" now a binder, removed translation;
wenzelm
parents: 37
diff changeset
   124
  "A * B"       => "Sigma(A, _K(B))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
  "lam x:A. f"  == "Lambda(A, %x. f)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
  "ALL x:A. P"  == "Ball(A, %x. P)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
  "EX x:A. P"   == "Bex(A, %x. P)"
37
cebe01deba80 added ~: for "not in"
lcp
parents: 0
diff changeset
   128
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   129
  "<x, y, z>"   == "<x, <y, z>>"
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   130
  "<x, y>"      == "Pair(x, y)"
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   131
  "%<x,y,zs>.b"   == "split(%x <y,zs>.b)"
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   132
  "%<x,y>.b"      == "split(%x y.b)"
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   133
(* The <= direction fails if split has more than one argument because
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   134
   ast-matching fails.  Otherwise it would work fine *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
690
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   136
defs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   138
  (* Bounded Quantifiers *)
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   139
  Ball_def      "Ball(A, P) == ALL x. x:A --> P(x)"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   140
  Bex_def       "Bex(A, P) == EX x. x:A & P(x)"
690
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   141
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   142
  subset_def    "A <= B == ALL x:A. x:B"
690
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   143
  succ_def      "succ(i) == cons(i, i)"
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   144
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   145
rules
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   147
  (* ZF axioms -- see Suppes p.238
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   148
     Axioms for Union, Pow and Replace state existence only,
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   149
     uniqueness is derivable using extensionality. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   151
  extension     "A = B <-> A <= B & B <= A"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   152
  Union_iff     "A : Union(C) <-> (EX B:C. A:B)"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   153
  Pow_iff       "A : Pow(B) <-> A <= B"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   155
  (*We may name this set, though it is not uniquely defined.*)
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   156
  infinity      "0:Inf & (ALL y:Inf. succ(y): Inf)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   158
  (*This formulation facilitates case analysis on A.*)
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   159
  foundation    "A=0 | (EX x:A. ALL y:x. y~:A)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   161
  (*Schema axiom since predicate P is a higher-order variable*)
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1116
diff changeset
   162
  replacement   "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> 
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1116
diff changeset
   163
                         b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   164
690
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   165
defs
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   166
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   167
  (* Derived form of replacement, restricting P to its functional part.
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   168
     The resulting set (for functional P) is the same as with
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   169
     PrimReplace, but the rules are simpler. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   171
  Replace_def   "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   172
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   173
  (* Functional form of replacement -- analgous to ML's map functional *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   175
  RepFun_def    "RepFun(A,f) == {y . x:A, y=f(x)}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   177
  (* Separation and Pairing can be derived from the Replacement
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   178
     and Powerset Axioms using the following definitions. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   180
  Collect_def   "Collect(A,P) == {y . x:A, x=y & P(x)}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   182
  (*Unordered pairs (Upair) express binary union/intersection and cons;
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   183
    set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   185
  Upair_def   "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   186
  cons_def    "cons(a,A) == Upair(a,a) Un A"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   187
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   188
  (* Difference, general intersection, binary union and small intersection *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   190
  Diff_def      "A - B    == { x:A . ~(x:B) }"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   191
  Inter_def     "Inter(A) == { x:Union(A) . ALL y:A. x:y}"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   192
  Un_def        "A Un  B  == Union(Upair(A,B))"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   193
  Int_def       "A Int B  == Inter(Upair(A,B))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   195
  (* Definite descriptions -- via Replace over the set "1" *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   197
  the_def       "The(P)    == Union({y . x:{0}, P(y)})"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   198
  if_def        "if(P,a,b) == THE z. P & z=a | ~P & z=b"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   200
  (* Ordered pairs and disjoint union of a family of sets *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   202
  (* this "symmetric" definition works better than {{a}, {a,b}} *)
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   203
  Pair_def      "<a,b>  == {{a,a}, {a,b}}"
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   204
  fst_def       "fst(p) == THE a. EX b. p=<a,b>"
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   205
  snd_def       "snd(p) == THE b. EX a. p=<a,b>"
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   206
  split_def     "split(c,p) == c(fst(p), snd(p))"
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   207
  Sigma_def     "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   209
  (* Operations on relations *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   211
  (*converse of relation r, inverse of function*)
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   212
  converse_def  "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   214
  domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   215
  range_def     "range(r) == domain(converse(r))"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   216
  field_def     "field(r) == domain(r) Un range(r)"
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
   217
  function_def  "function(r) == ALL x y. <x,y>:r -->   
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
   218
                                (ALL y'. <x,y'>:r --> y=y')"
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   219
  image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   220
  vimage_def    "r -`` A == converse(r)``A"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   222
  (* Abstraction, application and Cartesian product of a family of sets *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   224
  lam_def       "Lambda(A,b) == {<x,b(x)> . x:A}"
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   225
  apply_def     "f`a == THE y. <a,y> : f"
690
b2bd1d5a3d16 ZF: NEW DEFINITION OF PI(A,B)
lcp
parents: 675
diff changeset
   226
  Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
  (* Restrict the function f to the domain A *)
615
84ac5f101bd1 minor cleanup, added 'syntax' section;
wenzelm
parents: 516
diff changeset
   229
  restrict_def  "restrict(f,A) == lam x:A.f`x"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   236
(* Pattern-matching and 'Dependent' type operators *)
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   237
(*
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   238
local open Syntax
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   239
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   240
fun pttrn s = const"@pttrn" $ s;
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   241
fun pttrns s t = const"@pttrns" $ s $ t;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   243
fun split2(Abs(x,T,t)) =
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   244
      let val (pats,u) = split1 t
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   245
      in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   246
  | split2(Const("split",_) $ r) =
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   247
      let val (pats,s) = split2(r)
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   248
          val (pats2,t) = split1(s)
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   249
      in (pttrns (pttrn pats) pats2, t) end
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   250
and split1(Abs(x,T,t)) =  (Free(x,T), subst_bounds([free x],t))
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   251
  | split1(Const("split",_)$t) = split2(t);
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   252
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   253
fun split_tr'(t::args) =
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   254
  let val (pats,ft) = split2(t)
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   255
  in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   256
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   257
in
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   258
*)
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   259
val print_translation = 
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   260
  [(*("split", split_tr'),*)
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   261
   ("Pi",    dependent_tr' ("@PROD", "op ->")),
632
f9a3f77f71e8 fixed infix names in print_translations;
wenzelm
parents: 615
diff changeset
   262
   ("Sigma", dependent_tr' ("@SUM", "op *"))];
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   263
(*
1106
62bdb9e5722b Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents: 690
diff changeset
   264
end;
1116
7fca5aabcbb0 Modified translation for pattern abstraction.
nipkow
parents: 1106
diff changeset
   265
*)