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
begin
syntax
"_sats" :: "[i, i, i] ⇒ o" (‹(_, _ ⊨ _)› [36,36,36] 60)
syntax_consts
"_sats" ⇌ sats
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_trans =
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))"
and trans_M: "Transset(M)"
begin
lemma TranssetI :
"(⋀y x. y∈x ⟹ x∈M ⟹ y∈M) ⟹ Transset(M)"
by (auto simp add: Transset_def)
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
with trans_M have "z=0"
by (simp add: empty_def, blast intro: Transset_intf )
with zm show ?thesis
by simp
qed
subsection‹Interface with \<^term>‹M_trivial››
lemma mtrans :
"M_trans(##M)"
using Transset_intf[OF trans_M] zero_in_M exI[of "λx. x∈M"]
by unfold_locales auto
lemma mtriv :
"M_trivial(##M)"
using trans_M M_trivial.intro mtrans M_trivial_axioms.intro upair_ax Union_ax
by simp
end
sublocale M_ZF_trans ⊆ M_trivial "##M"
by (rule mtriv)
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_defs 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_defs 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_defs 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_defs 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_defs 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_defs 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_defs 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_defs 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_defs 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
lemma mbasic : "M_basic(##M)"
using trans_M zero_in_M power_ax M_basic_sep_instances funspace_succ_rep_intf mtriv
by unfold_locales auto
end
sublocale M_ZF_trans ⊆ M_basic "##M"
by (rule mbasic)
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_defs 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)+)
lemma (in M_ZF_trans) 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_defs trans_closure_fm_def
by (simp del:FOL_sats_iff pair_abs add: fm_defs 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
lemma (in M_ZF_trans) 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 (in M_ZF_trans) nat_subset_I' :
"⟦ I∈M ; 0∈I ; ⋀x. x∈I ⟹ succ(x)∈I ⟧ ⟹ nat ⊆ I"
by (rule subsetI,induct_tac x,simp+)
lemma (in M_ZF_trans) 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 Transset_intf[OF trans_M] 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 (in M_ZF_trans) 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
lemma (in M_ZF_trans) mtrancl : "M_trancl(##M)"
using mbasic rtrancl_separation_intf wftrancl_separation_intf nat_in_M
wellfounded_trancl_def
by unfold_locales auto
sublocale M_ZF_trans ⊆ M_trancl "##M"
by (rule mtrancl)
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) nat_trans_M :
"n∈M" if "n∈nat" for n
using that nat_in_M Transset_intf[OF trans_M] by simp
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_trans_M by simp
then have 1:"Memrel(succ(n))∈M"
using ‹n∈nat› Memrel_closed by simp
have "0∈M"
using nat_0I nat_trans_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 iterates_MH_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
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_trans_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 iterates_MH_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
restriction_fm_def pre_image_fm_def quasinat_fm_def fm_defs
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_trans_M by simp
have 1:"arity(formula_functor_fm(1,0)) = 2"
unfolding formula_functor_fm_def fm_defs sum_fm_def cartprod_fm_def number1_fm_def
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 tl_fm_def fm_defs quasilist_fm_def Cons_fm_def Nil_fm_def Inr_fm_def number1_fm_def
Inl_fm_def 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 big_union_fm_def fm_defs 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_trans_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 is_iterates_fm_def restriction_fm_def list_functor_fm_def number1_fm_def Memrel_fm_def
cartprod_fm_def sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs is_wfrec_fm_def
is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def
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_trans_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 is_iterates_fm_def formula_functor_fm_def fm_defs sum_fm_def quasinat_fm_def
cartprod_fm_def number1_fm_def Memrel_fm_def ordinal_fm_def transset_fm_def
is_wfrec_fm_def is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def subset_fm_def
pre_image_fm_def restriction_fm_def
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 is_iterates_fm_def formula_functor_fm_def fm_defs sum_fm_def quasinat_fm_def
cartprod_fm_def number1_fm_def Memrel_fm_def ordinal_fm_def transset_fm_def
is_wfrec_fm_def is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def subset_fm_def
pre_image_fm_def restriction_fm_def
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
lemma (in M_ZF_trans) mdatatypes : "M_datatypes(##M)"
using mtrancl list_repl1_intf list_repl2_intf formula_repl1_intf
formula_repl2_intf nth_repl_intf
by unfold_locales auto
sublocale M_ZF_trans ⊆ M_datatypes "##M"
by (rule mdatatypes)
lemma (in M_ZF_trans) meclose : "M_eclose(##M)"
using mdatatypes eclose_repl1_intf eclose_repl2_intf
by unfold_locales auto
sublocale M_ZF_trans ⊆ M_eclose "##M"
by (rule meclose)
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
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 is_Collect_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_defs 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 [simp]:
"⟦ 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_defs 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
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 [simp]:
"⟦ 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
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
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
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 is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def is_Hrank_fm_def PHrank_fm_def
restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
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)))))"
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 is_HVfrom_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
is_powapply_fm_def sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
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
lemma (in M_ZF_trans) meclose_pow : "M_eclose_pow(##M)"
using meclose power_ax powapply_repl phrank_repl trans_repl_HVFrom wfrec_rank
by unfold_locales auto
sublocale M_ZF_trans ⊆ M_eclose_pow "##M"
by (rule meclose_pow)
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