Theory Interface
section‹Interface between set models and Constructibility›
text‹This theory provides an interface between Paulson's
relativization results and set models of ZFC. In particular,
it is used to prove that the locale \<^term>‹forcing_data› is
a sublocale of all relevant locales in ZF-Constructibility
(\<^term>‹M_trivial›, \<^term>‹M_basic›, \<^term>‹M_eclose›, etc).›
theory Interface
imports
Nat_Miscellanea
Relative_Univ
Synthetic_Definition
Arities
Renaming_Auto
Discipline_Function
begin
abbreviation
dec10 :: i ("10") where "10 ≡ succ(9)"
abbreviation
dec11 :: i ("11") where "11 ≡ succ(10)"
abbreviation
dec12 :: i ("12") where "12 ≡ succ(11)"
abbreviation
dec13 :: i ("13") where "13 ≡ succ(12)"
abbreviation
dec14 :: i ("14") where "14 ≡ succ(13)"
definition
infinity_ax :: "(i ⇒ o) ⇒ o" where
"infinity_ax(M) ≡
(∃I[M]. (∃z[M]. empty(M,z) ∧ z∈I) ∧ (∀y[M]. y∈I ⟶ (∃sy[M]. successor(M,y,sy) ∧ sy∈I)))"
definition
choice_ax :: "(i⇒o) ⇒ o" where
"choice_ax(M) ≡ ∀x[M]. ∃a[M]. ∃f[M]. ordinal(M,a) ∧ surjection(M,a,x,f)"
context M_basic begin
lemma choice_ax_abs :
"choice_ax(M) ⟷ (∀x[M]. ∃a[M]. ∃f[M]. Ord(a) ∧ f ∈ surj(a,x))"
unfolding choice_ax_def
by (simp)
end
definition
wellfounded_trancl :: "[i=>o,i,i,i] => o" where
"wellfounded_trancl(M,Z,r,p) ≡
∃w[M]. ∃wx[M]. ∃rp[M].
w ∈ Z & pair(M,w,p,wx) & tran_closure(M,r,rp) & wx ∈ rp"
lemma empty_intf :
"infinity_ax(M) ⟹
(∃z[M]. empty(M,z))"
by (auto simp add: empty_def infinity_ax_def)
lemma Transset_intf :
"Transset(M) ⟹ y∈x ⟹ x ∈ M ⟹ y ∈ M"
by (simp add: Transset_def,auto)
locale M_ZF=
fixes M
assumes
upair_ax: "upair_ax(##M)" and
Union_ax: "Union_ax(##M)" and
power_ax: "power_ax(##M)" and
extensionality:"extensionality(##M)" and
foundation_ax: "foundation_ax(##M)" and
infinity_ax: "infinity_ax(##M)" and
separation_ax: "φ ∈ formula ⟹ env ∈ list(M) ⟹
arity(φ) ≤ 1 #+ length(env) ⟹
separation(##M,λx. sats(M,φ,[x] @ env))" and
replacement_ax:"φ ∈ formula ⟹ env ∈ list(M) ⟹
arity(φ) ≤ 2 #+ length(env) ⟹
strong_replacement(##M,λx y. sats(M,φ,[x,y] @ env))"
locale M_ZF_trans= M_ZF +
assumes
trans_M: "Transset(M)"
begin
lemmas transitivity= Transset_intf[OF trans_M]
subsection‹Interface with \<^term>‹M_trivial››
lemma zero_in_M : "0 ∈ M"
proof -
from infinity_ax
have "(∃z[##M]. empty(##M,z))"
by (rule empty_intf)
then obtain z where
zm: "empty(##M,z)" "z∈M"
by auto
then
have "z=0"
using transitivity empty_def by auto
with zm show ?thesis
by simp
qed
end
locale M_ZFC= M_ZF +
assumes
choice_ax:"choice_ax(##M)"
locale M_ZFC_trans= M_ZF_trans + M_ZFC
sublocale M_ZF_trans ⊆ M_trans "##M"
using transitivity zero_in_M exI[of "λx. x∈M"]
by unfold_locales simp_all
sublocale M_ZF_trans ⊆ M_trivial "##M"
using trans_M upair_ax Union_ax by unfold_locales
subsection‹Interface with \<^term>‹M_basic››
definition Intersection where
"Intersection(N,B,x) ≡ (∀y[N]. y∈B ⟶ x∈y)"
manual_schematic "Inter_fm" for "Intersection"
unfolding Intersection_def
by (rule sep_rules | simp)+
synthesize "Intersection" from_schematic Inter_fm
arity_theorem for "Intersection_fm"
context M_ZF_trans
begin
lemma inter_sep_intf :
assumes
"A∈M"
shows
"separation(##M,λx . ∀y∈M . y∈A ⟶ x∈y)"
proof -
have "arity(Intersection_fm(1,0)) = 2" "0∈nat" "1∈nat"
using arity_Intersection_fm pred_Un_distrib by auto
then
have "∀a∈M. separation(##M, λx. sats(M,Intersection_fm(1,0) , [x, a]))"
using separation_ax Intersection_fm_type
by simp
moreover
have "(∀y∈M . y∈a ⟶ x∈y) ⟷ sats(M,Intersection_fm(1,0),[x,a])"
if "a∈M" "x∈M" for a x
using that Intersection_iff_sats[of 1 "[x,a]" a 0 x M]
unfolding Intersection_def by simp
ultimately
have "∀a∈M. separation(##M, λx . ∀y∈M . y∈a ⟶ x∈y)"
unfolding separation_def by simp
with ‹A∈M› show ?thesis by simp
qed
schematic_goal diff_fm_auto :
assumes
"nth(i,env) = x" "nth(j,env) = B"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"x∉B ⟷ sats(A,?dfm(i,j),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma diff_sep_intf :
assumes
"B∈M"
shows
"separation(##M,λx . x∉B)"
proof -
obtain dfm where
fmsats:"⋀env. env∈list(M) ⟹ nth(0,env)∉nth(1,env)
⟷ sats(M,dfm(0,1),env)"
and
"dfm(0,1) ∈ formula"
and
"arity(dfm(0,1)) = 2"
using ‹B∈M› diff_fm_auto
by (simp del:FOL_sats_iff add: ord_simp_union)
then
have "∀b∈M. separation(##M, λx. sats(M,dfm(0,1) , [x, b]))"
using separation_ax by simp
moreover
have "x∉b ⟷ sats(M,dfm(0,1),[x,b])"
if "b∈M" "x∈M" for b x
using that fmsats[of "[x,b]"] by simp
ultimately
have "∀b∈M. separation(##M, λx . x∉b)"
unfolding separation_def by simp
with ‹B∈M› show ?thesis by simp
qed
schematic_goal cprod_fm_auto :
assumes
"nth(i,env) = z" "nth(j,env) = B" "nth(h,env) = C"
"i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
shows
"(∃x∈A. x∈B ∧ (∃y∈A. y∈C ∧ pair(##A,x,y,z))) ⟷ sats(A,?cpfm(i,j,h),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma cartprod_sep_intf :
assumes
"A∈M"
and
"B∈M"
shows
"separation(##M,λz. ∃x∈M. x∈A ∧ (∃y∈M. y∈B ∧ pair(##M,x,y,z)))"
proof -
obtain cpfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃x∈M. x∈nth(1,env) ∧ (∃y∈M. y∈nth(2,env) ∧ pair(##M,x,y,nth(0,env))))
⟷ sats(M,cpfm(0,1,2),env)"
and
"cpfm(0,1,2) ∈ formula"
and
"arity(cpfm(0,1,2)) = 3"
using cprod_fm_auto by (simp del:FOL_sats_iff add: fm_definitions ord_simp_union)
then
have "∀a∈M. ∀b∈M. separation(##M, λz. sats(M,cpfm(0,1,2) , [z, a, b]))"
using separation_ax by simp
moreover
have "(∃x∈M. x∈a ∧ (∃y∈M. y∈b ∧ pair(##M,x,y,z))) ⟷ sats(M,cpfm(0,1,2),[z,a,b])"
if "a∈M" "b∈M" "z∈M" for a b z
using that fmsats[of "[z,a,b]"] by simp
ultimately
have "∀a∈M. ∀b∈M. separation(##M, λz . (∃x∈M. x∈a ∧ (∃y∈M. y∈b ∧ pair(##M,x,y,z))))"
unfolding separation_def by simp
with ‹A∈M› ‹B∈M› show ?thesis by simp
qed
schematic_goal im_fm_auto :
assumes
"nth(i,env) = y" "nth(j,env) = r" "nth(h,env) = B"
"i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
shows
"(∃p∈A. p∈r & (∃x∈A. x∈B & pair(##A,x,y,p))) ⟷ sats(A,?imfm(i,j,h),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma image_sep_intf :
assumes
"A∈M"
and
"r∈M"
shows
"separation(##M, λy. ∃p∈M. p∈r & (∃x∈M. x∈A & pair(##M,x,y,p)))"
proof -
obtain imfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃p∈M. p∈nth(1,env) & (∃x∈M. x∈nth(2,env) & pair(##M,x,nth(0,env),p)))
⟷ sats(M,imfm(0,1,2),env)"
and
"imfm(0,1,2) ∈ formula"
and
"arity(imfm(0,1,2)) = 3"
using im_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀r∈M. ∀a∈M. separation(##M, λy. sats(M,imfm(0,1,2) , [y,r,a]))"
using separation_ax by simp
moreover
have "(∃p∈M. p∈k & (∃x∈M. x∈a & pair(##M,x,y,p))) ⟷ sats(M,imfm(0,1,2),[y,k,a])"
if "k∈M" "a∈M" "y∈M" for k a y
using that fmsats[of "[y,k,a]"] by simp
ultimately
have "∀k∈M. ∀a∈M. separation(##M, λy . ∃p∈M. p∈k & (∃x∈M. x∈a & pair(##M,x,y,p)))"
unfolding separation_def by simp
with ‹r∈M› ‹A∈M› show ?thesis by simp
qed
schematic_goal con_fm_auto :
assumes
"nth(i,env) = z" "nth(j,env) = R"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"(∃p∈A. p∈R & (∃x∈A.∃y∈A. pair(##A,x,y,p) & pair(##A,y,x,z)))
⟷ sats(A,?cfm(i,j),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma converse_sep_intf :
assumes
"R∈M"
shows
"separation(##M,λz. ∃p∈M. p∈R & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z)))"
proof -
obtain cfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃p∈M. p∈nth(1,env) & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,nth(0,env))))
⟷ sats(M,cfm(0,1),env)"
and
"cfm(0,1) ∈ formula"
and
"arity(cfm(0,1)) = 2"
using con_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀r∈M. separation(##M, λz. sats(M,cfm(0,1) , [z,r]))"
using separation_ax by simp
moreover
have "(∃p∈M. p∈r & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z))) ⟷
sats(M,cfm(0,1),[z,r])"
if "z∈M" "r∈M" for z r
using that fmsats[of "[z,r]"] by simp
ultimately
have "∀r∈M. separation(##M, λz . ∃p∈M. p∈r & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z)))"
unfolding separation_def by simp
with ‹R∈M› show ?thesis by simp
qed
schematic_goal rest_fm_auto :
assumes
"nth(i,env) = z" "nth(j,env) = C"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"(∃x∈A. x∈C & (∃y∈A. pair(##A,x,y,z)))
⟷ sats(A,?rfm(i,j),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma restrict_sep_intf :
assumes
"A∈M"
shows
"separation(##M,λz. ∃x∈M. x∈A & (∃y∈M. pair(##M,x,y,z)))"
proof -
obtain rfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃x∈M. x∈nth(1,env) & (∃y∈M. pair(##M,x,y,nth(0,env))))
⟷ sats(M,rfm(0,1),env)"
and
"rfm(0,1) ∈ formula"
and
"arity(rfm(0,1)) = 2"
using rest_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀a∈M. separation(##M, λz. sats(M,rfm(0,1) , [z,a]))"
using separation_ax by simp
moreover
have "(∃x∈M. x∈a & (∃y∈M. pair(##M,x,y,z))) ⟷
sats(M,rfm(0,1),[z,a])"
if "z∈M" "a∈M" for z a
using that fmsats[of "[z,a]"] by simp
ultimately
have "∀a∈M. separation(##M, λz . ∃x∈M. x∈a & (∃y∈M. pair(##M,x,y,z)))"
unfolding separation_def by simp
with ‹A∈M› show ?thesis by simp
qed
schematic_goal comp_fm_auto :
assumes
"nth(i,env) = xz" "nth(j,env) = S" "nth(h,env) = R"
"i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
shows
"(∃x∈A. ∃y∈A. ∃z∈A. ∃xy∈A. ∃yz∈A.
pair(##A,x,z,xz) & pair(##A,x,y,xy) & pair(##A,y,z,yz) & xy∈S & yz∈R)
⟷ sats(A,?cfm(i,j,h),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma comp_sep_intf :
assumes
"R∈M"
and
"S∈M"
shows
"separation(##M,λxz. ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈S & yz∈R)"
proof -
obtain cfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M. pair(##M,x,z,nth(0,env)) &
pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈nth(1,env) & yz∈nth(2,env))
⟷ sats(M,cfm(0,1,2),env)"
and
"cfm(0,1,2) ∈ formula"
and
"arity(cfm(0,1,2)) = 3"
using comp_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀r∈M. ∀s∈M. separation(##M, λy. sats(M,cfm(0,1,2) , [y,s,r]))"
using separation_ax by simp
moreover
have "(∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈s & yz∈r)
⟷ sats(M,cfm(0,1,2) , [xz,s,r])"
if "xz∈M" "s∈M" "r∈M" for xz s r
using that fmsats[of "[xz,s,r]"] by simp
ultimately
have "∀s∈M. ∀r∈M. separation(##M, λxz . ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈s & yz∈r)"
unfolding separation_def by simp
with ‹S∈M› ‹R∈M› show ?thesis by simp
qed
schematic_goal pred_fm_auto :
assumes
"nth(i,env) = y" "nth(j,env) = R" "nth(h,env) = X"
"i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
shows
"(∃p∈A. p∈R & pair(##A,y,X,p)) ⟷ sats(A,?pfm(i,j,h),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma pred_sep_intf :
assumes
"R∈M"
and
"X∈M"
shows
"separation(##M, λy. ∃p∈M. p∈R & pair(##M,y,X,p))"
proof -
obtain pfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃p∈M. p∈nth(1,env) & pair(##M,nth(0,env),nth(2,env),p)) ⟷ sats(M,pfm(0,1,2),env)"
and
"pfm(0,1,2) ∈ formula"
and
"arity(pfm(0,1,2)) = 3"
using pred_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀x∈M. ∀r∈M. separation(##M, λy. sats(M,pfm(0,1,2) , [y,r,x]))"
using separation_ax by simp
moreover
have "(∃p∈M. p∈r & pair(##M,y,x,p))
⟷ sats(M,pfm(0,1,2) , [y,r,x])"
if "y∈M" "r∈M" "x∈M" for y x r
using that fmsats[of "[y,r,x]"] by simp
ultimately
have "∀x∈M. ∀r∈M. separation(##M, λ y . ∃p∈M. p∈r & pair(##M,y,x,p))"
unfolding separation_def by simp
with ‹X∈M› ‹R∈M› show ?thesis by simp
qed
schematic_goal mem_fm_auto :
assumes
"nth(i,env) = z" "i ∈ nat" "env ∈ list(A)"
shows
"(∃x∈A. ∃y∈A. pair(##A,x,y,z) & x ∈ y) ⟷ sats(A,?mfm(i),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma memrel_sep_intf :
"separation(##M, λz. ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y)"
proof -
obtain mfm where
fmsats:"⋀env. env∈list(M) ⟹
(∃x∈M. ∃y∈M. pair(##M,x,y,nth(0,env)) & x ∈ y) ⟷ sats(M,mfm(0),env)"
and
"mfm(0) ∈ formula"
and
"arity(mfm(0)) = 1"
using mem_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "separation(##M, λz. sats(M,mfm(0) , [z]))"
using separation_ax by simp
moreover
have "(∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y) ⟷ sats(M,mfm(0),[z])"
if "z∈M" for z
using that fmsats[of "[z]"] by simp
ultimately
have "separation(##M, λz . ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y)"
unfolding separation_def by simp
then show ?thesis by simp
qed
schematic_goal recfun_fm_auto :
assumes
"nth(i1,env) = x" "nth(i2,env) = r" "nth(i3,env) = f" "nth(i4,env) = g" "nth(i5,env) = a"
"nth(i6,env) = b" "i1∈nat" "i2∈nat" "i3∈nat" "i4∈nat" "i5∈nat" "i6∈nat" "env ∈ list(A)"
shows
"(∃xa∈A. ∃xb∈A. pair(##A,x,a,xa) & xa ∈ r & pair(##A,x,b,xb) & xb ∈ r &
(∃fx∈A. ∃gx∈A. fun_apply(##A,f,x,fx) & fun_apply(##A,g,x,gx) & fx ≠ gx))
⟷ sats(A,?rffm(i1,i2,i3,i4,i5,i6),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma is_recfun_sep_intf :
assumes
"r∈M" "f∈M" "g∈M" "a∈M" "b∈M"
shows
"separation(##M,λx. ∃xa∈M. ∃xb∈M.
pair(##M,x,a,xa) & xa ∈ r & pair(##M,x,b,xb) & xb ∈ r &
(∃fx∈M. ∃gx∈M. fun_apply(##M,f,x,fx) & fun_apply(##M,g,x,gx) &
fx ≠ gx))"
proof -
obtain rffm where
fmsats:"⋀env. env∈list(M) ⟹
(∃xa∈M. ∃xb∈M. pair(##M,nth(0,env),nth(4,env),xa) & xa ∈ nth(1,env) &
pair(##M,nth(0,env),nth(5,env),xb) & xb ∈ nth(1,env) & (∃fx∈M. ∃gx∈M.
fun_apply(##M,nth(2,env),nth(0,env),fx) & fun_apply(##M,nth(3,env),nth(0,env),gx) & fx ≠ gx))
⟷ sats(M,rffm(0,1,2,3,4,5),env)"
and
"rffm(0,1,2,3,4,5) ∈ formula"
and
"arity(rffm(0,1,2,3,4,5)) = 6"
using recfun_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀a1∈M. ∀a2∈M. ∀a3∈M. ∀a4∈M. ∀a5∈M.
separation(##M, λx. sats(M,rffm(0,1,2,3,4,5) , [x,a1,a2,a3,a4,a5]))"
using separation_ax by simp
moreover
have "(∃xa∈M. ∃xb∈M. pair(##M,x,a4,xa) & xa ∈ a1 & pair(##M,x,a5,xb) & xb ∈ a1 &
(∃fx∈M. ∃gx∈M. fun_apply(##M,a2,x,fx) & fun_apply(##M,a3,x,gx) & fx ≠ gx))
⟷ sats(M,rffm(0,1,2,3,4,5) , [x,a1,a2,a3,a4,a5])"
if "x∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "a5∈M" for x a1 a2 a3 a4 a5
using that fmsats[of "[x,a1,a2,a3,a4,a5]"] by simp
ultimately
have "∀a1∈M. ∀a2∈M. ∀a3∈M. ∀a4∈M. ∀a5∈M. separation(##M, λ x .
∃xa∈M. ∃xb∈M. pair(##M,x,a4,xa) & xa ∈ a1 & pair(##M,x,a5,xb) & xb ∈ a1 &
(∃fx∈M. ∃gx∈M. fun_apply(##M,a2,x,fx) & fun_apply(##M,a3,x,gx) & fx ≠ gx))"
unfolding separation_def by simp
with ‹r∈M› ‹f∈M› ‹g∈M› ‹a∈M› ‹b∈M› show ?thesis by simp
qed
schematic_goal funsp_fm_auto :
assumes
"nth(i,env) = p" "nth(j,env) = z" "nth(h,env) = n"
"i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
shows
"(∃f∈A. ∃b∈A. ∃nb∈A. ∃cnbf∈A. pair(##A,f,b,p) & pair(##A,n,b,nb) & is_cons(##A,nb,f,cnbf) &
upair(##A,cnbf,cnbf,z)) ⟷ sats(A,?fsfm(i,j,h),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma funspace_succ_rep_intf :
assumes
"n∈M"
shows
"strong_replacement(##M,
λp z. ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M.
pair(##M,f,b,p) & pair(##M,n,b,nb) & is_cons(##M,nb,f,cnbf) &
upair(##M,cnbf,cnbf,z))"
proof -
obtain fsfm where
fmsats:"env∈list(M) ⟹
(∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,nth(0,env)) & pair(##M,nth(2,env),b,nb)
& is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,nth(1,env)))
⟷ sats(M,fsfm(0,1,2),env)"
and "fsfm(0,1,2) ∈ formula" and "arity(fsfm(0,1,2)) = 3" for env
using funsp_fm_auto[of concl:M] by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀n0∈M. strong_replacement(##M, λp z. sats(M,fsfm(0,1,2) , [p,z,n0]))"
using replacement_ax[of "fsfm(0,1,2)"] by simp
moreover
have "(∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,p) & pair(##M,n0,b,nb) &
is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,z))
⟷ sats(M,fsfm(0,1,2) , [p,z,n0])"
if "p∈M" "z∈M" "n0∈M" for p z n0
using that fmsats[of "[p,z,n0]"] by simp
ultimately
have "∀n0∈M. strong_replacement(##M, λ p z.
∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,p) & pair(##M,n0,b,nb) &
is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,z))"
unfolding strong_replacement_def univalent_def by simp
with ‹n∈M› show ?thesis by simp
qed
lemmas M_basic_sep_instances=
inter_sep_intf diff_sep_intf cartprod_sep_intf
image_sep_intf converse_sep_intf restrict_sep_intf
pred_sep_intf memrel_sep_intf comp_sep_intf is_recfun_sep_intf
end
sublocale M_ZF_trans ⊆ M_basic "##M"
using trans_M zero_in_M power_ax M_basic_sep_instances funspace_succ_rep_intf
by unfold_locales auto
subsection‹Interface with \<^term>‹M_trancl››
schematic_goal rtran_closure_mem_auto :
assumes
"nth(i,env) = p" "nth(j,env) = r" "nth(k,env) = B"
"i ∈ nat" "j ∈ nat" "k ∈ nat" "env ∈ list(A)"
shows
"rtran_closure_mem(##A,B,r,p) ⟷ sats(A,?rcfm(i,j,k),env)"
unfolding rtran_closure_mem_def
by (insert assms ; (rule sep_rules | simp)+)
lemma (in M_ZF_trans) rtrancl_separation_intf :
assumes
"r∈M"
and
"A∈M"
shows
"separation (##M, rtran_closure_mem(##M,A,r))"
proof -
obtain rcfm where
fmsats:"⋀env. env∈list(M) ⟹
(rtran_closure_mem(##M,nth(2,env),nth(1,env),nth(0,env))) ⟷ sats(M,rcfm(0,1,2),env)"
and
"rcfm(0,1,2) ∈ formula"
and
"arity(rcfm(0,1,2)) = 3"
using rtran_closure_mem_auto by (simp del:FOL_sats_iff pair_abs add: fm_definitions ord_simp_union)
then
have "∀x∈M. ∀a∈M. separation(##M, λy. sats(M,rcfm(0,1,2) , [y,x,a]))"
using separation_ax by simp
moreover
have "(rtran_closure_mem(##M,a,x,y))
⟷ sats(M,rcfm(0,1,2) , [y,x,a])"
if "y∈M" "x∈M" "a∈M" for y x a
using that fmsats[of "[y,x,a]"] by simp
ultimately
have "∀x∈M. ∀a∈M. separation(##M, rtran_closure_mem(##M,a,x))"
unfolding separation_def by simp
with ‹r∈M› ‹A∈M› show ?thesis by simp
qed
schematic_goal rtran_closure_fm_auto :
assumes
"nth(i,env) = r" "nth(j,env) = rp"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"rtran_closure(##A,r,rp) ⟷ sats(A,?rtc(i,j),env)"
unfolding rtran_closure_def
by (insert assms ; (rule sep_rules rtran_closure_mem_auto| simp)+)
schematic_goal trans_closure_fm_auto :
assumes
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"tran_closure(##A,nth(i,env),nth(j,env)) ⟷ sats(A,?tc(i,j),env)"
unfolding tran_closure_def
by (insert assms ; (rule sep_rules rtran_closure_fm_auto | simp))+
synthesize "trans_closure" from_schematic trans_closure_fm_auto
lemma arity_tran_closure_fm :
"⟦x∈nat;f∈nat⟧ ⟹ arity(trans_closure_fm(x,f)) = succ(x) ∪ succ(f)"
unfolding trans_closure_fm_def
using arity_omega_fm arity_field_fm arity_typed_function_fm arity_pair_fm arity_empty_fm arity_fun_apply_fm
arity_composition_fm arity_succ_fm union_abs2 pred_Un_distrib
by auto
schematic_goal wellfounded_trancl_fm_auto :
assumes
"nth(i,env) = p" "nth(j,env) = r" "nth(k,env) = B"
"i ∈ nat" "j ∈ nat" "k ∈ nat" "env ∈ list(A)"
shows
"wellfounded_trancl(##A,B,r,p) ⟷ sats(A,?wtf(i,j,k),env)"
unfolding wellfounded_trancl_def
by (insert assms ; (rule sep_rules trans_closure_iff_sats | simp)+)
context M_ZF_trans
begin
lemma wftrancl_separation_intf :
assumes
"r∈M" and "Z∈M"
shows
"separation (##M, wellfounded_trancl(##M,Z,r))"
proof -
obtain rcfm where
fmsats:"⋀env. env∈list(M) ⟹
(wellfounded_trancl(##M,nth(2,env),nth(1,env),nth(0,env))) ⟷ sats(M,rcfm(0,1,2),env)"
and
"rcfm(0,1,2) ∈ formula"
and
"arity(rcfm(0,1,2)) = 3"
using wellfounded_trancl_fm_auto[of concl:M "nth(2,_)"] unfolding fm_definitions
by (simp del:FOL_sats_iff pair_abs add: ord_simp_union)
then
have "∀x∈M. ∀z∈M. separation(##M, λy. sats(M,rcfm(0,1,2) , [y,x,z]))"
using separation_ax by simp
moreover
have "(wellfounded_trancl(##M,z,x,y))
⟷ sats(M,rcfm(0,1,2) , [y,x,z])"
if "y∈M" "x∈M" "z∈M" for y x z
using that fmsats[of "[y,x,z]"] by simp
ultimately
have "∀x∈M. ∀z∈M. separation(##M, wellfounded_trancl(##M,z,x))"
unfolding separation_def by simp
with ‹r∈M› ‹Z∈M› show ?thesis by simp
qed
text‹Proof that \<^term>‹nat ∈ M››
lemma finite_sep_intf : "separation(##M, λx. x∈nat)"
proof -
have "arity(finite_ordinal_fm(0)) = 1 "
unfolding finite_ordinal_fm_def limit_ordinal_fm_def empty_fm_def succ_fm_def cons_fm_def
union_fm_def upair_fm_def
by (simp add: union_abs1 Un_commute)
with separation_ax
have "(∀v∈M. separation(##M,λx. sats(M,finite_ordinal_fm(0),[x,v])))"
by simp
then have "(∀v∈M. separation(##M,finite_ordinal(##M)))"
unfolding separation_def by simp
then have "separation(##M,finite_ordinal(##M))"
using zero_in_M by auto
then show ?thesis unfolding separation_def by simp
qed
lemma nat_subset_I' :
"⟦ I∈M ; 0∈I ; ⋀x. x∈I ⟹ succ(x)∈I ⟧ ⟹ nat ⊆ I"
by (rule subsetI,induct_tac x,simp+)
lemma nat_subset_I : "∃I∈M. nat ⊆ I"
proof -
have "∃I∈M. 0∈I ∧ (∀x∈M. x∈I ⟶ succ(x)∈I)"
using infinity_ax unfolding infinity_ax_def by auto
then obtain I where
"I∈M" "0∈I" "(∀x∈M. x∈I ⟶ succ(x)∈I)"
by auto
then have "⋀x. x∈I ⟹ succ(x)∈I"
using transitivity by simp
then have "nat⊆I"
using ‹I∈M› ‹0∈I› nat_subset_I' by simp
then show ?thesis using ‹I∈M› by auto
qed
lemma nat_in_M : "nat ∈ M"
proof -
have 1:"{x∈B . x∈A}=A" if "A⊆B" for A B
using that by auto
obtain I where
"I∈M" "nat⊆I"
using nat_subset_I by auto
then have "{x∈I . x∈nat} ∈ M"
using finite_sep_intf separation_closed[of "λx . x∈nat"] by simp
then show ?thesis
using ‹nat⊆I› 1 by simp
qed
end
sublocale M_ZF_trans ⊆ M_trancl "##M"
using rtrancl_separation_intf wftrancl_separation_intf nat_in_M
wellfounded_trancl_def by unfold_locales auto
subsection‹Interface with \<^term>‹M_eclose››
lemma repl_sats :
assumes
sat:"⋀x z. x∈M ⟹ z∈M ⟹ sats(M,φ,Cons(x,Cons(z,env))) ⟷ P(x,z)"
shows
"strong_replacement(##M,λx z. sats(M,φ,Cons(x,Cons(z,env)))) ⟷
strong_replacement(##M,P)"
by (rule strong_replacement_cong,simp add:sat)
lemma (in M_ZF_trans) list_repl1_intf :
assumes
"A∈M"
shows
"iterates_replacement(##M, is_list_functor(##M,A), 0)"
proof -
{
fix n
assume "n∈nat"
have "succ(n)∈M"
using ‹n∈nat› nat_into_M by simp
then have 1:"Memrel(succ(n))∈M"
using ‹n∈nat› Memrel_closed by simp
have "0∈M"
using nat_0I nat_into_M by simp
then have "is_list_functor(##M, A, a, b)
⟷ sats(M, list_functor_fm(13,1,0), [b,a,c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),A,0])"
if "a∈M" "b∈M" "c∈M" "d∈M" "a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
for a b c d a0 a1 a2 a3 a4 y x z
using that 1 ‹A∈M› list_functor_iff_sats by simp
then have "sats(M, iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0), [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),A,0])
⟷ iterates_MH(##M,is_list_functor(##M,A),0,a2, a1, a0)"
if "a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
for a0 a1 a2 a3 a4 y x z
using that sats_iterates_MH_fm[of M "is_list_functor(##M,A)" _] 1 ‹0∈M› ‹A∈M› by simp
then have 2:"sats(M, is_wfrec_fm(iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0),3,1,0),
[y,x,z,Memrel(succ(n)),A,0])
⟷
is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) , Memrel(succ(n)), x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that sats_is_wfrec_fm 1 ‹0∈M› ‹A∈M› by simp
let
?f="Exists(And(pair_fm(1,0,2),
is_wfrec_fm(iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0),3,1,0)))"
have satsf:"sats(M, ?f, [x,z,Memrel(succ(n)),A,0])
⟷
(∃y∈M. pair(##M,x,y,z) &
is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) , Memrel(succ(n)), x, y))"
if "x∈M" "z∈M" for x z
using that 2 1 ‹0∈M› ‹A∈M› by (simp del:pair_abs)
have "arity(?f) = 5"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),A,0]))"
using replacement_ax[of ?f] 1 ‹A∈M› ‹0∈M› by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) ,
Memrel(succ(n)), x, y))"
using repl_sats[of M ?f "[Memrel(succ(n)),A,0]"] satsf by (simp del:pair_abs)
}
then
show ?thesis unfolding iterates_replacement_def wfrec_replacement_def by simp
qed
lemma (in M_ZF_trans) iterates_repl_intf :
assumes
"v∈M" and
isfm:"is_F_fm ∈ formula" and
arty:"arity(is_F_fm)=2" and
satsf: "⋀a b env'. ⟦ a∈M ; b∈M ; env'∈list(M) ⟧
⟹ is_F(a,b) ⟷ sats(M, is_F_fm, [b,a]@env')"
shows
"iterates_replacement(##M,is_F,v)"
proof -
{
fix n
assume "n∈nat"
have "succ(n)∈M"
using ‹n∈nat› nat_into_M by simp
then have 1:"Memrel(succ(n))∈M"
using ‹n∈nat› Memrel_closed by simp
{
fix a0 a1 a2 a3 a4 y x z
assume as:"a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
have "sats(M, is_F_fm, Cons(b,Cons(a,Cons(c,Cons(d,[a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v])))))
⟷ is_F(a,b)"
if "a∈M" "b∈M" "c∈M" "d∈M" for a b c d
using as that 1 satsf[of a b "[c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]"] ‹v∈M› by simp
then
have "sats(M, iterates_MH_fm(is_F_fm,9,2,1,0), [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v])
⟷ iterates_MH(##M,is_F,v,a2, a1, a0)"
using as
sats_iterates_MH_fm[of M "is_F" "is_F_fm"] 1 ‹v∈M› by simp
}
then have 2:"sats(M, is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0),
[y,x,z,Memrel(succ(n)),v])
⟷
is_wfrec(##M, iterates_MH(##M,is_F,v),Memrel(succ(n)), x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that sats_is_wfrec_fm 1 ‹v∈M› by simp
let
?f="Exists(And(pair_fm(1,0,2),
is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0)))"
have satsf:"sats(M, ?f, [x,z,Memrel(succ(n)),v])
⟷
(∃y∈M. pair(##M,x,y,z) &
is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))"
if "x∈M" "z∈M" for x z
using that 2 1 ‹v∈M› by (simp del:pair_abs)
have "arity(?f) = 4"
unfolding fm_definitions
using arty by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),v]))"
using replacement_ax[of ?f] 1 ‹v∈M› ‹is_F_fm∈formula› by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, iterates_MH(##M,is_F,v) ,
Memrel(succ(n)), x, y))"
using repl_sats[of M ?f "[Memrel(succ(n)),v]"] satsf by (simp del:pair_abs)
}
then
show ?thesis unfolding iterates_replacement_def wfrec_replacement_def by simp
qed
lemma (in M_ZF_trans) formula_repl1_intf :
"iterates_replacement(##M, is_formula_functor(##M), 0)"
proof -
have "0∈M"
using nat_0I nat_into_M by simp
have 1:"arity(formula_functor_fm(1,0)) = 2"
unfolding fm_definitions
by (simp add:ord_simp_union)
have 2:"formula_functor_fm(1,0)∈formula" by simp
have "is_formula_functor(##M,a,b) ⟷
sats(M, formula_functor_fm(1,0), [b,a])"
if "a∈M" "b∈M" for a b
using that by simp
then show ?thesis using ‹0∈M› 1 2
iterates_repl_intf[where is_F_fm="formula_functor_fm(1,0)"] by simp
qed
lemma (in M_ZF_trans) nth_repl_intf :
assumes
"l ∈ M"
shows
"iterates_replacement(##M,λl' t. is_tl(##M,l',t),l)"
proof -
have 1:"arity(tl_fm(1,0)) = 2"
unfolding fm_definitions by (simp add:ord_simp_union)
have 2:"tl_fm(1,0)∈formula" by simp
have "is_tl(##M,a,b) ⟷ sats(M, tl_fm(1,0), [b,a])"
if "a∈M" "b∈M" for a b
using that by simp
then show ?thesis using ‹l∈M› 1 2
iterates_repl_intf[where is_F_fm="tl_fm(1,0)"] by simp
qed
lemma (in M_ZF_trans) eclose_repl1_intf :
assumes
"A∈M"
shows
"iterates_replacement(##M, big_union(##M), A)"
proof -
have 1:"arity(big_union_fm(1,0)) = 2"
unfolding fm_definitions by (simp add:ord_simp_union)
have 2:"big_union_fm(1,0)∈formula" by simp
have "big_union(##M,a,b) ⟷ sats(M, big_union_fm(1,0), [b,a])"
if "a∈M" "b∈M" for a b
using that by simp
then show ?thesis using ‹A∈M› 1 2
iterates_repl_intf[where is_F_fm="big_union_fm(1,0)"] by simp
qed
lemma (in M_ZF_trans) list_repl2_intf :
assumes
"A∈M"
shows
"strong_replacement(##M,λn y. n∈nat & is_iterates(##M, is_list_functor(##M,A), 0, n, y))"
proof -
have "0∈M"
using nat_0I nat_into_M by simp
have "is_list_functor(##M,A,a,b) ⟷
sats(M,list_functor_fm(13,1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,A,0,nat])"
if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
for a b c d e f g h i j k n y
using that ‹0∈M› nat_in_M ‹A∈M› by simp
then
have 1:"sats(M, is_iterates_fm(list_functor_fm(13,1,0),3,0,1),[n,y,A,0,nat] ) ⟷
is_iterates(##M, is_list_functor(##M,A), 0, n , y)"
if "n∈M" "y∈M" for n y
using that ‹0∈M› ‹A∈M› nat_in_M
sats_is_iterates_fm[of M "is_list_functor(##M,A)"] by simp
let ?f = "And(Member(0,4),is_iterates_fm(list_functor_fm(13,1,0),3,0,1))"
have satsf:"sats(M, ?f,[n,y,A,0,nat] ) ⟷
n∈nat & is_iterates(##M, is_list_functor(##M,A), 0, n, y)"
if "n∈M" "y∈M" for n y
using that ‹0∈M› ‹A∈M› nat_in_M 1 by simp
have "arity(?f) = 5"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,0,nat]))"
using replacement_ax[of ?f] 1 nat_in_M ‹A∈M› ‹0∈M› by simp
then
show ?thesis using repl_sats[of M ?f "[A,0,nat]"] satsf by simp
qed
lemma (in M_ZF_trans) formula_repl2_intf :
"strong_replacement(##M,λn y. n∈nat & is_iterates(##M, is_formula_functor(##M), 0, n, y))"
proof -
have "0∈M"
using nat_0I nat_into_M by simp
have "is_formula_functor(##M,a,b) ⟷
sats(M,formula_functor_fm(1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,0,nat])"
if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
for a b c d e f g h i j k n y
using that ‹0∈M› nat_in_M by simp
then
have 1:"sats(M, is_iterates_fm(formula_functor_fm(1,0),2,0,1),[n,y,0,nat] ) ⟷
is_iterates(##M, is_formula_functor(##M), 0, n , y)"
if "n∈M" "y∈M" for n y
using that ‹0∈M› nat_in_M
sats_is_iterates_fm[of M "is_formula_functor(##M)"] by simp
let ?f = "And(Member(0,3),is_iterates_fm(formula_functor_fm(1,0),2,0,1))"
have satsf:"sats(M, ?f,[n,y,0,nat] ) ⟷
n∈nat & is_iterates(##M, is_formula_functor(##M), 0, n, y)"
if "n∈M" "y∈M" for n y
using that ‹0∈M› nat_in_M 1 by simp
have artyf:"arity(?f) = 4"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,0,nat]))"
using replacement_ax[of ?f] 1 artyf ‹0∈M› nat_in_M by simp
then
show ?thesis using repl_sats[of M ?f "[0,nat]"] satsf by simp
qed
lemma (in M_ZF_trans) eclose_repl2_intf :
assumes
"A∈M"
shows
"strong_replacement(##M,λn y. n∈nat & is_iterates(##M, big_union(##M), A, n, y))"
proof -
have "big_union(##M,a,b) ⟷
sats(M,big_union_fm(1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,A,nat])"
if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
for a b c d e f g h i j k n y
using that ‹A∈M› nat_in_M by simp
then
have 1:"sats(M, is_iterates_fm(big_union_fm(1,0),2,0,1),[n,y,A,nat] ) ⟷
is_iterates(##M, big_union(##M), A, n , y)"
if "n∈M" "y∈M" for n y
using that ‹A∈M› nat_in_M
sats_is_iterates_fm[of M "big_union(##M)"] by simp
let ?f = "And(Member(0,3),is_iterates_fm(big_union_fm(1,0),2,0,1))"
have satsf:"sats(M, ?f,[n,y,A,nat] ) ⟷
n∈nat & is_iterates(##M, big_union(##M), A, n, y)"
if "n∈M" "y∈M" for n y
using that ‹A∈M› nat_in_M 1 by simp
have artyf:"arity(?f) = 4"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,nat]))"
using replacement_ax[of ?f] 1 artyf ‹A∈M› nat_in_M by simp
then
show ?thesis using repl_sats[of M ?f "[A,nat]"] satsf by simp
qed
sublocale M_ZF_trans ⊆ M_datatypes "##M"
using list_repl1_intf list_repl2_intf formula_repl1_intf
formula_repl2_intf nth_repl_intf
by unfold_locales auto
sublocale M_ZF_trans ⊆ M_eclose "##M"
using eclose_repl1_intf eclose_repl2_intf
by unfold_locales auto
definition
powerset_fm :: "[i,i] ⇒ i" where
"powerset_fm(A,z) ≡ Forall(Iff(Member(0,succ(z)),subset_fm(0,succ(A))))"
lemma powerset_type [TC]:
"⟦ x ∈ nat; y ∈ nat ⟧ ⟹ powerset_fm(x,y) ∈ formula"
by (simp add:powerset_fm_def)
definition
is_powapply_fm :: "[i,i,i] ⇒ i" where
"is_powapply_fm(f,y,z) ≡
Exists(And(fun_apply_fm(succ(f), succ(y), 0),
Forall(Iff(Member(0, succ(succ(z))),
Forall(Implies(Member(0, 1), Member(0, 2)))))))"
lemma is_powapply_type [TC] :
"⟦f∈nat ; y∈nat; z∈nat⟧ ⟹ is_powapply_fm(f,y,z)∈formula"
unfolding is_powapply_fm_def by simp
declare is_powapply_fm_def[fm_definitions add]
lemma sats_is_powapply_fm :
assumes
"f∈nat" "y∈nat" "z∈nat" "env∈list(A)" "0∈A"
shows
"is_powapply(##A,nth(f, env),nth(y, env),nth(z, env))
⟷ sats(A,is_powapply_fm(f,y,z),env)"
unfolding is_powapply_def is_powapply_fm_def powerset_def subset_def
using nth_closed assms by simp
lemma (in M_ZF_trans) powapply_repl :
assumes
"f∈M"
shows
"strong_replacement(##M,is_powapply(##M,f))"
proof -
have "arity(is_powapply_fm(2,0,1)) = 3"
unfolding is_powapply_fm_def
by (simp add: fm_definitions ord_simp_union)
then
have "∀f0∈M. strong_replacement(##M, λp z. sats(M,is_powapply_fm(2,0,1) , [p,z,f0]))"
using replacement_ax[of "is_powapply_fm(2,0,1)"] by simp
moreover
have "is_powapply(##M,f0,p,z) ⟷ sats(M,is_powapply_fm(2,0,1) , [p,z,f0])"
if "p∈M" "z∈M" "f0∈M" for p z f0
using that zero_in_M sats_is_powapply_fm[of 2 0 1 "[p,z,f0]" M] by simp
ultimately
have "∀f0∈M. strong_replacement(##M, is_powapply(##M,f0))"
unfolding strong_replacement_def univalent_def by simp
with ‹f∈M› show ?thesis by simp
qed
definition
PHrank_fm :: "[i,i,i] ⇒ i" where
"PHrank_fm(f,y,z) ≡ Exists(And(fun_apply_fm(succ(f),succ(y),0)
,succ_fm(0,succ(z))))"
lemma PHrank_type [TC]:
"⟦ x ∈ nat; y ∈ nat; z ∈ nat ⟧ ⟹ PHrank_fm(x,y,z) ∈ formula"
by (simp add:PHrank_fm_def)
lemma (in M_ZF_trans) sats_PHrank_fm :
"⟦ x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(M) ⟧
⟹ sats(M,PHrank_fm(x,y,z),env) ⟷
PHrank(##M,nth(x,env),nth(y,env),nth(z,env))"
using zero_in_M Internalizations.nth_closed by (simp add: PHrank_def PHrank_fm_def)
lemma (in M_ZF_trans) phrank_repl :
assumes
"f∈M"
shows
"strong_replacement(##M,PHrank(##M,f))"
proof -
have "arity(PHrank_fm(2,0,1)) = 3"
unfolding PHrank_fm_def
by (simp add: fm_definitions ord_simp_union)
then
have "∀f0∈M. strong_replacement(##M, λp z. sats(M,PHrank_fm(2,0,1) , [p,z,f0]))"
using replacement_ax[of "PHrank_fm(2,0,1)"] by simp
then
have "∀f0∈M. strong_replacement(##M, PHrank(##M,f0))"
unfolding strong_replacement_def univalent_def by (simp add:sats_PHrank_fm)
with ‹f∈M› show ?thesis by simp
qed
definition
is_Hrank_fm :: "[i,i,i] ⇒ i" where
"is_Hrank_fm(x,f,hc) ≡ Exists(And(big_union_fm(0,succ(hc)),
Replace_fm(succ(x),PHrank_fm(succ(succ(succ(f))),0,1),0)))"
lemma is_Hrank_type [TC]:
"⟦ x ∈ nat; y ∈ nat; z ∈ nat ⟧ ⟹ is_Hrank_fm(x,y,z) ∈ formula"
by (simp add:is_Hrank_fm_def)
lemma (in M_ZF_trans) sats_is_Hrank_fm :
"⟦ x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(M)⟧
⟹ sats(M,is_Hrank_fm(x,y,z),env) ⟷
is_Hrank(##M,nth(x,env),nth(y,env),nth(z,env))"
using zero_in_M is_Hrank_def is_Hrank_fm_def sats_Replace_fm
by (simp add:sats_PHrank_fm)
declare is_Hrank_fm_def[fm_definitions add]
declare PHrank_fm_def[fm_definitions add]
lemma (in M_ZF_trans) wfrec_rank :
assumes
"X∈M"
shows
"wfrec_replacement(##M,is_Hrank(##M),rrank(X))"
proof -
have
"is_Hrank(##M,a2, a1, a0) ⟷
sats(M, is_Hrank_fm(2,1,0), [a0,a1,a2,a3,a4,y,x,z,rrank(X)])"
if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
using that rrank_in_M ‹X∈M› by (simp add:sats_is_Hrank_fm)
then
have
1:"sats(M, is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0),[y,x,z,rrank(X)])
⟷ is_wfrec(##M, is_Hrank(##M) ,rrank(X), x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that ‹X∈M› rrank_in_M sats_is_wfrec_fm by (simp add:sats_is_Hrank_fm)
let
?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)))"
have satsf:"sats(M, ?f, [x,z,rrank(X)])
⟷ (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
if "x∈M" "z∈M" for x z
using that 1 ‹X∈M› rrank_in_M by (simp del:pair_abs)
have "arity(?f) = 3"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,rrank(X)]))"
using replacement_ax[of ?f] 1 ‹X∈M› rrank_in_M by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
using repl_sats[of M ?f "[rrank(X)]"] satsf by (simp del:pair_abs)
then
show ?thesis unfolding wfrec_replacement_def by simp
qed
definition
is_HVfrom_fm :: "[i,i,i,i] ⇒ i" where
"is_HVfrom_fm(A,x,f,h) ≡ Exists(Exists(And(union_fm(A #+ 2,1,h #+ 2),
And(big_union_fm(0,1),
Replace_fm(x #+ 2,is_powapply_fm(f #+ 4,0,1),0)))))"
declare is_HVfrom_fm_def[fm_definitions add]
lemma is_HVfrom_type [TC]:
"⟦ A∈nat; x ∈ nat; f ∈ nat; h ∈ nat ⟧ ⟹ is_HVfrom_fm(A,x,f,h) ∈ formula"
by (simp add:is_HVfrom_fm_def)
lemma sats_is_HVfrom_fm :
"⟦ a∈nat; x ∈ nat; f ∈ nat; h ∈ nat; env ∈ list(A); 0∈A⟧
⟹ sats(A,is_HVfrom_fm(a,x,f,h),env) ⟷
is_HVfrom(##A,nth(a,env),nth(x,env),nth(f,env),nth(h,env))"
using is_HVfrom_def is_HVfrom_fm_def sats_Replace_fm[OF sats_is_powapply_fm]
by simp
lemma is_HVfrom_iff_sats :
assumes
"nth(a,env) = aa" "nth(x,env) = xx" "nth(f,env) = ff" "nth(h,env) = hh"
"a∈nat" "x∈nat" "f∈nat" "h∈nat" "env∈list(A)" "0∈A"
shows
"is_HVfrom(##A,aa,xx,ff,hh) ⟷ sats(A, is_HVfrom_fm(a,x,f,h), env)"
using assms sats_is_HVfrom_fm by simp
schematic_goal sats_is_Vset_fm_auto :
assumes
"i∈nat" "v∈nat" "env∈list(A)" "0∈A"
"i < length(env)" "v < length(env)"
shows
"is_Vset(##A,nth(i, env),nth(v, env))
⟷ sats(A,?ivs_fm(i,v),env)"
unfolding is_Vset_def is_Vfrom_def
by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+)
schematic_goal is_Vset_iff_sats :
assumes
"nth(i,env) = ii" "nth(v,env) = vv"
"i∈nat" "v∈nat" "env∈list(A)" "0∈A"
"i < length(env)" "v < length(env)"
shows
"is_Vset(##A,ii,vv) ⟷ sats(A, ?ivs_fm(i,v), env)"
unfolding ‹nth(i,env) = ii›[symmetric] ‹nth(v,env) = vv›[symmetric]
by (rule sats_is_Vset_fm_auto(1); simp add:assms)
lemma (in M_ZF_trans) memrel_eclose_sing :
"a∈M ⟹ ∃sa∈M. ∃esa∈M. ∃mesa∈M.
upair(##M,a,a,sa) & is_eclose(##M,sa,esa) & membership(##M,esa,mesa)"
using upair_ax eclose_closed Memrel_closed unfolding upair_ax_def
by (simp del:upair_abs)
lemma (in M_ZF_trans) trans_repl_HVFrom :
assumes
"A∈M" "i∈M"
shows
"transrec_replacement(##M,is_HVfrom(##M,A),i)"
proof -
{ fix mesa
assume "mesa∈M"
have
0:"is_HVfrom(##M,A,a2, a1, a0) ⟷
sats(M, is_HVfrom_fm(8,2,1,0), [a0,a1,a2,a3,a4,y,x,z,A,mesa])"
if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
using that zero_in_M sats_is_HVfrom_fm ‹mesa∈M› ‹A∈M› by simp
have
1:"sats(M, is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0),[y,x,z,A,mesa])
⟷ is_wfrec(##M, is_HVfrom(##M,A),mesa, x, y)"
if "y∈M" "x∈M" "z∈M" for y x z
using that ‹A∈M› ‹mesa∈M› sats_is_wfrec_fm[OF 0] by simp
let
?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)))"
have satsf:"sats(M, ?f, [x,z,A,mesa])
⟷ (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
if "x∈M" "z∈M" for x z
using that 1 ‹A∈M› ‹mesa∈M› by (simp del:pair_abs)
have "arity(?f) = 4"
unfolding fm_definitions
by (simp add:ord_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,A,mesa]))"
using replacement_ax[of ?f] 1 ‹A∈M› ‹mesa∈M› by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
using repl_sats[of M ?f "[A,mesa]"] satsf by (simp del:pair_abs)
then
have "wfrec_replacement(##M,is_HVfrom(##M,A),mesa)"
unfolding wfrec_replacement_def by simp
}
then show ?thesis unfolding transrec_replacement_def
using ‹i∈M› memrel_eclose_sing by simp
qed
sublocale M_ZF_trans ⊆ M_eclose_pow "##M"
using power_ax powapply_repl phrank_repl trans_repl_HVFrom
wfrec_rank by unfold_locales auto
subsection‹Interface for proving Collects and Replace in M.›
context M_ZF_trans
begin
lemma Collect_in_M :
assumes
"φ ∈ formula" "env∈list(M)"
"arity(φ) ≤ 1 #+ length(env)" "A∈M" and
satsQ: "⋀x. x∈M ⟹ sats(M,φ,[x]@env) ⟷ Q(x)"
shows
"{y∈A . Q(y)}∈M"
proof -
have "separation(##M,λx. sats(M,φ,[x] @ env))"
using assms separation_ax by simp
then show ?thesis using
‹A∈M› satsQ trans_M
separation_cong[of "##M" "λy. sats(M,φ,[y]@env)" "Q"]
separation_closed by simp
qed
lemma separation_in_M :
assumes
"φ ∈ formula" "env∈list(M)"
"arity(φ) ≤ 1 #+ length(env)" "A∈M" and
satsQ: "⋀x. x∈A ⟹ sats(M,φ,[x]@env) ⟷ Q(x)"
shows
"{y∈A . Q(y)} ∈ M"
proof -
let ?φ' = "And(φ,Member(0,length(env)#+1))"
have "arity(?φ') ≤ 1 #+ length(env@[A])"
using assms Un_le
le_trans[of "arity(φ)" "1#+length(env)" "2#+length(env)"]
by force
moreover from assms
have "?φ'∈formula"
"nth(length(env), env @ [A]) = A" using assms nth_append by auto
moreover from calculation
have "⋀ x . x ∈ M ⟹ sats(M,?φ',[x]@env@[A]) ⟷ Q(x) ∧ x∈A"
using arity_sats_iff[of _ "[A]" _ "[_]@env"] assms
by auto
ultimately
show ?thesis using assms
Collect_in_M[of ?φ' "env@[A]" _ "λx . Q(x) ∧ x∈A", OF _ _ _ ‹A∈M›]
by auto
qed
lemma Replace_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 #+ length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)"
shows "{f(x) . x∈A}∈M"
proof -
let ?φ' = "And(φ,Member(0,length(env)#+2))"
have "arity(?φ') ≤ 2 #+ length(env@[A])"
using assms Un_le
le_trans[of "arity(φ)" "2#+(length(env))" "3#+length(env)"]
by force
moreover from assms
have "?φ'∈formula" "nth(length(env), env @ [A]) = A"
using assms nth_append by auto
moreover from calculation
have "⋀ x y. x ∈ M ⟹ y∈M ⟹ (M,[x,y]@env@[A]⊨?φ') ⟷ y=f(x) ∧x∈A"
using arity_sats_iff[of _ "[A]" _ "[_,_]@env"] assms
by auto
moreover from calculation
have "strong_replacement(##M, λx y. M,[x,y]@env@[A] ⊨ ?φ')"
using replacement_ax[of ?φ'] ‹env∈list(M)› assms by simp
ultimately
have 4:"strong_replacement(##M, λx y. y = f(x) ∧ x∈A)"
using
strong_replacement_cong[of "##M" "λx y. M,[x,y]@env@[A]⊨?φ'" "λx y. y = f(x) ∧ x∈A"]
by simp
then
have "{y . x∈A , y = f(x)} ∈ M"
using ‹A∈M› strong_replacement_closed[OF 4,of A] fclosed by simp
moreover
have "{f(x). x∈A} = { y . x∈A , y = f(x)}"
by auto
ultimately show ?thesis by simp
qed
lemma Replace_relativized_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 #+ length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈A ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)"
shows "{f(x) . x∈A}∈M"
using assms Replace_in_M[of φ] by auto
definition ρ_repl :: "i⇒i" where
"ρ_repl(l) ≡ rsum({⟨0, 1⟩, ⟨1, 0⟩}, id(l), 2, 3, l)"
lemma f_type : "{⟨0, 1⟩, ⟨1, 0⟩} ∈ 2 → 3"
using Pi_iff unfolding function_def by auto
lemma ren_type :
assumes "l∈nat"
shows "ρ_repl(l) : 2#+l → 3#+l"
using sum_type[of 2 3 l l "{⟨0, 1⟩, ⟨1, 0⟩}" "id(l)"] f_type assms id_type
unfolding ρ_repl_def by auto
lemma ren_action :
assumes
"env∈list(M)" "x∈M" "y∈M" "z∈M"
shows "∀ i . i < 2#+length(env) ⟶
nth(i,[x,z]@env) = nth(ρ_repl(length(env))`i,[z,x,y]@env)"
proof -
let ?f="{⟨0, 1⟩, ⟨1, 0⟩}"
have 1:"(⋀j. j < length(env) ⟹ nth(j, env) = nth(id(length(env)) ` j, env))"
using assms ltD by simp
have 2:"nth(j, [x,z]) = nth(?f ` j, [z,x,y])" if "j<2" for j
proof -
consider "j=0" | "j=1" using ltD[OF ‹j<2›] by auto
then show ?thesis
proof(cases)
case 1
then show ?thesis using apply_equality f_type by simp
next
case 2
then show ?thesis using apply_equality f_type by simp
qed
qed
show ?thesis
using sum_action[OF _ _ _ _ f_type id_type _ _ _ _ _ _ _ 2 1,simplified] assms
unfolding ρ_repl_def by simp
qed
lemma Lambda_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 2 #+ length(env)" and
fsats: "⋀x y. x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ φ) ⟷ is_f(x,y)" and
fabs: "⋀x y. x∈A ⟹ y∈M ⟹ is_f(x,y) ⟷ y = f(x)" and
fclosed: "⋀x. x∈A ⟹ f(x) ∈ M" and
"A∈M" "env∈list(M)"
shows "(λx∈A . f(x)) ∈M"
unfolding lam_def
proof -
let ?ren="ρ_repl(length(env))"
let ?j="2#+length(env)"
let ?k="3#+length(env)"
let ?ψ="ren(φ)`?j`?k`?ren"
let ?φ'="Exists(And(pair_fm(1,0,2),?ψ))"
let ?p="λx y. ∃z∈M. pair(##M,x,z,y) ∧ is_f(x,z)"
have "?φ'∈formula" "?ψ∈formula"
using ‹env∈_› length_type f_fm ren_type ren_tc[of φ "2#+length(env)" "3#+length(env)" ?ren]
by simp_all
moreover from this
have "arity(?ψ)≤3#+(length(env))" "arity(?ψ)∈nat"
using assms arity_ren[OF f_fm _ _ ren_type,of "length(env)"] by simp_all
then
have "arity(?φ') ≤ 2#+(length(env))"
using arity_pair_fm Un_le pred_Un_distrib assms pred_le
by simp
moreover from this calculation
have "x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ ?φ') ⟷ ?p(x,y)" for x y
using ‹env∈_› length_type[OF ‹env∈_›] assms transitivity[OF _ ‹A∈M›]
sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type f_ar ren_action[rule_format,of _ x y],of _ M ]
by auto
moreover
have "x∈A ⟹ y∈M ⟹ ?p(x,y) ⟷ y = <x,f(x)>" for x y
using assms transitivity[OF _ ‹A∈_›] fclosed
by simp
moreover
have "⋀ x . x∈A ⟹ <x,f(x)> ∈ M"
using transitivity[OF _ ‹A∈M›] pair_in_M_iff fclosed by simp
ultimately
show "{⟨x,f(x)⟩ . x∈A } ∈ M"
using Replace_in_M[of ?φ'] ‹A∈M› ‹env∈_›
by simp
qed
definition ρ_pair_repl :: "i⇒i" where
"ρ_pair_repl(l) ≡ rsum({⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 3⟩}, id(l), 3, 4, l)"
lemma f_type' : "{⟨0,0 ⟩, ⟨1, 1⟩, ⟨2, 3⟩} ∈ 3 → 4"
using Pi_iff unfolding function_def by auto
lemma ren_type' :
assumes "l∈nat"
shows "ρ_pair_repl(l) : 3#+l → 4#+l"
using sum_type[of 3 4 l l "{⟨0, 0⟩, ⟨1, 1⟩, ⟨2, 3⟩}" "id(l)"] f_type' assms id_type
unfolding ρ_pair_repl_def by auto
lemma ren_action' :
assumes
"env∈list(M)" "x∈M" "y∈M" "z∈M" "u∈M"
shows "∀ i . i < 3#+length(env) ⟶
nth(i,[x,z,u]@env) = nth(ρ_pair_repl(length(env))`i,[x,z,y,u]@env)"
proof -
let ?f="{⟨0, 0⟩, ⟨1, 1⟩, ⟨2,3⟩}"
have 1:"(⋀j. j < length(env) ⟹ nth(j, env) = nth(id(length(env)) ` j, env))"
using assms ltD by simp
have 2:"nth(j, [x,z,u]) = nth(?f ` j, [x,z,y,u])" if "j<3" for j
proof -
consider "j=0" | "j=1" | "j=2" using ltD[OF ‹j<3›] by auto
then show ?thesis
proof(cases)
case 1
then show ?thesis using apply_equality f_type' by simp
next
case 2
then show ?thesis using apply_equality f_type' by simp
next
case 3
then show ?thesis using apply_equality f_type' by simp
qed
qed
show ?thesis
using sum_action[OF _ _ _ _ f_type' id_type _ _ _ _ _ _ _ 2 1,simplified] assms
unfolding ρ_pair_repl_def by simp
qed
lemma LambdaPair_in_M :
assumes
f_fm: "φ ∈ formula" and
f_ar: "arity(φ)≤ 3 #+ length(env)" and
fsats: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ (M,[x,z,r]@env ⊨ φ) ⟷ is_f(x,z,r)" and
fabs: "⋀x z r. x∈M ⟹ z∈M ⟹ r∈M ⟹ is_f(x,z,r) ⟷ r = f(x,z)" and
fclosed: "⋀x z. x∈M ⟹ z∈M ⟹ f(x,z) ∈ M" and
"A∈M" "env∈list(M)"
shows "(λx∈A . f(fst(x),snd(x))) ∈M"
proof -
let ?ren="ρ_pair_repl(length(env))"
let ?j="3#+length(env)"
let ?k="4#+length(env)"
let ?ψ="ren(φ)`?j`?k`?ren"
let ?φ'="Exists(Exists(And(fst_fm(2,0),(And(snd_fm(2,1),?ψ)))))"
let ?p="λx y. is_f(fst(x),snd(x),y)"
have "?φ'∈formula" "?ψ∈formula"
using ‹env∈_› length_type f_fm ren_type' ren_tc[of φ ?j ?k ?ren]
by simp_all
moreover from this
have "arity(?ψ)≤4#+(length(env))" "arity(?ψ)∈nat"
using assms arity_ren[OF f_fm _ _ ren_type',of "length(env)"] by simp_all
moreover from calculation
have 1:"arity(?φ') ≤ 2#+(length(env))" "?φ'∈formula"
using arity_fst_fm arity_snd_fm Un_le pred_Un_distrib assms pred_le
by simp_all
moreover from this calculation
have 2:"x∈A ⟹ y∈M ⟹ (M,[x,y]@env ⊨ ?φ') ⟷ ?p(x,y)" for x y
using
sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type' f_ar
ren_action'[rule_format,of _ "fst(x)" x "snd(x)" y],simplified]
‹env∈_› length_type[OF ‹env∈_›] transitivity[OF _ ‹A∈M›]
fst_snd_closed pair_in_M_iff fsats[of "fst(x)" "snd(x)" y,symmetric]
fst_abs snd_abs
by auto
moreover from assms
have 3:"x∈A ⟹ y∈M ⟹ ?p(x,y) ⟷ y = f(fst(x),snd(x))" for x y
using fclosed fst_snd_closed pair_in_M_iff fabs transitivity
by auto
moreover
have 4:"⋀ x . x∈A ⟹ <x,f(fst(x),snd(x))> ∈ M" "⋀ x . x∈A ⟹ f(fst(x),snd(x)) ∈ M"
using transitivity[OF _ ‹A∈M›] pair_in_M_iff fclosed fst_snd_closed
by simp_all
ultimately
show ?thesis
using Lambda_in_M[of ?φ'] ‹env∈_› ‹A∈_› by simp
qed
end
end