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