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