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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.269 +done
1.270 +
1.271 +lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
1.272 +     "M(Inl(a)) <-> M(a)"
1.274 +
1.275 +lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
1.276 +     "M(Inr(a)) <-> M(a)"
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.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.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.339 +
1.340 +lemma (in M_triv_axioms) number1_abs [simp]:
1.341 +     "M(a) ==> number2(M,a) <-> a = succ(1)"
1.343 +
1.344 +lemma (in M_triv_axioms) number3_abs [simp]:
1.345 +     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
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.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.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.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.456 -
1.457 -lemma (in M_axioms) pair_components_in_M:
1.458 -     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.661 -apply (insert vimage_separation [of A r], simp)
1.662 -done
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.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.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.704 -done
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.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.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.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.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.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.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.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.863 -
1.864 -lemma (in M_axioms) number1_abs [simp]:
1.865 -     "M(a) ==> number2(M,a) <-> a = succ(1)"
1.867 -
1.868 -lemma (in M_axioms) number3_abs [simp]:
1.869 -     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
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
```