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 :
"arity(φ) ≤ 6 #+ length(env) ⟹
[P,leq,o,p,ρ,τ] @ env ∈ list(M) ⟹
V ∈ M ⟹ α ∈ M ⟹
φ∈formula ⟹
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
apply (rule sats_iff_sats_ren,auto simp add:renrep1_thm(1)[of _ M,simplified])
apply (auto simp add: renrep1_thm(2)[simplified,of p M P leq o ρ τ V α _ env])
done
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
apply (rule sats_iff_sats_ren,auto simp add:renpbdy1_thm(1)[of _ M,simplified])
apply (auto simp add: renpbdy1_thm(2)[simplified,of ρ M p α P leq o x _ nenv])
done
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
apply (rule sats_iff_sats_ren,auto simp add:renbody1_thm(1)[of _ M,simplified])
apply (simp add: renbody1_thm(2)[of x α P leq o m M _ nenv,simplified])
done
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 "prebody_fm" from_schematic "sats_prebody_fm_auto"
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 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
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 arity_forces_le[OF _ _ ‹arity(φ) ≤ _›,simplified]
apply(simp add: new_fm_defs )
apply(simp add: nat_simp_union,rule, rule, (rule pred_le,simp+)+)
apply(subgoal_tac "arity(forces(φ)) ≤ 6 #+length(env)")
apply(subgoal_tac "forces(φ)∈ formula")
apply(drule arity_renrep[of "forces(φ)"], auto)
done
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
apply(simp add: new_fm_defs )
apply(simp add: nat_simp_union)
apply( rule, (rule pred_le,simp+)+)
apply(frule arity_prebody_fm,auto)
apply(subgoal_tac "prebody_fm(φ,env)∈formula")
apply(frule arity_renpbdy[of "prebody_fm(φ,env)"],auto)
done
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 -
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:"sats(M,body_fm(φ,nenv),[α,ρp,m,P,leq,one] @ 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))) ⟷
sats(M, body_fm(φ,nenv), Cons(α, [ρp, m, P, leq, one] @ nenv))" by simp
from inM
have "sats(M, ?f_fm,[ρp,m,P,leq,one] @ nenv) ⟷ least(##M, QQ(ρp), m)"
using sats_least_fm[OF body', of 1] unfolding QQ_def
by (simp, simp flip: setclass_iff)
}
then
have "sats(M, ?f_fm,[ρp,m,P,leq,one] @ nenv) ⟷ least(##M, QQ(ρp), m)"
if "ρp∈M" "ρp∈?π" "m∈M" for ρp m using that by simp
then
have "univalent(##M, ?π, λρp m. sats(M, ?f_fm, [ρp,m] @ ([P,leq,one] @ nenv)))"
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 ∈ ?π ∧
sats(M, ?f_fm, [ρp,m] @ ([P,leq,one] @ nenv)))"
using replacement_ax[of ?f_fm "[P,leq,one] @ nenv"]
unfolding strong_replacement_def by auto
with ‹least(_,QQ(_),f(_))› ‹f(_) ∈ M› ‹?π∈M›
‹_ ⟹ _ ⟹ _ ⟹ sats(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 "sats(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 ‹sats(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, v∈M[G]∧sats(M[G],φ,[x,v]@env)} ⊆ 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 )}"
apply (intro equality_iffI, subst Replace_iff)
apply (auto intro:transitivity_MG[OF _ GenExtI])
using ‹univalent(##M[G],_,_)› unfolding univalent_def
apply (rule_tac x=xa in bexI; simp)
apply (frule transitivity_MG[OF _ ‹c∈M[G]›])
apply (drule bspec, assumption, drule mp, assumption, clarify)
apply (drule_tac x=y in bspec, assumption)
by (drule_tac y=x in transitivity_MG[OF _ GenExtI], auto)
moreover
let ?ψ = "Exists(And(Member(0,2#+length(env)),φ))"
have "v∈M[G] ⟹ (∃x∈c. sats(M[G], φ, [x,v] @ env)) ⟷ sats(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. sats(M[G], φ, [x,v] @ env)) ⟷ sats(M[G], ?ψ, [v] @ env @ [c])"
proof
assume "∃x∈c. sats(M[G], φ, [x, v] @ env)"
with ‹c∈M[G]› obtain x where
"x∈c" "sats(M[G], φ, [x, v] @ env)" "x∈M[G]"
using transitivity_MG[OF _ ‹c∈M[G]›]
by auto
with ‹φ∈_› ‹arity(φ)≤2#+length(env)› inMG
show "sats(M[G], Exists(And(Member(0, 2 #+ length(env)), φ)), [v] @ env @ [c])"
using arity_sats_iff[of φ "[c]" _ "[x,v]@env"]
by auto
next
assume "sats(M[G], Exists(And(Member(0, 2 #+ length(env)), φ)), [v] @ env @ [c])"
with inMG
obtain x where
"x∈M[G]" "x∈c" "sats(M[G],φ,[x,v]@env@[c])"
by auto
with ‹φ∈_› ‹arity(φ)≤2#+length(env)› inMG
show "∃x∈c. sats(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. sats(M[G], φ, [x,v] @ env)} = {v∈?big. sats(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. sats(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 -
from assms
have "{v . x ∈ c, v ∈ M[G] ∧ sats(M[G], φ, [x,v] @ env)} ∈ M[G]"
if "c ∈ M[G]" "univalent(##M[G], c, λx v. sats(M[G], φ, [x, v] @ env))" for c
using that Replace_sats_in_MG by auto
then
show ?thesis
unfolding strong_replacement_def univalent_def using transitivity_MG
apply (intro ballI rallI impI)
apply (rule_tac x="{v . x ∈ A, v∈M[G] ∧ sats(M[G], φ, [x, v] @ env)}" in rexI)
apply (auto)
apply (drule_tac x=x in bspec; simp_all)
by (blast)
qed
end
end