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