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