src/ZF/Constructible/Relative.thy
changeset 13223 45be08fbdcff
child 13245 714f7a423a15
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jun 19 11:48:01 2002 +0200
     1.3 @@ -0,0 +1,956 @@
     1.4 +header {*Relativization and Absoluteness*}
     1.5 +
     1.6 +theory Relative = Main:
     1.7 +
     1.8 +subsection{* Relativized versions of standard set-theoretic concepts *}
     1.9 +
    1.10 +constdefs
    1.11 +  empty :: "[i=>o,i] => o"
    1.12 +    "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
    1.13 +
    1.14 +  subset :: "[i=>o,i,i] => o"
    1.15 +    "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
    1.16 +
    1.17 +  upair :: "[i=>o,i,i,i] => o"
    1.18 +    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
    1.19 +
    1.20 +  pair :: "[i=>o,i,i,i] => o"
    1.21 +    "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
    1.22 +                          (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
    1.23 +
    1.24 +  successor :: "[i=>o,i,i] => o"
    1.25 +    "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
    1.26 +
    1.27 +  powerset :: "[i=>o,i,i] => o"
    1.28 +    "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
    1.29 +
    1.30 +  union :: "[i=>o,i,i,i] => o"
    1.31 +    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
    1.32 +
    1.33 +  inter :: "[i=>o,i,i,i] => o"
    1.34 +    "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
    1.35 +
    1.36 +  setdiff :: "[i=>o,i,i,i] => o"
    1.37 +    "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
    1.38 +
    1.39 +  big_union :: "[i=>o,i,i] => o"
    1.40 +    "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
    1.41 +
    1.42 +  big_inter :: "[i=>o,i,i] => o"
    1.43 +    "big_inter(M,A,z) == 
    1.44 +             (A=0 --> z=0) &
    1.45 +	     (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
    1.46 +
    1.47 +  cartprod :: "[i=>o,i,i,i] => o"
    1.48 +    "cartprod(M,A,B,z) == 
    1.49 +	\<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
    1.50 +
    1.51 +  is_converse :: "[i=>o,i,i] => o"
    1.52 +    "is_converse(M,r,z) == 
    1.53 +	\<forall>x. M(x) --> 
    1.54 +            (x \<in> z <-> 
    1.55 +             (\<exists>w\<in>r. M(w) & 
    1.56 +              (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
    1.57 +
    1.58 +  pre_image :: "[i=>o,i,i,i] => o"
    1.59 +    "pre_image(M,r,A,z) == 
    1.60 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"
    1.61 +
    1.62 +  is_domain :: "[i=>o,i,i] => o"
    1.63 +    "is_domain(M,r,z) == 
    1.64 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"
    1.65 +
    1.66 +  image :: "[i=>o,i,i,i] => o"
    1.67 +    "image(M,r,A,z) == 
    1.68 +        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"
    1.69 +
    1.70 +  is_range :: "[i=>o,i,i] => o"
    1.71 +    --{*the cleaner 
    1.72 +      @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}
    1.73 +      unfortunately needs an instance of separation in order to prove 
    1.74 +        @{term "M(converse(r))"}.*}
    1.75 +    "is_range(M,r,z) == 
    1.76 +	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
    1.77 +
    1.78 +  is_relation :: "[i=>o,i] => o"
    1.79 +    "is_relation(M,r) == 
    1.80 +        (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
    1.81 +
    1.82 +  is_function :: "[i=>o,i] => o"
    1.83 +    "is_function(M,r) == 
    1.84 +	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') --> 
    1.85 +                      pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> 
    1.86 +                      y=y')"
    1.87 +
    1.88 +  fun_apply :: "[i=>o,i,i,i] => o"
    1.89 +    "fun_apply(M,f,x,y) == 
    1.90 +	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"
    1.91 +
    1.92 +  typed_function :: "[i=>o,i,i,i] => o"
    1.93 +    "typed_function(M,A,B,r) == 
    1.94 +        is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    1.95 +        (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    1.96 +
    1.97 +  injection :: "[i=>o,i,i,i] => o"
    1.98 +    "injection(M,A,B,f) == 
    1.99 +	typed_function(M,A,B,f) &
   1.100 +        (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') --> 
   1.101 +                      pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> 
   1.102 +                      x=x')"
   1.103 +
   1.104 +  surjection :: "[i=>o,i,i,i] => o"
   1.105 +    "surjection(M,A,B,f) == 
   1.106 +        typed_function(M,A,B,f) &
   1.107 +        (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"
   1.108 +
   1.109 +  bijection :: "[i=>o,i,i,i] => o"
   1.110 +    "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   1.111 +
   1.112 +  restriction :: "[i=>o,i,i,i] => o"
   1.113 +    "restriction(M,r,A,z) == 
   1.114 +	\<forall>x. M(x) --> 
   1.115 +            (x \<in> z <-> 
   1.116 +             (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"
   1.117 +
   1.118 +  transitive_set :: "[i=>o,i] => o"
   1.119 +    "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"
   1.120 +
   1.121 +  ordinal :: "[i=>o,i] => o"
   1.122 +     --{*an ordinal is a transitive set of transitive sets*}
   1.123 +    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"
   1.124 +
   1.125 +  limit_ordinal :: "[i=>o,i] => o"
   1.126 +    --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   1.127 +    "limit_ordinal(M,a) == 
   1.128 +	ordinal(M,a) & ~ empty(M,a) & 
   1.129 +        (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"
   1.130 +
   1.131 +  successor_ordinal :: "[i=>o,i] => o"
   1.132 +    --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   1.133 +    "successor_ordinal(M,a) == 
   1.134 +	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   1.135 +
   1.136 +  finite_ordinal :: "[i=>o,i] => o"
   1.137 +    --{*an ordinal is finite if neither it nor any of its elements are limit*}
   1.138 +    "finite_ordinal(M,a) == 
   1.139 +	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   1.140 +        (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   1.141 +
   1.142 +  omega :: "[i=>o,i] => o"
   1.143 +    --{*omega is a limit ordinal none of whose elements are limit*}
   1.144 +    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   1.145 +
   1.146 +  number1 :: "[i=>o,i] => o"
   1.147 +    "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"
   1.148 +
   1.149 +  number2 :: "[i=>o,i] => o"
   1.150 +    "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"
   1.151 +
   1.152 +  number3 :: "[i=>o,i] => o"
   1.153 +    "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"
   1.154 +
   1.155 +
   1.156 +subsection {*The relativized ZF axioms*}
   1.157 +constdefs
   1.158 +
   1.159 +  extensionality :: "(i=>o) => o"
   1.160 +    "extensionality(M) == 
   1.161 +	\<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"
   1.162 +
   1.163 +  separation :: "[i=>o, i=>o] => o"
   1.164 +    --{*Big problem: the formula @{text P} should only involve parameters
   1.165 +        belonging to @{text M}.  Don't see how to enforce that.*}
   1.166 +    "separation(M,P) == 
   1.167 +	\<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"
   1.168 +
   1.169 +  upair_ax :: "(i=>o) => o"
   1.170 +    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
   1.171 +
   1.172 +  Union_ax :: "(i=>o) => o"
   1.173 +    "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"
   1.174 +
   1.175 +  power_ax :: "(i=>o) => o"
   1.176 +    "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"
   1.177 +
   1.178 +  univalent :: "[i=>o, i, [i,i]=>o] => o"
   1.179 +    "univalent(M,A,P) == 
   1.180 +	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   1.181 +
   1.182 +  replacement :: "[i=>o, [i,i]=>o] => o"
   1.183 +    "replacement(M,P) == 
   1.184 +      \<forall>A. M(A) --> univalent(M,A,P) -->
   1.185 +      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"
   1.186 +
   1.187 +  strong_replacement :: "[i=>o, [i,i]=>o] => o"
   1.188 +    "strong_replacement(M,P) == 
   1.189 +      \<forall>A. M(A) --> univalent(M,A,P) -->
   1.190 +      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"
   1.191 +
   1.192 +  foundation_ax :: "(i=>o) => o"
   1.193 +    "foundation_ax(M) == 
   1.194 +	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))
   1.195 +                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"
   1.196 +
   1.197 +
   1.198 +subsection{*A trivial consistency proof for $V_\omega$ *}
   1.199 +
   1.200 +text{*We prove that $V_\omega$ 
   1.201 +      (or @{text univ} in Isabelle) satisfies some ZF axioms.
   1.202 +     Kunen, Theorem IV 3.13, page 123.*}
   1.203 +
   1.204 +lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   1.205 +apply (insert Transset_univ [OF Transset_0])  
   1.206 +apply (simp add: Transset_def, blast) 
   1.207 +done
   1.208 +
   1.209 +lemma univ0_Ball_abs [simp]: 
   1.210 +     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.211 +by (blast intro: univ0_downwards_mem) 
   1.212 +
   1.213 +lemma univ0_Bex_abs [simp]: 
   1.214 +     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.215 +by (blast intro: univ0_downwards_mem) 
   1.216 +
   1.217 +text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   1.218 +lemma [cong]:
   1.219 +     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
   1.220 +by (simp add: separation_def) 
   1.221 +
   1.222 +text{*Congruence rules for replacement*}
   1.223 +lemma [cong]:
   1.224 +     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   1.225 +      ==> univalent(M,A,P) <-> univalent(M,A',P')"
   1.226 +by (simp add: univalent_def) 
   1.227 +
   1.228 +lemma [cong]:
   1.229 +     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   1.230 +      ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
   1.231 +by (simp add: strong_replacement_def) 
   1.232 +
   1.233 +text{*The extensionality axiom*}
   1.234 +lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   1.235 +apply (simp add: extensionality_def)
   1.236 +apply (blast intro: univ0_downwards_mem) 
   1.237 +done
   1.238 +
   1.239 +text{*The separation axiom requires some lemmas*}
   1.240 +lemma Collect_in_Vfrom:
   1.241 +     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
   1.242 +apply (drule Transset_Vfrom)
   1.243 +apply (rule subset_mem_Vfrom)
   1.244 +apply (unfold Transset_def, blast)
   1.245 +done
   1.246 +
   1.247 +lemma Collect_in_VLimit:
   1.248 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   1.249 +      ==> Collect(X,P) \<in> Vfrom(A,i)"
   1.250 +apply (rule Limit_VfromE, assumption+)
   1.251 +apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   1.252 +done
   1.253 +
   1.254 +lemma Collect_in_univ:
   1.255 +     "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
   1.256 +by (simp add: univ_def Collect_in_VLimit Limit_nat)
   1.257 +
   1.258 +lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   1.259 +apply (simp add: separation_def)
   1.260 +apply (blast intro: Collect_in_univ Transset_0) 
   1.261 +done
   1.262 +
   1.263 +text{*Unordered pairing axiom*}
   1.264 +lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   1.265 +apply (simp add: upair_ax_def upair_def)  
   1.266 +apply (blast intro: doubleton_in_univ) 
   1.267 +done
   1.268 +
   1.269 +text{*Union axiom*}
   1.270 +lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   1.271 +apply (simp add: Union_ax_def big_union_def)  
   1.272 +apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem) 
   1.273 +done
   1.274 +
   1.275 +text{*Powerset axiom*}
   1.276 +
   1.277 +lemma Pow_in_univ:
   1.278 +     "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
   1.279 +apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   1.280 +done
   1.281 +
   1.282 +lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   1.283 +apply (simp add: power_ax_def powerset_def subset_def)  
   1.284 +apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem) 
   1.285 +done
   1.286 +
   1.287 +text{*Foundation axiom*}
   1.288 +lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   1.289 +apply (simp add: foundation_ax_def, clarify)
   1.290 +apply (cut_tac A=x in foundation, blast) 
   1.291 +done
   1.292 +
   1.293 +lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   1.294 +apply (simp add: replacement_def, clarify) 
   1.295 +oops
   1.296 +text{*no idea: maybe prove by induction on the rank of A?*}
   1.297 +
   1.298 +text{*Still missing: Replacement, Choice*}
   1.299 +
   1.300 +subsection{*lemmas needed to reduce some set constructions to instances
   1.301 +      of Separation*}
   1.302 +
   1.303 +lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   1.304 +apply (rule equalityI, auto) 
   1.305 +apply (simp add: Pair_def, blast) 
   1.306 +done
   1.307 +
   1.308 +lemma vimage_iff_Collect:
   1.309 +     "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   1.310 +apply (rule equalityI, auto) 
   1.311 +apply (simp add: Pair_def, blast) 
   1.312 +done
   1.313 +
   1.314 +text{*These two lemmas lets us prove @{text domain_closed} and 
   1.315 +      @{text range_closed} without new instances of separation*}
   1.316 +
   1.317 +lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   1.318 +apply (rule equalityI, auto)
   1.319 +apply (rule vimageI, assumption)
   1.320 +apply (simp add: Pair_def, blast) 
   1.321 +done
   1.322 +
   1.323 +lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   1.324 +apply (rule equalityI, auto)
   1.325 +apply (rule imageI, assumption)
   1.326 +apply (simp add: Pair_def, blast) 
   1.327 +done
   1.328 +
   1.329 +lemma replacementD:
   1.330 +    "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   1.331 +     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"
   1.332 +by (simp add: replacement_def) 
   1.333 +
   1.334 +lemma strong_replacementD:
   1.335 +    "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   1.336 +     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"
   1.337 +by (simp add: strong_replacement_def) 
   1.338 +
   1.339 +lemma separationD:
   1.340 +    "[| separation(M,P); M(z) |]
   1.341 +     ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"
   1.342 +by (simp add: separation_def) 
   1.343 +
   1.344 +
   1.345 +text{*More constants, for order types*}
   1.346 +constdefs
   1.347 +
   1.348 +  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   1.349 +    "order_isomorphism(M,A,r,B,s,f) == 
   1.350 +        bijection(M,A,B,f) & 
   1.351 +        (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q. 
   1.352 +            M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) --> 
   1.353 +            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   1.354 +            pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"
   1.355 +
   1.356 +
   1.357 +  pred_set :: "[i=>o,i,i,i,i] => o"
   1.358 +    "pred_set(M,A,x,r,B) == 
   1.359 +	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"
   1.360 +
   1.361 +  membership :: "[i=>o,i,i] => o" --{*membership relation*}
   1.362 +    "membership(M,A,r) == 
   1.363 +	\<forall>p. M(p) --> 
   1.364 +             (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"
   1.365 +
   1.366 +
   1.367 +subsection{*Absoluteness for a transitive class model*}
   1.368 +
   1.369 +text{*The class M is assumed to be transitive and to satisfy some
   1.370 +      relativized ZF axioms*}
   1.371 +locale M_axioms =
   1.372 +  fixes M
   1.373 +  assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   1.374 +      and nonempty [simp]:  "M(0)"
   1.375 +      and upair_ax:	    "upair_ax(M)"
   1.376 +      and Union_ax:	    "Union_ax(M)"
   1.377 +      and power_ax:         "power_ax(M)"
   1.378 +      and replacement:      "replacement(M,P)"
   1.379 +  and Inter_separation:
   1.380 +     "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
   1.381 +  and cartprod_separation:
   1.382 +     "[| M(A); M(B) |] 
   1.383 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
   1.384 +  and image_separation:
   1.385 +     "[| M(A); M(r) |] 
   1.386 +      ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
   1.387 +  and vimage_separation:
   1.388 +     "[| M(A); M(r) |] 
   1.389 +      ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
   1.390 +  and converse_separation:
   1.391 +     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) & 
   1.392 +				     pair(M,x,y,p) & pair(M,y,x,z)))"
   1.393 +  and restrict_separation:
   1.394 +     "M(A) 
   1.395 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
   1.396 +  and comp_separation:
   1.397 +     "[| M(r); M(s) |]
   1.398 +      ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
   1.399 +			   (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) & 
   1.400 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
   1.401 +  and pred_separation:
   1.402 +     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
   1.403 +  and Memrel_separation:
   1.404 +     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
   1.405 +  and obase_separation:
   1.406 +     --{*part of the order type formalization*}
   1.407 +     "[| M(A); M(r) |] 
   1.408 +      ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & 
   1.409 +	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   1.410 +	     order_isomorphism(M,par,r,x,mx,g))"
   1.411 +  and well_ord_iso_separation:
   1.412 +     "[| M(A); M(f); M(r) |] 
   1.413 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and> 
   1.414 +		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
   1.415 +  and obase_equals_separation:
   1.416 +     "[| M(A); M(r) |] 
   1.417 +      ==> separation
   1.418 +      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &
   1.419 +	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &
   1.420 +	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   1.421 +	      order_isomorphism(M,pxr,r,y,my,g)))))"
   1.422 +  and is_recfun_separation:
   1.423 +     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   1.424 +     "[| M(A); M(f); M(g); M(a); M(b) |] 
   1.425 +     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
   1.426 +  and omap_replacement:
   1.427 +     "[| M(A); M(r) |] 
   1.428 +      ==> strong_replacement(M,
   1.429 +             \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
   1.430 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   1.431 +	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   1.432 +
   1.433 +lemma (in M_axioms) Ball_abs [simp]: 
   1.434 +     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.435 +by (blast intro: transM) 
   1.436 +
   1.437 +lemma (in M_axioms) Bex_abs [simp]: 
   1.438 +     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.439 +by (blast intro: transM) 
   1.440 +
   1.441 +lemma (in M_axioms) Ball_iff_equiv: 
   1.442 +     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
   1.443 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   1.444 +by (blast intro: transM)
   1.445 +
   1.446 +lemma (in M_axioms) empty_abs [simp]: 
   1.447 +     "M(z) ==> empty(M,z) <-> z=0"
   1.448 +apply (simp add: empty_def)
   1.449 +apply (blast intro: transM) 
   1.450 +done
   1.451 +
   1.452 +lemma (in M_axioms) subset_abs [simp]: 
   1.453 +     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   1.454 +apply (simp add: subset_def) 
   1.455 +apply (blast intro: transM) 
   1.456 +done
   1.457 +
   1.458 +lemma (in M_axioms) upair_abs [simp]: 
   1.459 +     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   1.460 +apply (simp add: upair_def) 
   1.461 +apply (blast intro: transM) 
   1.462 +done
   1.463 +
   1.464 +lemma (in M_axioms) upair_in_M_iff [iff]:
   1.465 +     "M({a,b}) <-> M(a) & M(b)"
   1.466 +apply (insert upair_ax, simp add: upair_ax_def) 
   1.467 +apply (blast intro: transM) 
   1.468 +done
   1.469 +
   1.470 +lemma (in M_axioms) singleton_in_M_iff [iff]:
   1.471 +     "M({a}) <-> M(a)"
   1.472 +by (insert upair_in_M_iff [of a a], simp) 
   1.473 +
   1.474 +lemma (in M_axioms) pair_abs [simp]: 
   1.475 +     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   1.476 +apply (simp add: pair_def ZF.Pair_def)
   1.477 +apply (blast intro: transM) 
   1.478 +done
   1.479 +
   1.480 +lemma (in M_axioms) pair_in_M_iff [iff]:
   1.481 +     "M(<a,b>) <-> M(a) & M(b)"
   1.482 +by (simp add: ZF.Pair_def)
   1.483 +
   1.484 +lemma (in M_axioms) pair_components_in_M:
   1.485 +     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   1.486 +apply (simp add: Pair_def)
   1.487 +apply (blast dest: transM) 
   1.488 +done
   1.489 +
   1.490 +lemma (in M_axioms) cartprod_abs [simp]: 
   1.491 +     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   1.492 +apply (simp add: cartprod_def)
   1.493 +apply (rule iffI) 
   1.494 +apply (blast intro!: equalityI intro: transM dest!: spec) 
   1.495 +apply (blast dest: transM) 
   1.496 +done
   1.497 +
   1.498 +lemma (in M_axioms) union_abs [simp]: 
   1.499 +     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   1.500 +apply (simp add: union_def) 
   1.501 +apply (blast intro: transM) 
   1.502 +done
   1.503 +
   1.504 +lemma (in M_axioms) inter_abs [simp]: 
   1.505 +     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   1.506 +apply (simp add: inter_def) 
   1.507 +apply (blast intro: transM) 
   1.508 +done
   1.509 +
   1.510 +lemma (in M_axioms) setdiff_abs [simp]: 
   1.511 +     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   1.512 +apply (simp add: setdiff_def) 
   1.513 +apply (blast intro: transM) 
   1.514 +done
   1.515 +
   1.516 +lemma (in M_axioms) Union_abs [simp]: 
   1.517 +     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   1.518 +apply (simp add: big_union_def) 
   1.519 +apply (blast intro!: equalityI dest: transM) 
   1.520 +done
   1.521 +
   1.522 +lemma (in M_axioms) Union_closed [intro]:
   1.523 +     "M(A) ==> M(Union(A))"
   1.524 +by (insert Union_ax, simp add: Union_ax_def) 
   1.525 +
   1.526 +lemma (in M_axioms) Un_closed [intro]:
   1.527 +     "[| M(A); M(B) |] ==> M(A Un B)"
   1.528 +by (simp only: Un_eq_Union, blast) 
   1.529 +
   1.530 +lemma (in M_axioms) cons_closed [intro]:
   1.531 +     "[| M(a); M(A) |] ==> M(cons(a,A))"
   1.532 +by (subst cons_eq [symmetric], blast) 
   1.533 +
   1.534 +lemma (in M_axioms) successor_abs [simp]: 
   1.535 +     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
   1.536 +by (simp add: successor_def, blast)  
   1.537 +
   1.538 +lemma (in M_axioms) succ_in_M_iff [iff]:
   1.539 +     "M(succ(a)) <-> M(a)"
   1.540 +apply (simp add: succ_def) 
   1.541 +apply (blast intro: transM) 
   1.542 +done
   1.543 +
   1.544 +lemma (in M_axioms) separation_closed [intro]:
   1.545 +     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   1.546 +apply (insert separation, simp add: separation_def) 
   1.547 +apply (drule spec [THEN mp], assumption, clarify) 
   1.548 +apply (subgoal_tac "y = Collect(A,P)", blast)
   1.549 +apply (blast dest: transM) 
   1.550 +done
   1.551 +
   1.552 +text{*Probably the premise and conclusion are equivalent*}
   1.553 +lemma (in M_axioms) strong_replacementI [rule_format]:
   1.554 +    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   1.555 +     ==> strong_replacement(M,P)"
   1.556 +apply (simp add: strong_replacement_def) 
   1.557 +apply (clarify ); 
   1.558 +apply (frule replacementD [OF replacement]) 
   1.559 +apply assumption
   1.560 +apply (clarify ); 
   1.561 +apply (drule_tac x=A in spec)
   1.562 +apply (clarify );  
   1.563 +apply (drule_tac z=Y in separationD) 
   1.564 +apply assumption; 
   1.565 +apply (clarify ); 
   1.566 +apply (blast dest: transM) 
   1.567 +done
   1.568 +
   1.569 +
   1.570 +(*The last premise expresses that P takes M to M*)
   1.571 +lemma (in M_axioms) strong_replacement_closed [intro]:
   1.572 +     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   1.573 +       !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   1.574 +apply (simp add: strong_replacement_def) 
   1.575 +apply (drule spec [THEN mp], auto) 
   1.576 +apply (subgoal_tac "Replace(A,P) = Y")
   1.577 + apply (simp add: ); 
   1.578 +apply (rule equality_iffI) 
   1.579 +apply (simp add: Replace_iff) 
   1.580 +apply safe;
   1.581 + apply (blast dest: transM) 
   1.582 +apply (frule transM, assumption) 
   1.583 + apply (simp add: univalent_def);
   1.584 + apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
   1.585 + apply (blast dest: transM) 
   1.586 +done
   1.587 +
   1.588 +(*The first premise can't simply be assumed as a schema.
   1.589 +  It is essential to take care when asserting instances of Replacement.
   1.590 +  Let K be a nonconstructible subset of nat and define
   1.591 +  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   1.592 +  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   1.593 +  even for f : M -> M.
   1.594 +*)
   1.595 +lemma (in M_axioms) RepFun_closed [intro]:
   1.596 +     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
   1.597 +      ==> M(RepFun(A,f))"
   1.598 +apply (simp add: RepFun_def) 
   1.599 +apply (rule strong_replacement_closed) 
   1.600 +apply (auto dest: transM  simp add: univalent_def) 
   1.601 +done
   1.602 +
   1.603 +lemma (in M_axioms) converse_abs [simp]: 
   1.604 +     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   1.605 +apply (simp add: is_converse_def)
   1.606 +apply (rule iffI)
   1.607 + apply (rule equalityI) 
   1.608 +  apply (blast dest: transM) 
   1.609 + apply (clarify, frule transM, assumption, simp, blast) 
   1.610 +done
   1.611 +
   1.612 +lemma (in M_axioms) image_abs [simp]: 
   1.613 +     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.614 +apply (simp add: image_def)
   1.615 +apply (rule iffI) 
   1.616 + apply (blast intro!: equalityI dest: transM, blast) 
   1.617 +done
   1.618 +
   1.619 +text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   1.620 +      This result is one direction of absoluteness.*}
   1.621 +
   1.622 +lemma (in M_axioms) powerset_Pow: 
   1.623 +     "powerset(M, x, Pow(x))"
   1.624 +by (simp add: powerset_def)
   1.625 +
   1.626 +text{*But we can't prove that the powerset in @{text M} includes the
   1.627 +      real powerset.*}
   1.628 +lemma (in M_axioms) powerset_imp_subset_Pow: 
   1.629 +     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   1.630 +apply (simp add: powerset_def) 
   1.631 +apply (blast dest: transM) 
   1.632 +done
   1.633 +
   1.634 +lemma (in M_axioms) cartprod_iff_lemma:
   1.635 +     "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   1.636 +       powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
   1.637 +       ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   1.638 +apply (simp add: powerset_def) 
   1.639 +apply (rule equalityI, clarify, simp) 
   1.640 + apply (frule transM, assumption, simp) 
   1.641 + apply blast 
   1.642 +apply clarify
   1.643 +apply (frule transM, assumption, force) 
   1.644 +done
   1.645 +
   1.646 +lemma (in M_axioms) cartprod_iff:
   1.647 +     "[| M(A); M(B); M(C) |] 
   1.648 +      ==> cartprod(M,A,B,C) <-> 
   1.649 +          (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   1.650 +                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   1.651 +apply (simp add: Pair_def cartprod_def, safe)
   1.652 +defer 1 
   1.653 +  apply (simp add: powerset_def) 
   1.654 + apply blast 
   1.655 +txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   1.656 +apply (insert power_ax, simp add: power_ax_def) 
   1.657 +apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.658 +apply (erule impE, blast, clarify) 
   1.659 +apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.660 +apply (blast intro: cartprod_iff_lemma) 
   1.661 +done
   1.662 +
   1.663 +lemma (in M_axioms) cartprod_closed_lemma:
   1.664 +     "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"
   1.665 +apply (simp del: cartprod_abs add: cartprod_iff)
   1.666 +apply (insert power_ax, simp add: power_ax_def) 
   1.667 +apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.668 +apply (erule impE, blast, clarify) 
   1.669 +apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   1.670 +apply (erule impE, blast, clarify)
   1.671 +apply (intro exI conjI) 
   1.672 +prefer 6 apply (rule refl) 
   1.673 +prefer 4 apply assumption
   1.674 +prefer 4 apply assumption
   1.675 +apply (insert cartprod_separation [of A B], simp, blast+)
   1.676 +done
   1.677 +
   1.678 +
   1.679 +text{*All the lemmas above are necessary because Powerset is not absolute.
   1.680 +      I should have used Replacement instead!*}
   1.681 +lemma (in M_axioms) cartprod_closed [intro]: 
   1.682 +     "[| M(A); M(B) |] ==> M(A*B)"
   1.683 +by (frule cartprod_closed_lemma, assumption, force)
   1.684 +
   1.685 +lemma (in M_axioms) image_closed [intro]: 
   1.686 +     "[| M(A); M(r) |] ==> M(r``A)"
   1.687 +apply (simp add: image_iff_Collect)
   1.688 +apply (insert image_separation [of A r], simp, blast) 
   1.689 +done
   1.690 +
   1.691 +lemma (in M_axioms) vimage_abs [simp]: 
   1.692 +     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   1.693 +apply (simp add: pre_image_def)
   1.694 +apply (rule iffI) 
   1.695 + apply (blast intro!: equalityI dest: transM, blast) 
   1.696 +done
   1.697 +
   1.698 +lemma (in M_axioms) vimage_closed [intro]: 
   1.699 +     "[| M(A); M(r) |] ==> M(r-``A)"
   1.700 +apply (simp add: vimage_iff_Collect)
   1.701 +apply (insert vimage_separation [of A r], simp, blast) 
   1.702 +done
   1.703 +
   1.704 +lemma (in M_axioms) domain_abs [simp]: 
   1.705 +     "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   1.706 +apply (simp add: is_domain_def) 
   1.707 +apply (blast intro!: equalityI dest: transM) 
   1.708 +done
   1.709 +
   1.710 +lemma (in M_axioms) domain_closed [intro]: 
   1.711 +     "M(r) ==> M(domain(r))"
   1.712 +apply (simp add: domain_eq_vimage)
   1.713 +apply (blast intro: vimage_closed) 
   1.714 +done
   1.715 +
   1.716 +lemma (in M_axioms) range_abs [simp]: 
   1.717 +     "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   1.718 +apply (simp add: is_range_def)
   1.719 +apply (blast intro!: equalityI dest: transM)
   1.720 +done
   1.721 +
   1.722 +lemma (in M_axioms) range_closed [intro]: 
   1.723 +     "M(r) ==> M(range(r))"
   1.724 +apply (simp add: range_eq_image)
   1.725 +apply (blast intro: image_closed) 
   1.726 +done
   1.727 +
   1.728 +lemma (in M_axioms) M_converse_iff:
   1.729 +     "M(r) ==> 
   1.730 +      converse(r) = 
   1.731 +      {z \<in> range(r) * domain(r). 
   1.732 +        \<exists>p\<in>r. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"
   1.733 +by (blast dest: transM)
   1.734 +
   1.735 +lemma (in M_axioms) converse_closed [intro]: 
   1.736 +     "M(r) ==> M(converse(r))"
   1.737 +apply (simp add: M_converse_iff)
   1.738 +apply (insert converse_separation [of r], simp) 
   1.739 +apply (blast intro: image_closed) 
   1.740 +done
   1.741 +
   1.742 +lemma (in M_axioms) relation_abs [simp]: 
   1.743 +     "M(r) ==> is_relation(M,r) <-> relation(r)"
   1.744 +apply (simp add: is_relation_def relation_def) 
   1.745 +apply (blast dest!: bspec dest: pair_components_in_M)+
   1.746 +done
   1.747 +
   1.748 +lemma (in M_axioms) function_abs [simp]: 
   1.749 +     "M(r) ==> is_function(M,r) <-> function(r)"
   1.750 +apply (simp add: is_function_def function_def, safe) 
   1.751 +   apply (frule transM, assumption) 
   1.752 +  apply (blast dest: pair_components_in_M)+
   1.753 +done
   1.754 +
   1.755 +lemma (in M_axioms) apply_closed [intro]: 
   1.756 +     "[|M(f); M(a)|] ==> M(f`a)"
   1.757 +apply (simp add: apply_def) 
   1.758 +apply (blast intro: elim:); 
   1.759 +done
   1.760 +
   1.761 +lemma (in M_axioms) apply_abs: 
   1.762 +     "[| function(f); M(f); M(y) |] 
   1.763 +      ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
   1.764 +apply (simp add: fun_apply_def)
   1.765 +apply (blast intro: function_apply_equality function_apply_Pair) 
   1.766 +done
   1.767 +
   1.768 +lemma (in M_axioms) typed_apply_abs: 
   1.769 +     "[| f \<in> A -> B; M(f); M(y) |] 
   1.770 +      ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
   1.771 +by (simp add: apply_abs fun_is_function domain_of_fun) 
   1.772 +
   1.773 +lemma (in M_axioms) typed_function_abs [simp]: 
   1.774 +     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   1.775 +apply (auto simp add: typed_function_def relation_def Pi_iff) 
   1.776 +apply (blast dest: pair_components_in_M)+
   1.777 +done
   1.778 +
   1.779 +lemma (in M_axioms) injection_abs [simp]: 
   1.780 +     "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   1.781 +apply (simp add: injection_def apply_iff inj_def apply_closed)
   1.782 +apply (blast dest: transM [of _ A]); 
   1.783 +done
   1.784 +
   1.785 +lemma (in M_axioms) surjection_abs [simp]: 
   1.786 +     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   1.787 +by (simp add: typed_apply_abs surjection_def surj_def)
   1.788 +
   1.789 +lemma (in M_axioms) bijection_abs [simp]: 
   1.790 +     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   1.791 +by (simp add: bijection_def bij_def)
   1.792 +
   1.793 +text{*no longer needed*}
   1.794 +lemma (in M_axioms) restriction_is_function: 
   1.795 +     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   1.796 +      ==> function(z)"
   1.797 +apply (rotate_tac 1)
   1.798 +apply (simp add: restriction_def Ball_iff_equiv) 
   1.799 +apply (unfold function_def, blast) 
   1.800 +done
   1.801 +
   1.802 +lemma (in M_axioms) restriction_abs [simp]: 
   1.803 +     "[| M(f); M(A); M(z) |] 
   1.804 +      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   1.805 +apply (simp add: Ball_iff_equiv restriction_def restrict_def)
   1.806 +apply (blast intro!: equalityI dest: transM) 
   1.807 +done
   1.808 +
   1.809 +
   1.810 +lemma (in M_axioms) M_restrict_iff:
   1.811 +     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
   1.812 +by (simp add: restrict_def, blast dest: transM)
   1.813 +
   1.814 +lemma (in M_axioms) restrict_closed [intro]: 
   1.815 +     "[| M(A); M(r) |] ==> M(restrict(r,A))"
   1.816 +apply (simp add: M_restrict_iff)
   1.817 +apply (insert restrict_separation [of A], simp, blast) 
   1.818 +done
   1.819 +
   1.820 +
   1.821 +lemma (in M_axioms) M_comp_iff:
   1.822 +     "[| M(r); M(s) |] 
   1.823 +      ==> r O s = 
   1.824 +          {xz \<in> domain(s) * range(r).  
   1.825 +            \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and> 
   1.826 +                xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
   1.827 +apply (simp add: comp_def)
   1.828 +apply (rule equalityI) 
   1.829 + apply (clarify ); 
   1.830 + apply (simp add: ); 
   1.831 + apply  (blast dest:  transM)+
   1.832 +done
   1.833 +
   1.834 +lemma (in M_axioms) comp_closed [intro]: 
   1.835 +     "[| M(r); M(s) |] ==> M(r O s)"
   1.836 +apply (simp add: M_comp_iff)
   1.837 +apply (insert comp_separation [of r s], simp, blast) 
   1.838 +done
   1.839 +
   1.840 +lemma (in M_axioms) nat_into_M [intro]:
   1.841 +     "n \<in> nat ==> M(n)"
   1.842 +by (induct n rule: nat_induct, simp_all)
   1.843 +
   1.844 +lemma (in M_axioms) Inl_in_M_iff [iff]:
   1.845 +     "M(Inl(a)) <-> M(a)"
   1.846 +by (simp add: Inl_def) 
   1.847 +
   1.848 +lemma (in M_axioms) Inr_in_M_iff [iff]:
   1.849 +     "M(Inr(a)) <-> M(a)"
   1.850 +by (simp add: Inr_def) 
   1.851 +
   1.852 +lemma (in M_axioms) Inter_abs [simp]: 
   1.853 +     "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
   1.854 +apply (simp add: big_inter_def Inter_def) 
   1.855 +apply (blast intro!: equalityI dest: transM) 
   1.856 +done
   1.857 +
   1.858 +lemma (in M_axioms) Inter_closed [intro]:
   1.859 +     "M(A) ==> M(Inter(A))"
   1.860 +by (insert Inter_separation, simp add: Inter_def, blast)
   1.861 +
   1.862 +lemma (in M_axioms) Int_closed [intro]:
   1.863 +     "[| M(A); M(B) |] ==> M(A Int B)"
   1.864 +apply (subgoal_tac "M({A,B})")
   1.865 +apply (frule Inter_closed, force+); 
   1.866 +done
   1.867 +
   1.868 +subsection{*Absoluteness for ordinals*}
   1.869 +text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   1.870 +
   1.871 +lemma (in M_axioms) lt_closed:
   1.872 +     "[| j<i; M(i) |] ==> M(j)" 
   1.873 +by (blast dest: ltD intro: transM) 
   1.874 +
   1.875 +lemma (in M_axioms) transitive_set_abs [simp]: 
   1.876 +     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   1.877 +by (simp add: transitive_set_def Transset_def)
   1.878 +
   1.879 +lemma (in M_axioms) ordinal_abs [simp]: 
   1.880 +     "M(a) ==> ordinal(M,a) <-> Ord(a)"
   1.881 +by (simp add: ordinal_def Ord_def)
   1.882 +
   1.883 +lemma (in M_axioms) limit_ordinal_abs [simp]: 
   1.884 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   1.885 +apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   1.886 +apply (simp add: lt_def, blast) 
   1.887 +done
   1.888 +
   1.889 +lemma (in M_axioms) successor_ordinal_abs [simp]: 
   1.890 +     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
   1.891 +apply (simp add: successor_ordinal_def, safe)
   1.892 +apply (drule Ord_cases_disj, auto) 
   1.893 +done
   1.894 +
   1.895 +lemma finite_Ord_is_nat:
   1.896 +      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   1.897 +by (induct a rule: trans_induct3, simp_all)
   1.898 +
   1.899 +lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   1.900 +by (induct a rule: nat_induct, auto)
   1.901 +
   1.902 +lemma (in M_axioms) finite_ordinal_abs [simp]: 
   1.903 +     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   1.904 +apply (simp add: finite_ordinal_def)
   1.905 +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   1.906 +             dest: Ord_trans naturals_not_limit)
   1.907 +done
   1.908 +
   1.909 +lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   1.910 +apply (rule le_anti_sym) 
   1.911 +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   1.912 + apply (simp add: lt_def)  
   1.913 + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   1.914 +apply (erule nat_le_Limit)
   1.915 +done
   1.916 +
   1.917 +lemma (in M_axioms) omega_abs [simp]: 
   1.918 +     "M(a) ==> omega(M,a) <-> a = nat"
   1.919 +apply (simp add: omega_def) 
   1.920 +apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   1.921 +done
   1.922 +
   1.923 +lemma (in M_axioms) number1_abs [simp]: 
   1.924 +     "M(a) ==> number1(M,a) <-> a = 1"
   1.925 +by (simp add: number1_def) 
   1.926 +
   1.927 +lemma (in M_axioms) number1_abs [simp]: 
   1.928 +     "M(a) ==> number2(M,a) <-> a = succ(1)"
   1.929 +by (simp add: number2_def) 
   1.930 +
   1.931 +lemma (in M_axioms) number3_abs [simp]: 
   1.932 +     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   1.933 +by (simp add: number3_def) 
   1.934 +
   1.935 +text{*Kunen continued to 20...*}
   1.936 +
   1.937 +(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   1.938 +  but the recursion variable must stay unchanged.  But then the recursion
   1.939 +  equations only hold for x\<in>nat (or in some other set) and not for the 
   1.940 +  whole of the class M.
   1.941 +  consts
   1.942 +    natnumber_aux :: "[i=>o,i] => i"
   1.943 +
   1.944 +  primrec
   1.945 +      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   1.946 +      "natnumber_aux(M,succ(n)) = 
   1.947 +	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   1.948 +		     then 1 else 0)"
   1.949 +
   1.950 +  constdefs
   1.951 +    natnumber :: "[i=>o,i,i] => o"
   1.952 +      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   1.953 +
   1.954 +  lemma (in M_axioms) [simp]: 
   1.955 +       "natnumber(M,0,x) == x=0"
   1.956 +*)
   1.957 +
   1.958 +
   1.959 +end