src/ZF/ZF.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 23168 fcdd4346fa6b
child 24826 78e6a3cea367
permissions -rw-r--r--
added Tools/lin_arith.ML;
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
paulson@14076
     5
*)
clasohm@0
     6
paulson@14076
     7
header{*Zermelo-Fraenkel Set Theory*}
clasohm@0
     8
haftmann@16417
     9
theory ZF imports FOL begin
clasohm@0
    10
wenzelm@23168
    11
ML {* reset eta_contract *}
wenzelm@23168
    12
wenzelm@3906
    13
global
wenzelm@3906
    14
paulson@14076
    15
typedecl i
paulson@14076
    16
arities  i :: "term"
clasohm@0
    17
clasohm@0
    18
consts
clasohm@0
    19
paulson@14076
    20
  "0"         :: "i"                  ("0")   --{*the empty set*}
paulson@14076
    21
  Pow         :: "i => i"                     --{*power sets*}
paulson@14076
    22
  Inf         :: "i"                          --{*infinite set*}
clasohm@0
    23
paulson@14076
    24
text {*Bounded Quantifiers *}
paulson@14076
    25
consts
paulson@13780
    26
  Ball   :: "[i, i => o] => o"
paulson@13780
    27
  Bex   :: "[i, i => o] => o"
clasohm@0
    28
paulson@14076
    29
text {*General Union and Intersection *}
paulson@14076
    30
consts
paulson@13780
    31
  Union :: "i => i"
paulson@13780
    32
  Inter :: "i => i"
clasohm@0
    33
paulson@14076
    34
text {*Variations on Replacement *}
paulson@14076
    35
consts
paulson@13144
    36
  PrimReplace :: "[i, [i, i] => o] => i"
paulson@13144
    37
  Replace     :: "[i, [i, i] => o] => i"
paulson@13144
    38
  RepFun      :: "[i, i => i] => i"
paulson@13144
    39
  Collect     :: "[i, i => o] => i"
clasohm@0
    40
paulson@14883
    41
text{*Definite descriptions -- via Replace over the set "1"*}
paulson@14076
    42
consts
paulson@13780
    43
  The         :: "(i => o) => i"      (binder "THE " 10)
paulson@13144
    44
  If          :: "[o, i, i] => i"     ("(if (_)/ then (_)/ else (_))" [10] 10)
paulson@6068
    45
paulson@6068
    46
syntax
paulson@13144
    47
  old_if      :: "[o, i, i] => i"   ("if '(_,_,_')")
clasohm@0
    48
paulson@6068
    49
translations
paulson@6068
    50
  "if(P,a,b)" => "If(P,a,b)"
paulson@6068
    51
paulson@6068
    52
paulson@14076
    53
text {*Finite Sets *}
paulson@6068
    54
consts
paulson@13780
    55
  Upair :: "[i, i] => i"
paulson@13780
    56
  cons  :: "[i, i] => i"
paulson@13780
    57
  succ  :: "i => i"
clasohm@0
    58
paulson@14076
    59
text {*Ordered Pairing *}
paulson@14076
    60
consts
paulson@13780
    61
  Pair  :: "[i, i] => i"
paulson@13780
    62
  fst   :: "i => i"
paulson@13780
    63
  snd   :: "i => i"
wenzelm@14854
    64
  split :: "[[i, i] => 'a, i] => 'a::{}"  --{*for pattern-matching*}
clasohm@0
    65
paulson@14076
    66
text {*Sigma and Pi Operators *}
paulson@14076
    67
consts
paulson@13780
    68
  Sigma :: "[i, i => i] => i"
paulson@13780
    69
  Pi    :: "[i, i => i] => i"
clasohm@0
    70
paulson@14076
    71
text {*Relations and Functions *}
paulson@14076
    72
consts
paulson@14076
    73
  "domain"    :: "i => i"
paulson@13144
    74
  range       :: "i => i"
paulson@13144
    75
  field       :: "i => i"
paulson@13144
    76
  converse    :: "i => i"
paulson@14076
    77
  relation    :: "i => o"        --{*recognizes sets of pairs*}
paulson@14076
    78
  function    :: "i => o"        --{*recognizes functions; can have non-pairs*}
paulson@13144
    79
  Lambda      :: "[i, i => i] => i"
paulson@13144
    80
  restrict    :: "[i, i] => i"
clasohm@0
    81
paulson@14076
    82
text {*Infixes in order of decreasing precedence *}
paulson@14076
    83
consts
clasohm@0
    84
paulson@14076
    85
  "``"        :: "[i, i] => i"    (infixl 90) --{*image*}
paulson@14076
    86
  "-``"       :: "[i, i] => i"    (infixl 90) --{*inverse image*}
paulson@14076
    87
  "`"         :: "[i, i] => i"    (infixl 90) --{*function application*}
paulson@13780
    88
(*"*"         :: "[i, i] => i"    (infixr 80) [virtual] Cartesian product*)
paulson@14076
    89
  "Int"       :: "[i, i] => i"    (infixl 70) --{*binary intersection*}
paulson@14076
    90
  "Un"        :: "[i, i] => i"    (infixl 65) --{*binary union*}
paulson@14076
    91
  "-"         :: "[i, i] => i"    (infixl 65) --{*set difference*}
paulson@13780
    92
(*"->"        :: "[i, i] => i"    (infixr 60) [virtual] function spac\<epsilon>*)
paulson@14076
    93
  "<="        :: "[i, i] => o"    (infixl 50) --{*subset relation*}
paulson@14076
    94
  ":"         :: "[i, i] => o"    (infixl 50) --{*membership relation*}
paulson@13144
    95
(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
clasohm@0
    96
clasohm@0
    97
paulson@13780
    98
nonterminals "is" patterns
wenzelm@615
    99
wenzelm@615
   100
syntax
paulson@13144
   101
  ""          :: "i => is"                   ("_")
paulson@13144
   102
  "@Enum"     :: "[i, is] => is"             ("_,/ _")
paulson@13144
   103
  "~:"        :: "[i, i] => o"               (infixl 50)
paulson@13144
   104
  "@Finset"   :: "is => i"                   ("{(_)}")
paulson@13144
   105
  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
paulson@13144
   106
  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
paulson@13144
   107
  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
paulson@13144
   108
  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
paulson@13144
   109
  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
paulson@13144
   110
  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
paulson@13144
   111
  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
paulson@13144
   112
  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
paulson@13144
   113
  "->"        :: "[i, i] => i"               (infixr 60)
paulson@13144
   114
  "*"         :: "[i, i] => i"               (infixr 80)
paulson@13144
   115
  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
paulson@13144
   116
  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
paulson@13144
   117
  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
lcp@1106
   118
lcp@1106
   119
  (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
lcp@1106
   120
paulson@13144
   121
  "@pattern"  :: "patterns => pttrn"         ("<_>")
paulson@13144
   122
  ""          :: "pttrn => patterns"         ("_")
paulson@13144
   123
  "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
wenzelm@615
   124
clasohm@0
   125
translations
wenzelm@615
   126
  "x ~: y"      == "~ (x : y)"
clasohm@0
   127
  "{x, xs}"     == "cons(x, {xs})"
clasohm@0
   128
  "{x}"         == "cons(x, 0)"
clasohm@0
   129
  "{x:A. P}"    == "Collect(A, %x. P)"
clasohm@0
   130
  "{y. x:A, Q}" == "Replace(A, %x y. Q)"
wenzelm@615
   131
  "{b. x:A}"    == "RepFun(A, %x. b)"
clasohm@0
   132
  "INT x:A. B"  == "Inter({B. x:A})"
clasohm@0
   133
  "UN x:A. B"   == "Union({B. x:A})"
clasohm@0
   134
  "PROD x:A. B" => "Pi(A, %x. B)"
clasohm@0
   135
  "SUM x:A. B"  => "Sigma(A, %x. B)"
wenzelm@17782
   136
  "A -> B"      => "Pi(A, %_. B)"
wenzelm@17782
   137
  "A * B"       => "Sigma(A, %_. B)"
clasohm@0
   138
  "lam x:A. f"  == "Lambda(A, %x. f)"
clasohm@0
   139
  "ALL x:A. P"  == "Ball(A, %x. P)"
clasohm@0
   140
  "EX x:A. P"   == "Bex(A, %x. P)"
lcp@37
   141
lcp@1106
   142
  "<x, y, z>"   == "<x, <y, z>>"
lcp@1106
   143
  "<x, y>"      == "Pair(x, y)"
wenzelm@2286
   144
  "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
wenzelm@3840
   145
  "%<x,y>.b"    == "split(%x y. b)"
wenzelm@2286
   146
clasohm@0
   147
wenzelm@12114
   148
syntax (xsymbols)
paulson@13780
   149
  "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
paulson@13780
   150
  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
paulson@13780
   151
  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
paulson@13780
   152
  "op ->"     :: "[i, i] => i"               (infixr "\<rightarrow>" 60)
paulson@13780
   153
  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
paulson@13780
   154
  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
paulson@13780
   155
  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
paulson@13780
   156
  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
paulson@13780
   157
  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
paulson@13780
   158
  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
paulson@13780
   159
  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
paulson@13780
   160
  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
paulson@13780
   161
  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
paulson@13780
   162
  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
paulson@13780
   163
  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
paulson@13780
   164
  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
paulson@13780
   165
  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
paulson@13780
   166
  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
paulson@13780
   167
  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
paulson@13780
   168
  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
paulson@13780
   169
  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
wenzelm@2540
   170
wenzelm@6340
   171
syntax (HTML output)
paulson@13780
   172
  "op *"      :: "[i, i] => i"               (infixr "\<times>" 80)
kleing@14565
   173
  "op Int"    :: "[i, i] => i"    	     (infixl "\<inter>" 70)
kleing@14565
   174
  "op Un"     :: "[i, i] => i"    	     (infixl "\<union>" 65)
kleing@14565
   175
  "op <="     :: "[i, i] => o"    	     (infixl "\<subseteq>" 50)
kleing@14565
   176
  "op :"      :: "[i, i] => o"    	     (infixl "\<in>" 50)
kleing@14565
   177
  "op ~:"     :: "[i, i] => o"               (infixl "\<notin>" 50)
kleing@14565
   178
  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
kleing@14565
   179
  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
kleing@14565
   180
  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
kleing@14565
   181
  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
kleing@14565
   182
  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
kleing@14565
   183
  Union       :: "i =>i"                     ("\<Union>_" [90] 90)
kleing@14565
   184
  Inter       :: "i =>i"                     ("\<Inter>_" [90] 90)
kleing@14565
   185
  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
kleing@14565
   186
  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
kleing@14565
   187
  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
kleing@14565
   188
  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
kleing@14565
   189
  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
kleing@14565
   190
  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
kleing@14565
   191
  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
wenzelm@6340
   192
wenzelm@2540
   193
paulson@14227
   194
finalconsts
paulson@14227
   195
  0 Pow Inf Union PrimReplace 
paulson@14227
   196
  "op :"
paulson@14227
   197
paulson@13780
   198
defs 
paulson@13780
   199
(*don't try to use constdefs: the declaration order is tightly constrained*)
clasohm@0
   200
wenzelm@615
   201
  (* Bounded Quantifiers *)
paulson@14227
   202
  Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
paulson@14227
   203
  Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"
lcp@690
   204
paulson@14227
   205
  subset_def:    "A <= B == \<forall>x\<in>A. x\<in>B"
lcp@690
   206
wenzelm@3906
   207
wenzelm@3940
   208
local
wenzelm@3906
   209
paulson@13780
   210
axioms
clasohm@0
   211
wenzelm@615
   212
  (* ZF axioms -- see Suppes p.238
wenzelm@615
   213
     Axioms for Union, Pow and Replace state existence only,
wenzelm@615
   214
     uniqueness is derivable using extensionality. *)
clasohm@0
   215
paulson@13780
   216
  extension:     "A = B <-> A <= B & B <= A"
paulson@14227
   217
  Union_iff:     "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
paulson@14227
   218
  Pow_iff:       "A \<in> Pow(B) <-> A <= B"
clasohm@0
   219
wenzelm@615
   220
  (*We may name this set, though it is not uniquely defined.*)
paulson@14227
   221
  infinity:      "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
clasohm@0
   222
wenzelm@615
   223
  (*This formulation facilitates case analysis on A.*)
paulson@14227
   224
  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
clasohm@0
   225
wenzelm@615
   226
  (*Schema axiom since predicate P is a higher-order variable*)
paulson@14227
   227
  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
paulson@14227
   228
                         b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))"
wenzelm@615
   229
paulson@14883
   230
lcp@690
   231
defs
lcp@690
   232
wenzelm@615
   233
  (* Derived form of replacement, restricting P to its functional part.
wenzelm@615
   234
     The resulting set (for functional P) is the same as with
wenzelm@615
   235
     PrimReplace, but the rules are simpler. *)
clasohm@0
   236
paulson@13780
   237
  Replace_def:  "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
wenzelm@615
   238
wenzelm@615
   239
  (* Functional form of replacement -- analgous to ML's map functional *)
clasohm@0
   240
paulson@14227
   241
  RepFun_def:   "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
clasohm@0
   242
wenzelm@615
   243
  (* Separation and Pairing can be derived from the Replacement
wenzelm@615
   244
     and Powerset Axioms using the following definitions. *)
clasohm@0
   245
paulson@14227
   246
  Collect_def:  "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
clasohm@0
   247
wenzelm@615
   248
  (*Unordered pairs (Upair) express binary union/intersection and cons;
wenzelm@615
   249
    set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
clasohm@0
   250
paulson@14227
   251
  Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
paulson@13780
   252
  cons_def:  "cons(a,A) == Upair(a,a) Un A"
paulson@13780
   253
  succ_def:  "succ(i) == cons(i, i)"
wenzelm@615
   254
paulson@2872
   255
  (* Difference, general intersection, binary union and small intersection *)
paulson@2872
   256
paulson@14227
   257
  Diff_def:      "A - B    == { x\<in>A . ~(x\<in>B) }"
paulson@14227
   258
  Inter_def:     "Inter(A) == { x\<in>Union(A) . \<forall>y\<in>A. x\<in>y}"
paulson@13780
   259
  Un_def:        "A Un  B  == Union(Upair(A,B))"
paulson@13780
   260
  Int_def:      "A Int B  == Inter(Upair(A,B))"
paulson@2872
   261
paulson@14883
   262
  (* definite descriptions *)
paulson@14227
   263
  the_def:      "The(P)    == Union({y . x \<in> {0}, P(y)})"
paulson@13780
   264
  if_def:       "if(P,a,b) == THE z. P & z=a | ~P & z=b"
clasohm@0
   265
wenzelm@615
   266
  (* this "symmetric" definition works better than {{a}, {a,b}} *)
paulson@13780
   267
  Pair_def:     "<a,b>  == {{a,a}, {a,b}}"
paulson@14227
   268
  fst_def:      "fst(p) == THE a. \<exists>b. p=<a,b>"
paulson@14227
   269
  snd_def:      "snd(p) == THE b. \<exists>a. p=<a,b>"
paulson@13780
   270
  split_def:    "split(c) == %p. c(fst(p), snd(p))"
paulson@14227
   271
  Sigma_def:    "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}"
clasohm@0
   272
wenzelm@615
   273
  (* Operations on relations *)
clasohm@0
   274
wenzelm@615
   275
  (*converse of relation r, inverse of function*)
paulson@14227
   276
  converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}"
clasohm@0
   277
paulson@14227
   278
  domain_def:   "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}"
paulson@13780
   279
  range_def:    "range(r) == domain(converse(r))"
paulson@13780
   280
  field_def:    "field(r) == domain(r) Un range(r)"
paulson@14227
   281
  relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>"
paulson@13780
   282
  function_def: "function(r) ==
paulson@14227
   283
		    \<forall>x y. <x,y>:r --> (\<forall>y'. <x,y'>:r --> y=y')"
paulson@14227
   284
  image_def:    "r `` A  == {y : range(r) . \<exists>x\<in>A. <x,y> : r}"
paulson@13780
   285
  vimage_def:   "r -`` A == converse(r)``A"
clasohm@0
   286
wenzelm@615
   287
  (* Abstraction, application and Cartesian product of a family of sets *)
clasohm@0
   288
paulson@14227
   289
  lam_def:      "Lambda(A,b) == {<x,b(x)> . x\<in>A}"
paulson@13780
   290
  apply_def:    "f`a == Union(f``{a})"
paulson@14227
   291
  Pi_def:       "Pi(A,B)  == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
clasohm@0
   292
paulson@12891
   293
  (* Restrict the relation r to the domain A *)
paulson@14227
   294
  restrict_def: "restrict(r,A) == {z : r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
paulson@13780
   295
paulson@13780
   296
(* Pattern-matching and 'Dependent' type operators *)
paulson@13780
   297
paulson@13780
   298
print_translation {*
paulson@13780
   299
  [("Pi",    dependent_tr' ("@PROD", "op ->")),
paulson@13780
   300
   ("Sigma", dependent_tr' ("@SUM", "op *"))];
paulson@13780
   301
*}
paulson@13780
   302
paulson@13780
   303
subsection {* Substitution*}
paulson@13780
   304
paulson@13780
   305
(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
paulson@14227
   306
lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
paulson@13780
   307
by (erule ssubst, assumption)
paulson@13780
   308
paulson@13780
   309
paulson@13780
   310
subsection{*Bounded universal quantifier*}
paulson@13780
   311
paulson@14227
   312
lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
paulson@13780
   313
by (simp add: Ball_def)
paulson@13780
   314
paulson@15481
   315
lemmas strip = impI allI ballI
paulson@15481
   316
paulson@14227
   317
lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
paulson@13780
   318
by (simp add: Ball_def)
paulson@13780
   319
paulson@13780
   320
(*Instantiates x first: better for automatic theorem proving?*)
paulson@13780
   321
lemma rev_ballE [elim]: 
paulson@14227
   322
    "[| \<forall>x\<in>A. P(x);  x~:A ==> Q;  P(x) ==> Q |] ==> Q"
paulson@13780
   323
by (simp add: Ball_def, blast) 
paulson@13780
   324
paulson@14227
   325
lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q"
paulson@13780
   326
by blast
paulson@13780
   327
paulson@13780
   328
(*Used in the datatype package*)
paulson@14227
   329
lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
paulson@13780
   330
by (simp add: Ball_def)
paulson@13780
   331
paulson@14227
   332
(*Trival rewrite rule;   (\<forall>x\<in>A.P)<->P holds only if A is nonempty!*)
paulson@14227
   333
lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) --> P)"
paulson@13780
   334
by (simp add: Ball_def)
paulson@13780
   335
paulson@13780
   336
(*Congruence rule for rewriting*)
paulson@13780
   337
lemma ball_cong [cong]:
paulson@14227
   338
    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
paulson@13780
   339
by (simp add: Ball_def)
paulson@13780
   340
wenzelm@18845
   341
lemma atomize_ball:
wenzelm@18845
   342
    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
wenzelm@18845
   343
  by (simp only: Ball_def atomize_all atomize_imp)
wenzelm@18845
   344
wenzelm@18845
   345
lemmas [symmetric, rulify] = atomize_ball
wenzelm@18845
   346
  and [symmetric, defn] = atomize_ball
wenzelm@18845
   347
paulson@13780
   348
paulson@13780
   349
subsection{*Bounded existential quantifier*}
paulson@13780
   350
paulson@14227
   351
lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
paulson@13780
   352
by (simp add: Bex_def, blast)
paulson@13780
   353
paulson@14227
   354
(*The best argument order when there is only one x\<in>A*)
paulson@14227
   355
lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
paulson@13780
   356
by blast
paulson@13780
   357
paulson@14227
   358
(*Not of the general form for such rules; ~\<exists>has become ALL~ *)
paulson@14227
   359
lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
paulson@13780
   360
by blast
paulson@13780
   361
paulson@14227
   362
lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
paulson@13780
   363
by (simp add: Bex_def, blast)
paulson@13780
   364
paulson@14227
   365
(*We do not even have (\<exists>x\<in>A. True) <-> True unless A is nonempty!!*)
paulson@14227
   366
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
paulson@13780
   367
by (simp add: Bex_def)
paulson@13780
   368
paulson@13780
   369
lemma bex_cong [cong]:
paulson@14227
   370
    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] 
paulson@14227
   371
     ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
paulson@13780
   372
by (simp add: Bex_def cong: conj_cong)
paulson@13780
   373
paulson@13780
   374
paulson@13780
   375
paulson@13780
   376
subsection{*Rules for subsets*}
paulson@13780
   377
paulson@13780
   378
lemma subsetI [intro!]:
paulson@14227
   379
    "(!!x. x\<in>A ==> x\<in>B) ==> A <= B"
paulson@13780
   380
by (simp add: subset_def) 
paulson@13780
   381
paulson@13780
   382
(*Rule in Modus Ponens style [was called subsetE] *)
paulson@14227
   383
lemma subsetD [elim]: "[| A <= B;  c\<in>A |] ==> c\<in>B"
paulson@13780
   384
apply (unfold subset_def)
paulson@13780
   385
apply (erule bspec, assumption)
paulson@13780
   386
done
paulson@13780
   387
paulson@13780
   388
(*Classical elimination rule*)
paulson@13780
   389
lemma subsetCE [elim]:
paulson@14227
   390
    "[| A <= B;  c~:A ==> P;  c\<in>B ==> P |] ==> P"
paulson@13780
   391
by (simp add: subset_def, blast) 
paulson@13780
   392
paulson@13780
   393
(*Sometimes useful with premises in this order*)
paulson@14227
   394
lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
paulson@13780
   395
by blast
paulson@13780
   396
paulson@13780
   397
lemma contra_subsetD: "[| A <= B; c ~: B |] ==> c ~: A"
paulson@13780
   398
by blast
paulson@13780
   399
paulson@13780
   400
lemma rev_contra_subsetD: "[| c ~: B;  A <= B |] ==> c ~: A"
paulson@13780
   401
by blast
paulson@13780
   402
paulson@13780
   403
lemma subset_refl [simp]: "A <= A"
paulson@13780
   404
by blast
paulson@13780
   405
paulson@13780
   406
lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
paulson@13780
   407
by blast
paulson@13780
   408
paulson@13780
   409
(*Useful for proving A<=B by rewriting in some cases*)
paulson@13780
   410
lemma subset_iff: 
paulson@14227
   411
     "A<=B <-> (\<forall>x. x\<in>A --> x\<in>B)"
paulson@13780
   412
apply (unfold subset_def Ball_def)
paulson@13780
   413
apply (rule iff_refl)
paulson@13780
   414
done
paulson@13780
   415
paulson@13780
   416
paulson@13780
   417
subsection{*Rules for equality*}
paulson@13780
   418
paulson@13780
   419
(*Anti-symmetry of the subset relation*)
paulson@13780
   420
lemma equalityI [intro]: "[| A <= B;  B <= A |] ==> A = B"
paulson@13780
   421
by (rule extension [THEN iffD2], rule conjI) 
paulson@13780
   422
paulson@13780
   423
paulson@14227
   424
lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
paulson@13780
   425
by (rule equalityI, blast+)
paulson@13780
   426
paulson@13780
   427
lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard]
paulson@13780
   428
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard]
paulson@13780
   429
paulson@13780
   430
lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
paulson@13780
   431
by (blast dest: equalityD1 equalityD2) 
paulson@13780
   432
paulson@13780
   433
lemma equalityCE:
paulson@14227
   434
    "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P"
paulson@13780
   435
by (erule equalityE, blast) 
paulson@13780
   436
paulson@13780
   437
paulson@13780
   438
subsection{*Rules for Replace -- the derived form of replacement*}
paulson@13780
   439
paulson@13780
   440
lemma Replace_iff: 
paulson@14227
   441
    "b : {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) --> y=b))"
paulson@13780
   442
apply (unfold Replace_def)
paulson@13780
   443
apply (rule replacement [THEN iff_trans], blast+)
paulson@13780
   444
done
paulson@13780
   445
paulson@13780
   446
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
paulson@13780
   447
lemma ReplaceI [intro]: 
paulson@13780
   448
    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>  
paulson@14227
   449
     b : {y. x\<in>A, P(x,y)}"
paulson@13780
   450
by (rule Replace_iff [THEN iffD2], blast) 
paulson@13780
   451
paulson@13780
   452
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
paulson@13780
   453
lemma ReplaceE: 
paulson@14227
   454
    "[| b : {y. x\<in>A, P(x,y)};   
paulson@14227
   455
        !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)-->y=b |] ==> R  
paulson@13780
   456
     |] ==> R"
paulson@13780
   457
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
paulson@13780
   458
paulson@13780
   459
(*As above but without the (generally useless) 3rd assumption*)
paulson@13780
   460
lemma ReplaceE2 [elim!]: 
paulson@14227
   461
    "[| b : {y. x\<in>A, P(x,y)};   
paulson@13780
   462
        !!x. [| x: A;  P(x,b) |] ==> R  
paulson@13780
   463
     |] ==> R"
paulson@13780
   464
by (erule ReplaceE, blast) 
paulson@13780
   465
paulson@13780
   466
lemma Replace_cong [cong]:
paulson@14227
   467
    "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>  
paulson@13780
   468
     Replace(A,P) = Replace(B,Q)"
paulson@13780
   469
apply (rule equality_iffI) 
paulson@13780
   470
apply (simp add: Replace_iff) 
paulson@13780
   471
done
paulson@13780
   472
paulson@13780
   473
paulson@13780
   474
subsection{*Rules for RepFun*}
paulson@13780
   475
paulson@14227
   476
lemma RepFunI: "a \<in> A ==> f(a) : {f(x). x\<in>A}"
paulson@13780
   477
by (simp add: RepFun_def Replace_iff, blast)
paulson@13780
   478
paulson@13780
   479
(*Useful for coinduction proofs*)
paulson@14227
   480
lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b : {f(x). x\<in>A}"
paulson@13780
   481
apply (erule ssubst)
paulson@13780
   482
apply (erule RepFunI)
paulson@13780
   483
done
paulson@13780
   484
paulson@13780
   485
lemma RepFunE [elim!]:
paulson@14227
   486
    "[| b : {f(x). x\<in>A};   
paulson@14227
   487
        !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>  
paulson@13780
   488
     P"
paulson@13780
   489
by (simp add: RepFun_def Replace_iff, blast) 
paulson@13780
   490
paulson@13780
   491
lemma RepFun_cong [cong]: 
paulson@14227
   492
    "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
paulson@13780
   493
by (simp add: RepFun_def)
paulson@13780
   494
paulson@14227
   495
lemma RepFun_iff [simp]: "b : {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
paulson@13780
   496
by (unfold Bex_def, blast)
paulson@13780
   497
paulson@14227
   498
lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
paulson@13780
   499
by blast
paulson@13780
   500
paulson@13780
   501
paulson@13780
   502
subsection{*Rules for Collect -- forming a subset by separation*}
paulson@13780
   503
paulson@13780
   504
(*Separation is derivable from Replacement*)
paulson@14227
   505
lemma separation [simp]: "a : {x\<in>A. P(x)} <-> a\<in>A & P(a)"
paulson@13780
   506
by (unfold Collect_def, blast)
paulson@13780
   507
paulson@14227
   508
lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a : {x\<in>A. P(x)}"
paulson@13780
   509
by simp
paulson@13780
   510
paulson@14227
   511
lemma CollectE [elim!]: "[| a : {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
paulson@13780
   512
by simp
paulson@13780
   513
paulson@14227
   514
lemma CollectD1: "a : {x\<in>A. P(x)} ==> a\<in>A"
paulson@13780
   515
by (erule CollectE, assumption)
paulson@13780
   516
paulson@14227
   517
lemma CollectD2: "a : {x\<in>A. P(x)} ==> P(a)"
paulson@13780
   518
by (erule CollectE, assumption)
paulson@13780
   519
paulson@13780
   520
lemma Collect_cong [cong]:
paulson@14227
   521
    "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]  
paulson@13780
   522
     ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
paulson@13780
   523
by (simp add: Collect_def)
paulson@13780
   524
paulson@13780
   525
paulson@13780
   526
subsection{*Rules for Unions*}
paulson@13780
   527
paulson@13780
   528
declare Union_iff [simp]
paulson@13780
   529
paulson@13780
   530
(*The order of the premises presupposes that C is rigid; A may be flexible*)
paulson@13780
   531
lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: Union(C)"
paulson@13780
   532
by (simp, blast)
paulson@13780
   533
paulson@14227
   534
lemma UnionE [elim!]: "[| A \<in> Union(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
paulson@13780
   535
by (simp, blast)
paulson@13780
   536
paulson@13780
   537
paulson@13780
   538
subsection{*Rules for Unions of families*}
paulson@14227
   539
(* \<Union>x\<in>A. B(x) abbreviates Union({B(x). x\<in>A}) *)
paulson@13780
   540
paulson@14227
   541
lemma UN_iff [simp]: "b : (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
paulson@13780
   542
by (simp add: Bex_def, blast)
paulson@13780
   543
paulson@13780
   544
(*The order of the premises presupposes that A is rigid; b may be flexible*)
paulson@14227
   545
lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
paulson@13780
   546
by (simp, blast)
paulson@13780
   547
paulson@13780
   548
paulson@13780
   549
lemma UN_E [elim!]: 
paulson@14227
   550
    "[| b : (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
paulson@13780
   551
by blast 
paulson@13780
   552
paulson@13780
   553
lemma UN_cong: 
paulson@14227
   554
    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
paulson@13780
   555
by simp 
paulson@13780
   556
paulson@13780
   557
paulson@14227
   558
(*No "Addcongs [UN_cong]" because \<Union>is a combination of constants*)
paulson@13780
   559
paulson@13780
   560
(* UN_E appears before UnionE so that it is tried first, to avoid expensive
paulson@13780
   561
  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
paulson@13780
   562
  the search space.*)
paulson@13780
   563
paulson@13780
   564
paulson@13780
   565
subsection{*Rules for the empty set*}
paulson@13780
   566
paulson@14227
   567
(*The set {x\<in>0. False} is empty; by foundation it equals 0 
paulson@13780
   568
  See Suppes, page 21.*)
paulson@13780
   569
lemma not_mem_empty [simp]: "a ~: 0"
paulson@13780
   570
apply (cut_tac foundation)
paulson@13780
   571
apply (best dest: equalityD2)
paulson@13780
   572
done
paulson@13780
   573
paulson@13780
   574
lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard]
paulson@13780
   575
paulson@13780
   576
paulson@13780
   577
lemma empty_subsetI [simp]: "0 <= A"
paulson@13780
   578
by blast 
paulson@13780
   579
paulson@14227
   580
lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
paulson@13780
   581
by blast
paulson@13780
   582
paulson@13780
   583
lemma equals0D [dest]: "A=0 ==> a ~: A"
paulson@13780
   584
by blast
paulson@13780
   585
paulson@13780
   586
declare sym [THEN equals0D, dest]
paulson@13780
   587
paulson@14227
   588
lemma not_emptyI: "a\<in>A ==> A ~= 0"
paulson@13780
   589
by blast
paulson@13780
   590
paulson@14227
   591
lemma not_emptyE:  "[| A ~= 0;  !!x. x\<in>A ==> R |] ==> R"
paulson@13780
   592
by blast
paulson@13780
   593
paulson@13780
   594
paulson@14095
   595
subsection{*Rules for Inter*}
paulson@14095
   596
paulson@14095
   597
(*Not obviously useful for proving InterI, InterD, InterE*)
paulson@14227
   598
lemma Inter_iff: "A \<in> Inter(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
paulson@14095
   599
by (simp add: Inter_def Ball_def, blast)
paulson@14095
   600
paulson@14095
   601
(* Intersection is well-behaved only if the family is non-empty! *)
paulson@14095
   602
lemma InterI [intro!]: 
paulson@14227
   603
    "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> Inter(C)"
paulson@14095
   604
by (simp add: Inter_iff)
paulson@14095
   605
paulson@14095
   606
(*A "destruct" rule -- every B in C contains A as an element, but
paulson@14227
   607
  A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
paulson@14227
   608
lemma InterD [elim]: "[| A \<in> Inter(C);  B \<in> C |] ==> A \<in> B"
paulson@14095
   609
by (unfold Inter_def, blast)
paulson@14095
   610
paulson@14227
   611
(*"Classical" elimination rule -- does not require exhibiting B\<in>C *)
paulson@14095
   612
lemma InterE [elim]: 
paulson@14227
   613
    "[| A \<in> Inter(C);  B~:C ==> R;  A\<in>B ==> R |] ==> R"
paulson@14095
   614
by (simp add: Inter_def, blast) 
paulson@14095
   615
  
paulson@14095
   616
paulson@14095
   617
subsection{*Rules for Intersections of families*}
paulson@14095
   618
paulson@14227
   619
(* \<Inter>x\<in>A. B(x) abbreviates Inter({B(x). x\<in>A}) *)
paulson@14095
   620
paulson@14227
   621
lemma INT_iff: "b : (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
paulson@14095
   622
by (force simp add: Inter_def)
paulson@14095
   623
paulson@14227
   624
lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
paulson@14095
   625
by blast
paulson@14095
   626
paulson@14227
   627
lemma INT_E: "[| b : (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
paulson@14095
   628
by blast
paulson@14095
   629
paulson@14095
   630
lemma INT_cong:
paulson@14227
   631
    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
paulson@14095
   632
by simp
paulson@14095
   633
paulson@14227
   634
(*No "Addcongs [INT_cong]" because \<Inter>is a combination of constants*)
paulson@14095
   635
paulson@14095
   636
paulson@13780
   637
subsection{*Rules for Powersets*}
paulson@13780
   638
paulson@14227
   639
lemma PowI: "A <= B ==> A \<in> Pow(B)"
paulson@13780
   640
by (erule Pow_iff [THEN iffD2])
paulson@13780
   641
paulson@14227
   642
lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
paulson@13780
   643
by (erule Pow_iff [THEN iffD1])
paulson@13780
   644
paulson@13780
   645
declare Pow_iff [iff]
paulson@13780
   646
paulson@14227
   647
lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 \<in> Pow(B) *)
paulson@14227
   648
lemmas Pow_top = subset_refl [THEN PowI] (* A \<in> Pow(A) *)
paulson@13780
   649
paulson@13780
   650
paulson@13780
   651
subsection{*Cantor's Theorem: There is no surjection from a set to its powerset.*}
paulson@13780
   652
paulson@13780
   653
(*The search is undirected.  Allowing redundant introduction rules may 
paulson@13780
   654
  make it diverge.  Variable b represents ANY map, such as
paulson@14227
   655
  (lam x\<in>A.b(x)): A->Pow(A). *)
paulson@14227
   656
lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) ~= S"
paulson@13780
   657
by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
paulson@13780
   658
paulson@13780
   659
ML
paulson@13780
   660
{*
paulson@13780
   661
val lam_def = thm "lam_def";
paulson@13780
   662
val domain_def = thm "domain_def";
paulson@13780
   663
val range_def = thm "range_def";
paulson@13780
   664
val image_def = thm "image_def";
paulson@13780
   665
val vimage_def = thm "vimage_def";
paulson@13780
   666
val field_def = thm "field_def";
paulson@13780
   667
val Inter_def = thm "Inter_def";
paulson@13780
   668
val Ball_def = thm "Ball_def";
paulson@13780
   669
val Bex_def = thm "Bex_def";
paulson@13780
   670
paulson@13780
   671
val ballI = thm "ballI";
paulson@13780
   672
val bspec = thm "bspec";
paulson@13780
   673
val rev_ballE = thm "rev_ballE";
paulson@13780
   674
val ballE = thm "ballE";
paulson@13780
   675
val rev_bspec = thm "rev_bspec";
paulson@13780
   676
val ball_triv = thm "ball_triv";
paulson@13780
   677
val ball_cong = thm "ball_cong";
paulson@13780
   678
val bexI = thm "bexI";
paulson@13780
   679
val rev_bexI = thm "rev_bexI";
paulson@13780
   680
val bexCI = thm "bexCI";
paulson@13780
   681
val bexE = thm "bexE";
paulson@13780
   682
val bex_triv = thm "bex_triv";
paulson@13780
   683
val bex_cong = thm "bex_cong";
paulson@13780
   684
val subst_elem = thm "subst_elem";
paulson@13780
   685
val subsetI = thm "subsetI";
paulson@13780
   686
val subsetD = thm "subsetD";
paulson@13780
   687
val subsetCE = thm "subsetCE";
paulson@13780
   688
val rev_subsetD = thm "rev_subsetD";
paulson@13780
   689
val contra_subsetD = thm "contra_subsetD";
paulson@13780
   690
val rev_contra_subsetD = thm "rev_contra_subsetD";
paulson@13780
   691
val subset_refl = thm "subset_refl";
paulson@13780
   692
val subset_trans = thm "subset_trans";
paulson@13780
   693
val subset_iff = thm "subset_iff";
paulson@13780
   694
val equalityI = thm "equalityI";
paulson@13780
   695
val equality_iffI = thm "equality_iffI";
paulson@13780
   696
val equalityD1 = thm "equalityD1";
paulson@13780
   697
val equalityD2 = thm "equalityD2";
paulson@13780
   698
val equalityE = thm "equalityE";
paulson@13780
   699
val equalityCE = thm "equalityCE";
paulson@13780
   700
val Replace_iff = thm "Replace_iff";
paulson@13780
   701
val ReplaceI = thm "ReplaceI";
paulson@13780
   702
val ReplaceE = thm "ReplaceE";
paulson@13780
   703
val ReplaceE2 = thm "ReplaceE2";
paulson@13780
   704
val Replace_cong = thm "Replace_cong";
paulson@13780
   705
val RepFunI = thm "RepFunI";
paulson@13780
   706
val RepFun_eqI = thm "RepFun_eqI";
paulson@13780
   707
val RepFunE = thm "RepFunE";
paulson@13780
   708
val RepFun_cong = thm "RepFun_cong";
paulson@13780
   709
val RepFun_iff = thm "RepFun_iff";
paulson@13780
   710
val triv_RepFun = thm "triv_RepFun";
paulson@13780
   711
val separation = thm "separation";
paulson@13780
   712
val CollectI = thm "CollectI";
paulson@13780
   713
val CollectE = thm "CollectE";
paulson@13780
   714
val CollectD1 = thm "CollectD1";
paulson@13780
   715
val CollectD2 = thm "CollectD2";
paulson@13780
   716
val Collect_cong = thm "Collect_cong";
paulson@13780
   717
val UnionI = thm "UnionI";
paulson@13780
   718
val UnionE = thm "UnionE";
paulson@13780
   719
val UN_iff = thm "UN_iff";
paulson@13780
   720
val UN_I = thm "UN_I";
paulson@13780
   721
val UN_E = thm "UN_E";
paulson@13780
   722
val UN_cong = thm "UN_cong";
paulson@13780
   723
val Inter_iff = thm "Inter_iff";
paulson@13780
   724
val InterI = thm "InterI";
paulson@13780
   725
val InterD = thm "InterD";
paulson@13780
   726
val InterE = thm "InterE";
paulson@13780
   727
val INT_iff = thm "INT_iff";
paulson@13780
   728
val INT_I = thm "INT_I";
paulson@13780
   729
val INT_E = thm "INT_E";
paulson@13780
   730
val INT_cong = thm "INT_cong";
paulson@13780
   731
val PowI = thm "PowI";
paulson@13780
   732
val PowD = thm "PowD";
paulson@13780
   733
val Pow_bottom = thm "Pow_bottom";
paulson@13780
   734
val Pow_top = thm "Pow_top";
paulson@13780
   735
val not_mem_empty = thm "not_mem_empty";
paulson@13780
   736
val emptyE = thm "emptyE";
paulson@13780
   737
val empty_subsetI = thm "empty_subsetI";
paulson@13780
   738
val equals0I = thm "equals0I";
paulson@13780
   739
val equals0D = thm "equals0D";
paulson@13780
   740
val not_emptyI = thm "not_emptyI";
paulson@13780
   741
val not_emptyE = thm "not_emptyE";
paulson@13780
   742
val cantor = thm "cantor";
paulson@13780
   743
*}
paulson@13780
   744
paulson@13780
   745
(*Functions for ML scripts*)
paulson@13780
   746
ML
paulson@13780
   747
{*
paulson@14227
   748
(*Converts A<=B to x\<in>A ==> x\<in>B*)
paulson@13780
   749
fun impOfSubs th = th RSN (2, rev_subsetD);
paulson@13780
   750
paulson@14227
   751
(*Takes assumptions \<forall>x\<in>A.P(x) and a\<in>A; creates assumption P(a)*)
paulson@13780
   752
val ball_tac = dtac bspec THEN' assume_tac
paulson@13780
   753
*}
clasohm@0
   754
clasohm@0
   755
end
clasohm@0
   756