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