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
begin
syntax
"_sats" :: "[i, i, i] ⇒ o" ("(_, _ ⊨ _)" [36,36,36] 60)
translations
"(M,env ⊨ φ)" ⇌ "CONST sats(M,φ,env)"
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
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 M_trivial.intro M_trivial_axioms.intro upair_ax
Union_ax by unfold_locales
context M_ZF_trans
begin
subsection‹Interface with \<^term>‹M_basic››
schematic_goal inter_fm_auto:
assumes
"nth(i,env) = x" "nth(j,env) = B"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"(∀y∈A . y∈B ⟶ x∈y) ⟷ sats(A,?ifm(i,j),env)"
by (insert assms ; (rule sep_rules | simp)+)
lemma inter_sep_intf :
assumes
"A∈M"
shows
"separation(##M,λx . ∀y∈M . y∈A ⟶ x∈y)"
proof -
obtain ifm where
fmsats:"⋀env. env∈list(M) ⟹ (∀ y∈M. y∈(nth(1,env)) ⟶ nth(0,env)∈y)
⟷ sats(M,ifm(0,1),env)"
and
"ifm(0,1) ∈ formula"
and
"arity(ifm(0,1)) = 2"
using ‹A∈M› inter_fm_auto
by (simp del:FOL_sats_iff add: nat_simp_union)
then
have "∀a∈M. separation(##M, λx. sats(M,ifm(0,1) , [x, a]))"
using separation_ax by simp
moreover
have "(∀y∈M . y∈a ⟶ x∈y) ⟷ sats(M,ifm(0,1),[x,a])"
if "a∈M" "x∈M" for a x
using that fmsats[of "[x,a]"] 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: nat_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 nat_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 nat_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 nat_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 nat_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 nat_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 nat_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 nat_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 nat_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 nat_simp_union)
then
have "∀n0∈M. strong_replacement(##M, λp z. sats(M,fsfm(0,1,2) , [p,z,n0]))"
using replacement_ax 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 nat_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
"nth(i,env) = r" "nth(j,env) = rp"
"i ∈ nat" "j ∈ nat" "env ∈ list(A)"
shows
"tran_closure(##A,r,rp) ⟷ sats(A,?tc(i,j),env)"
unfolding tran_closure_def
by (insert assms ; (rule sep_rules rtran_closure_fm_auto | simp))+
synthesize "trans_closure_fm" from_schematic trans_closure_fm_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_fm_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: nat_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: nat_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:nat_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),A,0]))"
using replacement_ax 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:nat_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),v]))"
using replacement_ax 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:nat_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 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:nat_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 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:nat_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 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:nat_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,0,nat]))"
using replacement_ax 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:nat_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,0,nat]))"
using replacement_ax 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:nat_simp_union)
then
have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,nat]))"
using replacement_ax 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 nat_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 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 nat_simp_union)
then
have "∀f0∈M. strong_replacement(##M, λp z. sats(M,PHrank_fm(2,0,1) , [p,z,f0]))"
using replacement_ax 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:nat_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,rrank(X)]))"
using replacement_ax 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:nat_simp_union)
then
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,A,mesa]))"
using replacement_ax 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
lemma (in M_ZF_trans) repl_gen :
assumes
f_abs: "⋀x y. ⟦ x∈M; y∈M ⟧ ⟹ is_F(##M,x,y) ⟷ y = f(x)"
and
f_sats: "⋀x y. ⟦x∈M ; y∈M ⟧ ⟹
sats(M,f_fm,Cons(x,Cons(y,env))) ⟷ is_F(##M,x,y)"
and
f_form: "f_fm ∈ formula"
and
f_arty: "arity(f_fm) = 2"
and
"env∈list(M)"
shows
"strong_replacement(##M, λx y. y = f(x))"
proof -
have "sats(M,f_fm,[x,y]@env) ⟷ is_F(##M,x,y)" if "x∈M" "y∈M" for x y
using that f_sats[of x y] by simp
moreover
from f_form f_arty
have "strong_replacement(##M, λx y. sats(M,f_fm,[x,y]@env))"
using ‹env∈list(M)› replacement_ax by simp
ultimately
have "strong_replacement(##M, is_F(##M))"
using strong_replacement_cong[of "##M" "λx y. sats(M,f_fm,[x,y]@env)" "is_F(##M)"] by simp
with f_abs show ?thesis
using strong_replacement_cong[of "##M" "is_F(##M)" "λx y. y = f(x)"] by simp
qed
lemma (in M_ZF_trans) sep_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
end