src/ZF/Constructible/Relative.thy
changeset 13290 28ce81eff3de
parent 13269 3ba9be497c33
child 13298 b4f370679c65
     1.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 04 10:50:24 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Thu Jul 04 10:51:52 2002 +0200
     1.3 @@ -171,13 +171,13 @@
     1.4  
     1.5    extensionality :: "(i=>o) => o"
     1.6      "extensionality(M) == 
     1.7 -	\<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"
     1.8 +	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
     1.9  
    1.10    separation :: "[i=>o, i=>o] => o"
    1.11      --{*Big problem: the formula @{text P} should only involve parameters
    1.12          belonging to @{text M}.  Don't see how to enforce that.*}
    1.13      "separation(M,P) == 
    1.14 -	\<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"
    1.15 +	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
    1.16  
    1.17    upair_ax :: "(i=>o) => o"
    1.18      "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
    1.19 @@ -269,8 +269,9 @@
    1.20  by (simp add: univ_def Collect_in_VLimit Limit_nat)
    1.21  
    1.22  lemma "separation(\<lambda>x. x \<in> univ(0), P)"
    1.23 -apply (simp add: separation_def)
    1.24 -apply (blast intro: Collect_in_univ Transset_0) 
    1.25 +apply (simp add: separation_def, clarify) 
    1.26 +apply (rule_tac x = "Collect(x,P)" in bexI) 
    1.27 +apply (blast intro: Collect_in_univ Transset_0)+
    1.28  done
    1.29  
    1.30  text{*Unordered pairing axiom*}
    1.31 @@ -350,8 +351,7 @@
    1.32  by (simp add: strong_replacement_def) 
    1.33  
    1.34  lemma separationD:
    1.35 -    "[| separation(M,P); M(z) |]
    1.36 -     ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"
    1.37 +    "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
    1.38  by (simp add: separation_def) 
    1.39  
    1.40  
    1.41 @@ -381,7 +381,7 @@
    1.42  
    1.43  text{*The class M is assumed to be transitive and to satisfy some
    1.44        relativized ZF axioms*}
    1.45 -locale M_axioms =
    1.46 +locale M_triv_axioms =
    1.47    fixes M
    1.48    assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
    1.49        and nonempty [simp]:  "M(0)"
    1.50 @@ -390,7 +390,326 @@
    1.51        and power_ax:         "power_ax(M)"
    1.52        and replacement:      "replacement(M,P)"
    1.53        and M_nat [iff]:      "M(nat)"           (*i.e. the axiom of infinity*)
    1.54 -  and Inter_separation:
    1.55 +
    1.56 +lemma (in M_triv_axioms) ball_abs [simp]: 
    1.57 +     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    1.58 +by (blast intro: transM) 
    1.59 +
    1.60 +lemma (in M_triv_axioms) rall_abs [simp]: 
    1.61 +     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
    1.62 +by (blast intro: transM) 
    1.63 +
    1.64 +lemma (in M_triv_axioms) bex_abs [simp]: 
    1.65 +     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    1.66 +by (blast intro: transM) 
    1.67 +
    1.68 +lemma (in M_triv_axioms) rex_abs [simp]: 
    1.69 +     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
    1.70 +by (blast intro: transM) 
    1.71 +
    1.72 +lemma (in M_triv_axioms) ball_iff_equiv: 
    1.73 +     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
    1.74 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
    1.75 +by (blast intro: transM)
    1.76 +
    1.77 +text{*Simplifies proofs of equalities when there's an iff-equality
    1.78 +      available for rewriting, universally quantified over M. *}
    1.79 +lemma (in M_triv_axioms) M_equalityI: 
    1.80 +     "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
    1.81 +by (blast intro!: equalityI dest: transM) 
    1.82 +
    1.83 +lemma (in M_triv_axioms) empty_abs [simp]: 
    1.84 +     "M(z) ==> empty(M,z) <-> z=0"
    1.85 +apply (simp add: empty_def)
    1.86 +apply (blast intro: transM) 
    1.87 +done
    1.88 +
    1.89 +lemma (in M_triv_axioms) subset_abs [simp]: 
    1.90 +     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
    1.91 +apply (simp add: subset_def) 
    1.92 +apply (blast intro: transM) 
    1.93 +done
    1.94 +
    1.95 +lemma (in M_triv_axioms) upair_abs [simp]: 
    1.96 +     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
    1.97 +apply (simp add: upair_def) 
    1.98 +apply (blast intro: transM) 
    1.99 +done
   1.100 +
   1.101 +lemma (in M_triv_axioms) upair_in_M_iff [iff]:
   1.102 +     "M({a,b}) <-> M(a) & M(b)"
   1.103 +apply (insert upair_ax, simp add: upair_ax_def) 
   1.104 +apply (blast intro: transM) 
   1.105 +done
   1.106 +
   1.107 +lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
   1.108 +     "M({a}) <-> M(a)"
   1.109 +by (insert upair_in_M_iff [of a a], simp) 
   1.110 +
   1.111 +lemma (in M_triv_axioms) pair_abs [simp]: 
   1.112 +     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   1.113 +apply (simp add: pair_def ZF.Pair_def)
   1.114 +apply (blast intro: transM) 
   1.115 +done
   1.116 +
   1.117 +lemma (in M_triv_axioms) pair_in_M_iff [iff]:
   1.118 +     "M(<a,b>) <-> M(a) & M(b)"
   1.119 +by (simp add: ZF.Pair_def)
   1.120 +
   1.121 +lemma (in M_triv_axioms) pair_components_in_M:
   1.122 +     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   1.123 +apply (simp add: Pair_def)
   1.124 +apply (blast dest: transM) 
   1.125 +done
   1.126 +
   1.127 +lemma (in M_triv_axioms) cartprod_abs [simp]: 
   1.128 +     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   1.129 +apply (simp add: cartprod_def)
   1.130 +apply (rule iffI) 
   1.131 + apply (blast intro!: equalityI intro: transM dest!: rspec) 
   1.132 +apply (blast dest: transM) 
   1.133 +done
   1.134 +
   1.135 +lemma (in M_triv_axioms) union_abs [simp]: 
   1.136 +     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   1.137 +apply (simp add: union_def) 
   1.138 +apply (blast intro: transM) 
   1.139 +done
   1.140 +
   1.141 +lemma (in M_triv_axioms) inter_abs [simp]: 
   1.142 +     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   1.143 +apply (simp add: inter_def) 
   1.144 +apply (blast intro: transM) 
   1.145 +done
   1.146 +
   1.147 +lemma (in M_triv_axioms) setdiff_abs [simp]: 
   1.148 +     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   1.149 +apply (simp add: setdiff_def) 
   1.150 +apply (blast intro: transM) 
   1.151 +done
   1.152 +
   1.153 +lemma (in M_triv_axioms) Union_abs [simp]: 
   1.154 +     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   1.155 +apply (simp add: big_union_def) 
   1.156 +apply (blast intro!: equalityI dest: transM) 
   1.157 +done
   1.158 +
   1.159 +lemma (in M_triv_axioms) Union_closed [intro,simp]:
   1.160 +     "M(A) ==> M(Union(A))"
   1.161 +by (insert Union_ax, simp add: Union_ax_def) 
   1.162 +
   1.163 +lemma (in M_triv_axioms) Un_closed [intro,simp]:
   1.164 +     "[| M(A); M(B) |] ==> M(A Un B)"
   1.165 +by (simp only: Un_eq_Union, blast) 
   1.166 +
   1.167 +lemma (in M_triv_axioms) cons_closed [intro,simp]:
   1.168 +     "[| M(a); M(A) |] ==> M(cons(a,A))"
   1.169 +by (subst cons_eq [symmetric], blast) 
   1.170 +
   1.171 +lemma (in M_triv_axioms) successor_abs [simp]: 
   1.172 +     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
   1.173 +by (simp add: successor_def, blast)  
   1.174 +
   1.175 +lemma (in M_triv_axioms) succ_in_M_iff [iff]:
   1.176 +     "M(succ(a)) <-> M(a)"
   1.177 +apply (simp add: succ_def) 
   1.178 +apply (blast intro: transM) 
   1.179 +done
   1.180 +
   1.181 +lemma (in M_triv_axioms) separation_closed [intro,simp]:
   1.182 +     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   1.183 +apply (insert separation, simp add: separation_def) 
   1.184 +apply (drule rspec, assumption, clarify) 
   1.185 +apply (subgoal_tac "y = Collect(A,P)", blast)
   1.186 +apply (blast dest: transM) 
   1.187 +done
   1.188 +
   1.189 +text{*Probably the premise and conclusion are equivalent*}
   1.190 +lemma (in M_triv_axioms) strong_replacementI [rule_format]:
   1.191 +    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   1.192 +     ==> strong_replacement(M,P)"
   1.193 +apply (simp add: strong_replacement_def, clarify) 
   1.194 +apply (frule replacementD [OF replacement], assumption, clarify) 
   1.195 +apply (drule_tac x=A in spec, clarify)  
   1.196 +apply (drule_tac z=Y in separationD, assumption, clarify) 
   1.197 +apply (blast dest: transM) 
   1.198 +done
   1.199 +
   1.200 +
   1.201 +(*The last premise expresses that P takes M to M*)
   1.202 +lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   1.203 +     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   1.204 +       !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   1.205 +apply (simp add: strong_replacement_def) 
   1.206 +apply (drule spec [THEN mp], auto) 
   1.207 +apply (subgoal_tac "Replace(A,P) = Y")
   1.208 + apply simp 
   1.209 +apply (rule equality_iffI) 
   1.210 +apply (simp add: Replace_iff, safe)
   1.211 + apply (blast dest: transM) 
   1.212 +apply (frule transM, assumption) 
   1.213 + apply (simp add: univalent_def)
   1.214 + apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
   1.215 + apply (blast dest: transM) 
   1.216 +done
   1.217 +
   1.218 +(*The first premise can't simply be assumed as a schema.
   1.219 +  It is essential to take care when asserting instances of Replacement.
   1.220 +  Let K be a nonconstructible subset of nat and define
   1.221 +  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   1.222 +  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   1.223 +  even for f : M -> M.
   1.224 +*)
   1.225 +lemma (in M_triv_axioms) RepFun_closed [intro,simp]:
   1.226 +     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   1.227 +      ==> M(RepFun(A,f))"
   1.228 +apply (simp add: RepFun_def) 
   1.229 +apply (rule strong_replacement_closed) 
   1.230 +apply (auto dest: transM  simp add: univalent_def) 
   1.231 +done
   1.232 +
   1.233 +lemma (in M_triv_axioms) lam_closed [intro,simp]:
   1.234 +     "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   1.235 +      ==> M(\<lambda>x\<in>A. b(x))"
   1.236 +by (simp add: lam_def, blast dest: transM) 
   1.237 +
   1.238 +lemma (in M_triv_axioms) image_abs [simp]: 
   1.239 +     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.240 +apply (simp add: image_def)
   1.241 +apply (rule iffI) 
   1.242 + apply (blast intro!: equalityI dest: transM, blast) 
   1.243 +done
   1.244 +
   1.245 +text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   1.246 +      This result is one direction of absoluteness.*}
   1.247 +
   1.248 +lemma (in M_triv_axioms) powerset_Pow: 
   1.249 +     "powerset(M, x, Pow(x))"
   1.250 +by (simp add: powerset_def)
   1.251 +
   1.252 +text{*But we can't prove that the powerset in @{text M} includes the
   1.253 +      real powerset.*}
   1.254 +lemma (in M_triv_axioms) powerset_imp_subset_Pow: 
   1.255 +     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   1.256 +apply (simp add: powerset_def) 
   1.257 +apply (blast dest: transM) 
   1.258 +done
   1.259 +
   1.260 +lemma (in M_triv_axioms) nat_into_M [intro]:
   1.261 +     "n \<in> nat ==> M(n)"
   1.262 +by (induct n rule: nat_induct, simp_all)
   1.263 +
   1.264 +lemma (in M_triv_axioms) nat_case_closed:
   1.265 +  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   1.266 +apply (case_tac "k=0", simp) 
   1.267 +apply (case_tac "\<exists>m. k = succ(m)", force)
   1.268 +apply (simp add: nat_case_def) 
   1.269 +done
   1.270 +
   1.271 +lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
   1.272 +     "M(Inl(a)) <-> M(a)"
   1.273 +by (simp add: Inl_def) 
   1.274 +
   1.275 +lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
   1.276 +     "M(Inr(a)) <-> M(a)"
   1.277 +by (simp add: Inr_def)
   1.278 +
   1.279 +
   1.280 +subsection{*Absoluteness for ordinals*}
   1.281 +text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   1.282 +
   1.283 +lemma (in M_triv_axioms) lt_closed:
   1.284 +     "[| j<i; M(i) |] ==> M(j)" 
   1.285 +by (blast dest: ltD intro: transM) 
   1.286 +
   1.287 +lemma (in M_triv_axioms) transitive_set_abs [simp]: 
   1.288 +     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   1.289 +by (simp add: transitive_set_def Transset_def)
   1.290 +
   1.291 +lemma (in M_triv_axioms) ordinal_abs [simp]: 
   1.292 +     "M(a) ==> ordinal(M,a) <-> Ord(a)"
   1.293 +by (simp add: ordinal_def Ord_def)
   1.294 +
   1.295 +lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
   1.296 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   1.297 +apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   1.298 +apply (simp add: lt_def, blast) 
   1.299 +done
   1.300 +
   1.301 +lemma (in M_triv_axioms) successor_ordinal_abs [simp]: 
   1.302 +     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
   1.303 +apply (simp add: successor_ordinal_def, safe)
   1.304 +apply (drule Ord_cases_disj, auto) 
   1.305 +done
   1.306 +
   1.307 +lemma finite_Ord_is_nat:
   1.308 +      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   1.309 +by (induct a rule: trans_induct3, simp_all)
   1.310 +
   1.311 +lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   1.312 +by (induct a rule: nat_induct, auto)
   1.313 +
   1.314 +lemma (in M_triv_axioms) finite_ordinal_abs [simp]: 
   1.315 +     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   1.316 +apply (simp add: finite_ordinal_def)
   1.317 +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   1.318 +             dest: Ord_trans naturals_not_limit)
   1.319 +done
   1.320 +
   1.321 +lemma Limit_non_Limit_implies_nat:
   1.322 +     "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   1.323 +apply (rule le_anti_sym) 
   1.324 +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   1.325 + apply (simp add: lt_def)  
   1.326 + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   1.327 +apply (erule nat_le_Limit)
   1.328 +done
   1.329 +
   1.330 +lemma (in M_triv_axioms) omega_abs [simp]: 
   1.331 +     "M(a) ==> omega(M,a) <-> a = nat"
   1.332 +apply (simp add: omega_def) 
   1.333 +apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   1.334 +done
   1.335 +
   1.336 +lemma (in M_triv_axioms) number1_abs [simp]: 
   1.337 +     "M(a) ==> number1(M,a) <-> a = 1"
   1.338 +by (simp add: number1_def) 
   1.339 +
   1.340 +lemma (in M_triv_axioms) number1_abs [simp]: 
   1.341 +     "M(a) ==> number2(M,a) <-> a = succ(1)"
   1.342 +by (simp add: number2_def) 
   1.343 +
   1.344 +lemma (in M_triv_axioms) number3_abs [simp]: 
   1.345 +     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   1.346 +by (simp add: number3_def) 
   1.347 +
   1.348 +text{*Kunen continued to 20...*}
   1.349 +
   1.350 +(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   1.351 +  but the recursion variable must stay unchanged.  But then the recursion
   1.352 +  equations only hold for x\<in>nat (or in some other set) and not for the 
   1.353 +  whole of the class M.
   1.354 +  consts
   1.355 +    natnumber_aux :: "[i=>o,i] => i"
   1.356 +
   1.357 +  primrec
   1.358 +      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   1.359 +      "natnumber_aux(M,succ(n)) = 
   1.360 +	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   1.361 +		     then 1 else 0)"
   1.362 +
   1.363 +  constdefs
   1.364 +    natnumber :: "[i=>o,i,i] => o"
   1.365 +      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   1.366 +
   1.367 +  lemma (in M_triv_axioms) [simp]: 
   1.368 +       "natnumber(M,0,x) == x=0"
   1.369 +*)
   1.370 +
   1.371 +subsection{*Some instances of separation and strong replacement*}
   1.372 +
   1.373 +locale M_axioms = M_triv_axioms +
   1.374 +assumes Inter_separation:
   1.375       "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
   1.376    and cartprod_separation:
   1.377       "[| M(A); M(B) |] 
   1.378 @@ -398,9 +717,6 @@
   1.379    and image_separation:
   1.380       "[| M(A); M(r) |] 
   1.381        ==> separation(M, \<lambda>y. \<exists>p[M]. p\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,p)))"
   1.382 -  and vimage_separation:
   1.383 -     "[| M(A); M(r) |] 
   1.384 -      ==> separation(M, \<lambda>x. \<exists>p[M]. p\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,p)))"
   1.385    and converse_separation:
   1.386       "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. 
   1.387                      M(p) & (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,p) & pair(M,y,x,z)))"
   1.388 @@ -447,219 +763,13 @@
   1.389  	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   1.390  	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   1.391  
   1.392 -lemma (in M_axioms) ball_abs [simp]: 
   1.393 -     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.394 -by (blast intro: transM) 
   1.395 -
   1.396 -lemma (in M_axioms) rall_abs [simp]: 
   1.397 -     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   1.398 -by (blast intro: transM) 
   1.399 -
   1.400 -lemma (in M_axioms) bex_abs [simp]: 
   1.401 -     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.402 -by (blast intro: transM) 
   1.403 -
   1.404 -lemma (in M_axioms) rex_abs [simp]: 
   1.405 -     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   1.406 -by (blast intro: transM) 
   1.407 -
   1.408 -lemma (in M_axioms) ball_iff_equiv: 
   1.409 -     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
   1.410 -               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   1.411 -by (blast intro: transM)
   1.412 -
   1.413 -text{*Simplifies proofs of equalities when there's an iff-equality
   1.414 -      available for rewriting, universally quantified over M. *}
   1.415 -lemma (in M_axioms) M_equalityI: 
   1.416 -     "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
   1.417 -by (blast intro!: equalityI dest: transM) 
   1.418 -
   1.419 -lemma (in M_axioms) empty_abs [simp]: 
   1.420 -     "M(z) ==> empty(M,z) <-> z=0"
   1.421 -apply (simp add: empty_def)
   1.422 -apply (blast intro: transM) 
   1.423 -done
   1.424 -
   1.425 -lemma (in M_axioms) subset_abs [simp]: 
   1.426 -     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   1.427 -apply (simp add: subset_def) 
   1.428 -apply (blast intro: transM) 
   1.429 -done
   1.430 -
   1.431 -lemma (in M_axioms) upair_abs [simp]: 
   1.432 -     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   1.433 -apply (simp add: upair_def) 
   1.434 -apply (blast intro: transM) 
   1.435 -done
   1.436 -
   1.437 -lemma (in M_axioms) upair_in_M_iff [iff]:
   1.438 -     "M({a,b}) <-> M(a) & M(b)"
   1.439 -apply (insert upair_ax, simp add: upair_ax_def) 
   1.440 -apply (blast intro: transM) 
   1.441 -done
   1.442 -
   1.443 -lemma (in M_axioms) singleton_in_M_iff [iff]:
   1.444 -     "M({a}) <-> M(a)"
   1.445 -by (insert upair_in_M_iff [of a a], simp) 
   1.446 -
   1.447 -lemma (in M_axioms) pair_abs [simp]: 
   1.448 -     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   1.449 -apply (simp add: pair_def ZF.Pair_def)
   1.450 -apply (blast intro: transM) 
   1.451 -done
   1.452 -
   1.453 -lemma (in M_axioms) pair_in_M_iff [iff]:
   1.454 -     "M(<a,b>) <-> M(a) & M(b)"
   1.455 -by (simp add: ZF.Pair_def)
   1.456 -
   1.457 -lemma (in M_axioms) pair_components_in_M:
   1.458 -     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   1.459 -apply (simp add: Pair_def)
   1.460 -apply (blast dest: transM) 
   1.461 -done
   1.462 -
   1.463 -lemma (in M_axioms) cartprod_abs [simp]: 
   1.464 -     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   1.465 -apply (simp add: cartprod_def)
   1.466 -apply (rule iffI) 
   1.467 - apply (blast intro!: equalityI intro: transM dest!: rspec) 
   1.468 -apply (blast dest: transM) 
   1.469 -done
   1.470 -
   1.471 -lemma (in M_axioms) union_abs [simp]: 
   1.472 -     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   1.473 -apply (simp add: union_def) 
   1.474 -apply (blast intro: transM) 
   1.475 -done
   1.476 -
   1.477 -lemma (in M_axioms) inter_abs [simp]: 
   1.478 -     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   1.479 -apply (simp add: inter_def) 
   1.480 -apply (blast intro: transM) 
   1.481 -done
   1.482 -
   1.483 -lemma (in M_axioms) setdiff_abs [simp]: 
   1.484 -     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   1.485 -apply (simp add: setdiff_def) 
   1.486 -apply (blast intro: transM) 
   1.487 -done
   1.488 -
   1.489 -lemma (in M_axioms) Union_abs [simp]: 
   1.490 -     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   1.491 -apply (simp add: big_union_def) 
   1.492 -apply (blast intro!: equalityI dest: transM) 
   1.493 -done
   1.494 -
   1.495 -lemma (in M_axioms) Union_closed [intro,simp]:
   1.496 -     "M(A) ==> M(Union(A))"
   1.497 -by (insert Union_ax, simp add: Union_ax_def) 
   1.498 -
   1.499 -lemma (in M_axioms) Un_closed [intro,simp]:
   1.500 -     "[| M(A); M(B) |] ==> M(A Un B)"
   1.501 -by (simp only: Un_eq_Union, blast) 
   1.502 -
   1.503 -lemma (in M_axioms) cons_closed [intro,simp]:
   1.504 -     "[| M(a); M(A) |] ==> M(cons(a,A))"
   1.505 -by (subst cons_eq [symmetric], blast) 
   1.506 -
   1.507 -lemma (in M_axioms) successor_abs [simp]: 
   1.508 -     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
   1.509 -by (simp add: successor_def, blast)  
   1.510 -
   1.511 -lemma (in M_axioms) succ_in_M_iff [iff]:
   1.512 -     "M(succ(a)) <-> M(a)"
   1.513 -apply (simp add: succ_def) 
   1.514 -apply (blast intro: transM) 
   1.515 -done
   1.516 -
   1.517 -lemma (in M_axioms) separation_closed [intro,simp]:
   1.518 -     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   1.519 -apply (insert separation, simp add: separation_def) 
   1.520 -apply (drule spec [THEN mp], assumption, clarify) 
   1.521 -apply (subgoal_tac "y = Collect(A,P)", blast)
   1.522 -apply (blast dest: transM) 
   1.523 -done
   1.524 -
   1.525 -text{*Probably the premise and conclusion are equivalent*}
   1.526 -lemma (in M_axioms) strong_replacementI [rule_format]:
   1.527 -    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   1.528 -     ==> strong_replacement(M,P)"
   1.529 -apply (simp add: strong_replacement_def, clarify) 
   1.530 -apply (frule replacementD [OF replacement], assumption, clarify) 
   1.531 -apply (drule_tac x=A in spec, clarify)  
   1.532 -apply (drule_tac z=Y in separationD, assumption, clarify) 
   1.533 -apply (blast dest: transM) 
   1.534 -done
   1.535 -
   1.536 -
   1.537 -(*The last premise expresses that P takes M to M*)
   1.538 -lemma (in M_axioms) strong_replacement_closed [intro,simp]:
   1.539 -     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   1.540 -       !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   1.541 -apply (simp add: strong_replacement_def) 
   1.542 -apply (drule spec [THEN mp], auto) 
   1.543 -apply (subgoal_tac "Replace(A,P) = Y")
   1.544 - apply simp 
   1.545 -apply (rule equality_iffI) 
   1.546 -apply (simp add: Replace_iff, safe)
   1.547 - apply (blast dest: transM) 
   1.548 -apply (frule transM, assumption) 
   1.549 - apply (simp add: univalent_def)
   1.550 - apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
   1.551 - apply (blast dest: transM) 
   1.552 -done
   1.553 -
   1.554 -(*The first premise can't simply be assumed as a schema.
   1.555 -  It is essential to take care when asserting instances of Replacement.
   1.556 -  Let K be a nonconstructible subset of nat and define
   1.557 -  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   1.558 -  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   1.559 -  even for f : M -> M.
   1.560 -*)
   1.561 -lemma (in M_axioms) RepFun_closed [intro,simp]:
   1.562 -     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
   1.563 -      ==> M(RepFun(A,f))"
   1.564 -apply (simp add: RepFun_def) 
   1.565 -apply (rule strong_replacement_closed) 
   1.566 -apply (auto dest: transM  simp add: univalent_def) 
   1.567 -done
   1.568 -
   1.569 -lemma (in M_axioms) lam_closed [intro,simp]:
   1.570 -     "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
   1.571 -      ==> M(\<lambda>x\<in>A. b(x))"
   1.572 -by (simp add: lam_def, blast dest: transM) 
   1.573 -
   1.574 -lemma (in M_axioms) image_abs [simp]: 
   1.575 -     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.576 -apply (simp add: image_def)
   1.577 -apply (rule iffI) 
   1.578 - apply (blast intro!: equalityI dest: transM, blast) 
   1.579 -done
   1.580 -
   1.581 -text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   1.582 -      This result is one direction of absoluteness.*}
   1.583 -
   1.584 -lemma (in M_axioms) powerset_Pow: 
   1.585 -     "powerset(M, x, Pow(x))"
   1.586 -by (simp add: powerset_def)
   1.587 -
   1.588 -text{*But we can't prove that the powerset in @{text M} includes the
   1.589 -      real powerset.*}
   1.590 -lemma (in M_axioms) powerset_imp_subset_Pow: 
   1.591 -     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   1.592 -apply (simp add: powerset_def) 
   1.593 -apply (blast dest: transM) 
   1.594 -done
   1.595 -
   1.596  lemma (in M_axioms) cartprod_iff_lemma:
   1.597       "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   1.598           powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
   1.599         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   1.600  apply (simp add: powerset_def) 
   1.601  apply (rule equalityI, clarify, simp)
   1.602 -
   1.603   apply (frule transM, assumption) 
   1.604 -
   1.605   apply (frule transM, assumption, simp) 
   1.606   apply blast 
   1.607  apply clarify
   1.608 @@ -698,7 +808,6 @@
   1.609  apply (insert cartprod_separation [of A B], auto)
   1.610  done
   1.611  
   1.612 -
   1.613  text{*All the lemmas above are necessary because Powerset is not absolute.
   1.614        I should have used Replacement instead!*}
   1.615  lemma (in M_axioms) cartprod_closed [intro,simp]: 
   1.616 @@ -709,6 +818,39 @@
   1.617       "[| M(A); M(B) |] ==> M(A+B)"
   1.618  by (simp add: sum_def)
   1.619  
   1.620 +
   1.621 +subsubsection {*converse of a relation*}
   1.622 +
   1.623 +lemma (in M_axioms) M_converse_iff:
   1.624 +     "M(r) ==> 
   1.625 +      converse(r) = 
   1.626 +      {z \<in> Union(Union(r)) * Union(Union(r)). 
   1.627 +       \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
   1.628 +apply (rule equalityI)
   1.629 + prefer 2 apply (blast dest: transM, clarify, simp) 
   1.630 +apply (simp add: Pair_def) 
   1.631 +apply (blast dest: transM) 
   1.632 +done
   1.633 +
   1.634 +lemma (in M_axioms) converse_closed [intro,simp]: 
   1.635 +     "M(r) ==> M(converse(r))"
   1.636 +apply (simp add: M_converse_iff)
   1.637 +apply (insert converse_separation [of r], simp)
   1.638 +done
   1.639 +
   1.640 +lemma (in M_axioms) converse_abs [simp]: 
   1.641 +     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   1.642 +apply (simp add: is_converse_def)
   1.643 +apply (rule iffI)
   1.644 + prefer 2 apply blast 
   1.645 +apply (rule M_equalityI)
   1.646 +  apply simp
   1.647 +  apply (blast dest: transM)+
   1.648 +done
   1.649 +
   1.650 +
   1.651 +subsubsection {*image, preimage, domain, range*}
   1.652 +
   1.653  lemma (in M_axioms) image_closed [intro,simp]: 
   1.654       "[| M(A); M(r) |] ==> M(r``A)"
   1.655  apply (simp add: image_iff_Collect)
   1.656 @@ -724,9 +866,10 @@
   1.657  
   1.658  lemma (in M_axioms) vimage_closed [intro,simp]: 
   1.659       "[| M(A); M(r) |] ==> M(r-``A)"
   1.660 -apply (simp add: vimage_iff_Collect)
   1.661 -apply (insert vimage_separation [of A r], simp) 
   1.662 -done
   1.663 +by (simp add: vimage_def)
   1.664 +
   1.665 +
   1.666 +subsubsection{*Domain, range and field*}
   1.667  
   1.668  lemma (in M_axioms) domain_abs [simp]: 
   1.669       "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   1.670 @@ -759,27 +902,7 @@
   1.671  by (simp add: domain_closed range_closed Un_closed field_def) 
   1.672  
   1.673  
   1.674 -lemma (in M_axioms) M_converse_iff:
   1.675 -     "M(r) ==> 
   1.676 -      converse(r) = 
   1.677 -      {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>}"
   1.678 -by (blast dest: transM)
   1.679 -
   1.680 -lemma (in M_axioms) converse_closed [intro,simp]: 
   1.681 -     "M(r) ==> M(converse(r))"
   1.682 -apply (simp add: M_converse_iff)
   1.683 -apply (insert converse_separation [of r], simp)
   1.684 -done
   1.685 -
   1.686 -lemma (in M_axioms) converse_abs [simp]: 
   1.687 -     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   1.688 -apply (simp add: is_converse_def)
   1.689 -apply (rule iffI)
   1.690 - prefer 2 apply blast 
   1.691 -apply (rule M_equalityI)
   1.692 -  apply simp
   1.693 -  apply (blast dest: transM)+
   1.694 -done
   1.695 +subsubsection{*Relations, functions and application*}
   1.696  
   1.697  lemma (in M_axioms) relation_abs [simp]: 
   1.698       "M(r) ==> is_relation(M,r) <-> relation(r)"
   1.699 @@ -796,8 +919,7 @@
   1.700  
   1.701  lemma (in M_axioms) apply_closed [intro,simp]: 
   1.702       "[|M(f); M(a)|] ==> M(f`a)"
   1.703 -apply (simp add: apply_def)
   1.704 -done
   1.705 +by (simp add: apply_def)
   1.706  
   1.707  lemma (in M_axioms) apply_abs: 
   1.708       "[| function(f); M(f); M(y) |] 
   1.709 @@ -831,32 +953,8 @@
   1.710       "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   1.711  by (simp add: bijection_def bij_def)
   1.712  
   1.713 -text{*no longer needed*}
   1.714 -lemma (in M_axioms) restriction_is_function: 
   1.715 -     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   1.716 -      ==> function(z)"
   1.717 -apply (rotate_tac 1)
   1.718 -apply (simp add: restriction_def ball_iff_equiv) 
   1.719 -apply (unfold function_def, blast) 
   1.720 -done
   1.721  
   1.722 -lemma (in M_axioms) restriction_abs [simp]: 
   1.723 -     "[| M(f); M(A); M(z) |] 
   1.724 -      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   1.725 -apply (simp add: ball_iff_equiv restriction_def restrict_def)
   1.726 -apply (blast intro!: equalityI dest: transM) 
   1.727 -done
   1.728 -
   1.729 -
   1.730 -lemma (in M_axioms) M_restrict_iff:
   1.731 -     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
   1.732 -by (simp add: restrict_def, blast dest: transM)
   1.733 -
   1.734 -lemma (in M_axioms) restrict_closed [intro,simp]: 
   1.735 -     "[| M(A); M(r) |] ==> M(restrict(r,A))"
   1.736 -apply (simp add: M_restrict_iff)
   1.737 -apply (insert restrict_separation [of A], simp) 
   1.738 -done
   1.739 +subsubsection{*Composition of relations*}
   1.740  
   1.741  lemma (in M_axioms) M_comp_iff:
   1.742       "[| M(r); M(s) |] 
   1.743 @@ -890,24 +988,32 @@
   1.744    apply (blast del: allE dest: transM)+
   1.745  done
   1.746  
   1.747 -lemma (in M_axioms) nat_into_M [intro]:
   1.748 -     "n \<in> nat ==> M(n)"
   1.749 -by (induct n rule: nat_induct, simp_all)
   1.750 -
   1.751 -lemma (in M_axioms) nat_case_closed:
   1.752 -  "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
   1.753 -apply (case_tac "k=0", simp) 
   1.754 -apply (case_tac "\<exists>m. k = succ(m)", force)
   1.755 -apply (simp add: nat_case_def) 
   1.756 +text{*no longer needed*}
   1.757 +lemma (in M_axioms) restriction_is_function: 
   1.758 +     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   1.759 +      ==> function(z)"
   1.760 +apply (rotate_tac 1)
   1.761 +apply (simp add: restriction_def ball_iff_equiv) 
   1.762 +apply (unfold function_def, blast) 
   1.763  done
   1.764  
   1.765 -lemma (in M_axioms) Inl_in_M_iff [iff]:
   1.766 -     "M(Inl(a)) <-> M(a)"
   1.767 -by (simp add: Inl_def) 
   1.768 +lemma (in M_axioms) restriction_abs [simp]: 
   1.769 +     "[| M(f); M(A); M(z) |] 
   1.770 +      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   1.771 +apply (simp add: ball_iff_equiv restriction_def restrict_def)
   1.772 +apply (blast intro!: equalityI dest: transM) 
   1.773 +done
   1.774 +
   1.775  
   1.776 -lemma (in M_axioms) Inr_in_M_iff [iff]:
   1.777 -     "M(Inr(a)) <-> M(a)"
   1.778 -by (simp add: Inr_def) 
   1.779 +lemma (in M_axioms) M_restrict_iff:
   1.780 +     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
   1.781 +by (simp add: restrict_def, blast dest: transM)
   1.782 +
   1.783 +lemma (in M_axioms) restrict_closed [intro,simp]: 
   1.784 +     "[| M(A); M(r) |] ==> M(restrict(r,A))"
   1.785 +apply (simp add: M_restrict_iff)
   1.786 +apply (insert restrict_separation [of A], simp) 
   1.787 +done
   1.788  
   1.789  lemma (in M_axioms) Inter_abs [simp]: 
   1.790       "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
   1.791 @@ -925,7 +1031,7 @@
   1.792  apply (frule Inter_closed, force+) 
   1.793  done
   1.794  
   1.795 -subsection{*Functions and function space*}
   1.796 +subsubsection{*Functions and function space*}
   1.797  
   1.798  text{*M contains all finite functions*}
   1.799  lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: 
   1.800 @@ -977,96 +1083,4 @@
   1.801  apply (simp add: funspace_succ nat_into_M) 
   1.802  done
   1.803  
   1.804 -
   1.805 -subsection{*Absoluteness for ordinals*}
   1.806 -text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   1.807 -
   1.808 -lemma (in M_axioms) lt_closed:
   1.809 -     "[| j<i; M(i) |] ==> M(j)" 
   1.810 -by (blast dest: ltD intro: transM) 
   1.811 -
   1.812 -lemma (in M_axioms) transitive_set_abs [simp]: 
   1.813 -     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   1.814 -by (simp add: transitive_set_def Transset_def)
   1.815 -
   1.816 -lemma (in M_axioms) ordinal_abs [simp]: 
   1.817 -     "M(a) ==> ordinal(M,a) <-> Ord(a)"
   1.818 -by (simp add: ordinal_def Ord_def)
   1.819 -
   1.820 -lemma (in M_axioms) limit_ordinal_abs [simp]: 
   1.821 -     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   1.822 -apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   1.823 -apply (simp add: lt_def, blast) 
   1.824 -done
   1.825 -
   1.826 -lemma (in M_axioms) successor_ordinal_abs [simp]: 
   1.827 -     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
   1.828 -apply (simp add: successor_ordinal_def, safe)
   1.829 -apply (drule Ord_cases_disj, auto) 
   1.830 -done
   1.831 -
   1.832 -lemma finite_Ord_is_nat:
   1.833 -      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   1.834 -by (induct a rule: trans_induct3, simp_all)
   1.835 -
   1.836 -lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   1.837 -by (induct a rule: nat_induct, auto)
   1.838 -
   1.839 -lemma (in M_axioms) finite_ordinal_abs [simp]: 
   1.840 -     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   1.841 -apply (simp add: finite_ordinal_def)
   1.842 -apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   1.843 -             dest: Ord_trans naturals_not_limit)
   1.844 -done
   1.845 -
   1.846 -lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   1.847 -apply (rule le_anti_sym) 
   1.848 -apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   1.849 - apply (simp add: lt_def)  
   1.850 - apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   1.851 -apply (erule nat_le_Limit)
   1.852 -done
   1.853 -
   1.854 -lemma (in M_axioms) omega_abs [simp]: 
   1.855 -     "M(a) ==> omega(M,a) <-> a = nat"
   1.856 -apply (simp add: omega_def) 
   1.857 -apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   1.858 -done
   1.859 -
   1.860 -lemma (in M_axioms) number1_abs [simp]: 
   1.861 -     "M(a) ==> number1(M,a) <-> a = 1"
   1.862 -by (simp add: number1_def) 
   1.863 -
   1.864 -lemma (in M_axioms) number1_abs [simp]: 
   1.865 -     "M(a) ==> number2(M,a) <-> a = succ(1)"
   1.866 -by (simp add: number2_def) 
   1.867 -
   1.868 -lemma (in M_axioms) number3_abs [simp]: 
   1.869 -     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   1.870 -by (simp add: number3_def) 
   1.871 -
   1.872 -text{*Kunen continued to 20...*}
   1.873 -
   1.874 -(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   1.875 -  but the recursion variable must stay unchanged.  But then the recursion
   1.876 -  equations only hold for x\<in>nat (or in some other set) and not for the 
   1.877 -  whole of the class M.
   1.878 -  consts
   1.879 -    natnumber_aux :: "[i=>o,i] => i"
   1.880 -
   1.881 -  primrec
   1.882 -      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   1.883 -      "natnumber_aux(M,succ(n)) = 
   1.884 -	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   1.885 -		     then 1 else 0)"
   1.886 -
   1.887 -  constdefs
   1.888 -    natnumber :: "[i=>o,i,i] => o"
   1.889 -      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   1.890 -
   1.891 -  lemma (in M_axioms) [simp]: 
   1.892 -       "natnumber(M,0,x) == x=0"
   1.893 -*)
   1.894 -
   1.895 -
   1.896  end