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