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