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 6section \<open>Base of Zermelo-Fraenkel Set Theory\<close> 7 8theory ZF_Base 9imports FOL 10begin 11 12subsection \<open>Signature\<close> 13 14declare [[eta_contract = false]] 15 16typedecl i 17instance i :: "term" .. 18 19axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<in>\<close> 50) \<comment> \<open>membership relation\<close> 20 and zero :: "i" (\<open>0\<close>) \<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" (\<open>\<Union>_\<close> [90] 90) 24 and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" 25 26abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<notin>\<close> 50) \<comment> \<open>negated membership relation\<close> 27 where "x \<notin> y \<equiv> \<not> (x \<in> y)" 28 29 30subsection \<open>Bounded Quantifiers\<close> 31 32definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o" 33 where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)" 34 35definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o" 36 where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)" 37 38syntax 39 "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<forall>_\<in>_./ _)\<close> 10) 40 "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<exists>_\<in>_./ _)\<close> 10) 41translations 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 46subsection \<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. *) 51definition 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 54syntax 55 "_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _ \<in> _, _})\<close>) 56translations 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 62definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 63 where "RepFun(A,f) == {y . x\<in>A, y=f(x)}" 64 65syntax 66 "_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51]) 67translations 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. *) 73definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i" 74 where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" 75 76syntax 77 "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>) 78translations 79 "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)" 80 81 82subsection \<open>General union and intersection\<close> 83 84definition Inter :: "i => i" (\<open>\<Inter>_\<close> [90] 90) 85 where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" 86 87syntax 88 "_UNION" :: "[pttrn, i, i] => i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10) 89 "_INTER" :: "[pttrn, i, i] => i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10) 90translations 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 95subsection \<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 100definition 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 103definition Subset :: "[i, i] \<Rightarrow> o" (infixl \<open>\<subseteq>\<close> 50) \<comment> \<open>subset relation\<close> 104 where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B" 105 106definition Diff :: "[i, i] \<Rightarrow> i" (infixl \<open>-\<close> 65) \<comment> \<open>set difference\<close> 107 where "A - B == { x\<in>A . ~(x\<in>B) }" 108 109definition Un :: "[i, i] \<Rightarrow> i" (infixl \<open>\<union>\<close> 65) \<comment> \<open>binary union\<close> 110 where "A \<union> B == \<Union>(Upair(A,B))" 111 112definition Int :: "[i, i] \<Rightarrow> i" (infixl \<open>\<inter>\<close> 70) \<comment> \<open>binary intersection\<close> 113 where "A \<inter> B == \<Inter>(Upair(A,B))" 114 115definition cons :: "[i, i] => i" 116 where "cons(a,A) == Upair(a,a) \<union> A" 117 118definition succ :: "i => i" 119 where "succ(i) == cons(i, i)" 120 121nonterminal "is" 122syntax 123 "" :: "i \<Rightarrow> is" (\<open>_\<close>) 124 "_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>) 125 "_Finset" :: "is \<Rightarrow> i" (\<open>{(_)}\<close>) 126translations 127 "{x, xs}" == "CONST cons(x, {xs})" 128 "{x}" == "CONST cons(x, 0)" 129 130 131subsection \<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 137axiomatization 138where 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 154subsection \<open>Definite descriptions -- via Replace over the set "1"\<close> 155 156definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder \<open>THE \<close> 10) 157 where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" 158 159definition If :: "[o, i, i] \<Rightarrow> i" (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10) 160 where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b" 161 162abbreviation (input) 163 old_if :: "[o, i, i] => i" (\<open>if '(_,_,_')\<close>) 164 where "if(P,a,b) == If(P,a,b)" 165 166 167subsection \<open>Ordered Pairing\<close> 168 169(* this "symmetric" definition works better than {{a}, {a,b}} *) 170definition Pair :: "[i, i] => i" 171 where "Pair(a,b) == {{a,a}, {a,b}}" 172 173definition fst :: "i \<Rightarrow> i" 174 where "fst(p) == THE a. \<exists>b. p = Pair(a, b)" 175 176definition snd :: "i \<Rightarrow> i" 177 where "snd(p) == THE b. \<exists>a. p = Pair(a, b)" 178 179definition 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 *) 183nonterminal patterns 184syntax 185 "_pattern" :: "patterns => pttrn" (\<open>\<langle>_\<rangle>\<close>) 186 "" :: "pttrn => patterns" (\<open>_\<close>) 187 "_patterns" :: "[pttrn, patterns] => patterns" (\<open>_,/_\<close>) 188 "_Tuple" :: "[i, is] => i" (\<open>\<langle>(_,/ _)\<rangle>\<close>) 189translations 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 195definition 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 198abbreviation cart_prod :: "[i, i] => i" (infixr \<open>\<times>\<close> 80) \<comment> \<open>Cartesian product\<close> 199 where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)" 200 201 202subsection \<open>Relations and Functions\<close> 203 204(*converse of relation r, inverse of function*) 205definition 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 208definition domain :: "i \<Rightarrow> i" 209 where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}" 210 211definition range :: "i \<Rightarrow> i" 212 where "range(r) == domain(converse(r))" 213 214definition field :: "i \<Rightarrow> i" 215 where "field(r) == domain(r) \<union> range(r)" 216 217definition 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 220definition "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 223definition Image :: "[i, i] \<Rightarrow> i" (infixl \<open>``\<close> 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 226definition vimage :: "[i, i] \<Rightarrow> i" (infixl \<open>-``\<close> 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 *) 230definition 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 236definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i" 237 where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}" 238 239definition "apply" :: "[i, i] \<Rightarrow> i" (infixl \<open>`\<close> 90) \<comment> \<open>function application\<close> 240 where "f`a == \<Union>(f``{a})" 241 242definition 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 245abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr \<open>\<rightarrow>\<close> 60) \<comment> \<open>function space\<close> 246 where "A \<rightarrow> B \<equiv> Pi(A, \<lambda>_. B)" 247 248 249(* binder syntax *) 250 251syntax 252 "_PROD" :: "[pttrn, i, i] => i" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10) 253 "_SUM" :: "[pttrn, i, i] => i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10) 254 "_lam" :: "[pttrn, i, i] => i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 10) 255translations 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 261subsection \<open>ASCII syntax\<close> 262 263notation (ASCII) 264 cart_prod (infixr \<open>*\<close> 80) and 265 Int (infixl \<open>Int\<close> 70) and 266 Un (infixl \<open>Un\<close> 65) and 267 function_space (infixr \<open>->\<close> 60) and 268 Subset (infixl \<open><=\<close> 50) and 269 mem (infixl \<open>:\<close> 50) and 270 not_mem (infixl \<open>~:\<close> 50) 271 272syntax (ASCII) 273 "_Ball" :: "[pttrn, i, o] => o" (\<open>(3ALL _:_./ _)\<close> 10) 274 "_Bex" :: "[pttrn, i, o] => o" (\<open>(3EX _:_./ _)\<close> 10) 275 "_Collect" :: "[pttrn, i, o] => i" (\<open>(1{_: _ ./ _})\<close>) 276 "_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>) 277 "_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _: _})\<close> [51,0,51]) 278 "_UNION" :: "[pttrn, i, i] => i" (\<open>(3UN _:_./ _)\<close> 10) 279 "_INTER" :: "[pttrn, i, i] => i" (\<open>(3INT _:_./ _)\<close> 10) 280 "_PROD" :: "[pttrn, i, i] => i" (\<open>(3PROD _:_./ _)\<close> 10) 281 "_SUM" :: "[pttrn, i, i] => i" (\<open>(3SUM _:_./ _)\<close> 10) 282 "_lam" :: "[pttrn, i, i] => i" (\<open>(3lam _:_./ _)\<close> 10) 283 "_Tuple" :: "[i, is] => i" (\<open><(_,/ _)>\<close>) 284 "_pattern" :: "patterns => pttrn" (\<open><_>\<close>) 285 286 287subsection \<open>Substitution\<close> 288 289(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) 290lemma subst_elem: "[| b\<in>A; a=b |] ==> a\<in>A" 291by (erule ssubst, assumption) 292 293 294subsection\<open>Bounded universal quantifier\<close> 295 296lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)" 297by (simp add: Ball_def) 298 299lemmas strip = impI allI ballI 300 301lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x); x: A |] ==> P(x)" 302by (simp add: Ball_def) 303 304(*Instantiates x first: better for automatic theorem proving?*) 305lemma rev_ballE [elim]: 306 "[| \<forall>x\<in>A. P(x); x\<notin>A ==> Q; P(x) ==> Q |] ==> Q" 307by (simp add: Ball_def, blast) 308 309lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x\<notin>A ==> Q |] ==> Q" 310by blast 311 312(*Used in the datatype package*) 313lemma rev_bspec: "[| x: A; \<forall>x\<in>A. P(x) |] ==> P(x)" 314by (simp add: Ball_def) 315 316(*Trival rewrite rule; @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*) 317lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)" 318by (simp add: Ball_def) 319 320(*Congruence rule for rewriting*) 321lemma 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))" 323by (simp add: Ball_def) 324 325lemma 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 329lemmas [symmetric, rulify] = atomize_ball 330 and [symmetric, defn] = atomize_ball 331 332 333subsection\<open>Bounded existential quantifier\<close> 334 335lemma bexI [intro]: "[| P(x); x: A |] ==> \<exists>x\<in>A. P(x)" 336by (simp add: Bex_def, blast) 337 338(*The best argument order when there is only one @{term"x\<in>A"}*) 339lemma rev_bexI: "[| x\<in>A; P(x) |] ==> \<exists>x\<in>A. P(x)" 340by blast 341 342(*Not of the general form for such rules. The existential quanitifer becomes universal. *) 343lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a); a: A |] ==> \<exists>x\<in>A. P(x)" 344by blast 345 346lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x); !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q" 347by (simp add: Bex_def, blast) 348 349(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*) 350lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)" 351by (simp add: Bex_def) 352 353lemma 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))" 356by (simp add: Bex_def cong: conj_cong) 357 358 359 360subsection\<open>Rules for subsets\<close> 361 362lemma subsetI [intro!]: 363 "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B" 364by (simp add: subset_def) 365 366(*Rule in Modus Ponens style [was called subsetE] *) 367lemma subsetD [elim]: "[| A \<subseteq> B; c\<in>A |] ==> c\<in>B" 368apply (unfold subset_def) 369apply (erule bspec, assumption) 370done 371 372(*Classical elimination rule*) 373lemma subsetCE [elim]: 374 "[| A \<subseteq> B; c\<notin>A ==> P; c\<in>B ==> P |] ==> P" 375by (simp add: subset_def, blast) 376 377(*Sometimes useful with premises in this order*) 378lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B" 379by blast 380 381lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A" 382by blast 383 384lemma rev_contra_subsetD: "[| c \<notin> B; A \<subseteq> B |] ==> c \<notin> A" 385by blast 386 387lemma subset_refl [simp]: "A \<subseteq> A" 388by blast 389 390lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C" 391by blast 392 393(*Useful for proving A<=B by rewriting in some cases*) 394lemma subset_iff: 395 "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)" 396apply (unfold subset_def Ball_def) 397apply (rule iff_refl) 398done 399 400text\<open>For calculations\<close> 401declare subsetD [trans] rev_subsetD [trans] subset_trans [trans] 402 403 404subsection\<open>Rules for equality\<close> 405 406(*Anti-symmetry of the subset relation*) 407lemma equalityI [intro]: "[| A \<subseteq> B; B \<subseteq> A |] ==> A = B" 408by (rule extension [THEN iffD2], rule conjI) 409 410 411lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B" 412by (rule equalityI, blast+) 413 414lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1] 415lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2] 416 417lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P" 418by (blast dest: equalityD1 equalityD2) 419 420lemma equalityCE: 421 "[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c\<notin>A; c\<notin>B |] ==> P |] ==> P" 422by (erule equalityE, blast) 423 424lemma equality_iffD: 425 "A = B ==> (!!x. x \<in> A <-> x \<in> B)" 426 by auto 427 428 429subsection\<open>Rules for Replace -- the derived form of replacement\<close> 430 431lemma 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))" 433apply (unfold Replace_def) 434apply (rule replacement [THEN iff_trans], blast+) 435done 436 437(*Introduction; there must be a unique y such that P(x,y), namely y=b. *) 438lemma ReplaceI [intro]: 439 "[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==> 440 b \<in> {y. x\<in>A, P(x,y)}" 441by (rule Replace_iff [THEN iffD2], blast) 442 443(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *) 444lemma 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" 448by (rule Replace_iff [THEN iffD1, THEN bexE], simp+) 449 450(*As above but without the (generally useless) 3rd assumption*) 451lemma ReplaceE2 [elim!]: 452 "[| b \<in> {y. x\<in>A, P(x,y)}; 453 !!x. [| x: A; P(x,b) |] ==> R 454 |] ==> R" 455by (erule ReplaceE, blast) 456 457lemma Replace_cong [cong]: 458 "[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==> 459 Replace(A,P) = Replace(B,Q)" 460apply (rule equality_iffI) 461apply (simp add: Replace_iff) 462done 463 464 465subsection\<open>Rules for RepFun\<close> 466 467lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}" 468by (simp add: RepFun_def Replace_iff, blast) 469 470(*Useful for coinduction proofs*) 471lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b \<in> {f(x). x\<in>A}" 472apply (erule ssubst) 473apply (erule RepFunI) 474done 475 476lemma RepFunE [elim!]: 477 "[| b \<in> {f(x). x\<in>A}; 478 !!x.[| x\<in>A; b=f(x) |] ==> P |] ==> 479 P" 480by (simp add: RepFun_def Replace_iff, blast) 481 482lemma RepFun_cong [cong]: 483 "[| A=B; !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)" 484by (simp add: RepFun_def) 485 486lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))" 487by (unfold Bex_def, blast) 488 489lemma triv_RepFun [simp]: "{x. x\<in>A} = A" 490by blast 491 492 493subsection\<open>Rules for Collect -- forming a subset by separation\<close> 494 495(*Separation is derivable from Replacement*) 496lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)" 497by (unfold Collect_def, blast) 498 499lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a \<in> {x\<in>A. P(x)}" 500by simp 501 502lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R" 503by simp 504 505lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A" 506by (erule CollectE, assumption) 507 508lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)" 509by (erule CollectE, assumption) 510 511lemma 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))" 514by (simp add: Collect_def) 515 516 517subsection\<open>Rules for Unions\<close> 518 519declare Union_iff [simp] 520 521(*The order of the premises presupposes that C is rigid; A may be flexible*) 522lemma UnionI [intro]: "[| B: C; A: B |] ==> A: \<Union>(C)" 523by (simp, blast) 524 525lemma UnionE [elim!]: "[| A \<in> \<Union>(C); !!B.[| A: B; B: C |] ==> R |] ==> R" 526by (simp, blast) 527 528 529subsection\<open>Rules for Unions of families\<close> 530(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *) 531 532lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))" 533by (simp add: Bex_def, blast) 534 535(*The order of the premises presupposes that A is rigid; b may be flexible*) 536lemma UN_I: "[| a: A; b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))" 537by (simp, blast) 538 539 540lemma UN_E [elim!]: 541 "[| b \<in> (\<Union>x\<in>A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R" 542by blast 543 544lemma 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))" 546by 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 556subsection\<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.*) 560lemma not_mem_empty [simp]: "a \<notin> 0" 561apply (cut_tac foundation) 562apply (best dest: equalityD2) 563done 564 565lemmas emptyE [elim!] = not_mem_empty [THEN notE] 566 567 568lemma empty_subsetI [simp]: "0 \<subseteq> A" 569by blast 570 571lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0" 572by blast 573 574lemma equals0D [dest]: "A=0 ==> a \<notin> A" 575by blast 576 577declare sym [THEN equals0D, dest] 578 579lemma not_emptyI: "a\<in>A ==> A \<noteq> 0" 580by blast 581 582lemma not_emptyE: "[| A \<noteq> 0; !!x. x\<in>A ==> R |] ==> R" 583by blast 584 585 586subsection\<open>Rules for Inter\<close> 587 588(*Not obviously useful for proving InterI, InterD, InterE*) 589lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0" 590by (simp add: Inter_def Ball_def, blast) 591 592(* Intersection is well-behaved only if the family is non-empty! *) 593lemma InterI [intro!]: 594 "[| !!x. x: C ==> A: x; C\<noteq>0 |] ==> A \<in> \<Inter>(C)" 595by (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". *) 599lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C); B \<in> C |] ==> A \<in> B" 600by (unfold Inter_def, blast) 601 602(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *) 603lemma InterE [elim]: 604 "[| A \<in> \<Inter>(C); B\<notin>C ==> R; A\<in>B ==> R |] ==> R" 605by (simp add: Inter_def, blast) 606 607 608subsection\<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 612lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0" 613by (force simp add: Inter_def) 614 615lemma INT_I: "[| !!x. x: A ==> b: B(x); A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))" 616by blast 617 618lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x)); a: A |] ==> b \<in> B(a)" 619by blast 620 621lemma 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))" 623by simp 624 625(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*) 626 627 628subsection\<open>Rules for Powersets\<close> 629 630lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)" 631by (erule Pow_iff [THEN iffD2]) 632 633lemma PowD: "A \<in> Pow(B) ==> A<=B" 634by (erule Pow_iff [THEN iffD1]) 635 636declare Pow_iff [iff] 637 638lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment> \<open>\<^term>\<open>0 \<in> Pow(B)\<close>\<close> 639lemmas Pow_top = subset_refl [THEN PowI] \<comment> \<open>\<^term>\<open>A \<in> Pow(A)\<close>\<close> 640 641 642subsection\<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). *) 647lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S" 648by (best elim!: equalityCE del: ReplaceI RepFun_eqI) 649 650end 651