src/ZF/Constructible/Relative.thy
 author paulson Tue Jul 16 16:29:36 2002 +0200 (2002-07-16) changeset 13363 c26eeb000470 parent 13353 1800e7134d2e child 13382 b37764a46b16 permissions -rw-r--r--
instantiation of locales M_trancl and M_wfrank;
proofs of list_replacement{1,2}
 paulson@13223 1 header {*Relativization and Absoluteness*} paulson@13223 2 paulson@13223 3 theory Relative = Main: paulson@13223 4 paulson@13223 5 subsection{* Relativized versions of standard set-theoretic concepts *} paulson@13223 6 paulson@13223 7 constdefs paulson@13223 8 empty :: "[i=>o,i] => o" paulson@13254 9 "empty(M,z) == \x[M]. x \ z" paulson@13223 10 paulson@13223 11 subset :: "[i=>o,i,i] => o" paulson@13298 12 "subset(M,A,B) == \x[M]. x\A --> x \ B" paulson@13223 13 paulson@13223 14 upair :: "[i=>o,i,i,i] => o" paulson@13298 15 "upair(M,a,b,z) == a \ z & b \ z & (\x[M]. x\z --> x = a | x = b)" paulson@13223 16 paulson@13223 17 pair :: "[i=>o,i,i,i] => o" paulson@13254 18 "pair(M,a,b,z) == \x[M]. upair(M,a,a,x) & paulson@13254 19 (\y[M]. upair(M,a,b,y) & upair(M,x,y,z))" paulson@13223 20 paulson@13306 21 paulson@13245 22 union :: "[i=>o,i,i,i] => o" paulson@13254 23 "union(M,a,b,z) == \x[M]. x \ z <-> x \ a | x \ b" paulson@13245 24 paulson@13306 25 is_cons :: "[i=>o,i,i,i] => o" paulson@13306 26 "is_cons(M,a,b,z) == \x[M]. upair(M,a,a,x) & union(M,x,b,z)" paulson@13306 27 paulson@13223 28 successor :: "[i=>o,i,i] => o" paulson@13306 29 "successor(M,a,z) == is_cons(M,a,a,z)" paulson@13223 30 paulson@13363 31 number1 :: "[i=>o,i] => o" paulson@13363 32 "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" paulson@13363 33 paulson@13363 34 number2 :: "[i=>o,i] => o" paulson@13363 35 "number2(M,a) == (\x[M]. number1(M,x) & successor(M,x,a))" paulson@13363 36 paulson@13363 37 number3 :: "[i=>o,i] => o" paulson@13363 38 "number3(M,a) == (\x[M]. number2(M,x) & successor(M,x,a))" paulson@13363 39 paulson@13223 40 powerset :: "[i=>o,i,i] => o" paulson@13254 41 "powerset(M,A,z) == \x[M]. x \ z <-> subset(M,x,A)" paulson@13223 42 paulson@13223 43 inter :: "[i=>o,i,i,i] => o" paulson@13254 44 "inter(M,a,b,z) == \x[M]. x \ z <-> x \ a & x \ b" paulson@13223 45 paulson@13223 46 setdiff :: "[i=>o,i,i,i] => o" paulson@13254 47 "setdiff(M,a,b,z) == \x[M]. x \ z <-> x \ a & x \ b" paulson@13223 48 paulson@13223 49 big_union :: "[i=>o,i,i] => o" paulson@13298 50 "big_union(M,A,z) == \x[M]. x \ z <-> (\y[M]. y\A & x \ y)" paulson@13223 51 paulson@13223 52 big_inter :: "[i=>o,i,i] => o" paulson@13223 53 "big_inter(M,A,z) == paulson@13223 54 (A=0 --> z=0) & paulson@13298 55 (A\0 --> (\x[M]. x \ z <-> (\y[M]. y\A --> x \ y)))" paulson@13223 56 paulson@13223 57 cartprod :: "[i=>o,i,i,i] => o" paulson@13223 58 "cartprod(M,A,B,z) == paulson@13298 59 \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\B & pair(M,x,y,u)))" paulson@13223 60 paulson@13350 61 is_sum :: "[i=>o,i,i,i] => o" paulson@13350 62 "is_sum(M,A,B,Z) == paulson@13350 63 \A0[M]. \n1[M]. \s1[M]. \B1[M]. paulson@13350 64 number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & paulson@13350 65 cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" paulson@13350 66 paulson@13223 67 is_converse :: "[i=>o,i,i] => o" paulson@13223 68 "is_converse(M,r,z) == paulson@13299 69 \x[M]. x \ z <-> paulson@13299 70 (\w[M]. w\r & (\u[M]. \v[M]. pair(M,u,v,w) & pair(M,v,u,x)))" paulson@13223 71 paulson@13223 72 pre_image :: "[i=>o,i,i,i] => o" paulson@13223 73 "pre_image(M,r,A,z) == paulson@13299 74 \x[M]. x \ z <-> (\w[M]. w\r & (\y[M]. y\A & pair(M,x,y,w)))" paulson@13223 75 paulson@13223 76 is_domain :: "[i=>o,i,i] => o" paulson@13223 77 "is_domain(M,r,z) == paulson@13299 78 \x[M]. (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" paulson@13223 79 paulson@13223 80 image :: "[i=>o,i,i,i] => o" paulson@13223 81 "image(M,r,A,z) == paulson@13299 82 \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" paulson@13223 83 paulson@13223 84 is_range :: "[i=>o,i,i] => o" paulson@13223 85 --{*the cleaner paulson@13299 86 @{term "\r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"} paulson@13223 87 unfortunately needs an instance of separation in order to prove paulson@13223 88 @{term "M(converse(r))"}.*} paulson@13223 89 "is_range(M,r,z) == paulson@13299 90 \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" paulson@13223 91 paulson@13245 92 is_field :: "[i=>o,i,i] => o" paulson@13245 93 "is_field(M,r,z) == paulson@13298 94 \dr[M]. is_domain(M,r,dr) & paulson@13298 95 (\rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" paulson@13245 96 paulson@13223 97 is_relation :: "[i=>o,i] => o" paulson@13223 98 "is_relation(M,r) == paulson@13298 99 (\z[M]. z\r --> (\x[M]. \y[M]. pair(M,x,y,z)))" paulson@13223 100 paulson@13223 101 is_function :: "[i=>o,i] => o" paulson@13223 102 "is_function(M,r) == paulson@13299 103 \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. paulson@13299 104 pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\r --> y=y'" paulson@13223 105 paulson@13223 106 fun_apply :: "[i=>o,i,i,i] => o" paulson@13223 107 "fun_apply(M,f,x,y) == paulson@13352 108 (\xs[M]. \fxs[M]. paulson@13352 109 upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" paulson@13223 110 paulson@13223 111 typed_function :: "[i=>o,i,i,i] => o" paulson@13223 112 "typed_function(M,A,B,r) == paulson@13223 113 is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & paulson@13306 114 (\u[M]. u\r --> (\x[M]. \y[M]. pair(M,x,y,u) --> y\B))" paulson@13223 115 paulson@13268 116 is_funspace :: "[i=>o,i,i,i] => o" paulson@13268 117 "is_funspace(M,A,B,F) == paulson@13268 118 \f[M]. f \ F <-> typed_function(M,A,B,f)" paulson@13268 119 paulson@13245 120 composition :: "[i=>o,i,i,i] => o" paulson@13245 121 "composition(M,r,s,t) == paulson@13306 122 \p[M]. p \ t <-> paulson@13323 123 (\x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. paulson@13323 124 pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & paulson@13323 125 xy \ s & yz \ r)" paulson@13245 126 paulson@13223 127 injection :: "[i=>o,i,i,i] => o" paulson@13223 128 "injection(M,A,B,f) == paulson@13223 129 typed_function(M,A,B,f) & paulson@13306 130 (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. paulson@13306 131 pair(M,x,y,p) --> pair(M,x',y,p') --> p\f --> p'\f --> x=x')" paulson@13223 132 paulson@13223 133 surjection :: "[i=>o,i,i,i] => o" paulson@13223 134 "surjection(M,A,B,f) == paulson@13223 135 typed_function(M,A,B,f) & paulson@13299 136 (\y[M]. y\B --> (\x[M]. x\A & fun_apply(M,f,x,y)))" paulson@13223 137 paulson@13223 138 bijection :: "[i=>o,i,i,i] => o" paulson@13223 139 "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" paulson@13223 140 paulson@13223 141 restriction :: "[i=>o,i,i,i] => o" paulson@13223 142 "restriction(M,r,A,z) == paulson@13306 143 \x[M]. x \ z <-> (x \ r & (\u[M]. u\A & (\v[M]. pair(M,u,v,x))))" paulson@13223 144 paulson@13223 145 transitive_set :: "[i=>o,i] => o" paulson@13299 146 "transitive_set(M,a) == \x[M]. x\a --> subset(M,x,a)" paulson@13223 147 paulson@13223 148 ordinal :: "[i=>o,i] => o" paulson@13223 149 --{*an ordinal is a transitive set of transitive sets*} paulson@13299 150 "ordinal(M,a) == transitive_set(M,a) & (\x[M]. x\a --> transitive_set(M,x))" paulson@13223 151 paulson@13223 152 limit_ordinal :: "[i=>o,i] => o" paulson@13223 153 --{*a limit ordinal is a non-empty, successor-closed ordinal*} paulson@13223 154 "limit_ordinal(M,a) == paulson@13223 155 ordinal(M,a) & ~ empty(M,a) & paulson@13299 156 (\x[M]. x\a --> (\y[M]. y\a & successor(M,x,y)))" paulson@13223 157 paulson@13223 158 successor_ordinal :: "[i=>o,i] => o" paulson@13223 159 --{*a successor ordinal is any ordinal that is neither empty nor limit*} paulson@13223 160 "successor_ordinal(M,a) == paulson@13223 161 ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)" paulson@13223 162 paulson@13223 163 finite_ordinal :: "[i=>o,i] => o" paulson@13223 164 --{*an ordinal is finite if neither it nor any of its elements are limit*} paulson@13223 165 "finite_ordinal(M,a) == paulson@13223 166 ordinal(M,a) & ~ limit_ordinal(M,a) & paulson@13299 167 (\x[M]. x\a --> ~ limit_ordinal(M,x))" paulson@13223 168 paulson@13223 169 omega :: "[i=>o,i] => o" paulson@13223 170 --{*omega is a limit ordinal none of whose elements are limit*} paulson@13299 171 "omega(M,a) == limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x))" paulson@13223 172 paulson@13350 173 is_quasinat :: "[i=>o,i] => o" paulson@13350 174 "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" paulson@13350 175 paulson@13350 176 is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" paulson@13350 177 "is_nat_case(M, a, is_b, k, z) == paulson@13350 178 (empty(M,k) --> z=a) & paulson@13350 179 (\m[M]. successor(M,m,k) --> is_b(m,z)) & paulson@13363 180 (is_quasinat(M,k) | empty(M,z))" paulson@13350 181 paulson@13353 182 relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o" paulson@13353 183 "relativize1(M,is_f,f) == \x[M]. \y[M]. is_f(x,y) <-> y = f(x)" paulson@13353 184 paulson@13353 185 relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" paulson@13353 186 "relativize2(M,is_f,f) == \x[M]. \y[M]. \z[M]. is_f(x,y,z) <-> z = f(x,y)" paulson@13353 187 paulson@13353 188 relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" paulson@13353 189 "relativize3(M,is_f,f) == paulson@13353 190 \x[M]. \y[M]. \z[M]. \u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)" paulson@13353 191 paulson@13223 192 paulson@13223 193 subsection {*The relativized ZF axioms*} paulson@13223 194 constdefs paulson@13223 195 paulson@13223 196 extensionality :: "(i=>o) => o" paulson@13223 197 "extensionality(M) == paulson@13290 198 \x[M]. \y[M]. (\z[M]. z \ x <-> z \ y) --> x=y" paulson@13223 199 paulson@13223 200 separation :: "[i=>o, i=>o] => o" paulson@13223 201 --{*Big problem: the formula @{text P} should only involve parameters paulson@13223 202 belonging to @{text M}. Don't see how to enforce that.*} paulson@13223 203 "separation(M,P) == paulson@13290 204 \z[M]. \y[M]. \x[M]. x \ y <-> x \ z & P(x)" paulson@13223 205 paulson@13223 206 upair_ax :: "(i=>o) => o" paulson@13299 207 "upair_ax(M) == \x y. M(x) --> M(y) --> (\z[M]. upair(M,x,y,z))" paulson@13223 208 paulson@13223 209 Union_ax :: "(i=>o) => o" paulson@13299 210 "Union_ax(M) == \x[M]. (\z[M]. big_union(M,x,z))" paulson@13223 211 paulson@13223 212 power_ax :: "(i=>o) => o" paulson@13299 213 "power_ax(M) == \x[M]. (\z[M]. powerset(M,x,z))" paulson@13223 214 paulson@13223 215 univalent :: "[i=>o, i, [i,i]=>o] => o" paulson@13223 216 "univalent(M,A,P) == paulson@13299 217 (\x[M]. x\A --> (\y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))" paulson@13223 218 paulson@13223 219 replacement :: "[i=>o, [i,i]=>o] => o" paulson@13223 220 "replacement(M,P) == paulson@13299 221 \A[M]. univalent(M,A,P) --> paulson@13299 222 (\Y[M]. (\b[M]. ((\x[M]. x\A & P(x,b)) --> b \ Y)))" paulson@13223 223 paulson@13223 224 strong_replacement :: "[i=>o, [i,i]=>o] => o" paulson@13223 225 "strong_replacement(M,P) == paulson@13299 226 \A[M]. univalent(M,A,P) --> paulson@13299 227 (\Y[M]. (\b[M]. (b \ Y <-> (\x[M]. x\A & P(x,b)))))" paulson@13223 228 paulson@13223 229 foundation_ax :: "(i=>o) => o" paulson@13223 230 "foundation_ax(M) == paulson@13299 231 \x[M]. (\y\x. M(y)) paulson@13299 232 --> (\y[M]. y\x & ~(\z[M]. z\x & z \ y))" paulson@13223 233 paulson@13223 234 paulson@13223 235 subsection{*A trivial consistency proof for $V_\omega$ *} paulson@13223 236 paulson@13223 237 text{*We prove that $V_\omega$ paulson@13223 238 (or @{text univ} in Isabelle) satisfies some ZF axioms. paulson@13223 239 Kunen, Theorem IV 3.13, page 123.*} paulson@13223 240 paulson@13223 241 lemma univ0_downwards_mem: "[| y \ x; x \ univ(0) |] ==> y \ univ(0)" paulson@13223 242 apply (insert Transset_univ [OF Transset_0]) paulson@13223 243 apply (simp add: Transset_def, blast) paulson@13223 244 done paulson@13223 245 paulson@13223 246 lemma univ0_Ball_abs [simp]: paulson@13223 247 "A \ univ(0) ==> (\x\A. x \ univ(0) --> P(x)) <-> (\x\A. P(x))" paulson@13223 248 by (blast intro: univ0_downwards_mem) paulson@13223 249 paulson@13223 250 lemma univ0_Bex_abs [simp]: paulson@13223 251 "A \ univ(0) ==> (\x\A. x \ univ(0) & P(x)) <-> (\x\A. P(x))" paulson@13223 252 by (blast intro: univ0_downwards_mem) paulson@13223 253 paulson@13223 254 text{*Congruence rule for separation: can assume the variable is in @{text M}*} paulson@13254 255 lemma separation_cong [cong]: paulson@13339 256 "(!!x. M(x) ==> P(x) <-> P'(x)) paulson@13339 257 ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))" paulson@13223 258 by (simp add: separation_def) paulson@13223 259 paulson@13223 260 text{*Congruence rules for replacement*} paulson@13254 261 lemma univalent_cong [cong]: paulson@13223 262 "[| A=A'; !!x y. [| x\A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] paulson@13339 263 ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))" paulson@13223 264 by (simp add: univalent_def) paulson@13223 265 paulson@13254 266 lemma strong_replacement_cong [cong]: paulson@13223 267 "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] paulson@13339 268 ==> strong_replacement(M, %x y. P(x,y)) <-> paulson@13339 269 strong_replacement(M, %x y. P'(x,y))" paulson@13223 270 by (simp add: strong_replacement_def) paulson@13223 271 paulson@13223 272 text{*The extensionality axiom*} paulson@13223 273 lemma "extensionality(\x. x \ univ(0))" paulson@13223 274 apply (simp add: extensionality_def) paulson@13223 275 apply (blast intro: univ0_downwards_mem) paulson@13223 276 done paulson@13223 277 paulson@13223 278 text{*The separation axiom requires some lemmas*} paulson@13223 279 lemma Collect_in_Vfrom: paulson@13223 280 "[| X \ Vfrom(A,j); Transset(A) |] ==> Collect(X,P) \ Vfrom(A, succ(j))" paulson@13223 281 apply (drule Transset_Vfrom) paulson@13223 282 apply (rule subset_mem_Vfrom) paulson@13223 283 apply (unfold Transset_def, blast) paulson@13223 284 done paulson@13223 285 paulson@13223 286 lemma Collect_in_VLimit: paulson@13223 287 "[| X \ Vfrom(A,i); Limit(i); Transset(A) |] paulson@13223 288 ==> Collect(X,P) \ Vfrom(A,i)" paulson@13223 289 apply (rule Limit_VfromE, assumption+) paulson@13223 290 apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom) paulson@13223 291 done paulson@13223 292 paulson@13223 293 lemma Collect_in_univ: paulson@13223 294 "[| X \ univ(A); Transset(A) |] ==> Collect(X,P) \ univ(A)" paulson@13223 295 by (simp add: univ_def Collect_in_VLimit Limit_nat) paulson@13223 296 paulson@13223 297 lemma "separation(\x. x \ univ(0), P)" paulson@13290 298 apply (simp add: separation_def, clarify) paulson@13339 299 apply (rule_tac x = "Collect(z,P)" in bexI) paulson@13290 300 apply (blast intro: Collect_in_univ Transset_0)+ paulson@13223 301 done paulson@13223 302 paulson@13223 303 text{*Unordered pairing axiom*} paulson@13223 304 lemma "upair_ax(\x. x \ univ(0))" paulson@13223 305 apply (simp add: upair_ax_def upair_def) paulson@13223 306 apply (blast intro: doubleton_in_univ) paulson@13223 307 done paulson@13223 308 paulson@13223 309 text{*Union axiom*} paulson@13223 310 lemma "Union_ax(\x. x \ univ(0))" paulson@13299 311 apply (simp add: Union_ax_def big_union_def, clarify) paulson@13299 312 apply (rule_tac x="\x" in bexI) paulson@13299 313 apply (blast intro: univ0_downwards_mem) paulson@13299 314 apply (blast intro: Union_in_univ Transset_0) paulson@13223 315 done paulson@13223 316 paulson@13223 317 text{*Powerset axiom*} paulson@13223 318 paulson@13223 319 lemma Pow_in_univ: paulson@13223 320 "[| X \ univ(A); Transset(A) |] ==> Pow(X) \ univ(A)" paulson@13223 321 apply (simp add: univ_def Pow_in_VLimit Limit_nat) paulson@13223 322 done paulson@13223 323 paulson@13223 324 lemma "power_ax(\x. x \ univ(0))" paulson@13299 325 apply (simp add: power_ax_def powerset_def subset_def, clarify) paulson@13299 326 apply (rule_tac x="Pow(x)" in bexI) paulson@13299 327 apply (blast intro: univ0_downwards_mem) paulson@13299 328 apply (blast intro: Pow_in_univ Transset_0) paulson@13223 329 done paulson@13223 330 paulson@13223 331 text{*Foundation axiom*} paulson@13223 332 lemma "foundation_ax(\x. x \ univ(0))" paulson@13223 333 apply (simp add: foundation_ax_def, clarify) paulson@13299 334 apply (cut_tac A=x in foundation) paulson@13299 335 apply (blast intro: univ0_downwards_mem) paulson@13223 336 done paulson@13223 337 paulson@13223 338 lemma "replacement(\x. x \ univ(0), P)" paulson@13223 339 apply (simp add: replacement_def, clarify) paulson@13223 340 oops paulson@13223 341 text{*no idea: maybe prove by induction on the rank of A?*} paulson@13223 342 paulson@13223 343 text{*Still missing: Replacement, Choice*} paulson@13223 344 paulson@13223 345 subsection{*lemmas needed to reduce some set constructions to instances paulson@13223 346 of Separation*} paulson@13223 347 paulson@13223 348 lemma image_iff_Collect: "r  A = {y \ Union(Union(r)). \p\r. \x\A. p=}" paulson@13223 349 apply (rule equalityI, auto) paulson@13223 350 apply (simp add: Pair_def, blast) paulson@13223 351 done paulson@13223 352 paulson@13223 353 lemma vimage_iff_Collect: paulson@13223 354 "r - A = {x \ Union(Union(r)). \p\r. \y\A. p=}" paulson@13223 355 apply (rule equalityI, auto) paulson@13223 356 apply (simp add: Pair_def, blast) paulson@13223 357 done paulson@13223 358 paulson@13223 359 text{*These two lemmas lets us prove @{text domain_closed} and paulson@13223 360 @{text range_closed} without new instances of separation*} paulson@13223 361 paulson@13223 362 lemma domain_eq_vimage: "domain(r) = r - Union(Union(r))" paulson@13223 363 apply (rule equalityI, auto) paulson@13223 364 apply (rule vimageI, assumption) paulson@13223 365 apply (simp add: Pair_def, blast) paulson@13223 366 done paulson@13223 367 paulson@13223 368 lemma range_eq_image: "range(r) = r  Union(Union(r))" paulson@13223 369 apply (rule equalityI, auto) paulson@13223 370 apply (rule imageI, assumption) paulson@13223 371 apply (simp add: Pair_def, blast) paulson@13223 372 done paulson@13223 373 paulson@13223 374 lemma replacementD: paulson@13223 375 "[| replacement(M,P); M(A); univalent(M,A,P) |] paulson@13299 376 ==> \Y[M]. (\b[M]. ((\x[M]. x\A & P(x,b)) --> b \ Y))" paulson@13223 377 by (simp add: replacement_def) paulson@13223 378 paulson@13223 379 lemma strong_replacementD: paulson@13223 380 "[| strong_replacement(M,P); M(A); univalent(M,A,P) |] paulson@13299 381 ==> \Y[M]. (\b[M]. (b \ Y <-> (\x[M]. x\A & P(x,b))))" paulson@13223 382 by (simp add: strong_replacement_def) paulson@13223 383 paulson@13223 384 lemma separationD: paulson@13290 385 "[| separation(M,P); M(z) |] ==> \y[M]. \x[M]. x \ y <-> x \ z & P(x)" paulson@13223 386 by (simp add: separation_def) paulson@13223 387 paulson@13223 388 paulson@13223 389 text{*More constants, for order types*} paulson@13223 390 constdefs paulson@13223 391 paulson@13223 392 order_isomorphism :: "[i=>o,i,i,i,i,i] => o" paulson@13223 393 "order_isomorphism(M,A,r,B,s,f) == paulson@13223 394 bijection(M,A,B,f) & paulson@13306 395 (\x[M]. x\A --> (\y[M]. y\A --> paulson@13306 396 (\p[M]. \fx[M]. \fy[M]. \q[M]. paulson@13223 397 pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> paulson@13306 398 pair(M,fx,fy,q) --> (p\r <-> q\s))))" paulson@13223 399 paulson@13223 400 pred_set :: "[i=>o,i,i,i,i] => o" paulson@13223 401 "pred_set(M,A,x,r,B) == paulson@13299 402 \y[M]. y \ B <-> (\p[M]. p\r & y \ A & pair(M,y,x,p))" paulson@13223 403 paulson@13223 404 membership :: "[i=>o,i,i] => o" --{*membership relation*} paulson@13223 405 "membership(M,A,r) == paulson@13306 406 \p[M]. p \ r <-> (\x[M]. x\A & (\y[M]. y\A & x\y & pair(M,x,y,p)))" paulson@13223 407 paulson@13223 408 paulson@13223 409 subsection{*Absoluteness for a transitive class model*} paulson@13223 410 paulson@13223 411 text{*The class M is assumed to be transitive and to satisfy some paulson@13223 412 relativized ZF axioms*} paulson@13290 413 locale M_triv_axioms = paulson@13223 414 fixes M paulson@13223 415 assumes transM: "[| y\x; M(x) |] ==> M(y)" paulson@13223 416 and nonempty [simp]: "M(0)" paulson@13223 417 and upair_ax: "upair_ax(M)" paulson@13223 418 and Union_ax: "Union_ax(M)" paulson@13223 419 and power_ax: "power_ax(M)" paulson@13223 420 and replacement: "replacement(M,P)" paulson@13268 421 and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*) paulson@13290 422 paulson@13290 423 lemma (in M_triv_axioms) ball_abs [simp]: paulson@13290 424 "M(A) ==> (\x\A. M(x) --> P(x)) <-> (\x\A. P(x))" paulson@13290 425 by (blast intro: transM) paulson@13290 426 paulson@13290 427 lemma (in M_triv_axioms) rall_abs [simp]: paulson@13290 428 "M(A) ==> (\x[M]. x\A --> P(x)) <-> (\x\A. P(x))" paulson@13290 429 by (blast intro: transM) paulson@13290 430 paulson@13290 431 lemma (in M_triv_axioms) bex_abs [simp]: paulson@13290 432 "M(A) ==> (\x\A. M(x) & P(x)) <-> (\x\A. P(x))" paulson@13290 433 by (blast intro: transM) paulson@13290 434 paulson@13290 435 lemma (in M_triv_axioms) rex_abs [simp]: paulson@13290 436 "M(A) ==> (\x[M]. x\A & P(x)) <-> (\x\A. P(x))" paulson@13290 437 by (blast intro: transM) paulson@13290 438 paulson@13290 439 lemma (in M_triv_axioms) ball_iff_equiv: paulson@13299 440 "M(A) ==> (\x[M]. (x\A <-> P(x))) <-> paulson@13290 441 (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" paulson@13290 442 by (blast intro: transM) paulson@13290 443 paulson@13290 444 text{*Simplifies proofs of equalities when there's an iff-equality paulson@13290 445 available for rewriting, universally quantified over M. *} paulson@13290 446 lemma (in M_triv_axioms) M_equalityI: paulson@13290 447 "[| !!x. M(x) ==> x\A <-> x\B; M(A); M(B) |] ==> A=B" paulson@13290 448 by (blast intro!: equalityI dest: transM) paulson@13290 449 paulson@13290 450 lemma (in M_triv_axioms) empty_abs [simp]: paulson@13290 451 "M(z) ==> empty(M,z) <-> z=0" paulson@13290 452 apply (simp add: empty_def) paulson@13290 453 apply (blast intro: transM) paulson@13290 454 done paulson@13290 455 paulson@13290 456 lemma (in M_triv_axioms) subset_abs [simp]: paulson@13290 457 "M(A) ==> subset(M,A,B) <-> A \ B" paulson@13290 458 apply (simp add: subset_def) paulson@13290 459 apply (blast intro: transM) paulson@13290 460 done paulson@13290 461 paulson@13290 462 lemma (in M_triv_axioms) upair_abs [simp]: paulson@13290 463 "M(z) ==> upair(M,a,b,z) <-> z={a,b}" paulson@13290 464 apply (simp add: upair_def) paulson@13290 465 apply (blast intro: transM) paulson@13290 466 done paulson@13290 467 paulson@13290 468 lemma (in M_triv_axioms) upair_in_M_iff [iff]: paulson@13290 469 "M({a,b}) <-> M(a) & M(b)" paulson@13290 470 apply (insert upair_ax, simp add: upair_ax_def) paulson@13290 471 apply (blast intro: transM) paulson@13290 472 done paulson@13290 473 paulson@13290 474 lemma (in M_triv_axioms) singleton_in_M_iff [iff]: paulson@13290 475 "M({a}) <-> M(a)" paulson@13290 476 by (insert upair_in_M_iff [of a a], simp) paulson@13290 477 paulson@13290 478 lemma (in M_triv_axioms) pair_abs [simp]: paulson@13290 479 "M(z) ==> pair(M,a,b,z) <-> z=" paulson@13290 480 apply (simp add: pair_def ZF.Pair_def) paulson@13290 481 apply (blast intro: transM) paulson@13290 482 done paulson@13290 483 paulson@13290 484 lemma (in M_triv_axioms) pair_in_M_iff [iff]: paulson@13290 485 "M() <-> M(a) & M(b)" paulson@13290 486 by (simp add: ZF.Pair_def) paulson@13290 487 paulson@13290 488 lemma (in M_triv_axioms) pair_components_in_M: paulson@13290 489 "[| \ A; M(A) |] ==> M(x) & M(y)" paulson@13290 490 apply (simp add: Pair_def) paulson@13290 491 apply (blast dest: transM) paulson@13290 492 done paulson@13290 493 paulson@13290 494 lemma (in M_triv_axioms) cartprod_abs [simp]: paulson@13290 495 "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B" paulson@13290 496 apply (simp add: cartprod_def) paulson@13290 497 apply (rule iffI) paulson@13290 498 apply (blast intro!: equalityI intro: transM dest!: rspec) paulson@13290 499 apply (blast dest: transM) paulson@13290 500 done paulson@13290 501 paulson@13290 502 lemma (in M_triv_axioms) union_abs [simp]: paulson@13290 503 "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b" paulson@13290 504 apply (simp add: union_def) paulson@13290 505 apply (blast intro: transM) paulson@13290 506 done paulson@13290 507 paulson@13290 508 lemma (in M_triv_axioms) inter_abs [simp]: paulson@13290 509 "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b" paulson@13290 510 apply (simp add: inter_def) paulson@13290 511 apply (blast intro: transM) paulson@13290 512 done paulson@13290 513 paulson@13290 514 lemma (in M_triv_axioms) setdiff_abs [simp]: paulson@13290 515 "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b" paulson@13290 516 apply (simp add: setdiff_def) paulson@13290 517 apply (blast intro: transM) paulson@13290 518 done paulson@13290 519 paulson@13290 520 lemma (in M_triv_axioms) Union_abs [simp]: paulson@13290 521 "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)" paulson@13290 522 apply (simp add: big_union_def) paulson@13290 523 apply (blast intro!: equalityI dest: transM) paulson@13290 524 done paulson@13290 525 paulson@13290 526 lemma (in M_triv_axioms) Union_closed [intro,simp]: paulson@13290 527 "M(A) ==> M(Union(A))" paulson@13290 528 by (insert Union_ax, simp add: Union_ax_def) paulson@13290 529 paulson@13290 530 lemma (in M_triv_axioms) Un_closed [intro,simp]: paulson@13290 531 "[| M(A); M(B) |] ==> M(A Un B)" paulson@13290 532 by (simp only: Un_eq_Union, blast) paulson@13290 533 paulson@13290 534 lemma (in M_triv_axioms) cons_closed [intro,simp]: paulson@13290 535 "[| M(a); M(A) |] ==> M(cons(a,A))" paulson@13290 536 by (subst cons_eq [symmetric], blast) paulson@13290 537 paulson@13306 538 lemma (in M_triv_axioms) cons_abs [simp]: paulson@13306 539 "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)" paulson@13306 540 by (simp add: is_cons_def, blast intro: transM) paulson@13306 541 paulson@13290 542 lemma (in M_triv_axioms) successor_abs [simp]: paulson@13306 543 "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)" paulson@13290 544 by (simp add: successor_def, blast) paulson@13290 545 paulson@13290 546 lemma (in M_triv_axioms) succ_in_M_iff [iff]: paulson@13290 547 "M(succ(a)) <-> M(a)" paulson@13290 548 apply (simp add: succ_def) paulson@13290 549 apply (blast intro: transM) paulson@13290 550 done paulson@13290 551 paulson@13290 552 lemma (in M_triv_axioms) separation_closed [intro,simp]: paulson@13290 553 "[| separation(M,P); M(A) |] ==> M(Collect(A,P))" paulson@13290 554 apply (insert separation, simp add: separation_def) paulson@13290 555 apply (drule rspec, assumption, clarify) paulson@13290 556 apply (subgoal_tac "y = Collect(A,P)", blast) paulson@13290 557 apply (blast dest: transM) paulson@13290 558 done paulson@13290 559 paulson@13290 560 text{*Probably the premise and conclusion are equivalent*} paulson@13348 561 lemma (in M_triv_axioms) strong_replacementI [rule_format]: paulson@13306 562 "[| \A[M]. separation(M, %u. \x[M]. x\A & P(x,u)) |] paulson@13290 563 ==> strong_replacement(M,P)" paulson@13290 564 apply (simp add: strong_replacement_def, clarify) paulson@13290 565 apply (frule replacementD [OF replacement], assumption, clarify) paulson@13299 566 apply (drule_tac x=A in rspec, clarify) paulson@13290 567 apply (drule_tac z=Y in separationD, assumption, clarify) paulson@13299 568 apply (rule_tac x=y in rexI) paulson@13299 569 apply (blast dest: transM)+ paulson@13290 570 done paulson@13290 571 paulson@13290 572 paulson@13290 573 (*The last premise expresses that P takes M to M*) paulson@13290 574 lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]: paulson@13290 575 "[| strong_replacement(M,P); M(A); univalent(M,A,P); paulson@13290 576 !!x y. [| x\A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))" paulson@13290 577 apply (simp add: strong_replacement_def) paulson@13299 578 apply (drule rspec, auto) paulson@13290 579 apply (subgoal_tac "Replace(A,P) = Y") paulson@13290 580 apply simp paulson@13290 581 apply (rule equality_iffI) paulson@13290 582 apply (simp add: Replace_iff, safe) paulson@13290 583 apply (blast dest: transM) paulson@13290 584 apply (frule transM, assumption) paulson@13290 585 apply (simp add: univalent_def) paulson@13299 586 apply (drule rspec [THEN iffD1], assumption, assumption) paulson@13290 587 apply (blast dest: transM) paulson@13290 588 done paulson@13290 589 paulson@13290 590 (*The first premise can't simply be assumed as a schema. paulson@13290 591 It is essential to take care when asserting instances of Replacement. paulson@13290 592 Let K be a nonconstructible subset of nat and define paulson@13290 593 f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a paulson@13290 594 nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f)) paulson@13290 595 even for f : M -> M. paulson@13290 596 *) paulson@13353 597 lemma (in M_triv_axioms) RepFun_closed: paulson@13290 598 "[| strong_replacement(M, \x y. y = f(x)); M(A); \x\A. M(f(x)) |] paulson@13290 599 ==> M(RepFun(A,f))" paulson@13290 600 apply (simp add: RepFun_def) paulson@13290 601 apply (rule strong_replacement_closed) paulson@13290 602 apply (auto dest: transM simp add: univalent_def) paulson@13290 603 done paulson@13290 604 paulson@13353 605 lemma Replace_conj_eq: "{y . x \ A, x\A & y=f(x)} = {y . x\A, y=f(x)}" paulson@13353 606 by simp paulson@13353 607 paulson@13353 608 text{*Better than @{text RepFun_closed} when having the formula @{term "x\A"} paulson@13353 609 makes relativization easier.*} paulson@13353 610 lemma (in M_triv_axioms) RepFun_closed2: paulson@13353 611 "[| strong_replacement(M, \x y. x\A & y = f(x)); M(A); \x\A. M(f(x)) |] paulson@13353 612 ==> M(RepFun(A, %x. f(x)))" paulson@13353 613 apply (simp add: RepFun_def) paulson@13353 614 apply (frule strong_replacement_closed, assumption) paulson@13353 615 apply (auto dest: transM simp add: Replace_conj_eq univalent_def) paulson@13353 616 done paulson@13353 617 paulson@13290 618 lemma (in M_triv_axioms) lam_closed [intro,simp]: paulson@13290 619 "[| strong_replacement(M, \x y. y = ); M(A); \x\A. M(b(x)) |] paulson@13290 620 ==> M(\x\A. b(x))" paulson@13353 621 by (simp add: lam_def, blast intro: RepFun_closed dest: transM) paulson@13290 622 paulson@13290 623 lemma (in M_triv_axioms) image_abs [simp]: paulson@13290 624 "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = rA" paulson@13290 625 apply (simp add: image_def) paulson@13290 626 apply (rule iffI) paulson@13290 627 apply (blast intro!: equalityI dest: transM, blast) paulson@13290 628 done paulson@13290 629 paulson@13290 630 text{*What about @{text Pow_abs}? Powerset is NOT absolute! paulson@13290 631 This result is one direction of absoluteness.*} paulson@13290 632 paulson@13290 633 lemma (in M_triv_axioms) powerset_Pow: paulson@13290 634 "powerset(M, x, Pow(x))" paulson@13290 635 by (simp add: powerset_def) paulson@13290 636 paulson@13290 637 text{*But we can't prove that the powerset in @{text M} includes the paulson@13290 638 real powerset.*} paulson@13290 639 lemma (in M_triv_axioms) powerset_imp_subset_Pow: paulson@13290 640 "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)" paulson@13290 641 apply (simp add: powerset_def) paulson@13290 642 apply (blast dest: transM) paulson@13290 643 done paulson@13290 644 paulson@13290 645 lemma (in M_triv_axioms) nat_into_M [intro]: paulson@13290 646 "n \ nat ==> M(n)" paulson@13290 647 by (induct n rule: nat_induct, simp_all) paulson@13290 648 paulson@13350 649 lemma (in M_triv_axioms) nat_case_closed [intro,simp]: paulson@13290 650 "[|M(k); M(a); \m[M]. M(b(m))|] ==> M(nat_case(a,b,k))" paulson@13290 651 apply (case_tac "k=0", simp) paulson@13290 652 apply (case_tac "\m. k = succ(m)", force) paulson@13290 653 apply (simp add: nat_case_def) paulson@13290 654 done paulson@13290 655 paulson@13350 656 lemma (in M_triv_axioms) quasinat_abs [simp]: paulson@13350 657 "M(z) ==> is_quasinat(M,z) <-> quasinat(z)" paulson@13350 658 by (auto simp add: is_quasinat_def quasinat_def) paulson@13350 659 paulson@13350 660 lemma (in M_triv_axioms) nat_case_abs [simp]: paulson@13353 661 "[| relativize1(M,is_b,b); M(k); M(z) |] paulson@13353 662 ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)" paulson@13350 663 apply (case_tac "quasinat(k)") paulson@13350 664 prefer 2 paulson@13350 665 apply (simp add: is_nat_case_def non_nat_case) paulson@13350 666 apply (force simp add: quasinat_def) paulson@13350 667 apply (simp add: quasinat_def is_nat_case_def) paulson@13350 668 apply (elim disjE exE) paulson@13353 669 apply (simp_all add: relativize1_def) paulson@13350 670 done paulson@13350 671 paulson@13363 672 (*NOT for the simplifier. The assumption M(z') is apparently necessary, but paulson@13363 673 causes the error "Failed congruence proof!" It may be better to replace paulson@13363 674 is_nat_case by nat_case before attempting congruence reasoning.*) paulson@13363 675 lemma (in M_triv_axioms) is_nat_case_cong: paulson@13352 676 "[| a = a'; k = k'; z = z'; M(z'); paulson@13352 677 !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] paulson@13352 678 ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')" paulson@13352 679 by (simp add: is_nat_case_def) paulson@13352 680 paulson@13290 681 lemma (in M_triv_axioms) Inl_in_M_iff [iff]: paulson@13290 682 "M(Inl(a)) <-> M(a)" paulson@13290 683 by (simp add: Inl_def) paulson@13290 684 paulson@13290 685 lemma (in M_triv_axioms) Inr_in_M_iff [iff]: paulson@13290 686 "M(Inr(a)) <-> M(a)" paulson@13290 687 by (simp add: Inr_def) paulson@13290 688 paulson@13290 689 paulson@13290 690 subsection{*Absoluteness for ordinals*} paulson@13290 691 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} paulson@13290 692 paulson@13290 693 lemma (in M_triv_axioms) lt_closed: paulson@13290 694 "[| j M(j)" paulson@13290 695 by (blast dest: ltD intro: transM) paulson@13290 696 paulson@13290 697 lemma (in M_triv_axioms) transitive_set_abs [simp]: paulson@13290 698 "M(a) ==> transitive_set(M,a) <-> Transset(a)" paulson@13290 699 by (simp add: transitive_set_def Transset_def) paulson@13290 700 paulson@13290 701 lemma (in M_triv_axioms) ordinal_abs [simp]: paulson@13290 702 "M(a) ==> ordinal(M,a) <-> Ord(a)" paulson@13290 703 by (simp add: ordinal_def Ord_def) paulson@13290 704 paulson@13290 705 lemma (in M_triv_axioms) limit_ordinal_abs [simp]: paulson@13290 706 "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" paulson@13290 707 apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) paulson@13290 708 apply (simp add: lt_def, blast) paulson@13290 709 done paulson@13290 710 paulson@13290 711 lemma (in M_triv_axioms) successor_ordinal_abs [simp]: paulson@13299 712 "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\b[M]. a = succ(b))" paulson@13290 713 apply (simp add: successor_ordinal_def, safe) paulson@13290 714 apply (drule Ord_cases_disj, auto) paulson@13290 715 done paulson@13290 716 paulson@13290 717 lemma finite_Ord_is_nat: paulson@13290 718 "[| Ord(a); ~ Limit(a); \x\a. ~ Limit(x) |] ==> a \ nat" paulson@13290 719 by (induct a rule: trans_induct3, simp_all) paulson@13290 720 paulson@13290 721 lemma naturals_not_limit: "a \ nat ==> ~ Limit(a)" paulson@13290 722 by (induct a rule: nat_induct, auto) paulson@13290 723 paulson@13290 724 lemma (in M_triv_axioms) finite_ordinal_abs [simp]: paulson@13290 725 "M(a) ==> finite_ordinal(M,a) <-> a \ nat" paulson@13290 726 apply (simp add: finite_ordinal_def) paulson@13290 727 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord paulson@13290 728 dest: Ord_trans naturals_not_limit) paulson@13290 729 done paulson@13290 730 paulson@13290 731 lemma Limit_non_Limit_implies_nat: paulson@13290 732 "[| Limit(a); \x\a. ~ Limit(x) |] ==> a = nat" paulson@13290 733 apply (rule le_anti_sym) paulson@13290 734 apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) paulson@13290 735 apply (simp add: lt_def) paulson@13290 736 apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) paulson@13290 737 apply (erule nat_le_Limit) paulson@13290 738 done paulson@13290 739 paulson@13290 740 lemma (in M_triv_axioms) omega_abs [simp]: paulson@13290 741 "M(a) ==> omega(M,a) <-> a = nat" paulson@13290 742 apply (simp add: omega_def) paulson@13290 743 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit) paulson@13290 744 done paulson@13290 745 paulson@13290 746 lemma (in M_triv_axioms) number1_abs [simp]: paulson@13290 747 "M(a) ==> number1(M,a) <-> a = 1" paulson@13290 748 by (simp add: number1_def) paulson@13290 749 paulson@13290 750 lemma (in M_triv_axioms) number1_abs [simp]: paulson@13290 751 "M(a) ==> number2(M,a) <-> a = succ(1)" paulson@13290 752 by (simp add: number2_def) paulson@13290 753 paulson@13290 754 lemma (in M_triv_axioms) number3_abs [simp]: paulson@13290 755 "M(a) ==> number3(M,a) <-> a = succ(succ(1))" paulson@13290 756 by (simp add: number3_def) paulson@13290 757 paulson@13290 758 text{*Kunen continued to 20...*} paulson@13290 759 paulson@13290 760 (*Could not get this to work. The \x\nat is essential because everything paulson@13290 761 but the recursion variable must stay unchanged. But then the recursion paulson@13290 762 equations only hold for x\nat (or in some other set) and not for the paulson@13290 763 whole of the class M. paulson@13290 764 consts paulson@13290 765 natnumber_aux :: "[i=>o,i] => i" paulson@13290 766 paulson@13290 767 primrec paulson@13290 768 "natnumber_aux(M,0) = (\x\nat. if empty(M,x) then 1 else 0)" paulson@13290 769 "natnumber_aux(M,succ(n)) = paulson@13299 770 (\x\nat. if (\y[M]. natnumber_aux(M,n)y=1 & successor(M,y,x)) paulson@13290 771 then 1 else 0)" paulson@13290 772 paulson@13290 773 constdefs paulson@13290 774 natnumber :: "[i=>o,i,i] => o" paulson@13290 775 "natnumber(M,n,x) == natnumber_aux(M,n)x = 1" paulson@13290 776 paulson@13290 777 lemma (in M_triv_axioms) [simp]: paulson@13290 778 "natnumber(M,0,x) == x=0" paulson@13290 779 *) paulson@13290 780 paulson@13290 781 subsection{*Some instances of separation and strong replacement*} paulson@13290 782 paulson@13290 783 locale M_axioms = M_triv_axioms + paulson@13290 784 assumes Inter_separation: paulson@13268 785 "M(A) ==> separation(M, \x. \y[M]. y\A --> x\y)" paulson@13223 786 and cartprod_separation: paulson@13223 787 "[| M(A); M(B) |] paulson@13298 788 ==> separation(M, \z. \x[M]. x\A & (\y[M]. y\B & pair(M,x,y,z)))" paulson@13223 789 and image_separation: paulson@13223 790 "[| M(A); M(r) |] paulson@13268 791 ==> separation(M, \y. \p[M]. p\r & (\x[M]. x\A & pair(M,x,y,p)))" paulson@13223 792 and converse_separation: paulson@13298 793 "M(r) ==> separation(M, paulson@13298 794 \z. \p[M]. p\r & (\x[M]. \y[M]. pair(M,x,y,p) & pair(M,y,x,z)))" paulson@13223 795 and restrict_separation: paulson@13268 796 "M(A) ==> separation(M, \z. \x[M]. x\A & (\y[M]. pair(M,x,y,z)))" paulson@13223 797 and comp_separation: paulson@13223 798 "[| M(r); M(s) |] paulson@13268 799 ==> separation(M, \xz. \x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. paulson@13268 800 pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & paulson@13268 801 xy\s & yz\r)" paulson@13223 802 and pred_separation: paulson@13298 803 "[| M(r); M(x) |] ==> separation(M, \y. \p[M]. p\r & pair(M,y,x,p))" paulson@13223 804 and Memrel_separation: paulson@13298 805 "separation(M, \z. \x[M]. \y[M]. pair(M,x,y,z) & x \ y)" paulson@13268 806 and funspace_succ_replacement: paulson@13268 807 "M(n) ==> paulson@13306 808 strong_replacement(M, \p z. \f[M]. \b[M]. \nb[M]. \cnbf[M]. paulson@13306 809 pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) & paulson@13306 810 upair(M,cnbf,cnbf,z))" paulson@13223 811 and well_ord_iso_separation: paulson@13223 812 "[| M(A); M(f); M(r) |] paulson@13299 813 ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. paulson@13245 814 fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" paulson@13306 815 and obase_separation: paulson@13306 816 --{*part of the order type formalization*} paulson@13306 817 "[| M(A); M(r) |] paulson@13306 818 ==> separation(M, \a. \x[M]. \g[M]. \mx[M]. \par[M]. paulson@13306 819 ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & paulson@13306 820 order_isomorphism(M,par,r,x,mx,g))" paulson@13223 821 and obase_equals_separation: paulson@13223 822 "[| M(A); M(r) |] paulson@13316 823 ==> separation (M, \x. x\A --> ~(\y[M]. \g[M]. paulson@13316 824 ordinal(M,y) & (\my[M]. \pxr[M]. paulson@13316 825 membership(M,y,my) & pred_set(M,A,x,r,pxr) & paulson@13316 826 order_isomorphism(M,pxr,r,y,my,g))))" paulson@13306 827 and omap_replacement: paulson@13306 828 "[| M(A); M(r) |] paulson@13306 829 ==> strong_replacement(M, paulson@13306 830 \a z. \x[M]. \g[M]. \mx[M]. \par[M]. paulson@13306 831 ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & paulson@13306 832 pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" paulson@13223 833 and is_recfun_separation: paulson@13319 834 --{*for well-founded recursion*} paulson@13319 835 "[| M(r); M(f); M(g); M(a); M(b) |] paulson@13319 836 ==> separation(M, paulson@13319 837 \x. \xa[M]. \xb[M]. paulson@13319 838 pair(M,x,a,xa) & xa \ r & pair(M,x,b,xb) & xb \ r & paulson@13319 839 (\fx[M]. \gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & paulson@13319 840 fx \ gx))" paulson@13223 841 paulson@13223 842 lemma (in M_axioms) cartprod_iff_lemma: paulson@13254 843 "[| M(C); \u[M]. u \ C <-> (\x\A. \y\B. u = {{x}, {x,y}}); paulson@13254 844 powerset(M, A \ B, p1); powerset(M, p1, p2); M(p2) |] paulson@13223 845 ==> C = {u \ p2 . \x\A. \y\B. u = {{x}, {x,y}}}" paulson@13223 846 apply (simp add: powerset_def) paulson@13254 847 apply (rule equalityI, clarify, simp) paulson@13254 848 apply (frule transM, assumption) paulson@13223 849 apply (frule transM, assumption, simp) paulson@13223 850 apply blast paulson@13223 851 apply clarify paulson@13223 852 apply (frule transM, assumption, force) paulson@13223 853 done paulson@13223 854 paulson@13223 855 lemma (in M_axioms) cartprod_iff: paulson@13223 856 "[| M(A); M(B); M(C) |] paulson@13223 857 ==> cartprod(M,A,B,C) <-> paulson@13223 858 (\p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) & paulson@13223 859 C = {z \ p2. \x\A. \y\B. z = })" paulson@13223 860 apply (simp add: Pair_def cartprod_def, safe) paulson@13223 861 defer 1 paulson@13223 862 apply (simp add: powerset_def) paulson@13223 863 apply blast paulson@13223 864 txt{*Final, difficult case: the left-to-right direction of the theorem.*} paulson@13223 865 apply (insert power_ax, simp add: power_ax_def) paulson@13299 866 apply (frule_tac x="A Un B" and P="\x. rex(M,?Q(x))" in rspec) paulson@13299 867 apply (blast, clarify) paulson@13299 868 apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec) paulson@13299 869 apply assumption paulson@13223 870 apply (blast intro: cartprod_iff_lemma) paulson@13223 871 done paulson@13223 872 paulson@13223 873 lemma (in M_axioms) cartprod_closed_lemma: paulson@13299 874 "[| M(A); M(B) |] ==> \C[M]. cartprod(M,A,B,C)" paulson@13223 875 apply (simp del: cartprod_abs add: cartprod_iff) paulson@13223 876 apply (insert power_ax, simp add: power_ax_def) paulson@13299 877 apply (frule_tac x="A Un B" and P="\x. rex(M,?Q(x))" in rspec) paulson@13299 878 apply (blast, clarify) paulson@13299 879 apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec) paulson@13299 880 apply (blast, clarify) paulson@13299 881 apply (intro rexI exI conjI) paulson@13299 882 prefer 5 apply (rule refl) paulson@13299 883 prefer 3 apply assumption paulson@13299 884 prefer 3 apply assumption paulson@13245 885 apply (insert cartprod_separation [of A B], auto) paulson@13223 886 done paulson@13223 887 paulson@13223 888 text{*All the lemmas above are necessary because Powerset is not absolute. paulson@13223 889 I should have used Replacement instead!*} paulson@13245 890 lemma (in M_axioms) cartprod_closed [intro,simp]: paulson@13223 891 "[| M(A); M(B) |] ==> M(A*B)" paulson@13223 892 by (frule cartprod_closed_lemma, assumption, force) paulson@13223 893 paulson@13268 894 lemma (in M_axioms) sum_closed [intro,simp]: paulson@13268 895 "[| M(A); M(B) |] ==> M(A+B)" paulson@13268 896 by (simp add: sum_def) paulson@13268 897 paulson@13350 898 lemma (in M_axioms) sum_abs [simp]: paulson@13350 899 "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)" paulson@13350 900 by (simp add: is_sum_def sum_def singleton_0 nat_into_M) paulson@13350 901 paulson@13290 902 paulson@13290 903 subsubsection {*converse of a relation*} paulson@13290 904 paulson@13290 905 lemma (in M_axioms) M_converse_iff: paulson@13290 906 "M(r) ==> paulson@13290 907 converse(r) = paulson@13290 908 {z \ Union(Union(r)) * Union(Union(r)). paulson@13290 909 \p\r. \x[M]. \y[M]. p = \x,y\ & z = \y,x\}" paulson@13290 910 apply (rule equalityI) paulson@13290 911 prefer 2 apply (blast dest: transM, clarify, simp) paulson@13290 912 apply (simp add: Pair_def) paulson@13290 913 apply (blast dest: transM) paulson@13290 914 done paulson@13290 915 paulson@13290 916 lemma (in M_axioms) converse_closed [intro,simp]: paulson@13290 917 "M(r) ==> M(converse(r))" paulson@13290 918 apply (simp add: M_converse_iff) paulson@13290 919 apply (insert converse_separation [of r], simp) paulson@13290 920 done paulson@13290 921 paulson@13290 922 lemma (in M_axioms) converse_abs [simp]: paulson@13290 923 "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)" paulson@13290 924 apply (simp add: is_converse_def) paulson@13290 925 apply (rule iffI) paulson@13290 926 prefer 2 apply blast paulson@13290 927 apply (rule M_equalityI) paulson@13290 928 apply simp paulson@13290 929 apply (blast dest: transM)+ paulson@13290 930 done paulson@13290 931 paulson@13290 932 paulson@13290 933 subsubsection {*image, preimage, domain, range*} paulson@13290 934 paulson@13245 935 lemma (in M_axioms) image_closed [intro,simp]: paulson@13223 936 "[| M(A); M(r) |] ==> M(rA)" paulson@13223 937 apply (simp add: image_iff_Collect) paulson@13245 938 apply (insert image_separation [of A r], simp) paulson@13223 939 done paulson@13223 940 paulson@13223 941 lemma (in M_axioms) vimage_abs [simp]: paulson@13223 942 "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-A" paulson@13223 943 apply (simp add: pre_image_def) paulson@13223 944 apply (rule iffI) paulson@13223 945 apply (blast intro!: equalityI dest: transM, blast) paulson@13223 946 done paulson@13223 947 paulson@13245 948 lemma (in M_axioms) vimage_closed [intro,simp]: paulson@13223 949 "[| M(A); M(r) |] ==> M(r-A)" paulson@13290 950 by (simp add: vimage_def) paulson@13290 951 paulson@13290 952 paulson@13290 953 subsubsection{*Domain, range and field*} paulson@13223 954 paulson@13223 955 lemma (in M_axioms) domain_abs [simp]: paulson@13223 956 "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)" paulson@13223 957 apply (simp add: is_domain_def) paulson@13223 958 apply (blast intro!: equalityI dest: transM) paulson@13223 959 done paulson@13223 960 paulson@13245 961 lemma (in M_axioms) domain_closed [intro,simp]: paulson@13223 962 "M(r) ==> M(domain(r))" paulson@13223 963 apply (simp add: domain_eq_vimage) paulson@13223 964 done paulson@13223 965 paulson@13223 966 lemma (in M_axioms) range_abs [simp]: paulson@13223 967 "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)" paulson@13223 968 apply (simp add: is_range_def) paulson@13223 969 apply (blast intro!: equalityI dest: transM) paulson@13223 970 done paulson@13223 971 paulson@13245 972 lemma (in M_axioms) range_closed [intro,simp]: paulson@13223 973 "M(r) ==> M(range(r))" paulson@13223 974 apply (simp add: range_eq_image) paulson@13223 975 done paulson@13223 976 paulson@13245 977 lemma (in M_axioms) field_abs [simp]: paulson@13245 978 "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)" paulson@13245 979 by (simp add: domain_closed range_closed is_field_def field_def) paulson@13245 980 paulson@13245 981 lemma (in M_axioms) field_closed [intro,simp]: paulson@13245 982 "M(r) ==> M(field(r))" paulson@13245 983 by (simp add: domain_closed range_closed Un_closed field_def) paulson@13245 984 paulson@13245 985 paulson@13290 986 subsubsection{*Relations, functions and application*} paulson@13254 987 paulson@13223 988 lemma (in M_axioms) relation_abs [simp]: paulson@13223 989 "M(r) ==> is_relation(M,r) <-> relation(r)" paulson@13223 990 apply (simp add: is_relation_def relation_def) paulson@13223 991 apply (blast dest!: bspec dest: pair_components_in_M)+ paulson@13223 992 done paulson@13223 993 paulson@13223 994 lemma (in M_axioms) function_abs [simp]: paulson@13223 995 "M(r) ==> is_function(M,r) <-> function(r)" paulson@13223 996 apply (simp add: is_function_def function_def, safe) paulson@13223 997 apply (frule transM, assumption) paulson@13223 998 apply (blast dest: pair_components_in_M)+ paulson@13223 999 done paulson@13223 1000 paulson@13245 1001 lemma (in M_axioms) apply_closed [intro,simp]: paulson@13223 1002 "[|M(f); M(a)|] ==> M(fa)" paulson@13290 1003 by (simp add: apply_def) paulson@13223 1004 paulson@13352 1005 lemma (in M_axioms) apply_abs [simp]: paulson@13352 1006 "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> fx = y" paulson@13353 1007 apply (simp add: fun_apply_def apply_def, blast) paulson@13223 1008 done paulson@13223 1009 paulson@13223 1010 lemma (in M_axioms) typed_function_abs [simp]: paulson@13223 1011 "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \ A -> B" paulson@13223 1012 apply (auto simp add: typed_function_def relation_def Pi_iff) paulson@13223 1013 apply (blast dest: pair_components_in_M)+ paulson@13223 1014 done paulson@13223 1015 paulson@13223 1016 lemma (in M_axioms) injection_abs [simp]: paulson@13223 1017 "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \ inj(A,B)" paulson@13223 1018 apply (simp add: injection_def apply_iff inj_def apply_closed) paulson@13247 1019 apply (blast dest: transM [of _ A]) paulson@13223 1020 done paulson@13223 1021 paulson@13223 1022 lemma (in M_axioms) surjection_abs [simp]: paulson@13223 1023 "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \ surj(A,B)" paulson@13352 1024 by (simp add: surjection_def surj_def) paulson@13223 1025 paulson@13223 1026 lemma (in M_axioms) bijection_abs [simp]: paulson@13223 1027 "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \ bij(A,B)" paulson@13223 1028 by (simp add: bijection_def bij_def) paulson@13223 1029 paulson@13223 1030 paulson@13290 1031 subsubsection{*Composition of relations*} paulson@13223 1032 paulson@13223 1033 lemma (in M_axioms) M_comp_iff: paulson@13223 1034 "[| M(r); M(s) |] paulson@13223 1035 ==> r O s = paulson@13223 1036 {xz \ domain(s) * range(r). paulson@13268 1037 \x[M]. \y[M]. \z[M]. xz = \x,z\ & \x,y\ \ s & \y,z\ \ r}" paulson@13223 1038 apply (simp add: comp_def) paulson@13223 1039 apply (rule equalityI) paulson@13247 1040 apply clarify paulson@13247 1041 apply simp paulson@13223 1042 apply (blast dest: transM)+ paulson@13223 1043 done paulson@13223 1044 paulson@13245 1045 lemma (in M_axioms) comp_closed [intro,simp]: paulson@13223 1046 "[| M(r); M(s) |] ==> M(r O s)" paulson@13223 1047 apply (simp add: M_comp_iff) paulson@13245 1048 apply (insert comp_separation [of r s], simp) paulson@13245 1049 done paulson@13245 1050 paulson@13245 1051 lemma (in M_axioms) composition_abs [simp]: paulson@13245 1052 "[| M(r); M(s); M(t) |] paulson@13245 1053 ==> composition(M,r,s,t) <-> t = r O s" paulson@13247 1054 apply safe paulson@13245 1055 txt{*Proving @{term "composition(M, r, s, r O s)"}*} paulson@13245 1056 prefer 2 paulson@13245 1057 apply (simp add: composition_def comp_def) paulson@13245 1058 apply (blast dest: transM) paulson@13245 1059 txt{*Opposite implication*} paulson@13245 1060 apply (rule M_equalityI) paulson@13245 1061 apply (simp add: composition_def comp_def) paulson@13245 1062 apply (blast del: allE dest: transM)+ paulson@13223 1063 done paulson@13223 1064 paulson@13290 1065 text{*no longer needed*} paulson@13290 1066 lemma (in M_axioms) restriction_is_function: paulson@13290 1067 "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] paulson@13290 1068 ==> function(z)" paulson@13290 1069 apply (rotate_tac 1) paulson@13290 1070 apply (simp add: restriction_def ball_iff_equiv) paulson@13290 1071 apply (unfold function_def, blast) paulson@13269 1072 done paulson@13269 1073 paulson@13290 1074 lemma (in M_axioms) restriction_abs [simp]: paulson@13290 1075 "[| M(f); M(A); M(z) |] paulson@13290 1076 ==> restriction(M,f,A,z) <-> z = restrict(f,A)" paulson@13290 1077 apply (simp add: ball_iff_equiv restriction_def restrict_def) paulson@13290 1078 apply (blast intro!: equalityI dest: transM) paulson@13290 1079 done paulson@13290 1080 paulson@13223 1081 paulson@13290 1082 lemma (in M_axioms) M_restrict_iff: paulson@13290 1083 "M(r) ==> restrict(r,A) = {z \ r . \x\A. \y[M]. z = \x, y\}" paulson@13290 1084 by (simp add: restrict_def, blast dest: transM) paulson@13290 1085 paulson@13290 1086 lemma (in M_axioms) restrict_closed [intro,simp]: paulson@13290 1087 "[| M(A); M(r) |] ==> M(restrict(r,A))" paulson@13290 1088 apply (simp add: M_restrict_iff) paulson@13290 1089 apply (insert restrict_separation [of A], simp) paulson@13290 1090 done paulson@13223 1091 paulson@13223 1092 lemma (in M_axioms) Inter_abs [simp]: paulson@13223 1093 "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)" paulson@13223 1094 apply (simp add: big_inter_def Inter_def) paulson@13223 1095 apply (blast intro!: equalityI dest: transM) paulson@13223 1096 done paulson@13223 1097 paulson@13245 1098 lemma (in M_axioms) Inter_closed [intro,simp]: paulson@13223 1099 "M(A) ==> M(Inter(A))" paulson@13245 1100 by (insert Inter_separation, simp add: Inter_def) paulson@13223 1101 paulson@13245 1102 lemma (in M_axioms) Int_closed [intro,simp]: paulson@13223 1103 "[| M(A); M(B) |] ==> M(A Int B)" paulson@13223 1104 apply (subgoal_tac "M({A,B})") paulson@13247 1105 apply (frule Inter_closed, force+) paulson@13223 1106 done paulson@13223 1107 paulson@13290 1108 subsubsection{*Functions and function space*} paulson@13268 1109 paulson@13245 1110 text{*M contains all finite functions*} paulson@13245 1111 lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: paulson@13245 1112 "[| n \ nat; M(A) |] ==> \f \ n -> A. M(f)" paulson@13245 1113 apply (induct_tac n, simp) paulson@13245 1114 apply (rule ballI) paulson@13245 1115 apply (simp add: succ_def) paulson@13245 1116 apply (frule fun_cons_restrict_eq) paulson@13245 1117 apply (erule ssubst) paulson@13245 1118 apply (subgoal_tac "M(f`x) & restrict(f,x) \ x -> A") paulson@13245 1119 apply (simp add: cons_closed nat_into_M apply_closed) paulson@13245 1120 apply (blast intro: apply_funtype transM restrict_type2) paulson@13245 1121 done paulson@13245 1122 paulson@13245 1123 lemma (in M_axioms) finite_fun_closed [rule_format]: paulson@13245 1124 "[| f \ n -> A; n \ nat; M(A) |] ==> M(f)" paulson@13245 1125 by (blast intro: finite_fun_closed_lemma) paulson@13245 1126 paulson@13268 1127 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in paulson@13268 1128 all but trivial cases, A->B cannot be expected to belong to @{term M}.*} paulson@13268 1129 lemma (in M_axioms) is_funspace_abs [simp]: paulson@13268 1130 "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B"; paulson@13268 1131 apply (simp add: is_funspace_def) paulson@13268 1132 apply (rule iffI) paulson@13268 1133 prefer 2 apply blast paulson@13268 1134 apply (rule M_equalityI) paulson@13268 1135 apply simp_all paulson@13268 1136 done paulson@13268 1137 paulson@13268 1138 lemma (in M_axioms) succ_fun_eq2: paulson@13268 1139 "[|M(B); M(n->B)|] ==> paulson@13268 1140 succ(n) -> B = paulson@13268 1141 \{z. p \ (n->B)*B, \f[M]. \b[M]. p = & z = {cons(, f)}}" paulson@13268 1142 apply (simp add: succ_fun_eq) paulson@13268 1143 apply (blast dest: transM) paulson@13268 1144 done paulson@13268 1145 paulson@13268 1146 lemma (in M_axioms) funspace_succ: paulson@13268 1147 "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)" paulson@13306 1148 apply (insert funspace_succ_replacement [of n], simp) paulson@13268 1149 apply (force simp add: succ_fun_eq2 univalent_def) paulson@13268 1150 done paulson@13268 1151 paulson@13268 1152 text{*@{term M} contains all finite function spaces. Needed to prove the paulson@13268 1153 absoluteness of transitive closure.*} paulson@13268 1154 lemma (in M_axioms) finite_funspace_closed [intro,simp]: paulson@13268 1155 "[|n\nat; M(B)|] ==> M(n->B)" paulson@13268 1156 apply (induct_tac n, simp) paulson@13268 1157 apply (simp add: funspace_succ nat_into_M) paulson@13268 1158 done paulson@13268 1159 paulson@13350 1160 paulson@13223 1161 end