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