Theory Replacement_Axiom
section‹The Axiom of Replacement in $M[G]$›
theory Replacement_Axiom
imports
Least Relative_Univ Separation_Axiom Renaming_Auto
begin
rename "renrep1" src "[p,P,leq,o,ρ,τ]" tgt "[V,τ,ρ,p,α,P,leq,o]"
definition renrep_fn :: "i ⇒ i" where
"renrep_fn(env) ≡ sum(renrep1_fn,id(length(env)),6,8,length(env))"
definition
renrep :: "[i,i] ⇒ i" where
"renrep(φ,env) = ren(φ)`(6#+length(env))`(8#+length(env))`renrep_fn(env)"
lemma renrep_type [TC]:
assumes "φ∈formula" "env ∈ list(M)"
shows "renrep(φ,env) ∈ formula"
unfolding renrep_def renrep_fn_def renrep1_fn_def
using assms renrep1_thm(1) ren_tc
by simp
lemma arity_renrep:
assumes "φ∈formula" "arity(φ)≤ 6#+length(env)" "env ∈ list(M)"
shows "arity(renrep(φ,env)) ≤ 8#+length(env)"
unfolding renrep_def renrep_fn_def renrep1_fn_def
using assms renrep1_thm(1) arity_ren
by simp
lemma renrep_sats :
assumes "arity(φ) ≤ 6 #+ length(env)"
"[P,leq,o,p,ρ,τ] @ env ∈ list(M)"
"V ∈ M" "α ∈ M"
"φ∈formula"
shows "sats(M, φ, [p,P,leq,o,ρ,τ] @ env) ⟷ sats(M, renrep(φ,env), [V,τ,ρ,p,α,P,leq,o] @ env)"
unfolding renrep_def renrep_fn_def renrep1_fn_def
by (rule sats_iff_sats_ren,insert assms, auto simp add:renrep1_thm(1)[of _ M,simplified]
renrep1_thm(2)[simplified,where p=p and α=α])
rename "renpbdy1" src "[ρ,p,α,P,leq,o]" tgt "[ρ,p,x,α,P,leq,o]"
definition renpbdy_fn :: "i ⇒ i" where
"renpbdy_fn(env) ≡ sum(renpbdy1_fn,id(length(env)),6,7,length(env))"
definition
renpbdy :: "[i,i] ⇒ i" where
"renpbdy(φ,env) = ren(φ)`(6#+length(env))`(7#+length(env))`renpbdy_fn(env)"
lemma
renpbdy_type [TC]: "φ∈formula ⟹ env∈list(M) ⟹ renpbdy(φ,env) ∈ formula"
unfolding renpbdy_def renpbdy_fn_def renpbdy1_fn_def
using renpbdy1_thm(1) ren_tc
by simp
lemma arity_renpbdy: "φ∈formula ⟹ arity(φ) ≤ 6 #+ length(env) ⟹ env∈list(M) ⟹ arity(renpbdy(φ,env)) ≤ 7 #+ length(env)"
unfolding renpbdy_def renpbdy_fn_def renpbdy1_fn_def
using renpbdy1_thm(1) arity_ren
by simp
lemma
sats_renpbdy: "arity(φ) ≤ 6 #+ length(nenv) ⟹ [ρ,p,x,α,P,leq,o,π] @ nenv ∈ list(M) ⟹ φ∈formula ⟹
sats(M, φ, [ρ,p,α,P,leq,o] @ nenv) ⟷ sats(M, renpbdy(φ,nenv), [ρ,p,x,α,P,leq,o] @ nenv)"
unfolding renpbdy_def renpbdy_fn_def renpbdy1_fn_def
by (rule sats_iff_sats_ren,auto simp add: renpbdy1_thm(1)[of _ M,simplified]
renpbdy1_thm(2)[simplified,where α=α and x=x])
rename "renbody1" src "[x,α,P,leq,o]" tgt "[α,x,m,P,leq,o]"
definition renbody_fn :: "i ⇒ i" where
"renbody_fn(env) ≡ sum(renbody1_fn,id(length(env)),5,6,length(env))"
definition
renbody :: "[i,i] ⇒ i" where
"renbody(φ,env) = ren(φ)`(5#+length(env))`(6#+length(env))`renbody_fn(env)"
lemma
renbody_type [TC]: "φ∈formula ⟹ env∈list(M) ⟹ renbody(φ,env) ∈ formula"
unfolding renbody_def renbody_fn_def renbody1_fn_def
using renbody1_thm(1) ren_tc
by simp
lemma arity_renbody: "φ∈formula ⟹ arity(φ) ≤ 5 #+ length(env) ⟹ env∈list(M) ⟹
arity(renbody(φ,env)) ≤ 6 #+ length(env)"
unfolding renbody_def renbody_fn_def renbody1_fn_def
using renbody1_thm(1) arity_ren
by simp
lemma
sats_renbody: "arity(φ) ≤ 5 #+ length(nenv) ⟹ [α,x,m,P,leq,o] @ nenv ∈ list(M) ⟹ φ∈formula ⟹
sats(M, φ, [x,α,P,leq,o] @ nenv) ⟷ sats(M, renbody(φ,nenv), [α,x,m,P,leq,o] @ nenv)"
unfolding renbody_def renbody_fn_def renbody1_fn_def
by (rule sats_iff_sats_ren, auto simp add:renbody1_thm(1)[of _ M,simplified]
renbody1_thm(2)[where α=α and m=m,simplified])
context G_generic
begin
lemma pow_inter_M:
assumes
"x∈M" "y∈M"
shows
"powerset(##M,x,y) ⟷ y = Pow(x) ∩ M"
using assms by auto
schematic_goal sats_prebody_fm_auto:
assumes
"φ∈formula" "[P,leq,one,p,ρ,π] @ nenv ∈list(M)" "α∈M" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"(∃τ∈M. ∃V∈M. is_Vset(##M,α,V) ∧ τ∈V ∧ sats(M,forces(φ),[p,P,leq,one,ρ,τ] @ nenv))
⟷ sats(M,?prebody_fm,[ρ,p,α,P,leq,one] @ nenv)"
apply (insert assms; (rule sep_rules is_Vset_iff_sats[OF _ _ _ _ _ nonempty[simplified]] | simp))
apply (rule sep_rules is_Vset_iff_sats is_Vset_iff_sats[OF _ _ _ _ _ nonempty[simplified]] | simp)+
apply (rule nonempty[simplified])
apply (simp_all)
apply (rule length_type[THEN nat_into_Ord], blast)+
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply ((rule sep_rules | simp))
apply (rule renrep_sats[simplified])
apply (insert assms)
apply(auto simp add: renrep_type definability)
proof -
from assms
have "nenv∈list(M)" by simp
with ‹arity(φ)≤_› ‹φ∈_›
show "arity(forces(φ)) ≤ succ(succ(succ(succ(succ(succ(length(nenv)))))))"
using arity_forces_le by simp
qed
synthesize_notc "prebody_fm" from_schematic sats_prebody_fm_auto
lemma prebody_fm_type [TC]:
assumes "φ∈formula"
"env ∈ list(M)"
shows "prebody_fm(φ,env)∈formula"
proof -
from ‹φ∈formula›
have "forces(φ)∈formula" by simp
then
have "renrep(forces(φ),env)∈formula"
using ‹env∈list(M)› by simp
then show ?thesis unfolding prebody_fm_def by simp
qed
lemmas new_fm_defs = fm_defs is_transrec_fm_def is_eclose_fm_def mem_eclose_fm_def
finite_ordinal_fm_def is_wfrec_fm_def Memrel_fm_def eclose_n_fm_def is_recfun_fm_def is_iterates_fm_def
iterates_MH_fm_def is_nat_case_fm_def quasinat_fm_def pre_image_fm_def restriction_fm_def
lemma sats_prebody_fm:
assumes
"[P,leq,one,p,ρ] @ nenv ∈list(M)" "φ∈formula" "α∈M" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"sats(M,prebody_fm(φ,nenv),[ρ,p,α,P,leq,one] @ nenv) ⟷
(∃τ∈M. ∃V∈M. is_Vset(##M,α,V) ∧ τ∈V ∧ sats(M,forces(φ),[p,P,leq,one,ρ,τ] @ nenv))"
unfolding prebody_fm_def using assms sats_prebody_fm_auto by force
lemma arity_prebody_fm:
assumes
"φ∈formula" "α∈M" "env ∈ list(M)" "arity(φ) ≤ 2 #+ length(env)"
shows
"arity(prebody_fm(φ,env))≤6 #+ length(env)"
unfolding prebody_fm_def is_HVfrom_fm_def is_powapply_fm_def
using assms new_fm_defs nat_simp_union
arity_renrep[of "forces(φ)"] arity_forces_le[simplified] pred_le by auto
definition
body_fm' :: "[i,i]⇒i" where
"body_fm'(φ,env) ≡ Exists(Exists(And(pair_fm(0,1,2),renpbdy(prebody_fm(φ,env),env))))"
lemma body_fm'_type[TC]: "φ∈formula ⟹ env∈list(M) ⟹ body_fm'(φ,env)∈formula"
unfolding body_fm'_def using prebody_fm_type
by simp
lemma arity_body_fm':
assumes
"φ∈formula" "α∈M" "env∈list(M)" "arity(φ) ≤ 2 #+ length(env)"
shows
"arity(body_fm'(φ,env))≤5 #+ length(env)"
unfolding body_fm'_def
using assms new_fm_defs nat_simp_union arity_prebody_fm pred_le arity_renpbdy[of "prebody_fm(φ,env)"]
by auto
lemma sats_body_fm':
assumes
"∃t p. x=⟨t,p⟩" "x∈M" "[α,P,leq,one,p,ρ] @ nenv ∈list(M)" "φ∈formula" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"sats(M,body_fm'(φ,nenv),[x,α,P,leq,one] @ nenv) ⟷
sats(M,renpbdy(prebody_fm(φ,nenv),nenv),[fst(x),snd(x),x,α,P,leq,one] @ nenv)"
using assms fst_snd_closed[OF ‹x∈M›] unfolding body_fm'_def
by (auto)
definition
body_fm :: "[i,i]⇒i" where
"body_fm(φ,env) ≡ renbody(body_fm'(φ,env),env)"
lemma body_fm_type [TC]: "env∈list(M) ⟹ φ∈formula ⟹ body_fm(φ,env)∈formula"
unfolding body_fm_def by simp
lemma sats_body_fm:
assumes
"∃t p. x=⟨t,p⟩" "[α,x,m,P,leq,one] @ nenv ∈list(M)"
"φ∈formula" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"sats(M,body_fm(φ,nenv),[α,x,m,P,leq,one] @ nenv) ⟷
sats(M,renpbdy(prebody_fm(φ,nenv),nenv),[fst(x),snd(x),x,α,P,leq,one] @ nenv)"
using assms sats_body_fm' sats_renbody[OF _ assms(2), symmetric] arity_body_fm'
unfolding body_fm_def
by auto
lemma sats_renpbdy_prebody_fm:
assumes
"∃t p. x=⟨t,p⟩" "x∈M" "[α,m,P,leq,one] @ nenv ∈list(M)"
"φ∈formula" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"sats(M,renpbdy(prebody_fm(φ,nenv),nenv),[fst(x),snd(x),x,α,P,leq,one] @ nenv) ⟷
sats(M,prebody_fm(φ,nenv),[fst(x),snd(x),α,P,leq,one] @ nenv)"
using assms fst_snd_closed[OF ‹x∈M›]
sats_renpbdy[OF arity_prebody_fm _ prebody_fm_type, of concl:M, symmetric]
by force
lemma body_lemma:
assumes
"∃t p. x=⟨t,p⟩" "x∈M" "[x,α,m,P,leq,one] @ nenv ∈list(M)"
"φ∈formula" "arity(φ) ≤ 2 #+ length(nenv)"
shows
"sats(M,body_fm(φ,nenv),[α,x,m,P,leq,one] @ nenv) ⟷
(∃τ∈M. ∃V∈M. is_Vset(λa. (##M)(a),α,V) ∧ τ ∈ V ∧ (snd(x) ⊩ φ ([fst(x),τ]@nenv)))"
using assms sats_body_fm[of x α m nenv] sats_renpbdy_prebody_fm[of x α]
sats_prebody_fm[of "snd(x)" "fst(x)"] fst_snd_closed[OF ‹x∈M›]
by (simp, simp flip: setclass_iff,simp)
lemma Replace_sats_in_MG:
assumes
"c∈M[G]" "env ∈ list(M[G])"
"φ ∈ formula" "arity(φ) ≤ 2 #+ length(env)"
"univalent(##M[G], c, λx v. (M[G] , [x,v]@env ⊨ φ) )"
shows
"{v. x∈c, v∈M[G] ∧ (M[G] , [x,v]@env ⊨ φ)} ∈ M[G]"
proof -
let ?R = "λ x v . v∈M[G] ∧ (M[G] , [x,v]@env ⊨ φ)"
from ‹c∈M[G]›
obtain π' where "val(G, π') = c" "π' ∈ M"
using GenExt_def by auto
then
have "domain(π')×P∈M" (is "?π∈M")
using cartprod_closed P_in_M domain_closed by simp
from ‹val(G, π') = c›
have "c ⊆ val(G,?π)"
using def_val[of G ?π] one_in_P one_in_G[OF generic] elem_of_val
domain_of_prod[OF one_in_P, of "domain(π')"] by force
from ‹env ∈ _›
obtain nenv where "nenv∈list(M)" "env = map(val(G),nenv)"
using map_val by auto
then
have "length(nenv) = length(env)" by simp
define f where "f(ρp) ≡ μ α. α∈M ∧ (∃τ∈M. τ ∈ Vset(α) ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv)))" (is "_ ≡ μ α. ?P(ρp,α)") for ρp
have "f(ρp) = (μ α. α∈M ∧ (∃τ∈M. ∃V∈M. is_Vset(##M,α,V) ∧ τ∈V ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv))))" (is "_ = (μ α. α∈M ∧ ?Q(ρp,α))") for ρp
unfolding f_def using Vset_abs Vset_closed Ord_Least_cong[of "?P(ρp)" "λ α. α∈M ∧ ?Q(ρp,α)"]
by (simp, simp del:setclass_iff)
moreover
have "f(ρp) ∈ M" for ρp
unfolding f_def using Least_closed[of "?P(ρp)"] by simp
ultimately
have 1:"least(##M,λα. ?Q(ρp,α),f(ρp))" for ρp
using least_abs[of "λα. α∈M ∧ ?Q(ρp,α)" "f(ρp)"] least_conj
by (simp flip: setclass_iff)
have "Ord(f(ρp))" for ρp unfolding f_def by simp
define QQ where "QQ≡?Q"
from 1
have "least(##M,λα. QQ(ρp,α),f(ρp))" for ρp
unfolding QQ_def .
from ‹arity(φ) ≤ _› ‹length(nenv) = _›
have "arity(φ) ≤ 2 #+ length(nenv)"
by simp
moreover
note assms ‹nenv∈list(M)› ‹?π∈M›
moreover
have "ρp∈?π ⟹ ∃t p. ρp=⟨t,p⟩" for ρp
by auto
ultimately
have body:"M , [α,ρp,m,P,leq,one] @ nenv ⊨ body_fm(φ,nenv) ⟷ ?Q(ρp,α)"
if "ρp∈?π" "ρp∈M" "m∈M" "α∈M" for α ρp m
using that P_in_M leq_in_M one_in_M body_lemma[of ρp α m nenv φ] by simp
let ?f_fm="least_fm(body_fm(φ,nenv),1)"
{
fix ρp m
assume asm: "ρp∈M" "ρp∈?π" "m∈M"
note inM = this P_in_M leq_in_M one_in_M ‹nenv∈list(M)›
with body
have body':"⋀α. α ∈ M ⟹ (∃τ∈M. ∃V∈M. is_Vset(λa. (##M)(a), α, V) ∧ τ ∈ V ∧
(snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv))) ⟷
M, Cons(α, [ρp, m, P, leq, one] @ nenv) ⊨ body_fm(φ,nenv)" by simp
from inM
have "M , [ρp,m,P,leq,one] @ nenv ⊨ ?f_fm ⟷ least(##M, QQ(ρp), m)"
using sats_least_fm[OF body', of 1] unfolding QQ_def
by (simp, simp flip: setclass_iff)
}
then
have "M, [ρp,m,P,leq,one] @ nenv ⊨ ?f_fm ⟷ least(##M, QQ(ρp), m)"
if "ρp∈M" "ρp∈?π" "m∈M" for ρp m using that by simp
then
have "univalent(##M, ?π, λρp m. M , [ρp,m] @ ([P,leq,one] @ nenv) ⊨ ?f_fm)"
unfolding univalent_def by (auto intro:unique_least)
moreover from ‹length(_) = _› ‹env ∈ _›
have "length([P,leq,one] @ nenv) = 3 #+ length(env)" by simp
moreover from ‹arity(_) ≤ 2 #+ length(nenv)›
‹length(_) = length(_)›[symmetric] ‹nenv∈_› ‹φ∈_›
have "arity(?f_fm) ≤ 5 #+ length(env)"
unfolding body_fm_def new_fm_defs least_fm_def
using arity_forces arity_renrep arity_renbody arity_body_fm' nonempty
by (simp add: pred_Un Un_assoc, simp add: Un_assoc[symmetric] nat_union_abs1 pred_Un)
(auto simp add: nat_simp_union, rule pred_le, auto intro:leI)
moreover from ‹φ∈formula› ‹nenv∈list(M)›
have "?f_fm∈formula" by simp
moreover
note inM = P_in_M leq_in_M one_in_M ‹nenv∈list(M)› ‹?π∈M›
ultimately
obtain Y where "Y∈M"
"∀m∈M. m ∈ Y ⟷ (∃ρp∈M. ρp ∈ ?π ∧ M, [ρp,m] @ ([P,leq,one] @ nenv) ⊨ ?f_fm)"
using replacement_ax[of ?f_fm "[P,leq,one] @ nenv"]
unfolding strong_replacement_def by auto
with ‹least(_,QQ(_),f(_))› ‹f(_) ∈ M› ‹?π∈M›
‹_ ⟹ _ ⟹ _ ⟹ M,_ ⊨ ?f_fm ⟷ least(_,_,_)›
have "f(ρp)∈Y" if "ρp∈?π" for ρp
using that transitivity[OF _ ‹?π∈M›]
by (clarsimp, rule_tac x="⟨x,y⟩" in bexI, auto)
moreover
have "{y∈Y. Ord(y)} ∈ M"
using ‹Y∈M› separation_ax sats_ordinal_fm trans_M
separation_cong[of "##M" "λy. sats(M,ordinal_fm(0),[y])" "Ord"]
separation_closed by simp
then
have "⋃ {y∈Y. Ord(y)} ∈ M" (is "?sup ∈ M")
using Union_closed by simp
then
have "{x∈Vset(?sup). x ∈ M} ∈ M"
using Vset_closed by simp
moreover
have "{one} ∈ M"
using one_in_M singletonM by simp
ultimately
have "{x∈Vset(?sup). x ∈ M} × {one} ∈ M" (is "?big_name ∈ M")
using cartprod_closed by simp
then
have "val(G,?big_name) ∈ M[G]"
by (blast intro:GenExtI)
{
fix v x
assume "x∈c"
moreover
note ‹val(G,π')=c› ‹π'∈M›
moreover
from calculation
obtain ρ p where "⟨ρ,p⟩∈π'" "val(G,ρ) = x" "p∈G" "ρ∈M"
using elem_of_val_pair'[of π' x G] by blast
moreover
assume "v∈M[G]"
then
obtain σ where "val(G,σ) = v" "σ∈M"
using GenExtD by auto
moreover
assume "sats(M[G], φ, [x,v] @ env)"
moreover
note ‹φ∈_› ‹nenv∈_› ‹env = _› ‹arity(φ)≤ 2 #+ length(env)›
ultimately
obtain q where "q∈G" "q ⊩ φ ([ρ,σ]@nenv)"
using truth_lemma[OF ‹φ∈_› generic, symmetric, of "[ρ,σ] @ nenv"]
by auto
with ‹⟨ρ,p⟩∈π'› ‹⟨ρ,q⟩∈?π ⟹ f(⟨ρ,q⟩)∈Y›
have "f(⟨ρ,q⟩)∈Y"
using generic unfolding M_generic_def filter_def by blast
let ?α="succ(rank(σ))"
note ‹σ∈M›
moreover from this
have "?α ∈ M"
using rank_closed cons_closed by (simp flip: setclass_iff)
moreover
have "σ ∈ Vset(?α)"
using Vset_Ord_rank_iff by auto
moreover
note ‹q ⊩ φ ([ρ,σ] @ nenv)›
ultimately
have "?P(⟨ρ,q⟩,?α)" by (auto simp del: Vset_rank_iff)
moreover
have "(μ α. ?P(⟨ρ,q⟩,α)) = f(⟨ρ,q⟩)"
unfolding f_def by simp
ultimately
obtain τ where "τ∈M" "τ ∈ Vset(f(⟨ρ,q⟩))" "q ⊩ φ ([ρ,τ] @ nenv)"
using LeastI[of "λ α. ?P(⟨ρ,q⟩,α)" ?α] by auto
with ‹q∈G› ‹ρ∈M› ‹nenv∈_› ‹arity(φ)≤ 2 #+ length(nenv)›
have "M[G], map(val(G),[ρ,τ] @ nenv) ⊨ φ"
using truth_lemma[OF ‹φ∈_› generic, of "[ρ,τ] @ nenv"] by auto
moreover from ‹x∈c› ‹c∈M[G]›
have "x∈M[G]" using transitivity_MG by simp
moreover
note ‹M[G],[x,v] @ env⊨ φ› ‹env = map(val(G),nenv)› ‹τ∈M› ‹val(G,ρ)=x›
‹univalent(##M[G],_,_)› ‹x∈c› ‹v∈M[G]›
ultimately
have "v=val(G,τ)"
using GenExtI[of τ G] unfolding univalent_def by (auto)
from ‹τ ∈ Vset(f(⟨ρ,q⟩))› ‹Ord(f(_))› ‹f(⟨ρ,q⟩)∈Y›
have "τ ∈ Vset(?sup)"
using Vset_Ord_rank_iff lt_Union_iff[of _ "rank(τ)"] by auto
with ‹τ∈M›
have "val(G,τ) ∈ val(G,?big_name)"
using domain_of_prod[of one "{one}" "{x∈Vset(?sup). x ∈ M}" ] def_val[of G ?big_name]
one_in_G[OF generic] one_in_P by (auto simp del: Vset_rank_iff)
with ‹v=val(G,τ)›
have "v ∈ val(G,{x∈Vset(?sup). x ∈ M} × {one})"
by simp
}
then
have "{v. x∈c, ?R(x,v)} ⊆ val(G,?big_name)" (is "?repl⊆?big")
by blast
with ‹?big_name∈M›
have "?repl = {v∈?big. ∃x∈c. sats(M[G], φ, [x,v] @ env )}" (is "_ = ?rhs")
proof(intro equalityI subsetI)
fix v
assume "v∈?repl"
with ‹?repl⊆?big›
obtain x where "x∈c" "M[G], [x, v] @ env ⊨ φ" "v∈?big"
using subsetD by auto
with ‹univalent(##M[G],_,_)› ‹c∈M[G]›
show "v ∈ ?rhs"
unfolding univalent_def
using transitivity_MG ReplaceI[of "λ x v. ∃x∈c. M[G], [x, v] @ env ⊨ φ"] by blast
next
fix v
assume "v∈?rhs"
then
obtain x where
"v∈val(G, ?big_name)" "M[G], [x, v] @ env ⊨ φ" "x∈c"
by blast
moreover from this ‹c∈M[G]›
have "v∈M[G]" "x∈M[G]"
using transitivity_MG GenExtI[OF ‹?big_name∈_›,of G] by auto
moreover from calculation ‹univalent(##M[G],_,_)›
have "?R(x,y) ⟹ y = v" for y
unfolding univalent_def by auto
ultimately
show "v∈?repl"
using ReplaceI[of ?R x v c]
by blast
qed
moreover
let ?ψ = "Exists(And(Member(0,2#+length(env)),φ))"
have "v∈M[G] ⟹ (∃x∈c. M[G], [x,v] @ env ⊨ φ) ⟷ M[G], [v] @ env @ [c] ⊨ ?ψ"
"arity(?ψ) ≤ 2 #+ length(env)" "?ψ∈formula"
for v
proof -
fix v
assume "v∈M[G]"
with ‹c∈M[G]›
have "nth(length(env)#+1,[v]@env@[c]) = c"
using ‹env∈_›nth_concat[of v c "M[G]" env]
by auto
note inMG= ‹nth(length(env)#+1,[v]@env@[c]) = c› ‹c∈M[G]› ‹v∈M[G]› ‹env∈_›
show "(∃x∈c. M[G], [x,v] @ env ⊨ φ) ⟷ M[G], [v] @ env @ [c] ⊨ ?ψ"
proof
assume "∃x∈c. M[G], [x, v] @ env ⊨ φ"
then obtain x where
"x∈c" "M[G], [x, v] @ env ⊨ φ" "x∈M[G]"
using transitivity_MG[OF _ ‹c∈M[G]›]
by auto
with ‹φ∈_› ‹arity(φ)≤2#+length(env)› inMG
show "M[G], [v] @ env @ [c] ⊨ Exists(And(Member(0, 2 #+ length(env)), φ))"
using arity_sats_iff[of φ "[c]" _ "[x,v]@env"]
by auto
next
assume "M[G], [v] @ env @ [c] ⊨ Exists(And(Member(0, 2 #+ length(env)), φ))"
with inMG
obtain x where
"x∈M[G]" "x∈c" "M[G], [x,v]@env@[c] ⊨ φ"
by auto
with ‹φ∈_› ‹arity(φ)≤2#+length(env)› inMG
show "∃x∈c. M[G], [x, v] @ env⊨ φ"
using arity_sats_iff[of φ "[c]" _ "[x,v]@env"]
by auto
qed
next
from ‹env∈_› ‹φ∈_›
show "arity(?ψ)≤2#+length(env)"
using pred_mono[OF _ ‹arity(φ)≤2#+length(env)›] lt_trans[OF _ le_refl]
by (auto simp add:nat_simp_union)
next
from ‹φ∈_›
show "?ψ∈formula" by simp
qed
moreover from this
have "{v∈?big. ∃x∈c. M[G], [x,v] @ env ⊨ φ} = {v∈?big. M[G], [v] @ env @ [c] ⊨ ?ψ}"
using transitivity_MG[OF _ GenExtI, OF _ ‹?big_name∈M›]
by simp
moreover from calculation and ‹env∈_› ‹c∈_› ‹?big∈M[G]›
have "{v∈?big. M[G] , [v] @ env @ [c] ⊨ ?ψ} ∈ M[G]"
using Collect_sats_in_MG by auto
ultimately
show ?thesis by simp
qed
theorem strong_replacement_in_MG:
assumes
"φ∈formula" and "arity(φ) ≤ 2 #+ length(env)" "env ∈ list(M[G])"
shows
"strong_replacement(##M[G],λx v. sats(M[G],φ,[x,v] @ env))"
proof -
let ?R="λx y . M[G], [x, y] @ env ⊨ φ"
{
fix A
let ?Y="{v . x ∈ A, v∈M[G] ∧ ?R(x,v)}"
assume 1: "(##M[G])(A)"
"∀x[##M[G]]. x ∈ A ⟶ (∀y[##M[G]]. ∀z[##M[G]]. ?R(x,y) ∧ ?R(x,z) ⟶ y = z)"
then
have "univalent(##M[G], A, ?R)" "A∈M[G]"
unfolding univalent_def by simp_all
with assms ‹A∈_›
have "(##M[G])(?Y)"
using Replace_sats_in_MG by auto
have "b ∈ ?Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b))" if "(##M[G])(b)" for b
proof(rule)
from ‹A∈_›
show "∃x[##M[G]]. x ∈ A ∧ ?R(x,b)" if "b ∈ ?Y"
using that transitivity_MG by auto
next
show "b ∈ ?Y" if "∃x[##M[G]]. x ∈ A ∧ ?R(x,b)"
proof -
from ‹(##M[G])(b)›
have "b∈M[G]" by simp
with that
obtain x where "(##M[G])(x)" "x∈A" "b∈M[G] ∧ ?R(x,b)"
by blast
moreover from this 1 ‹(##M[G])(b)›
have "x∈M[G]" "z∈M[G] ∧ ?R(x,z) ⟹ b = z" for z
by auto
ultimately
show ?thesis
using ReplaceI[of "λ x y. y∈M[G] ∧ ?R(x,y)"] by auto
qed
qed
then
have "∀b[##M[G]]. b ∈ ?Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b))"
by simp
with ‹(##M[G])(?Y)›
have " (∃Y[##M[G]]. ∀b[##M[G]]. b ∈ Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b)))"
by auto
}
then show ?thesis unfolding strong_replacement_def univalent_def
by auto
qed
end
end