Theory Replacement_Instances
theory Replacement_Instances
imports
Discipline_Function
Forcing_Data
Aleph_Relative
FiniteFun_Relative
Cardinal_Relative
Separation_Instances
begin
subsection‹More Instances of Replacement›
text‹This is the same way that we used for instances of separation.›
lemma (in M_ZF_trans) replacement_is_range :
"strong_replacement(##M, λf y. is_range(##M,f,y))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ range_fm(0,1)",THEN iffD1])
apply(rule_tac range_iff_sats[where env="[_,_]",symmetric])
apply(simp_all)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add:arity_range_fm ord_simp_union range_type)
done
lemma (in M_ZF_trans) replacement_range :
"strong_replacement(##M, λf y. y = range(f))"
using strong_replacement_cong[THEN iffD2,OF _ replacement_is_range] range_abs
by simp
lemma (in M_ZF_trans) replacement_is_domain :
"strong_replacement(##M, λf y. is_domain(##M,f,y))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ domain_fm(0,1)",THEN iffD1])
apply(rule_tac domain_iff_sats[where env="[_,_]",symmetric])
apply(simp_all)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add:arity_domain_fm ord_simp_union domain_type)
done
lemma (in M_ZF_trans) replacement_domain :
"strong_replacement(##M, λf y. y = domain(f))"
using strong_replacement_cong[THEN iffD2,OF _ replacement_is_domain]
by simp
text‹Alternatively, we can use closure under lambda and get the stronger version.›
lemma (in M_ZF_trans) lam_replacement_domain : "lam_replacement(##M, domain)"
using lam_replacement_iff_lam_closed[THEN iffD2,of domain]
Lambda_in_M[where φ="domain_fm(0,1)" and env="[]",
OF domain_type _ domain_iff_sats[symmetric] domain_abs,simplified]
arity_domain_fm[of 0 1] ord_simp_union transitivity domain_closed
by simp
text‹Then we recover the original version. Notice that we need closure because we
haven't yet interpreted \<^term>‹M_replacement›.›
lemma (in M_ZF_trans) replacement_domain' :
"strong_replacement(##M, λf y. y = domain(f))"
using lam_replacement_imp_strong_replacement_aux lam_replacement_domain domain_closed
by simp
lemma (in M_ZF_trans) lam_replacement_fst : "lam_replacement(##M, fst)"
using lam_replacement_iff_lam_closed[THEN iffD2,of fst]
Lambda_in_M[where φ="fst_fm(0,1)" and env="[]",OF
_ _ fst_iff_sats[symmetric] fst_abs] fst_type
arity_fst_fm[of 0 1] ord_simp_union transitivity fst_closed
by simp
lemma (in M_ZF_trans) replacement_fst' :
"strong_replacement(##M, λf y. y = fst(f))"
using lam_replacement_imp_strong_replacement_aux lam_replacement_fst fst_closed
by simp
lemma (in M_ZF_trans) lam_replacement_domain1 : "lam_replacement(##M, domain)"
using lam_replacement_iff_lam_closed[THEN iffD2,of domain]
Lambda_in_M[where φ="domain_fm(0,1)" and env="[]",OF
_ _ domain_iff_sats[symmetric] domain_abs] domain_type
arity_domain_fm[of 0 1] ord_simp_union transitivity domain_closed
by simp
lemma (in M_ZF_trans) lam_replacement_snd : "lam_replacement(##M, snd)"
using lam_replacement_iff_lam_closed[THEN iffD2,of snd]
Lambda_in_M[where φ="snd_fm(0,1)" and env="[]",OF
_ _ snd_iff_sats[symmetric] snd_abs] snd_type
arity_snd_fm[of 0 1] ord_simp_union transitivity snd_closed
by simp
lemma (in M_ZF_trans) replacement_snd' :
"strong_replacement(##M, λf y. y = snd(f))"
using lam_replacement_imp_strong_replacement_aux lam_replacement_snd snd_closed
by simp
lemma (in M_ZF_trans) lam_replacement_Union : "lam_replacement(##M, Union)"
using lam_replacement_iff_lam_closed[THEN iffD2,of Union]
Lambda_in_M[where φ="big_union_fm(0,1)" and env="[]",OF
_ _ _ Union_abs] union_fm_def big_union_iff_sats[symmetric]
arity_big_union_fm[of 0 1] ord_simp_union transitivity Union_closed
by simp
lemma (in M_ZF_trans) replacement_Union' :
"strong_replacement(##M, λf y. y = Union(f))"
using lam_replacement_imp_strong_replacement_aux lam_replacement_Union Union_closed
by simp
lemma (in M_ZF_trans) lam_replacement_Un :
"lam_replacement(##M, λp. fst(p) ∪ snd(p))"
using lam_replacement_iff_lam_closed[THEN iffD2,of "λp. fst(p)∪snd(p)"]
LambdaPair_in_M[where φ="union_fm(0,1,2)" and is_f="union(##M)" and env="[]",OF
union_type _ union_iff_sats[symmetric] union_abs]
arity_union_fm[of 0 1 2] ord_simp_union transitivity Un_closed fst_snd_closed
by simp
lemma (in M_ZF_trans) lam_replacement_image :
"lam_replacement(##M, λp. fst(p) `` snd(p))"
using lam_replacement_iff_lam_closed[THEN iffD2,of "λp. fst(p)``snd(p)"]
LambdaPair_in_M[where φ="image_fm(0,1,2)" and is_f="image(##M)" and env="[]",OF
image_type _ image_iff_sats[symmetric] image_abs]
arity_image_fm[of 0 1 2] ord_simp_union transitivity image_closed fst_snd_closed
by simp
synthesize "setdiff" from_definition "setdiff" assuming "nonempty"
arity_theorem for "setdiff_fm"
lemma (in M_ZF_trans) lam_replacement_Diff :
"lam_replacement(##M, λp. fst(p) - snd(p))"
using lam_replacement_iff_lam_closed[THEN iffD2,of "λp. fst(p) - snd(p)"]
LambdaPair_in_M[where φ="setdiff_fm(0,1,2)" and is_f="setdiff(##M)" and env="[]",
OF setdiff_fm_type _ setdiff_iff_sats[symmetric] setdiff_abs]
arity_setdiff_fm[of 0 1 2] ord_simp_union transitivity Diff_closed fst_snd_closed
nonempty
by simp
relationalize "first_rel" "is_first" external
synthesize "first_fm" from_definition "is_first" assuming "nonempty"
lemma (in M_ZF_trans) minimum_closed :
assumes "B∈M"
shows "minimum(r,B) ∈ M"
proof(cases "∃!b. first(b,B,r)")
case True
then
obtain b where "b = minimum(r,B)" "first(b,B,r)"
using the_equality2
unfolding minimum_def
by auto
then
show ?thesis
using first_is_elem transitivity[of b B] assms
by simp
next
case False
then show ?thesis
using zero_in_M the_0
unfolding minimum_def
by auto
qed
relationalize "minimum_rel" "is_minimum" external
definition is_minimum' where
"is_minimum'(M,R,X,u) ≡ (M(u) ∧ u ∈ X ∧ (∀v[M]. ∃a[M]. (v ∈ X ⟶ v ≠ u ⟶ a ∈ R) ∧ pair(M, u, v, a))) ∧
(∃x[M].
(M(x) ∧ x ∈ X ∧ (∀v[M]. ∃a[M]. (v ∈ X ⟶ v ≠ x ⟶ a ∈ R) ∧ pair(M, x, v, a))) ∧
(∀y[M]. M(y) ∧ y ∈ X ∧ (∀v[M]. ∃a[M]. (v ∈ X ⟶ v ≠ y ⟶ a ∈ R) ∧ pair(M, y, v, a)) ⟶ y = x)) ∨
¬ (∃x[M]. (M(x) ∧ x ∈ X ∧ (∀v[M]. ∃a[M]. (v ∈ X ⟶ v ≠ x ⟶ a ∈ R) ∧ pair(M, x, v, a))) ∧
(∀y[M]. M(y) ∧ y ∈ X ∧ (∀v[M]. ∃a[M]. (v ∈ X ⟶ v ≠ y ⟶ a ∈ R) ∧ pair(M, y, v, a)) ⟶ y = x)) ∧
empty(M, u)"
synthesize "minimum" from_definition "is_minimum'" assuming "nonempty"
arity_theorem for "minimum_fm"
lemma is_minimum_eq :
"M(R) ⟹ M(X) ⟹ M(u) ⟹ is_minimum(M,R,X,u) ⟷ is_minimum'(M,R,X,u)"
unfolding is_minimum_def is_minimum'_def is_The_def is_first_def by simp
context M_trivial
begin
lemma first_closed :
"M(B) ⟹ M(r) ⟹ first(u,r,B) ⟹ M(u)"
using transM[OF first_is_elem] by simp
is_iff_rel for "first"
unfolding is_first_def first_rel_def by auto
is_iff_rel for "minimum"
unfolding is_minimum_def minimum_rel_def
using is_first_iff The_abs nonempty
by force
end
lemma (in M_ZF_trans) lam_replacement_minimum :
"lam_replacement(##M, λp. minimum(fst(p), snd(p)))"
apply(rule_tac lam_replacement_iff_lam_closed[THEN iffD2,of "λp. minimum(fst(p),snd(p))"])
apply (auto) apply(rule minimum_closed[simplified],auto simp add:fst_snd_closed[simplified])
apply (rule_tac
LambdaPair_in_M[where φ="minimum_fm(0,1,2)" and is_f="is_minimum'(##M)" and env="[]",OF
minimum_fm_type _ minimum_iff_sats[symmetric]])
apply (auto simp: arity_minimum_fm[of 0 1 2] ord_simp_union transitivity fst_snd_closed zero_in_M)
using Upair_closed[simplified] minimum_closed is_minimum_eq is_minimum_iff minimum_abs
by simp_all
lemma (in M_ZF_trans) lam_replacement_Upair :
"lam_replacement(##M, λp. Upair(fst(p), snd(p)))"
apply(rule_tac lam_replacement_iff_lam_closed[THEN iffD2,of "λp. Upair(fst(p),snd(p))"])
apply (auto) apply(rule Upair_closed[simplified],auto simp add:fst_snd_closed[simplified])
apply (rule_tac
LambdaPair_in_M[where φ="upair_fm(0,1,2)" and is_f="upair(##M)" and env="[]",OF
upair_type _ upair_iff_sats[symmetric]])
apply (auto simp: arity_upair_fm[of 0 1 2] ord_simp_union transitivity fst_snd_closed)
using Upair_closed[simplified]
by simp
lemma (in M_ZF_trans) lam_replacement_cartprod :
"lam_replacement(##M, λp. fst(p) × snd(p))"
apply(rule_tac lam_replacement_iff_lam_closed[THEN iffD2,of "λp. fst(p)×snd(p)"])
apply (auto) apply(rule cartprod_closed[simplified],auto simp add:fst_snd_closed[simplified])
apply (rule_tac
LambdaPair_in_M[where φ="cartprod_fm(0,1,2)" and is_f="cartprod(##M)" and env="[]",OF
cartprod_type _ cartprod_iff_sats[symmetric]])
apply (auto simp: arity_cartprod_fm[of 0 1 2] ord_simp_union transitivity fst_snd_closed)
using cartprod_closed[simplified]
by simp
synthesize "pre_image" from_definition assuming "nonempty"
arity_theorem for "pre_image_fm"
lemma (in M_ZF_trans) lam_replacement_vimage :
"lam_replacement(##M, λp. fst(p) -`` snd(p))"
apply(rule_tac lam_replacement_iff_lam_closed[THEN iffD2,of "λp. fst(p)-``snd(p)"])
apply (auto) apply(rule vimage_closed[simplified],auto simp add:fst_snd_closed[simplified])
apply (rule_tac
LambdaPair_in_M[where φ="pre_image_fm(0,1,2)" and is_f="pre_image(##M)" and env="[]",OF
pre_image_fm_type _ pre_image_iff_sats[symmetric]])
apply (auto simp: arity_pre_image_fm[of 0 1 2] ord_simp_union transitivity zero_in_M)
using vimage_closed[simplified]
by simp
definition is_omega_funspace :: "[i⇒o,i,i,i]⇒o" where
"is_omega_funspace(N,B,n,z) ≡ ∃o[N]. omega(N,o) ∧ n∈o ∧is_funspace(N, n, B, z)"
synthesize "omega_funspace" from_definition "is_omega_funspace" assuming "nonempty"
arity_theorem for "omega_funspace_fm"
lemma (in M_ZF_trans) omega_funspace_abs :
"B∈M ⟹ n∈M ⟹ z∈M ⟹ is_omega_funspace(##M,B,n,z) ⟷ n∈ω ∧ is_funspace(##M,n,B,z)"
unfolding is_omega_funspace_def using nat_in_M by simp
lemma (in M_ZF_trans) replacement_is_omega_funspace :
"B∈M ⟹ strong_replacement(##M, is_omega_funspace(##M,B))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,B] ⊨ omega_funspace_fm(2,0,1)",THEN iffD1])
apply(rule_tac omega_funspace_iff_sats[where env="[_,_,B]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[B]",simplified])
apply(simp_all add:arity_omega_funspace_fm ord_simp_union)
done
lemma (in M_ZF_trans) replacement_omega_funspace :
"b∈M⟹strong_replacement(##M, λn z. n∈ω ∧ is_funspace(##M,n,b,z))"
using strong_replacement_cong[THEN iffD2,OF _ replacement_is_omega_funspace[of b]]
omega_funspace_abs[of b] setclass_iff[THEN iffD1]
by (simp del:setclass_iff)
definition HAleph_wfrec_repl_body where
"HAleph_wfrec_repl_body(N,mesa,x,z) ≡ ∃y[N].
pair(N, x, y, z) ∧
(∃f[N].
(∀z[N].
z ∈ f ⟷
(∃xa[N].
∃y[N].
∃xaa[N].
∃sx[N].
∃r_sx[N].
∃f_r_sx[N].
pair(N, xa, y, z) ∧
pair(N, xa, x, xaa) ∧
upair(N, xa, xa, sx) ∧
pre_image(N, mesa, sx, r_sx) ∧ restriction(N, f, r_sx, f_r_sx) ∧ xaa ∈ mesa ∧ is_HAleph(N, xa, f_r_sx, y))) ∧
is_HAleph(N, x, f, y))"
arity_theorem for "ordinal_fm"
arity_theorem for "is_Limit_fm"
arity_theorem for "empty_fm"
arity_theorem for "fun_apply_fm"
synthesize "HAleph_wfrec_repl_body" from_definition assuming "nonempty"
arity_theorem for "HAleph_wfrec_repl_body_fm"
lemma arity_HAleph_wfrec_repl_body : "arity(HAleph_wfrec_repl_body_fm(2,0,1)) = 3"
by (simp_all add: arity_HAleph_wfrec_repl_body_fm arity_is_If_fm ord_simp_union arity_fun_apply_fm
arity_is_Limit_fm arity_empty_fm arity_Replace_fm[where i=11])
lemma (in M_ZF_trans) replacement_HAleph_wfrec_repl_body :
"B∈M ⟹ strong_replacement(##M, HAleph_wfrec_repl_body(##M,B))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,B] ⊨ HAleph_wfrec_repl_body_fm(2,0,1)",THEN iffD1])
apply(rule_tac HAleph_wfrec_repl_body_iff_sats[where env="[_,_,B]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[B]",simplified])
apply(simp_all add: arity_HAleph_wfrec_repl_body)
done
lemma (in M_ZF_trans) HAleph_wfrec_repl :
"(##M)(sa) ⟹
(##M)(esa) ⟹
(##M)(mesa) ⟹
strong_replacement
(##M,
λx z. ∃y[##M].
pair(##M, x, y, z) ∧
(∃f[##M].
(∀z[##M].
z ∈ f ⟷
(∃xa[##M].
∃y[##M].
∃xaa[##M].
∃sx[##M].
∃r_sx[##M].
∃f_r_sx[##M].
pair(##M, xa, y, z) ∧
pair(##M, xa, x, xaa) ∧
upair(##M, xa, xa, sx) ∧
pre_image(##M, mesa, sx, r_sx) ∧ restriction(##M, f, r_sx, f_r_sx) ∧ xaa ∈ mesa ∧ is_HAleph(##M, xa, f_r_sx, y))) ∧
is_HAleph(##M, x, f, y)))"
using replacement_HAleph_wfrec_repl_body unfolding HAleph_wfrec_repl_body_def by simp
definition fst2_snd2
where "fst2_snd2(x) ≡ ⟨fst(fst(x)), snd(snd(x))⟩"
relativize functional "fst2_snd2" "fst2_snd2_rel"
relationalize "fst2_snd2_rel" "is_fst2_snd2"
lemma (in M_trivial) fst2_snd2_abs :
assumes "M(x)" "M(res)"
shows "is_fst2_snd2(M, x, res) ⟷ res = fst2_snd2(x)"
unfolding is_fst2_snd2_def fst2_snd2_def
using fst_rel_abs[symmetric] snd_rel_abs[symmetric] fst_abs snd_abs assms
by simp
synthesize "is_fst2_snd2" from_definition assuming "nonempty"
arity_theorem for "is_fst2_snd2_fm"
lemma (in M_ZF_trans) replacement_is_fst2_snd2 :
"strong_replacement(##M, is_fst2_snd2(##M))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ is_fst2_snd2_fm(0,1)",THEN iffD1])
apply(rule_tac is_fst2_snd2_iff_sats[where env="[_,_]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add: arity_is_fst2_snd2_fm ord_simp_union)
done
lemma (in M_ZF_trans) replacement_fst2_snd2 : "strong_replacement(##M, λx y. y = ⟨fst(fst(x)), snd(snd(x))⟩)"
using strong_replacement_cong[THEN iffD1,OF fst2_snd2_abs replacement_is_fst2_snd2,simplified]
unfolding fst2_snd2_def
by simp
definition fst2_sndfst_snd2
where "fst2_sndfst_snd2(x) ≡ ⟨fst(fst(x)), snd(fst(x)), snd(snd(x))⟩"
relativize functional "fst2_sndfst_snd2" "fst2_sndfst_snd2_rel"
relationalize "fst2_sndfst_snd2_rel" "is_fst2_sndfst_snd2"
lemma (in M_trivial) fst2_sndfst_snd2_abs :
assumes "M(x)" "M(res)"
shows "is_fst2_sndfst_snd2(M, x, res) ⟷ res = fst2_sndfst_snd2(x)"
unfolding is_fst2_sndfst_snd2_def fst2_sndfst_snd2_def
using fst_rel_abs[symmetric] snd_rel_abs[symmetric] fst_abs snd_abs assms
by simp
synthesize "is_fst2_sndfst_snd2" from_definition assuming "nonempty"
arity_theorem for "is_fst2_sndfst_snd2_fm"
lemma (in M_ZF_trans) replacement_is_fst2_sndfst_snd2 :
"strong_replacement(##M, is_fst2_sndfst_snd2(##M))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f] ⊨ is_fst2_sndfst_snd2_fm(0,1)",THEN iffD1])
apply(rule_tac is_fst2_sndfst_snd2_iff_sats[where env="[_,_]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[]",simplified])
apply(simp_all add: arity_is_fst2_sndfst_snd2_fm ord_simp_union)
done
lemma (in M_ZF_trans) replacement_fst2_sndfst_snd2 :
"strong_replacement(##M, λx y. y = ⟨fst(fst(x)), snd(fst(x)), snd(snd(x))⟩)"
using strong_replacement_cong[THEN iffD1,OF fst2_sndfst_snd2_abs replacement_is_fst2_sndfst_snd2,simplified]
unfolding fst2_sndfst_snd2_def
by simp
lemmas (in M_ZF_trans) M_replacement_ZF_instances = lam_replacement_domain
lam_replacement_fst lam_replacement_snd lam_replacement_Union
lam_replacement_Upair lam_replacement_image
lam_replacement_Diff lam_replacement_vimage
separation_fst_equal separation_id_rel[simplified]
separation_equal_apply separation_sndfst_eq_fstsnd
separation_fstfst_eq_fstsnd separation_fstfst_eq
separation_restrict_elem
replacement_fst2_snd2 replacement_fst2_sndfst_snd2
sublocale M_ZF_trans ⊆ M_replacement "##M"
by unfold_locales (simp_all add: M_replacement_ZF_instances del:setclass_iff)
definition RepFun_body :: "i ⇒ i ⇒ i"where
"RepFun_body(u,v) ≡ {{⟨v, x⟩} . x ∈ u}"
relativize functional "RepFun_body" "RepFun_body_rel"
relationalize "RepFun_body_rel" "is_RepFun_body"
lemma (in M_trivial) RepFun_body_abs :
assumes "M(u)" "M(v)" "M(res)"
shows "is_RepFun_body(M, u, v, res) ⟷ res = RepFun_body(u,v)"
unfolding is_RepFun_body_def RepFun_body_def
using fst_rel_abs[symmetric] snd_rel_abs[symmetric] fst_abs snd_abs assms
Replace_abs[where P="λxa a. a = {⟨v, xa⟩}" and A="u"]
univalent_triv transM[of _ u]
by auto
synthesize "is_RepFun_body" from_definition assuming "nonempty"
arity_theorem for "is_RepFun_body_fm"
lemma arity_body_repfun :
"arity( ⋅(⋅∃⋅0 = 0⋅⋅) ∧ ⋅(⋅∃⋅0 = 0⋅⋅) ∧ (⋅∃⋅cons_fm(0, 3, 2) ∧ pair_fm(5, 1, 0) ⋅⋅)⋅⋅ ) = 5"
using arity_cons_fm arity_pair_fm pred_Un_distrib union_abs1
by auto
lemma arity_RepFun : "arity(is_RepFun_body_fm(0, 1, 2)) = 3"
unfolding is_RepFun_body_fm_def
using arity_Replace_fm[OF _ _ _ _ arity_body_repfun] arity_fst_fm arity_snd_fm arity_empty_fm
pred_Un_distrib union_abs2 union_abs1
by simp
lemma (in M_ZF_trans) RepFun_SigFun_closed : "x ∈ M ⟹ z ∈ M ⟹ {{⟨z, x⟩} . x ∈ x} ∈ M"
using lam_replacement_sing_const_id lam_replacement_imp_strong_replacement RepFun_closed
transitivity singleton_in_M_iff pair_in_M_iff
by simp
lemma (in M_ZF_trans) replacement_RepFun_body :
"lam_replacement(##M, λp . {{⟨snd(p), x⟩} . x ∈ fst(p)})"
apply(rule_tac lam_replacement_iff_lam_closed[THEN iffD2,of "λp. {{⟨snd(p), x⟩} . x ∈ fst(p)}"])
using RepFun_SigFun_closed[OF fst_snd_closed[THEN conjunct1,simplified]
fst_snd_closed[THEN conjunct2,simplified]] transitivity
apply auto
apply (rule_tac
LambdaPair_in_M[where φ="is_RepFun_body_fm(0,1,2)" and is_f="is_RepFun_body(##M)" and env="[]",OF
is_RepFun_body_fm_type _ is_RepFun_body_iff_sats[symmetric]])
apply (auto simp: arity_RepFun ord_simp_union transitivity zero_in_M RepFun_body_def RepFun_body_abs RepFun_SigFun_closed)
done
sublocale M_ZF_trans ⊆ M_replacement_extra "##M"
by unfold_locales (simp_all add: replacement_RepFun_body
lam_replacement_minimum del:setclass_iff)
sublocale M_ZF_trans ⊆ M_Perm "##M"
using separation_PiP_rel separation_injP_rel separation_surjP_rel
lam_replacement_imp_strong_replacement[OF
lam_replacement_Sigfun[OF lam_replacement_constant]]
Pi_replacement1 unfolding Sigfun_def
by unfold_locales simp_all
definition order_eq_map where
"order_eq_map(M,A,r,a,z) ≡ ∃x[M]. ∃g[M]. ∃mx[M]. ∃par[M].
ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)"
synthesize "order_eq_map" from_definition assuming "nonempty"
arity_theorem for "is_ord_iso_fm"
arity_theorem for "order_eq_map_fm"
lemma (in M_ZF_trans) replacement_is_order_eq_map :
"A∈M ⟹ r∈M ⟹ strong_replacement(##M, order_eq_map(##M,A,r))"
apply(rule_tac strong_replacement_cong[
where P="λ x f. M,[x,f,A,r] ⊨ order_eq_map_fm(2,3,0,1)",THEN iffD1])
apply(rule_tac order_eq_map_iff_sats[where env="[_,_,A,r]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[A,r]",simplified])
apply(simp_all add: arity_order_eq_map_fm ord_simp_union)
done
synthesize "is_banach_functor" from_definition assuming "nonempty"
arity_theorem for "is_banach_functor_fm"
definition banach_body_iterates where
"banach_body_iterates(M,X,Y,f,g,W,n,x,z) ≡
∃y[M].
pair(M, x, y, z) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃xa[M].
∃y[M].
∃xaa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M]. ∃sn[M]. ∃msn[M]. successor(M,n,sn) ∧
membership(M,sn,msn) ∧
pair(M, xa, y, z) ∧
pair(M, xa, x, xaa) ∧
upair(M, xa, xa, sx) ∧
pre_image(M, msn, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xaa ∈ msn ∧
(empty(M, xa) ⟶ y = W) ∧
(∀m[M].
successor(M, m, xa) ⟶
(∃gm[M].
is_apply(M, f_r_sx, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, xa) ∨ empty(M, y)))) ∧
(empty(M, x) ⟶ y = W) ∧
(∀m[M].
successor(M, m, x) ⟶
(∃gm[M]. is_apply(M, fa, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, x) ∨ empty(M, y)))"
synthesize "is_quasinat" from_definition assuming "nonempty"
arity_theorem for "is_quasinat_fm"
synthesize "banach_body_iterates" from_definition assuming "nonempty"
arity_theorem for "banach_body_iterates_fm"
lemma (in M_ZF_trans) banach_iterates :
assumes "X∈M" "Y∈M" "f∈M" "g∈M" "W∈M"
shows "iterates_replacement(##M, is_banach_functor(##M,X,Y,f,g), W)"
proof -
have "strong_replacement(##M, λ x z . banach_body_iterates(##M,X,Y,f,g,W,n,x,z))" if "n∈ω" for n
apply(rule_tac strong_replacement_cong[
where P="λ x z. M,[x,z,_,W,g,f,Y,X] ⊨ banach_body_iterates_fm(7,6,5,4,3,2,0,1)",THEN iffD1])
prefer 2
apply(rule_tac replacement_ax[where env="[n,W,g,f,Y,X]",simplified])
using assms that
by(simp_all add:zero_in_M arity_banach_body_iterates_fm ord_simp_union transitivity[OF _ nat_in_M])
then
show ?thesis
using assms zero_in_M transitivity[OF _ nat_in_M] Memrel_closed
unfolding iterates_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
is_nat_case_def iterates_MH_def banach_body_iterates_def
by simp
qed
definition banach_is_iterates_body where
"banach_is_iterates_body(M,X,Y,f,g,W,n,y) ≡ ∃om[M]. omega(M,om) ∧ n ∈ om ∧
(∃sn[M].
∃msn[M].
successor(M, n, sn) ∧
membership(M, sn, msn) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃x[M].
∃y[M].
∃xa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, x, y, z) ∧
pair(M, x, n, xa) ∧
upair(M, x, x, sx) ∧
pre_image(M, msn, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xa ∈ msn ∧
(empty(M, x) ⟶ y = W) ∧
(∀m[M].
successor(M, m, x) ⟶
(∃gm[M].
fun_apply(M, f_r_sx, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, x) ∨ empty(M, y)))) ∧
(empty(M, n) ⟶ y = W) ∧
(∀m[M].
successor(M, m, n) ⟶
(∃gm[M]. fun_apply(M, fa, m, gm) ∧ is_banach_functor(M, X, Y, f, g, gm, y))) ∧
(is_quasinat(M, n) ∨ empty(M, y))))"
synthesize "banach_is_iterates_body" from_definition assuming "nonempty"
arity_theorem for "banach_is_iterates_body_fm"
lemma (in M_ZF_trans) banach_replacement_iterates :
assumes "X∈M" "Y∈M" "f∈M" "g∈M" "W∈M"
shows "strong_replacement(##M, λn y. n∈ω ∧ is_iterates(##M,is_banach_functor(##M,X, Y, f, g),W,n,y))"
proof -
have "strong_replacement(##M, λ n z . banach_is_iterates_body(##M,X,Y,f,g,W,n,z))"
apply(rule_tac strong_replacement_cong[
where P="λ n z. M,[n,z,W,g,f,Y,X] ⊨ banach_is_iterates_body_fm(6,5,4,3,2,0,1)",THEN iffD1])
prefer 2
apply(rule_tac replacement_ax[where env="[W,g,f,Y,X]",simplified])
using assms
by(simp_all add:zero_in_M arity_banach_is_iterates_body_fm ord_simp_union transitivity[OF _ nat_in_M])
then
show ?thesis
using assms nat_in_M
unfolding is_iterates_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
is_nat_case_def iterates_MH_def banach_is_iterates_body_def
by simp
qed
lemma (in M_ZF_trans) banach_replacement :
assumes "(##M)(X)" "(##M)(Y)" "(##M)(f)" "(##M)(g)"
shows "strong_replacement(##M, λn y. n∈nat ∧ y = banach_functor(X, Y, f, g)^n (0))"
using iterates_abs[OF banach_iterates banach_functor_abs,of X Y f g]
assms banach_functor_closed zero_in_M
apply (rule_tac strong_replacement_cong[THEN iffD1, OF _ banach_replacement_iterates[of X Y f g 0]])
by(rule_tac conj_cong,simp_all)
lemma (in M_ZF_trans) lam_replacement_cardinal : "lam_replacement(##M, cardinal_rel(##M))"
using lam_replacement_iff_lam_closed[THEN iffD2,of "cardinal_rel(##M)"]
cardinal_rel_closed[of _]
Lambda_in_M[where φ="is_cardinal_fm(0,1)" and env="[]",OF
is_cardinal_fm_type[of 0 1] _ is_cardinal_iff_sats[symmetric] is_cardinal_iff]
arity_is_cardinal_fm[of 0 1] ord_simp_union cardinal_rel_closed transitivity zero_in_M
by simp_all
definition trans_apply_image where
"trans_apply_image(f) ≡ λa g. f ` (g `` a)"
relativize functional "trans_apply_image" "trans_apply_image_rel"
relationalize "trans_apply_image" "is_trans_apply_image"
schematic_goal arity_is_recfun_fm [arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ r ∈ ω ⟹ arity(is_recfun_fm(p, a, z ,r)) = ?ar"
unfolding is_recfun_fm_def
by (simp add:arity)
schematic_goal arity_is_wfrec_fm [arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ r ∈ ω ⟹ arity(is_wfrec_fm(p, a, z ,r)) = ?ar"
unfolding is_wfrec_fm_def
by (simp add:arity)
schematic_goal arity_is_transrec_fm [arity]:
"p ∈ formula ⟹ a ∈ ω ⟹ z ∈ ω ⟹ arity(is_transrec_fm(p, a, z)) = ?ar"
unfolding is_transrec_fm_def
by (simp add:arity)
synthesize "is_trans_apply_image" from_definition assuming "nonempty"
arity_theorem for "is_trans_apply_image_fm"
lemma (in M_basic) rel2_trans_apply :
"M(f) ⟹ relation2(M,is_trans_apply_image(M,f),trans_apply_image(f))"
unfolding is_trans_apply_image_def trans_apply_image_def relation2_def
by auto
lemma (in M_basic) apply_image_closed :
shows "M(f) ⟹ ∀x[M]. ∀g[M]. function(g) ⟶ M(trans_apply_image(f, x, g))"
unfolding trans_apply_image_def by simp
lemma (in M_basic) apply_image_closed' :
shows "M(f) ⟹ ∀x[M]. ∀g[M]. M(trans_apply_image(f, x, g))"
unfolding trans_apply_image_def by simp
definition transrec_apply_image_body where
"transrec_apply_image_body(M,f,mesa,x,z) ≡ ∃y[M]. pair(M, x, y, z) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃xa[M].
∃y[M].
∃xaa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, xa, y, z) ∧
pair(M, xa, x, xaa) ∧
upair(M, xa, xa, sx) ∧
pre_image(M, mesa, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xaa ∈ mesa ∧ is_trans_apply_image(M, f, xa, f_r_sx, y))) ∧
is_trans_apply_image(M, f, x, fa, y))"
synthesize "transrec_apply_image_body" from_definition assuming "nonempty"
arity_theorem for "transrec_apply_image_body_fm"
lemma (in M_ZF_trans) replacement_transrec_apply_image_body :
"(##M)(f) ⟹ (##M)(mesa) ⟹ strong_replacement(##M,transrec_apply_image_body(##M,f,mesa))"
apply(rule_tac strong_replacement_cong[
where P="λ x z. M,[x,z,mesa,f] ⊨ transrec_apply_image_body_fm(3,2,0,1)",THEN iffD1])
apply(rule_tac transrec_apply_image_body_iff_sats[where env="[_,_,mesa,f]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[mesa,f]",simplified])
apply(simp_all add: arity_transrec_apply_image_body_fm ord_simp_union)
done
lemma (in M_ZF_trans) transrec_replacement_apply_image :
assumes "(##M)(f)" "(##M)(α)"
shows "transrec_replacement(##M, is_trans_apply_image(##M, f), α)"
unfolding transrec_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
using replacement_transrec_apply_image_body[unfolded transrec_apply_image_body_def] assms
Memrel_closed singleton_closed eclose_closed
by simp
lemma (in M_ZF_trans) rec_trans_apply_image_abs :
assumes "(##M)(f)" "(##M)(x)" "(##M)(y)" "Ord(x)"
shows "is_transrec(##M,is_trans_apply_image(##M, f),x,y) ⟷ y = transrec(x,trans_apply_image(f))"
using transrec_abs[OF transrec_replacement_apply_image rel2_trans_apply] assms apply_image_closed
by simp
definition is_trans_apply_image_body where
"is_trans_apply_image_body(M,f,β,a,w) ≡ ∃z[M]. pair(M,a,z,w) ∧ a∈β ∧ (∃sa[M].
∃esa[M].
∃mesa[M].
upair(M, a, a, sa) ∧
is_eclose(M, sa, esa) ∧
membership(M, esa, mesa) ∧
(∃fa[M].
(∀z[M].
z ∈ fa ⟷
(∃x[M].
∃y[M].
∃xa[M].
∃sx[M].
∃r_sx[M].
∃f_r_sx[M].
pair(M, x, y, z) ∧
pair(M, x, a, xa) ∧
upair(M, x, x, sx) ∧
pre_image(M, mesa, sx, r_sx) ∧
restriction(M, fa, r_sx, f_r_sx) ∧
xa ∈ mesa ∧ is_trans_apply_image(M, f, x, f_r_sx, y))) ∧
is_trans_apply_image(M, f, a, fa, z)))"
manual_schematic "is_trans_apply_image_body_schematic" for "is_trans_apply_image_body"assuming "nonempty"
unfolding is_trans_apply_image_body_def
by (rule sep_rules is_eclose_iff_sats is_trans_apply_image_iff_sats | simp)+
synthesize "is_trans_apply_image_body" from_schematic "is_trans_apply_image_body_schematic"
arity_theorem for "is_trans_apply_image_body_fm"
lemma (in M_ZF_trans) replacement_is_trans_apply_image :
"(##M)(f) ⟹ (##M)(β) ⟹ strong_replacement(##M, λ x z .
∃y[##M]. pair(##M,x,y,z) ∧ x∈β ∧ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
unfolding is_transrec_def is_wfrec_def M_is_recfun_def
apply(rule_tac strong_replacement_cong[
where P="λ x z. M,[x,z,β,f] ⊨ is_trans_apply_image_body_fm(3,2,0,1)",THEN iffD1])
apply(rule_tac is_trans_apply_image_body_iff_sats[symmetric,unfolded is_trans_apply_image_body_def,where env="[_,_,β,f]"])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[β,f]",simplified])
apply(simp_all add: arity_is_trans_apply_image_body_fm is_trans_apply_image_body_fm_type ord_simp_union)
done
lemma (in M_ZF_trans) trans_apply_abs :
"(##M)(f) ⟹ (##M)(β) ⟹ Ord(β) ⟹ (##M)(x) ⟹ (##M)(z) ⟹
(x∈β ∧ z = ⟨x, transrec(x, λa g. f ` (g `` a)) ⟩) ⟷
(∃y[##M]. pair(##M,x,y,z) ∧ x∈β ∧ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
using rec_trans_apply_image_abs Ord_in_Ord
transrec_closed[OF transrec_replacement_apply_image rel2_trans_apply,of f,simplified]
apply_image_closed'[of f]
unfolding trans_apply_image_def
by auto
lemma (in M_ZF_trans) replacement_trans_apply_image :
"(##M)(f) ⟹ (##M)(β) ⟹ Ord(β) ⟹
strong_replacement(##M, λx y. x∈β ∧ y = ⟨x, transrec(x, λa g. f ` (g `` a))⟩)"
using strong_replacement_cong[THEN iffD1,OF _ replacement_is_trans_apply_image,simplified]
trans_apply_abs Ord_in_Ord
by simp
definition abs_apply_pair where
"abs_apply_pair(A,f,x) ≡ ⟨x, λn∈A. f ` ⟨x, n⟩⟩"
relativize functional "abs_apply_pair" "abs_apply_pair_rel"
relationalize "abs_apply_pair_rel" "is_abs_apply_pair"
lemma (in M_basic) abs_apply_pair_rel :
assumes "M(A)" "M(f)" "M(x)"
shows "Relation1(M,A,λn a. ∃b[M]. is_apply(M, f, b, a) ∧ pair(M, x, n, b), λn. f ` ⟨x, n⟩)"
using fst_rel_abs[symmetric] snd_rel_abs[symmetric] fst_abs snd_abs assms
unfolding Relation1_def
by auto
lemma (in M_basic) abs_apply_pair_abs :
assumes "M(A)" "M(f)" "M(x)" "M(res)"
shows "is_abs_apply_pair(M,A,f, x, res) ⟷ res = abs_apply_pair(A,f,x)"
unfolding is_abs_apply_pair_def abs_apply_pair_def
using fst_rel_abs[symmetric] snd_rel_abs[symmetric] fst_abs snd_abs assms
pair_abs lambda_abs2[OF abs_apply_pair_rel]
by auto
synthesize "is_abs_apply_pair" from_definition assuming "nonempty"
lemma arity_is_abs_aux : "arity((⋅∃⋅⋅7`0 is 1⋅ ∧ pair_fm(5, 2, 0) ⋅⋅)) = 7"
using arity_fun_apply_fm arity_pair_fm pred_Un_distrib
ord_simp_union by simp
lemma arity_is_abs_apply_pair_fm :
shows "arity(is_abs_apply_pair_fm(3, 2, 0, 1)) = 4"
unfolding is_abs_apply_pair_fm_def
using arity_lambda_fm[OF _ _ _ _ arity_is_abs_aux] arity_pair_fm
pred_Un_distrib ord_simp_union
by simp
lemma (in M_ZF_trans) replacement_is_abs_apply_pair :
assumes "A∈M" "f∈M"
shows "strong_replacement(##M, is_abs_apply_pair(##M,A,f))"
using assms
apply(rule_tac strong_replacement_cong[
where P="λ x z. M,[x,z,f,A] ⊨ is_abs_apply_pair_fm(3,2,0,1)",THEN iffD1])
apply(rule_tac is_abs_apply_pair_iff_sats[where env="[_,_,f,A]",symmetric])
apply(simp_all add:zero_in_M)
apply(rule_tac replacement_ax[where env="[f,A]",simplified])
apply(simp_all add: arity_is_abs_apply_pair_fm ord_simp_union)
done
lemma (in M_ZF_trans) replacement_abs_apply_pair :
"(##M)(A) ⟹ (##M)(f) ⟹ strong_replacement(##M, λx y. y = ⟨x, λn∈A. f ` ⟨x, n⟩⟩)"
using strong_replacement_cong[THEN iffD1,OF abs_apply_pair_abs replacement_is_abs_apply_pair,simplified]
unfolding abs_apply_pair_def
by simp
end