Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf
--- a/src/ZF/Constructible/AC_in_L.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Tue Feb 04 16:19:15 2020 +0000
@@ -311,7 +311,7 @@
"well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))"
apply (simp add: DPow_r_def)
apply (rule well_ord_measure)
- apply (simp add: DPow_least_def Ord_Least)
+ apply (simp add: DPow_least_def)
apply (drule DPow_imp_DPow_least, assumption)+
apply simp
apply (blast intro: DPow_ord_unique)
@@ -357,7 +357,7 @@
Ord_mem_iff_lt)
apply (blast intro: lt_trans)
apply (rule_tac x = "succ(lrank(x))" in bexI)
- apply (simp add: Lset_succ_lrank_iff)
+ apply (simp)
apply (blast intro: Limit_has_succ ltD)
done
--- a/src/ZF/Constructible/DPow_absolute.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Tue Feb 04 16:19:15 2020 +0000
@@ -92,14 +92,13 @@
"[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
==> sats(A, satisfies_fm(x,y,z), env) \<longleftrightarrow>
is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
-by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
- sats_formula_rec_fm)
+by (simp add: satisfies_fm_def is_satisfies_def sats_formula_rec_fm)
lemma satisfies_iff_sats:
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> is_satisfies(##A, x, y, z) \<longleftrightarrow> sats(A, satisfies_fm(i,j,k), env)"
-by (simp add: sats_satisfies_fm)
+by (simp)
theorem satisfies_reflection:
"REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
@@ -294,7 +293,7 @@
apply (assumption | rule DPow_separation DPow_replacement)+
done
-theorem M_DPow_L: "PROP M_DPow(L)"
+theorem M_DPow_L: "M_DPow(L)"
apply (rule M_DPow.intro)
apply (rule M_satisfies_L)
apply (rule M_DPow_axioms_L)
@@ -443,7 +442,7 @@
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
==> is_DPow'(##A, x, y) \<longleftrightarrow> sats(A, DPow'_fm(i,j), env)"
-by (simp add: sats_DPow'_fm)
+by (simp)
theorem DPow'_reflection:
"REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
@@ -600,7 +599,7 @@
apply (assumption | rule strong_rep transrec_rep)+
done
-theorem M_Lset_L: "PROP M_Lset(L)"
+theorem M_Lset_L: "M_Lset(L)"
apply (rule M_Lset.intro)
apply (rule M_DPow_L)
apply (rule M_Lset_axioms_L)
--- a/src/ZF/Constructible/Datatype_absolute.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Feb 04 16:19:15 2020 +0000
@@ -137,7 +137,7 @@
by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
relation1_def iterates_MH_def)
-lemma (in M_basic) iterates_imp_wfrec_replacement:
+lemma (in M_trancl) iterates_imp_wfrec_replacement:
"[|relation1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|]
==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n),
Memrel(succ(n)))"
@@ -148,7 +148,7 @@
n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |]
==> is_iterates(M,isF,v,n,z) \<longleftrightarrow> z = iterates(F,n,v)"
apply (frule iterates_imp_wfrec_replacement, assumption+)
-apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
+apply (simp add: wf_Memrel trans_Memrel relation_Memrel
is_iterates_def relation2_def iterates_MH_abs
iterates_nat_def recursor_def transrec_def
eclose_sing_Ord_eq nat_into_M
@@ -161,7 +161,7 @@
n \<in> nat; M(v); \<forall>x[M]. M(F(x)) |]
==> M(iterates(F,n,v))"
apply (frule iterates_imp_wfrec_replacement, assumption+)
-apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
+apply (simp add: wf_Memrel trans_Memrel relation_Memrel
relation2_def iterates_MH_abs
iterates_nat_def recursor_def transrec_def
eclose_sing_Ord_eq nat_into_M
@@ -270,7 +270,7 @@
cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) &
is_sum(M,natnatsum,X3,Z)"
-lemma (in M_basic) formula_functor_abs [simp]:
+lemma (in M_trancl) formula_functor_abs [simp]:
"[| M(X); M(Z) |]
==> is_formula_functor(M,X,Z) \<longleftrightarrow>
Z = ((nat*nat) + (nat*nat)) + (X*X + X)"
@@ -935,13 +935,13 @@
is_formula_case (M, is_a, is_b, is_c, is_d),
formula_rec_case(a, b, c, d, h))"
apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
-apply (simp add: formula_case_abs)
+apply (simp)
done
text\<open>This locale packages the premises of the following theorems,
which is the normal purpose of locales. It doesn't accumulate
- constraints on the class \<^term>\<open>M\<close>, as in most of this deveopment.\<close>
+ constraints on the class \<^term>\<open>M\<close>, as in most of this development.\<close>
locale Formula_Rec = M_eclose +
fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
defines
--- a/src/ZF/Constructible/Formula.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Formula.thy Tue Feb 04 16:19:15 2020 +0000
@@ -162,32 +162,32 @@
lemma conj_iff_sats:
"[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
==> (P & Q) \<longleftrightarrow> sats(A, And(p,q), env)"
-by (simp add: sats_And_iff)
+by (simp)
lemma disj_iff_sats:
"[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
==> (P | Q) \<longleftrightarrow> sats(A, Or(p,q), env)"
-by (simp add: sats_Or_iff)
+by (simp)
lemma iff_iff_sats:
"[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
==> (P \<longleftrightarrow> Q) \<longleftrightarrow> sats(A, Iff(p,q), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
lemma imp_iff_sats:
"[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
==> (P \<longrightarrow> Q) \<longleftrightarrow> sats(A, Implies(p,q), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
lemma ball_iff_sats:
"[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
==> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Forall(p), env)"
-by (simp add: sats_Forall_iff)
+by (simp)
lemma bex_iff_sats:
"[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
==> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Exists(p), env)"
-by (simp add: sats_Exists_iff)
+by (simp)
lemmas FOL_iff_sats =
mem_iff_sats equal_iff_sats not_iff_sats conj_iff_sats
@@ -451,7 +451,7 @@
apply typecheck
apply (rule conjI)
(*finally check the arity!*)
- apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
+ apply (simp add: arity_iterates_incr_bv1_eq Un_least_lt_iff)
apply (force intro: add_le_self le_trans)
apply (simp add: arity_sats1_iff formula_add_params1, blast)
done
--- a/src/ZF/Constructible/Internalize.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Internalize.thy Tue Feb 04 16:19:15 2020 +0000
@@ -343,7 +343,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> is_Member(##A, x, y, z) \<longleftrightarrow> sats(A, Member_fm(i,j,k), env)"
-by (simp add: sats_Member_fm)
+by (simp)
theorem Member_reflection:
"REFLECTS[\<lambda>x. is_Member(L,f(x),g(x),h(x)),
@@ -376,7 +376,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> is_Equal(##A, x, y, z) \<longleftrightarrow> sats(A, Equal_fm(i,j,k), env)"
-by (simp add: sats_Equal_fm)
+by (simp)
theorem Equal_reflection:
"REFLECTS[\<lambda>x. is_Equal(L,f(x),g(x),h(x)),
@@ -409,7 +409,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> is_Nand(##A, x, y, z) \<longleftrightarrow> sats(A, Nand_fm(i,j,k), env)"
-by (simp add: sats_Nand_fm)
+by (simp)
theorem Nand_reflection:
"REFLECTS[\<lambda>x. is_Nand(L,f(x),g(x),h(x)),
@@ -440,7 +440,7 @@
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j \<in> nat; env \<in> list(A)|]
==> is_Forall(##A, x, y) \<longleftrightarrow> sats(A, Forall_fm(i,j), env)"
-by (simp add: sats_Forall_fm)
+by (simp)
theorem Forall_reflection:
"REFLECTS[\<lambda>x. is_Forall(L,f(x),g(x)),
@@ -737,7 +737,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> cartprod(##A, x, y, z) \<longleftrightarrow> sats(A, cartprod_fm(i,j,k), env)"
-by (simp add: sats_cartprod_fm)
+by (simp)
theorem cartprod_reflection:
"REFLECTS[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
@@ -1043,7 +1043,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
==> is_eclose_n(##A, x, y, z) \<longleftrightarrow> sats(A, eclose_n_fm(i,j,k), env)"
-by (simp add: sats_eclose_n_fm)
+by (simp)
theorem eclose_n_reflection:
"REFLECTS[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),
@@ -1186,7 +1186,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
==> is_list_N(##A, x, y, z) \<longleftrightarrow> sats(A, list_N_fm(i,j,k), env)"
-by (simp add: sats_list_N_fm)
+by (simp)
theorem list_N_reflection:
"REFLECTS[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
@@ -1336,7 +1336,7 @@
"[| nth(i,env) = x; nth(j,env) = y;
i < length(env); j < length(env); env \<in> list(A)|]
==> is_formula_N(##A, x, y) \<longleftrightarrow> sats(A, formula_N_fm(i,j), env)"
-by (simp add: sats_formula_N_fm)
+by (simp)
theorem formula_N_reflection:
"REFLECTS[\<lambda>x. is_formula_N(L, f(x), g(x)),
--- a/src/ZF/Constructible/L_axioms.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Feb 04 16:19:15 2020 +0000
@@ -78,6 +78,17 @@
apply (simp_all add: Replace_iff univalent_def, blast)
done
+lemma strong_replacementI [rule_format]:
+ "[| \<forall>B[L]. separation(L, %u. \<exists>x[L]. x\<in>B & P(x,u)) |]
+ ==> strong_replacement(L,P)"
+apply (simp add: strong_replacement_def, clarify)
+apply (frule replacementD [OF replacement], assumption, clarify)
+apply (drule_tac x=A in rspec, clarify)
+apply (drule_tac z=Y in separationD, assumption, clarify)
+apply (rule_tac x=y in rexI, force, assumption)
+done
+
+
subsection\<open>Instantiating the locale \<open>M_trivial\<close>\<close>
text\<open>No instances of Separation yet.\<close>
@@ -89,14 +100,14 @@
lemmas L_nat = Ord_in_L [OF Ord_nat]
-theorem M_trivial_L: "PROP M_trivial(L)"
+theorem M_trivial_L: "M_trivial(L)"
apply (rule M_trivial.intro)
- apply (erule (1) transL)
+ apply (rule M_trans.intro)
+ apply (erule (1) transL)
+ apply(rule exI,rule nonempty)
+ apply (rule M_trivial_axioms.intro)
apply (rule upair_ax)
- apply (rule Union_ax)
- apply (rule power_ax)
- apply (rule replacement)
- apply (rule L_nat)
+ apply (rule Union_ax)
done
interpretation L?: M_trivial L by (rule M_trivial_L)
@@ -352,7 +363,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> upair(##A, x, y, z) \<longleftrightarrow> sats(A, upair_fm(i,j,k), env)"
-by (simp add: sats_upair_fm)
+by (simp)
text\<open>Useful? At least it refers to "real" unordered pairs\<close>
lemma sats_upair_fm2 [simp]:
@@ -394,7 +405,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> pair(##A, x, y, z) \<longleftrightarrow> sats(A, pair_fm(i,j,k), env)"
-by (simp add: sats_pair_fm)
+by (simp)
theorem pair_reflection:
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),
@@ -426,7 +437,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> union(##A, x, y, z) \<longleftrightarrow> sats(A, union_fm(i,j,k), env)"
-by (simp add: sats_union_fm)
+by (simp)
theorem union_reflection:
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),
@@ -671,7 +682,7 @@
"[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)|]
==> pred_set(##A,U,x,r,B) \<longleftrightarrow> sats(A, pred_set_fm(i,j,k,l), env)"
-by (simp add: sats_pred_set_fm)
+by (simp)
theorem pred_set_reflection:
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),
@@ -815,7 +826,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> image(##A, x, y, z) \<longleftrightarrow> sats(A, image_fm(i,j,k), env)"
-by (simp add: sats_image_fm)
+by (simp)
theorem image_reflection:
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),
@@ -851,7 +862,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> pre_image(##A, x, y, z) \<longleftrightarrow> sats(A, pre_image_fm(i,j,k), env)"
-by (simp add: sats_pre_image_fm)
+by (simp)
theorem pre_image_reflection:
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)),
--- a/src/ZF/Constructible/Normal.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Normal.thy Tue Feb 04 16:19:15 2020 +0000
@@ -64,12 +64,12 @@
apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union,
clarify)
apply (rule_tac x="i++nat" in exI)
-apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0)
+apply (blast intro: oadd_lt_self oadd_LimitI Limit_has_0)
done
text\<open>The class of cardinals, \<^term>\<open>Card\<close>, is closed and unbounded.\<close>
theorem Closed_Unbounded_Card [simp]: "Closed_Unbounded(Card)"
-apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def)
apply (blast intro: lt_csucc Card_csucc)
done
@@ -101,7 +101,7 @@
lemma (in cub_family) Ord_next_greater:
"Ord(next_greater(a,x))"
-by (simp add: next_greater_def Ord_Least)
+by (simp add: next_greater_def)
text\<open>\<^term>\<open>next_greater\<close> works as expected: it returns a larger value
and one that belongs to class \<^term>\<open>P(a)\<close>.\<close>
@@ -146,10 +146,10 @@
@{subgoals[display,indent=0,margin=65]}
\<close>
apply (rule UN_least_le)
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+apply (blast intro: Ord_iterates Ord_sup_greater)
apply (rule_tac a="succ(n)" in UN_upper_le)
apply (simp_all add: next_greater_le_sup_greater)
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+apply (blast intro: Ord_iterates Ord_sup_greater)
done
lemma (in cub_family) P_omega_sup_greater:
@@ -166,7 +166,7 @@
apply (simp add: iterates_omega_def)
apply (rule UN_upper_lt [of 1], simp_all)
apply (blast intro: sup_greater_gt)
-apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+apply (blast intro: Ord_iterates Ord_sup_greater)
done
lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
@@ -299,7 +299,7 @@
apply (simp add: mono_le_subset_def, blast intro: leI)
txt\<open>Second inclusion:\<close>
apply (rule UN_least)
-apply (frule Union_upper_le, blast, blast intro: Ord_Union)
+apply (frule Union_upper_le, blast, blast)
apply (erule leE, drule ltD, elim UnionE)
apply (simp add: OUnion_def)
apply blast+
@@ -327,7 +327,7 @@
lemma Ord_iterates_Normal:
"[| n\<in>nat; Normal(F); Ord(x) |] ==> Ord(F^n (x))"
-by (simp add: Ord_iterates)
+by (simp)
text\<open>THIS RESULT IS UNUSED\<close>
lemma iterates_omega_Limit:
@@ -337,7 +337,7 @@
apply (rule increasing_LimitI)
\<comment> \<open>this lemma is @{thm increasing_LimitI [no_vars]}\<close>
apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord
- Ord_UN Ord_iterates lt_imp_0_lt
+ Ord_iterates lt_imp_0_lt
iterates_Normal_increasing, clarify)
apply (rule bexI)
apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])
--- a/src/ZF/Constructible/Rank.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rank.thy Tue Feb 04 16:19:15 2020 +0000
@@ -109,7 +109,7 @@
apply (blast intro: wellordered_subset [OF _ pred_subset])
apply (simp add: trans_pred_pred_eq)
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
- apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
+ apply (simp_all add: pred_iff)
txt\<open>case \<^term>\<open>j<i\<close> also yields a contradiction\<close>
apply (frule restrict_ord_iso2, assumption+)
apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun])
@@ -162,7 +162,7 @@
==> z \<in> f \<longleftrightarrow>
(\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) &
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
-apply (simp add: omap_def Memrel_closed pred_closed)
+apply (simp add: omap_def)
apply (rule iffI)
apply (drule_tac [2] x=z in rspec)
apply (drule_tac x=z in rspec)
@@ -222,7 +222,7 @@
lemma (in M_ordertype) domain_omap:
"[| omap(M,A,r,f); M(A); M(r); M(B); M(f) |]
==> domain(f) = obase(M,A,r)"
-apply (simp add: domain_closed obase_def)
+apply (simp add: obase_def)
apply (rule equality_iffI)
apply (simp add: domain_iff omap_iff, blast)
done
@@ -354,16 +354,14 @@
apply (simp add: strong_replacement_def)
apply (drule_tac x="obase(M,A,r)" in rspec)
apply (simp add: obase_exists)
-apply (simp add: Memrel_closed pred_closed obase_def)
+apply (simp add: obase_def)
apply (erule impE)
apply (clarsimp simp add: univalent_def)
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)
apply (rule_tac x=Y in rexI)
-apply (simp add: Memrel_closed pred_closed obase_def, blast, assumption)
+apply (simp add: obase_def, blast, assumption)
done
-declare rall_simps [simp] rex_simps [simp]
-
lemma (in M_ordertype) otype_exists:
"[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)"
apply (insert omap_exists [of A r])
@@ -379,7 +377,7 @@
apply (rename_tac i)
apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
apply (rule Ord_otype)
- apply (force simp add: otype_def range_closed)
+ apply (force simp add: otype_def)
apply (simp_all add: wellordered_is_trans_on)
done
@@ -484,9 +482,9 @@
==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) \<longrightarrow> x < a \<longrightarrow> f`x = i \<union> f``x)"
apply (frule lt_Ord)
-apply (simp add: is_oadd_fun_def Memrel_closed Un_closed
+apply (simp add: is_oadd_fun_def
relation2_def is_recfun_abs [of "%x g. i \<union> g``x"]
- image_closed is_recfun_iff_equation
+ is_recfun_iff_equation
Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
apply (simp add: lt_def)
apply (blast dest: transM)
@@ -559,7 +557,7 @@
apply (simp add: oadd_eq_if_raw_oadd, clarify)
apply (simp add: raw_oadd_eq_oadd)
apply (frule exists_oadd_fun [of j i], auto)
-apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric])
+apply (simp add: is_oadd_fun_iff_oadd [symmetric])
done
@@ -605,7 +603,7 @@
prefer 2 apply (simp add: omult_eqns_Not) \<comment> \<open>trivial, non-Ord case\<close>
apply (erule Ord_cases)
apply (simp add: omult_eqns_0)
- apply (simp add: omult_eqns_succ apply_closed oadd_closed)
+ apply (simp add: omult_eqns_succ)
apply (simp add: omult_eqns_Limit)
done
@@ -642,7 +640,7 @@
lemma (in M_ord_arith) is_omult_fun_apply_Limit:
"[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |]
==> f ` x = (\<Union>y\<in>x. f`y)"
-apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
+apply (simp add: is_omult_fun_def omult_eqns_def lt_def, clarify)
apply (drule subset_trans [OF OrdmemD], assumption+)
apply (simp add: ball_conj_distrib omult_Limit image_function)
done
@@ -905,7 +903,7 @@
for \<open>is_recfun\<close>.\<close>
apply (rule_tac a=a in rangeI)
apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
- r_into_trancl apply_recfun r_into_trancl)
+ r_into_trancl apply_recfun)
done
--- a/src/ZF/Constructible/Rank_Separation.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Tue Feb 04 16:19:15 2020 +0000
@@ -120,7 +120,7 @@
omap_replacement)+
done
-theorem M_ordertype_L: "PROP M_ordertype(L)"
+theorem M_ordertype_L: "M_ordertype(L)"
apply (rule M_ordertype.intro)
apply (rule M_basic_L)
apply (rule M_ordertype_axioms_L)
@@ -221,7 +221,7 @@
wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
done
-theorem M_wfrank_L: "PROP M_wfrank(L)"
+theorem M_wfrank_L: "M_wfrank(L)"
apply (rule M_wfrank.intro)
apply (rule M_trancl_L)
apply (rule M_wfrank_axioms_L)
--- a/src/ZF/Constructible/Rec_Separation.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Tue Feb 04 16:19:15 2020 +0000
@@ -62,7 +62,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> rtran_closure_mem(##A, x, y, z) \<longleftrightarrow> sats(A, rtran_closure_mem_fm(i,j,k), env)"
-by (simp add: sats_rtran_closure_mem_fm)
+by (simp)
lemma rtran_closure_mem_reflection:
"REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
@@ -178,10 +178,10 @@
lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
apply (rule M_trancl_axioms.intro)
- apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
+ apply (assumption | rule rtrancl_separation wellfounded_trancl_separation L_nat)+
done
-theorem M_trancl_L: "PROP M_trancl(L)"
+theorem M_trancl_L: "M_trancl(L)"
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
interpretation L?: M_trancl L by (rule M_trancl_L)
@@ -209,7 +209,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}"
in gen_separation_multi [OF list_replacement1_Reflects],
- auto simp add: nonempty)
+ auto)
apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI)
apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
@@ -231,7 +231,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{A,B,0,nat}"
in gen_separation_multi [OF list_replacement2_Reflects],
- auto simp add: L_nat nonempty)
+ auto)
apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
done
@@ -260,7 +260,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{B,n,0,Memrel(succ(n))}"
in gen_separation_multi [OF formula_replacement1_Reflects],
- auto simp add: nonempty)
+ auto)
apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI)
apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
@@ -281,7 +281,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{B,0,nat}"
in gen_separation_multi [OF formula_replacement2_Reflects],
- auto simp add: nonempty L_nat)
+ auto)
apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
done
@@ -316,7 +316,7 @@
"[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
==> is_nth(##A, x, y, z) \<longleftrightarrow> sats(A, nth_fm(i,j,k), env)"
-by (simp add: sats_nth_fm)
+by (simp)
theorem nth_reflection:
"REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),
@@ -365,7 +365,7 @@
nth_replacement)+
done
-theorem M_datatypes_L: "PROP M_datatypes(L)"
+theorem M_datatypes_L: "M_datatypes(L)"
apply (rule M_datatypes.intro)
apply (rule M_trancl_L)
apply (rule M_datatypes_axioms_L)
@@ -415,7 +415,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{A,B,nat}"
in gen_separation_multi [OF eclose_replacement2_Reflects],
- auto simp add: L_nat)
+ auto)
apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
done
@@ -428,7 +428,7 @@
apply (assumption | rule eclose_replacement1 eclose_replacement2)+
done
-theorem M_eclose_L: "PROP M_eclose(L)"
+theorem M_eclose_L: "M_eclose(L)"
apply (rule M_eclose.intro)
apply (rule M_datatypes_L)
apply (rule M_eclose_axioms_L)
--- a/src/ZF/Constructible/Reflection.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Reflection.thy Tue Feb 04 16:19:15 2020 +0000
@@ -121,7 +121,7 @@
"[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
apply (simp add: FF_def)
apply (simp_all add: cont_Ord_Union [of concl: Mset]
- Mset_cont Mset_mono_le not_emptyI Ord_F0)
+ Mset_cont Mset_mono_le not_emptyI)
apply (blast intro: F0_works)
done
--- a/src/ZF/Constructible/Relative.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Relative.thy Tue Feb 04 16:19:15 2020 +0000
@@ -1,5 +1,7 @@
(* Title: ZF/Constructible/Relative.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ With modifications by E. Gunther, M. Pagano,
+ and P. Sánchez Terraf
*)
section \<open>Relativization and Absoluteness\<close>
@@ -404,7 +406,7 @@
lemma Collect_in_univ:
"[| X \<in> univ(A); Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
-by (simp add: univ_def Collect_in_VLimit Limit_nat)
+by (simp add: univ_def Collect_in_VLimit)
lemma "separation(\<lambda>x. x \<in> univ(0), P)"
apply (simp add: separation_def, clarify)
@@ -430,7 +432,7 @@
lemma Pow_in_univ:
"[| X \<in> univ(A); Transset(A) |] ==> Pow(X) \<in> univ(A)"
-apply (simp add: univ_def Pow_in_VLimit Limit_nat)
+apply (simp add: univ_def Pow_in_VLimit)
done
lemma "power_ax(\<lambda>x. x \<in> univ(0))"
@@ -522,32 +524,52 @@
subsection\<open>Introducing a Transitive Class Model\<close>
+text\<open>The class M is assumed to be transitive and inhabited\<close>
+locale M_trans =
+ fixes M
+ assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
+ and M_inhabited: "\<exists>x . M(x)"
+
+lemma (in M_trans) nonempty [simp]: "M(0)"
+proof -
+ have "M(x) \<longrightarrow> M(0)" for x
+ proof (rule_tac P="\<lambda>w. M(w) \<longrightarrow> M(0)" in eps_induct)
+ {
+ fix x
+ assume "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" "M(x)"
+ consider (a) "\<exists>y. y\<in>x" | (b) "x=0" by auto
+ then
+ have "M(x) \<longrightarrow> M(0)"
+ proof cases
+ case a
+ then show ?thesis using \<open>\<forall>y\<in>x._\<close> \<open>M(x)\<close> transM by auto
+ next
+ case b
+ then show ?thesis by simp
+ qed
+ }
+ then show "M(x) \<longrightarrow> M(0)" if "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" for x
+ using that by auto
+ qed
+ with M_inhabited
+ show "M(0)" using M_inhabited by blast
+qed
+
text\<open>The class M is assumed to be transitive and to satisfy some
relativized ZF axioms\<close>
-locale M_trivial =
- fixes M
- assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
- and upair_ax: "upair_ax(M)"
+locale M_trivial = M_trans +
+ assumes upair_ax: "upair_ax(M)"
and Union_ax: "Union_ax(M)"
- and power_ax: "power_ax(M)"
- and replacement: "replacement(M,P)"
- and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*)
-
-text\<open>Automatically discovers the proof using \<open>transM\<close>, \<open>nat_0I\<close>
-and \<open>M_nat\<close>.\<close>
-lemma (in M_trivial) nonempty [simp]: "M(0)"
-by (blast intro: transM)
-
-lemma (in M_trivial) rall_abs [simp]:
+lemma (in M_trans) rall_abs [simp]:
"M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_trivial) rex_abs [simp]:
+lemma (in M_trans) rex_abs [simp]:
"M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_trivial) ball_iff_equiv:
+lemma (in M_trans) ball_iff_equiv:
"M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow>
(\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)"
by (blast intro: transM)
@@ -556,56 +578,76 @@
available for rewriting, universally quantified over M.
But it's not the only way to prove such equalities: its
premises \<^term>\<open>M(A)\<close> and \<^term>\<open>M(B)\<close> can be too strong.\<close>
-lemma (in M_trivial) M_equalityI:
+lemma (in M_trans) M_equalityI:
"[| !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) |] ==> A=B"
-by (blast intro!: equalityI dest: transM)
+by (blast dest: transM)
subsubsection\<open>Trivial Absoluteness Proofs: Empty Set, Pairs, etc.\<close>
-lemma (in M_trivial) empty_abs [simp]:
+lemma (in M_trans) empty_abs [simp]:
"M(z) ==> empty(M,z) \<longleftrightarrow> z=0"
apply (simp add: empty_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) subset_abs [simp]:
+lemma (in M_trans) subset_abs [simp]:
"M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B"
apply (simp add: subset_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) upair_abs [simp]:
+lemma (in M_trans) upair_abs [simp]:
"M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}"
apply (simp add: upair_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) upair_in_M_iff [iff]:
- "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
-apply (insert upair_ax, simp add: upair_ax_def)
-apply (blast intro: transM)
-done
+lemma (in M_trivial) upair_in_MI [intro!]:
+ " M(a) & M(b) \<Longrightarrow> M({a,b})"
+by (insert upair_ax, simp add: upair_ax_def)
+
+lemma (in M_trans) upair_in_MD [dest!]:
+ "M({a,b}) \<Longrightarrow> M(a) & M(b)"
+ by (blast intro: transM)
+
+lemma (in M_trivial) upair_in_M_iff [simp]:
+ "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
+ by blast
-lemma (in M_trivial) singleton_in_M_iff [iff]:
+lemma (in M_trivial) singleton_in_MI [intro!]:
+ "M(a) \<Longrightarrow> M({a})"
+ by (insert upair_in_M_iff [of a a], simp)
+
+lemma (in M_trans) singleton_in_MD [dest!]:
+ "M({a}) \<Longrightarrow> M(a)"
+ by (insert upair_in_MD [of a a], simp)
+
+lemma (in M_trivial) singleton_in_M_iff [simp]:
"M({a}) \<longleftrightarrow> M(a)"
-by (insert upair_in_M_iff [of a a], simp)
+ by blast
-lemma (in M_trivial) pair_abs [simp]:
+lemma (in M_trans) pair_abs [simp]:
"M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
apply (simp add: pair_def Pair_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) pair_in_M_iff [iff]:
- "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
-by (simp add: Pair_def)
+lemma (in M_trans) pair_in_MD [dest!]:
+ "M(<a,b>) \<Longrightarrow> M(a) & M(b)"
+ by (simp add: Pair_def, blast intro: transM)
+
+lemma (in M_trivial) pair_in_MI [intro!]:
+ "M(a) & M(b) \<Longrightarrow> M(<a,b>)"
+ by (simp add: Pair_def)
-lemma (in M_trivial) pair_components_in_M:
+lemma (in M_trivial) pair_in_M_iff [simp]:
+ "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
+ by blast
+
+lemma (in M_trans) pair_components_in_M:
"[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
-apply (simp add: Pair_def)
-apply (blast dest: transM)
-done
+ by (blast dest: transM)
lemma (in M_trivial) cartprod_abs [simp]:
"[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B"
@@ -617,29 +659,25 @@
subsubsection\<open>Absoluteness for Unions and Intersections\<close>
-lemma (in M_trivial) union_abs [simp]:
+lemma (in M_trans) union_abs [simp]:
"[| M(a); M(b); M(z) |] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b"
-apply (simp add: union_def)
-apply (blast intro: transM)
-done
+ unfolding union_def
+ by (blast intro: transM )
-lemma (in M_trivial) inter_abs [simp]:
+lemma (in M_trans) inter_abs [simp]:
"[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b"
-apply (simp add: inter_def)
-apply (blast intro: transM)
-done
+ unfolding inter_def
+ by (blast intro: transM)
-lemma (in M_trivial) setdiff_abs [simp]:
+lemma (in M_trans) setdiff_abs [simp]:
"[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = a-b"
-apply (simp add: setdiff_def)
-apply (blast intro: transM)
-done
+ unfolding setdiff_def
+ by (blast intro: transM)
-lemma (in M_trivial) Union_abs [simp]:
+lemma (in M_trans) Union_abs [simp]:
"[| M(A); M(z) |] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)"
-apply (simp add: big_union_def)
-apply (blast intro!: equalityI dest: transM)
-done
+ unfolding big_union_def
+ by (blast dest: transM)
lemma (in M_trivial) Union_closed [intro,simp]:
"M(A) ==> M(\<Union>(A))"
@@ -661,15 +699,23 @@
"[| M(a); M(z) |] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)"
by (simp add: successor_def, blast)
-lemma (in M_trivial) succ_in_M_iff [iff]:
+lemma (in M_trans) succ_in_MD [dest!]:
+ "M(succ(a)) \<Longrightarrow> M(a)"
+ unfolding succ_def
+ by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_MI [intro!]:
+ "M(a) \<Longrightarrow> M(succ(a))"
+ unfolding succ_def
+ by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_M_iff [simp]:
"M(succ(a)) \<longleftrightarrow> M(a)"
-apply (simp add: succ_def)
-apply (blast intro: transM)
-done
+ by blast
subsubsection\<open>Absoluteness for Separation and Replacement\<close>
-lemma (in M_trivial) separation_closed [intro,simp]:
+lemma (in M_trans) separation_closed [intro,simp]:
"[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
apply (insert separation, simp add: separation_def)
apply (drule rspec, assumption, clarify)
@@ -681,22 +727,10 @@
"separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
by (simp add: separation_def is_Collect_def)
-lemma (in M_trivial) Collect_abs [simp]:
+lemma (in M_trans) Collect_abs [simp]:
"[| M(A); M(z) |] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)"
-apply (simp add: is_Collect_def)
-apply (blast intro!: equalityI dest: transM)
-done
-
-text\<open>Probably the premise and conclusion are equivalent\<close>
-lemma (in M_trivial) strong_replacementI [rule_format]:
- "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
- ==> strong_replacement(M,P)"
-apply (simp add: strong_replacement_def, clarify)
-apply (frule replacementD [OF replacement], assumption, clarify)
-apply (drule_tac x=A in rspec, clarify)
-apply (drule_tac z=Y in separationD, assumption, clarify)
-apply (rule_tac x=y in rexI, force, assumption)
-done
+ unfolding is_Collect_def
+ by (blast dest: transM)
subsubsection\<open>The Operator \<^term>\<open>is_Replace\<close>\<close>
@@ -709,16 +743,15 @@
is_Replace(M, A', %x y. P'(x,y), z')"
by (simp add: is_Replace_def)
-lemma (in M_trivial) univalent_Replace_iff:
+lemma (in M_trans) univalent_Replace_iff:
"[| M(A); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))"
-apply (simp add: Replace_iff univalent_def)
-apply (blast dest: transM)
-done
+ unfolding Replace_iff univalent_def
+ by (blast dest: transM)
(*The last premise expresses that P takes M to M*)
-lemma (in M_trivial) strong_replacement_closed [intro,simp]:
+lemma (in M_trans) strong_replacement_closed [intro,simp]:
"[| strong_replacement(M,P); M(A); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
apply (simp add: strong_replacement_def)
@@ -730,7 +763,7 @@
apply (blast dest: transM)
done
-lemma (in M_trivial) Replace_abs:
+lemma (in M_trans) Replace_abs:
"[| M(A); M(z); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)"
@@ -749,7 +782,7 @@
nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f))
even for f \<in> M -> M.
*)
-lemma (in M_trivial) RepFun_closed:
+lemma (in M_trans) RepFun_closed:
"[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A,f))"
apply (simp add: RepFun_def)
@@ -760,7 +793,7 @@
text\<open>Better than \<open>RepFun_closed\<close> when having the formula \<^term>\<open>x\<in>A\<close>
makes relativization easier.\<close>
-lemma (in M_trivial) RepFun_closed2:
+lemma (in M_trans) RepFun_closed2:
"[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A, %x. f(x)))"
apply (simp add: RepFun_def)
@@ -809,35 +842,60 @@
is_lambda(M, A', %x y. is_b'(x,y), z')"
by (simp add: is_lambda_def)
-lemma (in M_trivial) image_abs [simp]:
+lemma (in M_trans) image_abs [simp]:
"[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A"
apply (simp add: image_def)
apply (rule iffI)
apply (blast intro!: equalityI dest: transM, blast)
done
+subsubsection\<open>Relativization of Powerset\<close>
+
text\<open>What about \<open>Pow_abs\<close>? Powerset is NOT absolute!
This result is one direction of absoluteness.\<close>
-lemma (in M_trivial) powerset_Pow:
+lemma (in M_trans) powerset_Pow:
"powerset(M, x, Pow(x))"
by (simp add: powerset_def)
text\<open>But we can't prove that the powerset in \<open>M\<close> includes the
real powerset.\<close>
-lemma (in M_trivial) powerset_imp_subset_Pow:
+
+lemma (in M_trans) powerset_imp_subset_Pow:
"[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
apply (simp add: powerset_def)
apply (blast dest: transM)
done
+lemma (in M_trans) powerset_abs:
+ assumes
+ "M(y)"
+ shows
+ "powerset(M,x,y) \<longleftrightarrow> y = {a\<in>Pow(x) . M(a)}"
+proof (intro iffI equalityI)
+ (* First show the converse implication by double inclusion *)
+ assume "powerset(M,x,y)"
+ with \<open>M(y)\<close>
+ show "y \<subseteq> {a\<in>Pow(x) . M(a)}"
+ using powerset_imp_subset_Pow transM by blast
+ from \<open>powerset(M,x,y)\<close>
+ show "{a\<in>Pow(x) . M(a)} \<subseteq> y"
+ using transM unfolding powerset_def by auto
+next (* we show the direct implication *)
+ assume
+ "y = {a \<in> Pow(x) . M(a)}"
+ then
+ show "powerset(M, x, y)"
+ unfolding powerset_def subset_def using transM by blast
+qed
+
subsubsection\<open>Absoluteness for the Natural Numbers\<close>
lemma (in M_trivial) nat_into_M [intro]:
"n \<in> nat ==> M(n)"
by (induct n rule: nat_induct, simp_all)
-lemma (in M_trivial) nat_case_closed [intro,simp]:
+lemma (in M_trans) nat_case_closed [intro,simp]:
"[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
apply (case_tac "k=0", simp)
apply (case_tac "\<exists>m. k = succ(m)", force)
@@ -873,15 +931,15 @@
subsection\<open>Absoluteness for Ordinals\<close>
text\<open>These results constitute Theorem IV 5.1 of Kunen (page 126).\<close>
-lemma (in M_trivial) lt_closed:
+lemma (in M_trans) lt_closed:
"[| j<i; M(i) |] ==> M(j)"
by (blast dest: ltD intro: transM)
-lemma (in M_trivial) transitive_set_abs [simp]:
+lemma (in M_trans) transitive_set_abs [simp]:
"M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)"
by (simp add: transitive_set_def Transset_def)
-lemma (in M_trivial) ordinal_abs [simp]:
+lemma (in M_trans) ordinal_abs [simp]:
"M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)"
by (simp add: ordinal_def Ord_def)
@@ -999,8 +1057,9 @@
pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
(\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
fx \<noteq> gx))"
+ and power_ax: "power_ax(M)"
-lemma (in M_basic) cartprod_iff_lemma:
+lemma (in M_trivial) cartprod_iff_lemma:
"[| M(C); \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
@@ -1125,7 +1184,7 @@
subsubsection\<open>Domain, range and field\<close>
-lemma (in M_basic) domain_abs [simp]:
+lemma (in M_trans) domain_abs [simp]:
"[| M(r); M(z) |] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)"
apply (simp add: is_domain_def)
apply (blast intro!: equalityI dest: transM)
@@ -1136,7 +1195,7 @@
apply (simp add: domain_eq_vimage)
done
-lemma (in M_basic) range_abs [simp]:
+lemma (in M_trans) range_abs [simp]:
"[| M(r); M(z) |] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)"
apply (simp add: is_range_def)
apply (blast intro!: equalityI dest: transM)
@@ -1149,22 +1208,22 @@
lemma (in M_basic) field_abs [simp]:
"[| M(r); M(z) |] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)"
-by (simp add: domain_closed range_closed is_field_def field_def)
+by (simp add: is_field_def field_def)
lemma (in M_basic) field_closed [intro,simp]:
"M(r) ==> M(field(r))"
-by (simp add: domain_closed range_closed Un_closed field_def)
+by (simp add: field_def)
subsubsection\<open>Relations, functions and application\<close>
-lemma (in M_basic) relation_abs [simp]:
+lemma (in M_trans) relation_abs [simp]:
"M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)"
apply (simp add: is_relation_def relation_def)
apply (blast dest!: bspec dest: pair_components_in_M)+
done
-lemma (in M_basic) function_abs [simp]:
+lemma (in M_trivial) function_abs [simp]:
"M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)"
apply (simp add: is_function_def function_def, safe)
apply (frule transM, assumption)
@@ -1180,7 +1239,7 @@
apply (simp add: fun_apply_def apply_def, blast)
done
-lemma (in M_basic) typed_function_abs [simp]:
+lemma (in M_trivial) typed_function_abs [simp]:
"[| M(A); M(f) |] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A -> B"
apply (auto simp add: typed_function_def relation_def Pi_iff)
apply (blast dest: pair_components_in_M)+
@@ -1188,7 +1247,7 @@
lemma (in M_basic) injection_abs [simp]:
"[| M(A); M(f) |] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)"
-apply (simp add: injection_def apply_iff inj_def apply_closed)
+apply (simp add: injection_def apply_iff inj_def)
apply (blast dest: transM [of _ A])
done
@@ -1242,7 +1301,7 @@
apply (unfold function_def, blast)
done
-lemma (in M_basic) restriction_abs [simp]:
+lemma (in M_trans) restriction_abs [simp]:
"[| M(f); M(A); M(z) |]
==> restriction(M,f,A,z) \<longleftrightarrow> z = restrict(f,A)"
apply (simp add: ball_iff_equiv restriction_def restrict_def)
@@ -1250,7 +1309,7 @@
done
-lemma (in M_basic) M_restrict_iff:
+lemma (in M_trans) M_restrict_iff:
"M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
by (simp add: restrict_def, blast dest: transM)
@@ -1260,7 +1319,7 @@
apply (insert restrict_separation [of A], simp)
done
-lemma (in M_basic) Inter_abs [simp]:
+lemma (in M_trans) Inter_abs [simp]:
"[| M(A); M(z) |] ==> big_inter(M,A,z) \<longleftrightarrow> z = \<Inter>(A)"
apply (simp add: big_inter_def Inter_def)
apply (blast intro!: equalityI dest: transM)
@@ -1296,12 +1355,11 @@
"A - Collect(A,P) = Collect(A, %x. ~ P(x))"
by blast
-lemma (in M_trivial) Collect_rall_eq:
+lemma (in M_trans) Collect_rall_eq:
"M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
(if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
-apply simp
-apply (blast intro!: equalityI dest: transM)
-done
+ by (simp,blast dest: transM)
+
lemma (in M_basic) separation_disj:
"[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
@@ -1327,7 +1385,7 @@
==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y))"
apply (simp del: separation_closed rall_abs
add: separation_iff Collect_rall_eq)
-apply (blast intro!: Inter_closed RepFun_closed dest: transM)
+apply (blast intro!: RepFun_closed dest: transM)
done
@@ -1335,7 +1393,7 @@
text\<open>The assumption \<^term>\<open>M(A->B)\<close> is unusual, but essential: in
all but trivial cases, A->B cannot be expected to belong to \<^term>\<open>M\<close>.\<close>
-lemma (in M_basic) is_funspace_abs [simp]:
+lemma (in M_trivial) is_funspace_abs [simp]:
"[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B"
apply (simp add: is_funspace_def)
apply (rule iffI)
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Feb 04 16:19:15 2020 +0000
@@ -41,7 +41,7 @@
"[| nth(i,env) = x; nth(j,env) = y;
i \<in> nat; j < length(env); env \<in> list(A)|]
==> is_depth(##A, x, y) \<longleftrightarrow> sats(A, depth_fm(i,j), env)"
-by (simp add: sats_depth_fm)
+by (simp)
theorem depth_reflection:
"REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),
@@ -443,7 +443,7 @@
g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
\<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
x))"
-by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed)
+by (blast intro: a_closed b_closed c_closed d_closed)
lemma (in M_satisfies) fr_lam_replace:
"[|M(g); M(A)|] ==>
@@ -479,7 +479,7 @@
theorem (in M_satisfies) Formula_Rec_M:
"M(A) ==>
- PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A),
+ Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A),
satisfies_b(A), satisfies_is_b(M,A),
satisfies_c(A), satisfies_is_c(M,A),
satisfies_d(A), satisfies_is_d(M,A))"
@@ -842,7 +842,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,x,y}"
in gen_separation_multi [OF Member_Reflects],
- auto simp add: nat_into_M list_closed)
+ auto)
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
done
@@ -872,7 +872,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,x,y}"
in gen_separation_multi [OF Equal_Reflects],
- auto simp add: nat_into_M list_closed)
+ auto)
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
done
@@ -904,7 +904,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,rp,rq}"
in gen_separation_multi [OF Nand_Reflects],
- auto simp add: list_closed)
+ auto)
apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
done
@@ -943,7 +943,7 @@
apply (rule strong_replacementI)
apply (rule_tac u="{A,list(A),B,rp}"
in gen_separation_multi [OF Forall_Reflects],
- auto simp add: list_closed)
+ auto)
apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
done
@@ -1026,7 +1026,7 @@
formula_rec_replacement formula_rec_lambda_replacement)+
done
-theorem M_satisfies_L: "PROP M_satisfies(L)"
+theorem M_satisfies_L: "M_satisfies(L)"
apply (rule M_satisfies.intro)
apply (rule M_eclose_L)
apply (rule M_satisfies_axioms_L)
--- a/src/ZF/Constructible/Separation.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Separation.thy Tue Feb 04 16:19:15 2020 +0000
@@ -298,10 +298,10 @@
Inter_separation Diff_separation cartprod_separation image_separation
converse_separation restrict_separation
comp_separation pred_separation Memrel_separation
- funspace_succ_replacement is_recfun_separation)+
+ funspace_succ_replacement is_recfun_separation power_ax)+
done
-theorem M_basic_L: "PROP M_basic(L)"
+theorem M_basic_L: " M_basic(L)"
by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
interpretation L?: M_basic L by (rule M_basic_L)
--- a/src/ZF/Constructible/WF_absolute.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Feb 04 16:19:15 2020 +0000
@@ -82,17 +82,7 @@
tran_closure :: "[i=>o,i,i] => o" where
"tran_closure(M,r,t) ==
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"
-
-lemma (in M_basic) rtran_closure_mem_iff:
- "[|M(A); M(r); M(p)|]
- ==> rtran_closure_mem(M,A,r,p) \<longleftrightarrow>
- (\<exists>n[M]. n\<in>nat &
- (\<exists>f[M]. f \<in> succ(n) -> A &
- (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
- (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
-by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD])
-
-
+
locale M_trancl = M_basic +
assumes rtrancl_separation:
"[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
@@ -101,7 +91,17 @@
separation (M, \<lambda>x.
\<exists>w[M]. \<exists>wx[M]. \<exists>rp[M].
w \<in> Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \<in> rp)"
+ and M_nat [iff] : "M(nat)"
+lemma (in M_trancl) rtran_closure_mem_iff:
+ "[|M(A); M(r); M(p)|]
+ ==> rtran_closure_mem(M,A,r,p) \<longleftrightarrow>
+ (\<exists>n[M]. n\<in>nat &
+ (\<exists>f[M]. f \<in> succ(n) -> A &
+ (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
+ (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
+ apply (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD])
+done
lemma (in M_trancl) rtran_closure_rtrancl:
"M(r) ==> rtran_closure(M,r,rtrancl(r))"
@@ -130,7 +130,7 @@
lemma (in M_trancl) trancl_closed [intro,simp]:
"M(r) ==> M(trancl(r))"
-by (simp add: trancl_def comp_closed rtrancl_closed)
+by (simp add: trancl_def)
lemma (in M_trancl) trancl_abs [simp]:
"[| M(r); M(z) |] ==> tran_closure(M,r,z) \<longleftrightarrow> z = trancl(r)"
@@ -144,7 +144,7 @@
relativized version. Original version is on theory WF.\<close>
lemma "[| wf[A](r); r-``A \<subseteq> A |] ==> wf[A](r^+)"
apply (simp add: wf_on_def wf_def)
-apply (safe intro!: equalityI)
+apply (safe)
apply (drule_tac x = "{x\<in>A. \<exists>w. \<langle>w,x\<rangle> \<in> r^+ & w \<in> Z}" in spec)
apply (blast elim: tranclE)
done
--- a/src/ZF/Constructible/Wellorderings.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Feb 04 16:19:15 2020 +0000
@@ -162,7 +162,7 @@
lemma (in M_basic) order_isomorphism_abs [simp]:
"[| M(A); M(B); M(f) |]
==> order_isomorphism(M,A,r,B,s,f) \<longleftrightarrow> f \<in> ord_iso(A,r,B,s)"
-by (simp add: apply_closed order_isomorphism_def ord_iso_def)
+by (simp add: order_isomorphism_def ord_iso_def)
lemma (in M_basic) pred_set_abs [simp]:
"[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) \<longleftrightarrow> B = Order.pred(A,x,r)"