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