1.1 --- a/src/ZF/Constructible/Relative.thy Tue Sep 10 16:47:17 2002 +0200
1.2 +++ b/src/ZF/Constructible/Relative.thy Tue Sep 10 16:51:31 2002 +0200
1.3 @@ -465,7 +465,7 @@
1.4
1.5 text{*The class M is assumed to be transitive and to satisfy some
1.6 relativized ZF axioms*}
1.7 -locale M_triv_axioms =
1.8 +locale M_trivial =
1.9 fixes M
1.10 assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
1.11 and nonempty [simp]: "M(0)"
1.12 @@ -475,73 +475,73 @@
1.13 and replacement: "replacement(M,P)"
1.14 and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*)
1.15
1.16 -lemma (in M_triv_axioms) rall_abs [simp]:
1.17 +lemma (in M_trivial) rall_abs [simp]:
1.18 "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
1.19 by (blast intro: transM)
1.20
1.21 -lemma (in M_triv_axioms) rex_abs [simp]:
1.22 +lemma (in M_trivial) rex_abs [simp]:
1.23 "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
1.24 by (blast intro: transM)
1.25
1.26 -lemma (in M_triv_axioms) ball_iff_equiv:
1.27 +lemma (in M_trivial) ball_iff_equiv:
1.28 "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <->
1.29 (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
1.30 by (blast intro: transM)
1.31
1.32 text{*Simplifies proofs of equalities when there's an iff-equality
1.33 available for rewriting, universally quantified over M. *}
1.34 -lemma (in M_triv_axioms) M_equalityI:
1.35 +lemma (in M_trivial) M_equalityI:
1.36 "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
1.37 by (blast intro!: equalityI dest: transM)
1.38
1.39
1.40 subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
1.41
1.42 -lemma (in M_triv_axioms) empty_abs [simp]:
1.43 +lemma (in M_trivial) empty_abs [simp]:
1.44 "M(z) ==> empty(M,z) <-> z=0"
1.45 apply (simp add: empty_def)
1.46 apply (blast intro: transM)
1.47 done
1.48
1.49 -lemma (in M_triv_axioms) subset_abs [simp]:
1.50 +lemma (in M_trivial) subset_abs [simp]:
1.51 "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
1.52 apply (simp add: subset_def)
1.53 apply (blast intro: transM)
1.54 done
1.55
1.56 -lemma (in M_triv_axioms) upair_abs [simp]:
1.57 +lemma (in M_trivial) upair_abs [simp]:
1.58 "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
1.59 apply (simp add: upair_def)
1.60 apply (blast intro: transM)
1.61 done
1.62
1.63 -lemma (in M_triv_axioms) upair_in_M_iff [iff]:
1.64 +lemma (in M_trivial) upair_in_M_iff [iff]:
1.65 "M({a,b}) <-> M(a) & M(b)"
1.66 apply (insert upair_ax, simp add: upair_ax_def)
1.67 apply (blast intro: transM)
1.68 done
1.69
1.70 -lemma (in M_triv_axioms) singleton_in_M_iff [iff]:
1.71 +lemma (in M_trivial) singleton_in_M_iff [iff]:
1.72 "M({a}) <-> M(a)"
1.73 by (insert upair_in_M_iff [of a a], simp)
1.74
1.75 -lemma (in M_triv_axioms) pair_abs [simp]:
1.76 +lemma (in M_trivial) pair_abs [simp]:
1.77 "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
1.78 apply (simp add: pair_def ZF.Pair_def)
1.79 apply (blast intro: transM)
1.80 done
1.81
1.82 -lemma (in M_triv_axioms) pair_in_M_iff [iff]:
1.83 +lemma (in M_trivial) pair_in_M_iff [iff]:
1.84 "M(<a,b>) <-> M(a) & M(b)"
1.85 by (simp add: ZF.Pair_def)
1.86
1.87 -lemma (in M_triv_axioms) pair_components_in_M:
1.88 +lemma (in M_trivial) pair_components_in_M:
1.89 "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
1.90 apply (simp add: Pair_def)
1.91 apply (blast dest: transM)
1.92 done
1.93
1.94 -lemma (in M_triv_axioms) cartprod_abs [simp]:
1.95 +lemma (in M_trivial) cartprod_abs [simp]:
1.96 "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
1.97 apply (simp add: cartprod_def)
1.98 apply (rule iffI)
1.99 @@ -551,51 +551,51 @@
1.100
1.101 subsubsection{*Absoluteness for Unions and Intersections*}
1.102
1.103 -lemma (in M_triv_axioms) union_abs [simp]:
1.104 +lemma (in M_trivial) union_abs [simp]:
1.105 "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
1.106 apply (simp add: union_def)
1.107 apply (blast intro: transM)
1.108 done
1.109
1.110 -lemma (in M_triv_axioms) inter_abs [simp]:
1.111 +lemma (in M_trivial) inter_abs [simp]:
1.112 "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
1.113 apply (simp add: inter_def)
1.114 apply (blast intro: transM)
1.115 done
1.116
1.117 -lemma (in M_triv_axioms) setdiff_abs [simp]:
1.118 +lemma (in M_trivial) setdiff_abs [simp]:
1.119 "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
1.120 apply (simp add: setdiff_def)
1.121 apply (blast intro: transM)
1.122 done
1.123
1.124 -lemma (in M_triv_axioms) Union_abs [simp]:
1.125 +lemma (in M_trivial) Union_abs [simp]:
1.126 "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
1.127 apply (simp add: big_union_def)
1.128 apply (blast intro!: equalityI dest: transM)
1.129 done
1.130
1.131 -lemma (in M_triv_axioms) Union_closed [intro,simp]:
1.132 +lemma (in M_trivial) Union_closed [intro,simp]:
1.133 "M(A) ==> M(Union(A))"
1.134 by (insert Union_ax, simp add: Union_ax_def)
1.135
1.136 -lemma (in M_triv_axioms) Un_closed [intro,simp]:
1.137 +lemma (in M_trivial) Un_closed [intro,simp]:
1.138 "[| M(A); M(B) |] ==> M(A Un B)"
1.139 by (simp only: Un_eq_Union, blast)
1.140
1.141 -lemma (in M_triv_axioms) cons_closed [intro,simp]:
1.142 +lemma (in M_trivial) cons_closed [intro,simp]:
1.143 "[| M(a); M(A) |] ==> M(cons(a,A))"
1.144 by (subst cons_eq [symmetric], blast)
1.145
1.146 -lemma (in M_triv_axioms) cons_abs [simp]:
1.147 +lemma (in M_trivial) cons_abs [simp]:
1.148 "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
1.149 by (simp add: is_cons_def, blast intro: transM)
1.150
1.151 -lemma (in M_triv_axioms) successor_abs [simp]:
1.152 +lemma (in M_trivial) successor_abs [simp]:
1.153 "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
1.154 by (simp add: successor_def, blast)
1.155
1.156 -lemma (in M_triv_axioms) succ_in_M_iff [iff]:
1.157 +lemma (in M_trivial) succ_in_M_iff [iff]:
1.158 "M(succ(a)) <-> M(a)"
1.159 apply (simp add: succ_def)
1.160 apply (blast intro: transM)
1.161 @@ -603,7 +603,7 @@
1.162
1.163 subsubsection{*Absoluteness for Separation and Replacement*}
1.164
1.165 -lemma (in M_triv_axioms) separation_closed [intro,simp]:
1.166 +lemma (in M_trivial) separation_closed [intro,simp]:
1.167 "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
1.168 apply (insert separation, simp add: separation_def)
1.169 apply (drule rspec, assumption, clarify)
1.170 @@ -615,14 +615,14 @@
1.171 "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
1.172 by (simp add: separation_def is_Collect_def)
1.173
1.174 -lemma (in M_triv_axioms) Collect_abs [simp]:
1.175 +lemma (in M_trivial) Collect_abs [simp]:
1.176 "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
1.177 apply (simp add: is_Collect_def)
1.178 apply (blast intro!: equalityI dest: transM)
1.179 done
1.180
1.181 text{*Probably the premise and conclusion are equivalent*}
1.182 -lemma (in M_triv_axioms) strong_replacementI [rule_format]:
1.183 +lemma (in M_trivial) strong_replacementI [rule_format]:
1.184 "[| \<forall>A[M]. separation(M, %u. \<exists>x[M]. x\<in>A & P(x,u)) |]
1.185 ==> strong_replacement(M,P)"
1.186 apply (simp add: strong_replacement_def, clarify)
1.187 @@ -645,7 +645,7 @@
1.188 is_Replace(M, A', %x y. P'(x,y), z')"
1.189 by (simp add: is_Replace_def)
1.190
1.191 -lemma (in M_triv_axioms) univalent_Replace_iff:
1.192 +lemma (in M_trivial) univalent_Replace_iff:
1.193 "[| M(A); univalent(M,A,P);
1.194 !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
1.195 ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
1.196 @@ -654,7 +654,7 @@
1.197 done
1.198
1.199 (*The last premise expresses that P takes M to M*)
1.200 -lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
1.201 +lemma (in M_trivial) strong_replacement_closed [intro,simp]:
1.202 "[| strong_replacement(M,P); M(A); univalent(M,A,P);
1.203 !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
1.204 apply (simp add: strong_replacement_def)
1.205 @@ -666,7 +666,7 @@
1.206 apply (blast dest: transM)
1.207 done
1.208
1.209 -lemma (in M_triv_axioms) Replace_abs:
1.210 +lemma (in M_trivial) Replace_abs:
1.211 "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
1.212 !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
1.213 ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
1.214 @@ -683,7 +683,7 @@
1.215 nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f))
1.216 even for f : M -> M.
1.217 *)
1.218 -lemma (in M_triv_axioms) RepFun_closed:
1.219 +lemma (in M_trivial) RepFun_closed:
1.220 "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
1.221 ==> M(RepFun(A,f))"
1.222 apply (simp add: RepFun_def)
1.223 @@ -696,7 +696,7 @@
1.224
1.225 text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
1.226 makes relativization easier.*}
1.227 -lemma (in M_triv_axioms) RepFun_closed2:
1.228 +lemma (in M_trivial) RepFun_closed2:
1.229 "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
1.230 ==> M(RepFun(A, %x. f(x)))"
1.231 apply (simp add: RepFun_def)
1.232 @@ -712,20 +712,20 @@
1.233 \<forall>p[M]. p \<in> z <->
1.234 (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
1.235
1.236 -lemma (in M_triv_axioms) lam_closed:
1.237 +lemma (in M_trivial) lam_closed:
1.238 "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
1.239 ==> M(\<lambda>x\<in>A. b(x))"
1.240 by (simp add: lam_def, blast intro: RepFun_closed dest: transM)
1.241
1.242 text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
1.243 -lemma (in M_triv_axioms) lam_closed2:
1.244 +lemma (in M_trivial) lam_closed2:
1.245 "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
1.246 M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
1.247 apply (simp add: lam_def)
1.248 apply (blast intro: RepFun_closed2 dest: transM)
1.249 done
1.250
1.251 -lemma (in M_triv_axioms) lambda_abs2 [simp]:
1.252 +lemma (in M_trivial) lambda_abs2 [simp]:
1.253 "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
1.254 Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
1.255 ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
1.256 @@ -744,7 +744,7 @@
1.257 is_lambda(M, A', %x y. is_b'(x,y), z')"
1.258 by (simp add: is_lambda_def)
1.259
1.260 -lemma (in M_triv_axioms) image_abs [simp]:
1.261 +lemma (in M_trivial) image_abs [simp]:
1.262 "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
1.263 apply (simp add: image_def)
1.264 apply (rule iffI)
1.265 @@ -754,13 +754,13 @@
1.266 text{*What about @{text Pow_abs}? Powerset is NOT absolute!
1.267 This result is one direction of absoluteness.*}
1.268
1.269 -lemma (in M_triv_axioms) powerset_Pow:
1.270 +lemma (in M_trivial) powerset_Pow:
1.271 "powerset(M, x, Pow(x))"
1.272 by (simp add: powerset_def)
1.273
1.274 text{*But we can't prove that the powerset in @{text M} includes the
1.275 real powerset.*}
1.276 -lemma (in M_triv_axioms) powerset_imp_subset_Pow:
1.277 +lemma (in M_trivial) powerset_imp_subset_Pow:
1.278 "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
1.279 apply (simp add: powerset_def)
1.280 apply (blast dest: transM)
1.281 @@ -768,22 +768,22 @@
1.282
1.283 subsubsection{*Absoluteness for the Natural Numbers*}
1.284
1.285 -lemma (in M_triv_axioms) nat_into_M [intro]:
1.286 +lemma (in M_trivial) nat_into_M [intro]:
1.287 "n \<in> nat ==> M(n)"
1.288 by (induct n rule: nat_induct, simp_all)
1.289
1.290 -lemma (in M_triv_axioms) nat_case_closed [intro,simp]:
1.291 +lemma (in M_trivial) nat_case_closed [intro,simp]:
1.292 "[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
1.293 apply (case_tac "k=0", simp)
1.294 apply (case_tac "\<exists>m. k = succ(m)", force)
1.295 apply (simp add: nat_case_def)
1.296 done
1.297
1.298 -lemma (in M_triv_axioms) quasinat_abs [simp]:
1.299 +lemma (in M_trivial) quasinat_abs [simp]:
1.300 "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
1.301 by (auto simp add: is_quasinat_def quasinat_def)
1.302
1.303 -lemma (in M_triv_axioms) nat_case_abs [simp]:
1.304 +lemma (in M_trivial) nat_case_abs [simp]:
1.305 "[| relativize1(M,is_b,b); M(k); M(z) |]
1.306 ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
1.307 apply (case_tac "quasinat(k)")
1.308 @@ -808,26 +808,26 @@
1.309 subsection{*Absoluteness for Ordinals*}
1.310 text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
1.311
1.312 -lemma (in M_triv_axioms) lt_closed:
1.313 +lemma (in M_trivial) lt_closed:
1.314 "[| j<i; M(i) |] ==> M(j)"
1.315 by (blast dest: ltD intro: transM)
1.316
1.317 -lemma (in M_triv_axioms) transitive_set_abs [simp]:
1.318 +lemma (in M_trivial) transitive_set_abs [simp]:
1.319 "M(a) ==> transitive_set(M,a) <-> Transset(a)"
1.320 by (simp add: transitive_set_def Transset_def)
1.321
1.322 -lemma (in M_triv_axioms) ordinal_abs [simp]:
1.323 +lemma (in M_trivial) ordinal_abs [simp]:
1.324 "M(a) ==> ordinal(M,a) <-> Ord(a)"
1.325 by (simp add: ordinal_def Ord_def)
1.326
1.327 -lemma (in M_triv_axioms) limit_ordinal_abs [simp]:
1.328 +lemma (in M_trivial) limit_ordinal_abs [simp]:
1.329 "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
1.330 apply (unfold Limit_def limit_ordinal_def)
1.331 apply (simp add: Ord_0_lt_iff)
1.332 apply (simp add: lt_def, blast)
1.333 done
1.334
1.335 -lemma (in M_triv_axioms) successor_ordinal_abs [simp]:
1.336 +lemma (in M_trivial) successor_ordinal_abs [simp]:
1.337 "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
1.338 apply (simp add: successor_ordinal_def, safe)
1.339 apply (drule Ord_cases_disj, auto)
1.340 @@ -840,7 +840,7 @@
1.341 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
1.342 by (induct a rule: nat_induct, auto)
1.343
1.344 -lemma (in M_triv_axioms) finite_ordinal_abs [simp]:
1.345 +lemma (in M_trivial) finite_ordinal_abs [simp]:
1.346 "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
1.347 apply (simp add: finite_ordinal_def)
1.348 apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
1.349 @@ -856,21 +856,21 @@
1.350 apply (erule nat_le_Limit)
1.351 done
1.352
1.353 -lemma (in M_triv_axioms) omega_abs [simp]:
1.354 +lemma (in M_trivial) omega_abs [simp]:
1.355 "M(a) ==> omega(M,a) <-> a = nat"
1.356 apply (simp add: omega_def)
1.357 apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
1.358 done
1.359
1.360 -lemma (in M_triv_axioms) number1_abs [simp]:
1.361 +lemma (in M_trivial) number1_abs [simp]:
1.362 "M(a) ==> number1(M,a) <-> a = 1"
1.363 by (simp add: number1_def)
1.364
1.365 -lemma (in M_triv_axioms) number2_abs [simp]:
1.366 +lemma (in M_trivial) number2_abs [simp]:
1.367 "M(a) ==> number2(M,a) <-> a = succ(1)"
1.368 by (simp add: number2_def)
1.369
1.370 -lemma (in M_triv_axioms) number3_abs [simp]:
1.371 +lemma (in M_trivial) number3_abs [simp]:
1.372 "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
1.373 by (simp add: number3_def)
1.374
1.375 @@ -893,13 +893,13 @@
1.376 natnumber :: "[i=>o,i,i] => o"
1.377 "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
1.378
1.379 - lemma (in M_triv_axioms) [simp]:
1.380 + lemma (in M_trivial) [simp]:
1.381 "natnumber(M,0,x) == x=0"
1.382 *)
1.383
1.384 subsection{*Some instances of separation and strong replacement*}
1.385
1.386 -locale M_axioms = M_triv_axioms +
1.387 +locale M_basic = M_trivial +
1.388 assumes Inter_separation:
1.389 "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
1.390 and Diff_separation:
1.391 @@ -960,7 +960,7 @@
1.392 (\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
1.393 fx \<noteq> gx))"
1.394
1.395 -lemma (in M_axioms) cartprod_iff_lemma:
1.396 +lemma (in M_basic) cartprod_iff_lemma:
1.397 "[| M(C); \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
1.398 powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
1.399 ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
1.400 @@ -973,7 +973,7 @@
1.401 apply (frule transM, assumption, force)
1.402 done
1.403
1.404 -lemma (in M_axioms) cartprod_iff:
1.405 +lemma (in M_basic) cartprod_iff:
1.406 "[| M(A); M(B); M(C) |]
1.407 ==> cartprod(M,A,B,C) <->
1.408 (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
1.409 @@ -991,7 +991,7 @@
1.410 apply (blast intro: cartprod_iff_lemma)
1.411 done
1.412
1.413 -lemma (in M_axioms) cartprod_closed_lemma:
1.414 +lemma (in M_basic) cartprod_closed_lemma:
1.415 "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
1.416 apply (simp del: cartprod_abs add: cartprod_iff)
1.417 apply (insert power_ax, simp add: power_ax_def)
1.418 @@ -1008,38 +1008,38 @@
1.419
1.420 text{*All the lemmas above are necessary because Powerset is not absolute.
1.421 I should have used Replacement instead!*}
1.422 -lemma (in M_axioms) cartprod_closed [intro,simp]:
1.423 +lemma (in M_basic) cartprod_closed [intro,simp]:
1.424 "[| M(A); M(B) |] ==> M(A*B)"
1.425 by (frule cartprod_closed_lemma, assumption, force)
1.426
1.427 -lemma (in M_axioms) sum_closed [intro,simp]:
1.428 +lemma (in M_basic) sum_closed [intro,simp]:
1.429 "[| M(A); M(B) |] ==> M(A+B)"
1.430 by (simp add: sum_def)
1.431
1.432 -lemma (in M_axioms) sum_abs [simp]:
1.433 +lemma (in M_basic) sum_abs [simp]:
1.434 "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
1.435 by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
1.436
1.437 -lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
1.438 +lemma (in M_trivial) Inl_in_M_iff [iff]:
1.439 "M(Inl(a)) <-> M(a)"
1.440 by (simp add: Inl_def)
1.441
1.442 -lemma (in M_triv_axioms) Inl_abs [simp]:
1.443 +lemma (in M_trivial) Inl_abs [simp]:
1.444 "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
1.445 by (simp add: is_Inl_def Inl_def)
1.446
1.447 -lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
1.448 +lemma (in M_trivial) Inr_in_M_iff [iff]:
1.449 "M(Inr(a)) <-> M(a)"
1.450 by (simp add: Inr_def)
1.451
1.452 -lemma (in M_triv_axioms) Inr_abs [simp]:
1.453 +lemma (in M_trivial) Inr_abs [simp]:
1.454 "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
1.455 by (simp add: is_Inr_def Inr_def)
1.456
1.457
1.458 subsubsection {*converse of a relation*}
1.459
1.460 -lemma (in M_axioms) M_converse_iff:
1.461 +lemma (in M_basic) M_converse_iff:
1.462 "M(r) ==>
1.463 converse(r) =
1.464 {z \<in> Union(Union(r)) * Union(Union(r)).
1.465 @@ -1050,13 +1050,13 @@
1.466 apply (blast dest: transM)
1.467 done
1.468
1.469 -lemma (in M_axioms) converse_closed [intro,simp]:
1.470 +lemma (in M_basic) converse_closed [intro,simp]:
1.471 "M(r) ==> M(converse(r))"
1.472 apply (simp add: M_converse_iff)
1.473 apply (insert converse_separation [of r], simp)
1.474 done
1.475
1.476 -lemma (in M_axioms) converse_abs [simp]:
1.477 +lemma (in M_basic) converse_abs [simp]:
1.478 "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
1.479 apply (simp add: is_converse_def)
1.480 apply (rule iffI)
1.481 @@ -1069,105 +1069,105 @@
1.482
1.483 subsubsection {*image, preimage, domain, range*}
1.484
1.485 -lemma (in M_axioms) image_closed [intro,simp]:
1.486 +lemma (in M_basic) image_closed [intro,simp]:
1.487 "[| M(A); M(r) |] ==> M(r``A)"
1.488 apply (simp add: image_iff_Collect)
1.489 apply (insert image_separation [of A r], simp)
1.490 done
1.491
1.492 -lemma (in M_axioms) vimage_abs [simp]:
1.493 +lemma (in M_basic) vimage_abs [simp]:
1.494 "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
1.495 apply (simp add: pre_image_def)
1.496 apply (rule iffI)
1.497 apply (blast intro!: equalityI dest: transM, blast)
1.498 done
1.499
1.500 -lemma (in M_axioms) vimage_closed [intro,simp]:
1.501 +lemma (in M_basic) vimage_closed [intro,simp]:
1.502 "[| M(A); M(r) |] ==> M(r-``A)"
1.503 by (simp add: vimage_def)
1.504
1.505
1.506 subsubsection{*Domain, range and field*}
1.507
1.508 -lemma (in M_axioms) domain_abs [simp]:
1.509 +lemma (in M_basic) domain_abs [simp]:
1.510 "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
1.511 apply (simp add: is_domain_def)
1.512 apply (blast intro!: equalityI dest: transM)
1.513 done
1.514
1.515 -lemma (in M_axioms) domain_closed [intro,simp]:
1.516 +lemma (in M_basic) domain_closed [intro,simp]:
1.517 "M(r) ==> M(domain(r))"
1.518 apply (simp add: domain_eq_vimage)
1.519 done
1.520
1.521 -lemma (in M_axioms) range_abs [simp]:
1.522 +lemma (in M_basic) range_abs [simp]:
1.523 "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
1.524 apply (simp add: is_range_def)
1.525 apply (blast intro!: equalityI dest: transM)
1.526 done
1.527
1.528 -lemma (in M_axioms) range_closed [intro,simp]:
1.529 +lemma (in M_basic) range_closed [intro,simp]:
1.530 "M(r) ==> M(range(r))"
1.531 apply (simp add: range_eq_image)
1.532 done
1.533
1.534 -lemma (in M_axioms) field_abs [simp]:
1.535 +lemma (in M_basic) field_abs [simp]:
1.536 "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
1.537 by (simp add: domain_closed range_closed is_field_def field_def)
1.538
1.539 -lemma (in M_axioms) field_closed [intro,simp]:
1.540 +lemma (in M_basic) field_closed [intro,simp]:
1.541 "M(r) ==> M(field(r))"
1.542 by (simp add: domain_closed range_closed Un_closed field_def)
1.543
1.544
1.545 subsubsection{*Relations, functions and application*}
1.546
1.547 -lemma (in M_axioms) relation_abs [simp]:
1.548 +lemma (in M_basic) relation_abs [simp]:
1.549 "M(r) ==> is_relation(M,r) <-> relation(r)"
1.550 apply (simp add: is_relation_def relation_def)
1.551 apply (blast dest!: bspec dest: pair_components_in_M)+
1.552 done
1.553
1.554 -lemma (in M_axioms) function_abs [simp]:
1.555 +lemma (in M_basic) function_abs [simp]:
1.556 "M(r) ==> is_function(M,r) <-> function(r)"
1.557 apply (simp add: is_function_def function_def, safe)
1.558 apply (frule transM, assumption)
1.559 apply (blast dest: pair_components_in_M)+
1.560 done
1.561
1.562 -lemma (in M_axioms) apply_closed [intro,simp]:
1.563 +lemma (in M_basic) apply_closed [intro,simp]:
1.564 "[|M(f); M(a)|] ==> M(f`a)"
1.565 by (simp add: apply_def)
1.566
1.567 -lemma (in M_axioms) apply_abs [simp]:
1.568 +lemma (in M_basic) apply_abs [simp]:
1.569 "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
1.570 apply (simp add: fun_apply_def apply_def, blast)
1.571 done
1.572
1.573 -lemma (in M_axioms) typed_function_abs [simp]:
1.574 +lemma (in M_basic) typed_function_abs [simp]:
1.575 "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
1.576 apply (auto simp add: typed_function_def relation_def Pi_iff)
1.577 apply (blast dest: pair_components_in_M)+
1.578 done
1.579
1.580 -lemma (in M_axioms) injection_abs [simp]:
1.581 +lemma (in M_basic) injection_abs [simp]:
1.582 "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
1.583 apply (simp add: injection_def apply_iff inj_def apply_closed)
1.584 apply (blast dest: transM [of _ A])
1.585 done
1.586
1.587 -lemma (in M_axioms) surjection_abs [simp]:
1.588 +lemma (in M_basic) surjection_abs [simp]:
1.589 "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
1.590 by (simp add: surjection_def surj_def)
1.591
1.592 -lemma (in M_axioms) bijection_abs [simp]:
1.593 +lemma (in M_basic) bijection_abs [simp]:
1.594 "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
1.595 by (simp add: bijection_def bij_def)
1.596
1.597
1.598 subsubsection{*Composition of relations*}
1.599
1.600 -lemma (in M_axioms) M_comp_iff:
1.601 +lemma (in M_basic) M_comp_iff:
1.602 "[| M(r); M(s) |]
1.603 ==> r O s =
1.604 {xz \<in> domain(s) * range(r).
1.605 @@ -1179,13 +1179,13 @@
1.606 apply (blast dest: transM)+
1.607 done
1.608
1.609 -lemma (in M_axioms) comp_closed [intro,simp]:
1.610 +lemma (in M_basic) comp_closed [intro,simp]:
1.611 "[| M(r); M(s) |] ==> M(r O s)"
1.612 apply (simp add: M_comp_iff)
1.613 apply (insert comp_separation [of r s], simp)
1.614 done
1.615
1.616 -lemma (in M_axioms) composition_abs [simp]:
1.617 +lemma (in M_basic) composition_abs [simp]:
1.618 "[| M(r); M(s); M(t) |]
1.619 ==> composition(M,r,s,t) <-> t = r O s"
1.620 apply safe
1.621 @@ -1200,7 +1200,7 @@
1.622 done
1.623
1.624 text{*no longer needed*}
1.625 -lemma (in M_axioms) restriction_is_function:
1.626 +lemma (in M_basic) restriction_is_function:
1.627 "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
1.628 ==> function(z)"
1.629 apply (rotate_tac 1)
1.630 @@ -1208,7 +1208,7 @@
1.631 apply (unfold function_def, blast)
1.632 done
1.633
1.634 -lemma (in M_axioms) restriction_abs [simp]:
1.635 +lemma (in M_basic) restriction_abs [simp]:
1.636 "[| M(f); M(A); M(z) |]
1.637 ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
1.638 apply (simp add: ball_iff_equiv restriction_def restrict_def)
1.639 @@ -1216,39 +1216,39 @@
1.640 done
1.641
1.642
1.643 -lemma (in M_axioms) M_restrict_iff:
1.644 +lemma (in M_basic) M_restrict_iff:
1.645 "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
1.646 by (simp add: restrict_def, blast dest: transM)
1.647
1.648 -lemma (in M_axioms) restrict_closed [intro,simp]:
1.649 +lemma (in M_basic) restrict_closed [intro,simp]:
1.650 "[| M(A); M(r) |] ==> M(restrict(r,A))"
1.651 apply (simp add: M_restrict_iff)
1.652 apply (insert restrict_separation [of A], simp)
1.653 done
1.654
1.655 -lemma (in M_axioms) Inter_abs [simp]:
1.656 +lemma (in M_basic) Inter_abs [simp]:
1.657 "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
1.658 apply (simp add: big_inter_def Inter_def)
1.659 apply (blast intro!: equalityI dest: transM)
1.660 done
1.661
1.662 -lemma (in M_axioms) Inter_closed [intro,simp]:
1.663 +lemma (in M_basic) Inter_closed [intro,simp]:
1.664 "M(A) ==> M(Inter(A))"
1.665 by (insert Inter_separation, simp add: Inter_def)
1.666
1.667 -lemma (in M_axioms) Int_closed [intro,simp]:
1.668 +lemma (in M_basic) Int_closed [intro,simp]:
1.669 "[| M(A); M(B) |] ==> M(A Int B)"
1.670 apply (subgoal_tac "M({A,B})")
1.671 apply (frule Inter_closed, force+)
1.672 done
1.673
1.674 -lemma (in M_axioms) Diff_closed [intro,simp]:
1.675 +lemma (in M_basic) Diff_closed [intro,simp]:
1.676 "[|M(A); M(B)|] ==> M(A-B)"
1.677 by (insert Diff_separation, simp add: Diff_def)
1.678
1.679 subsubsection{*Some Facts About Separation Axioms*}
1.680
1.681 -lemma (in M_axioms) separation_conj:
1.682 +lemma (in M_basic) separation_conj:
1.683 "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
1.684 by (simp del: separation_closed
1.685 add: separation_iff Collect_Int_Collect_eq [symmetric])
1.686 @@ -1262,24 +1262,24 @@
1.687 "A - Collect(A,P) = Collect(A, %x. ~ P(x))"
1.688 by blast
1.689
1.690 -lemma (in M_triv_axioms) Collect_rall_eq:
1.691 +lemma (in M_trivial) Collect_rall_eq:
1.692 "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) =
1.693 (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
1.694 apply simp
1.695 apply (blast intro!: equalityI dest: transM)
1.696 done
1.697
1.698 -lemma (in M_axioms) separation_disj:
1.699 +lemma (in M_basic) separation_disj:
1.700 "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
1.701 by (simp del: separation_closed
1.702 add: separation_iff Collect_Un_Collect_eq [symmetric])
1.703
1.704 -lemma (in M_axioms) separation_neg:
1.705 +lemma (in M_basic) separation_neg:
1.706 "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
1.707 by (simp del: separation_closed
1.708 add: separation_iff Diff_Collect_eq [symmetric])
1.709
1.710 -lemma (in M_axioms) separation_imp:
1.711 +lemma (in M_basic) separation_imp:
1.712 "[|separation(M,P); separation(M,Q)|]
1.713 ==> separation(M, \<lambda>z. P(z) --> Q(z))"
1.714 by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])
1.715 @@ -1287,7 +1287,7 @@
1.716 text{*This result is a hint of how little can be done without the Reflection
1.717 Theorem. The quantifier has to be bounded by a set. We also need another
1.718 instance of Separation!*}
1.719 -lemma (in M_axioms) separation_rall:
1.720 +lemma (in M_basic) separation_rall:
1.721 "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
1.722 \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
1.723 ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))"
1.724 @@ -1300,7 +1300,7 @@
1.725 subsubsection{*Functions and function space*}
1.726
1.727 text{*M contains all finite functions*}
1.728 -lemma (in M_axioms) finite_fun_closed_lemma [rule_format]:
1.729 +lemma (in M_basic) finite_fun_closed_lemma [rule_format]:
1.730 "[| n \<in> nat; M(A) |] ==> \<forall>f \<in> n -> A. M(f)"
1.731 apply (induct_tac n, simp)
1.732 apply (rule ballI)
1.733 @@ -1312,13 +1312,13 @@
1.734 apply (blast intro: apply_funtype transM restrict_type2)
1.735 done
1.736
1.737 -lemma (in M_axioms) finite_fun_closed [rule_format]:
1.738 +lemma (in M_basic) finite_fun_closed [rule_format]:
1.739 "[| f \<in> n -> A; n \<in> nat; M(A) |] ==> M(f)"
1.740 by (blast intro: finite_fun_closed_lemma)
1.741
1.742 text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
1.743 all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
1.744 -lemma (in M_axioms) is_funspace_abs [simp]:
1.745 +lemma (in M_basic) is_funspace_abs [simp]:
1.746 "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
1.747 apply (simp add: is_funspace_def)
1.748 apply (rule iffI)
1.749 @@ -1327,7 +1327,7 @@
1.750 apply simp_all
1.751 done
1.752
1.753 -lemma (in M_axioms) succ_fun_eq2:
1.754 +lemma (in M_basic) succ_fun_eq2:
1.755 "[|M(B); M(n->B)|] ==>
1.756 succ(n) -> B =
1.757 \<Union>{z. p \<in> (n->B)*B, \<exists>f[M]. \<exists>b[M]. p = <f,b> & z = {cons(<n,b>, f)}}"
1.758 @@ -1335,7 +1335,7 @@
1.759 apply (blast dest: transM)
1.760 done
1.761
1.762 -lemma (in M_axioms) funspace_succ:
1.763 +lemma (in M_basic) funspace_succ:
1.764 "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)"
1.765 apply (insert funspace_succ_replacement [of n], simp)
1.766 apply (force simp add: succ_fun_eq2 univalent_def)
1.767 @@ -1343,7 +1343,7 @@
1.768
1.769 text{*@{term M} contains all finite function spaces. Needed to prove the
1.770 absoluteness of transitive closure.*}
1.771 -lemma (in M_axioms) finite_funspace_closed [intro,simp]:
1.772 +lemma (in M_basic) finite_funspace_closed [intro,simp]:
1.773 "[|n\<in>nat; M(B)|] ==> M(n->B)"
1.774 apply (induct_tac n, simp)
1.775 apply (simp add: funspace_succ nat_into_M)
1.776 @@ -1368,37 +1368,37 @@
1.777 "is_or(M,a,b,z) == (number1(M,a) & number1(M,z)) |
1.778 (~number1(M,a) & z=b)"
1.779
1.780 -lemma (in M_triv_axioms) bool_of_o_abs [simp]:
1.781 +lemma (in M_trivial) bool_of_o_abs [simp]:
1.782 "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)"
1.783 by (simp add: is_bool_of_o_def bool_of_o_def)
1.784
1.785
1.786 -lemma (in M_triv_axioms) not_abs [simp]:
1.787 +lemma (in M_trivial) not_abs [simp]:
1.788 "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
1.789 by (simp add: Bool.not_def cond_def is_not_def)
1.790
1.791 -lemma (in M_triv_axioms) and_abs [simp]:
1.792 +lemma (in M_trivial) and_abs [simp]:
1.793 "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
1.794 by (simp add: Bool.and_def cond_def is_and_def)
1.795
1.796 -lemma (in M_triv_axioms) or_abs [simp]:
1.797 +lemma (in M_trivial) or_abs [simp]:
1.798 "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
1.799 by (simp add: Bool.or_def cond_def is_or_def)
1.800
1.801
1.802 -lemma (in M_triv_axioms) bool_of_o_closed [intro,simp]:
1.803 +lemma (in M_trivial) bool_of_o_closed [intro,simp]:
1.804 "M(bool_of_o(P))"
1.805 by (simp add: bool_of_o_def)
1.806
1.807 -lemma (in M_triv_axioms) and_closed [intro,simp]:
1.808 +lemma (in M_trivial) and_closed [intro,simp]:
1.809 "[| M(p); M(q) |] ==> M(p and q)"
1.810 by (simp add: and_def cond_def)
1.811
1.812 -lemma (in M_triv_axioms) or_closed [intro,simp]:
1.813 +lemma (in M_trivial) or_closed [intro,simp]:
1.814 "[| M(p); M(q) |] ==> M(p or q)"
1.815 by (simp add: or_def cond_def)
1.816
1.817 -lemma (in M_triv_axioms) not_closed [intro,simp]:
1.818 +lemma (in M_trivial) not_closed [intro,simp]:
1.819 "M(p) ==> M(not(p))"
1.820 by (simp add: Bool.not_def cond_def)
1.821
1.822 @@ -1416,16 +1416,16 @@
1.823 "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
1.824
1.825
1.826 -lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
1.827 +lemma (in M_trivial) Nil_in_M [intro,simp]: "M(Nil)"
1.828 by (simp add: Nil_def)
1.829
1.830 -lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
1.831 +lemma (in M_trivial) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
1.832 by (simp add: is_Nil_def Nil_def)
1.833
1.834 -lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
1.835 +lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
1.836 by (simp add: Cons_def)
1.837
1.838 -lemma (in M_triv_axioms) Cons_abs [simp]:
1.839 +lemma (in M_trivial) Cons_abs [simp]:
1.840 "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
1.841 by (simp add: is_Cons_def Cons_def)
1.842
1.843 @@ -1499,18 +1499,18 @@
1.844 "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
1.845 by (erule list.cases, simp_all)
1.846
1.847 -lemma (in M_axioms) list_case'_closed [intro,simp]:
1.848 +lemma (in M_basic) list_case'_closed [intro,simp]:
1.849 "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
1.850 apply (case_tac "quasilist(k)")
1.851 apply (simp add: quasilist_def, force)
1.852 apply (simp add: non_list_case)
1.853 done
1.854
1.855 -lemma (in M_triv_axioms) quasilist_abs [simp]:
1.856 +lemma (in M_trivial) quasilist_abs [simp]:
1.857 "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
1.858 by (auto simp add: is_quasilist_def quasilist_def)
1.859
1.860 -lemma (in M_triv_axioms) list_case_abs [simp]:
1.861 +lemma (in M_trivial) list_case_abs [simp]:
1.862 "[| relativize2(M,is_b,b); M(k); M(z) |]
1.863 ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
1.864 apply (case_tac "quasilist(k)")
1.865 @@ -1525,14 +1525,14 @@
1.866
1.867 subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
1.868
1.869 -lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
1.870 +lemma (in M_trivial) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
1.871 by (simp add: is_hd_def)
1.872
1.873 -lemma (in M_triv_axioms) is_hd_Cons:
1.874 +lemma (in M_trivial) is_hd_Cons:
1.875 "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
1.876 by (force simp add: is_hd_def)
1.877
1.878 -lemma (in M_triv_axioms) hd_abs [simp]:
1.879 +lemma (in M_trivial) hd_abs [simp]:
1.880 "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
1.881 apply (simp add: hd'_def)
1.882 apply (intro impI conjI)
1.883 @@ -1541,14 +1541,14 @@
1.884 apply (elim disjE exE, auto)
1.885 done
1.886
1.887 -lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
1.888 +lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
1.889 by (simp add: is_tl_def)
1.890
1.891 -lemma (in M_triv_axioms) is_tl_Cons:
1.892 +lemma (in M_trivial) is_tl_Cons:
1.893 "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
1.894 by (force simp add: is_tl_def)
1.895
1.896 -lemma (in M_triv_axioms) tl_abs [simp]:
1.897 +lemma (in M_trivial) tl_abs [simp]:
1.898 "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
1.899 apply (simp add: tl'_def)
1.900 apply (intro impI conjI)
1.901 @@ -1557,7 +1557,7 @@
1.902 apply (elim disjE exE, auto)
1.903 done
1.904
1.905 -lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"
1.906 +lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"
1.907 by (simp add: relativize1_def)
1.908
1.909 lemma hd'_Nil: "hd'([]) = 0"
1.910 @@ -1577,7 +1577,7 @@
1.911 apply (simp_all add: tl'_Nil)
1.912 done
1.913
1.914 -lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
1.915 +lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))"
1.916 apply (simp add: tl'_def)
1.917 apply (force simp add: quasilist_def)
1.918 done