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