section‹The Axiom of Replacement in $M[G]$› theory Replacement_Axiom imports Separation_Axiom begin context forcing_data1 begin bundle sharp_simps1 = snd_abs[simp] fst_abs[simp] fst_closed[simp del, simplified, simp] snd_closed[simp del, simplified, simp] M_inhabited[simplified, simp] pair_in_M_iff[simp del, simplified, simp] lemma sats_body_ground_repl_fm: includes sharp_simps1 assumes "∃t p. x=⟨t,p⟩" "[x,α,m,ℙ,leq,𝟭] @ nenv ∈list(M)" "φ∈formula" shows "(∃τ∈M. ∃V∈M. is_Vset(λa. (##M)(a),α,V) ∧ τ ∈ V ∧ (snd(x) ⊩ φ ([fst(x),τ]@nenv))) ⟷ M, [α, x, m, ℙ, leq, 𝟭] @ nenv ⊨ body_ground_repl_fm(φ)" unfolding body_ground_repl_fm_def rename_split_fm_def by ((insert assms,rule iff_sats | simp add:nonempty[simplified])+, insert sats_incr_bv_iff[where bvs="[_,_,_,_,_,_]", simplified],auto del: iffI) end ― ‹\<^locale>‹forcing_data1›› context G_generic1 begin 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 ⊨ φ) )" and ground_replacement: "⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)" 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(π')×ℙ∈M" (is "?π∈M") using cartprod_closed domain_closed by simp from ‹val(G, π') = c› have "c ⊆ val(G,?π)" using def_val[of G ?π] elem_of_val[of _ G π'] one_in_G domain_of_prod[OF one_in_P, of "domain(π')"] by (force del:M_genericD) 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 with ‹arity(φ) ≤ _› have "arity(φ) ≤ 2 +⇩_{ω}length(nenv)" 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 note inM = ‹nenv∈list(M)› ‹?π∈M› moreover have "f(ρp) ∈ M" "Ord(f(ρp))" for ρp unfolding f_def using Least_closed'[of "?P(ρp)"] by simp_all 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) define QQ where "QQ≡?Q" from 1 have "least(##M,λα. QQ(ρp,α),f(ρp))" for ρp unfolding QQ_def . have body:"(M, [ρp,m,ℙ,leq,𝟭] @ nenv ⊨ ground_repl_fm(φ)) ⟷ least(##M, QQ(ρp), m)" if "ρp∈M" "ρp∈?π" "m∈M" for ρp m proof - note inM that moreover from this assms 1 have "(M , [α,ρp,m,ℙ,leq,𝟭] @ nenv ⊨ body_ground_repl_fm(φ)) ⟷ ?Q(ρp,α)" if "α∈M" for α using that sats_body_ground_repl_fm[of ρp α m nenv φ] by auto moreover from calculation have body:"⋀α. α ∈ M ⟹ (∃τ∈M. ∃V∈M. is_Vset(λa. a∈M, α, V) ∧ τ ∈ V ∧ (snd(ρp) ⊩ φ ([fst(ρp),τ] @ nenv))) ⟷ M, Cons(α, [ρp, m, ℙ, leq, 𝟭] @ nenv) ⊨ body_ground_repl_fm(φ)" by simp ultimately show "(M , [ρp,m,ℙ,leq,𝟭] @ nenv ⊨ ground_repl_fm(φ)) ⟷ least(##M, QQ(ρp), m)" using sats_least_fm[OF body,of 1] unfolding QQ_def ground_repl_fm_def by (simp, simp flip: setclass_iff) qed then have "univalent(##M, ?π, λρp m. M , [ρp,m] @ ([ℙ,leq,𝟭] @ nenv) ⊨ ground_repl_fm(φ))" unfolding univalent_def by (auto intro:unique_least) moreover from ‹length(_) = _› ‹env ∈ _› have "length([ℙ,leq,𝟭] @ nenv) = 3 +⇩_{ω}length(env)" by simp moreover from ‹arity(φ) ≤ 2 +⇩_{ω}length(nenv)› ‹length(_) = length(_)›[symmetric] ‹nenv∈_› ‹φ∈_› have "arity(ground_repl_fm(φ)) ≤ 5 +⇩_{ω}length(env)" using arity_ground_repl_fm[of φ] le_trans Un_le by auto moreover from ‹φ∈formula› have "ground_repl_fm(φ)∈formula" by simp moreover note ‹length(nenv) = length(env)› inM ultimately obtain Y where "Y∈M" "∀m∈M. m ∈ Y ⟷ (∃ρp∈M. ρp ∈ ?π ∧ (M, [ρp,m] @ ([ℙ,leq,𝟭] @ nenv) ⊨ ground_repl_fm(φ)))" using ground_replacement[of nenv] unfolding strong_replacement_def ground_replacement_assm_def replacement_assm_def by auto with ‹least(_,QQ(_),f(_))› ‹f(_) ∈ M› ‹?π∈M› body have "f(ρp)∈Y" if "ρp∈?π" for ρp using that transitivity[OF _ ‹?π∈M›] by (clarsimp,rename_tac ρ p ρp, rule_tac x="⟨ρ,p⟩" in bexI, auto) from ‹Y∈M› have "⋃ {y∈Y. Ord(y)} ∈ M" (is "?sup ∈ M") using separation_Ord separation_closed Union_closed by simp then have "{x∈Vset(?sup). x ∈ M} × {𝟭} ∈ M" (is "?big_name ∈ M") using Vset_closed cartprod_closed singleton_closed by simp then have "val(G,?big_name) ∈ M[G]" by (blast intro:GenExtI) have "{v. x∈c, ?R(x,v)} ⊆ val(G,?big_name)" (is "?repl⊆?big") proof(intro subsetI) fix v assume "v∈?repl" moreover from this obtain x where "x∈c" "M[G], [x, v] @ env ⊨ φ" "v∈M[G]" by auto moreover note ‹val(G,π')=c› ‹π'∈M› moreover from calculation obtain ρ p where "⟨ρ,p⟩∈π'" "val(G,ρ) = x" "p∈G" "ρ∈M" using elem_of_val_pair' by blast moreover from this ‹v∈M[G]› obtain σ where "val(G,σ) = v" "σ∈M" using GenExtD by (force del:M_genericD) moreover note ‹φ∈_› ‹nenv∈_› ‹env = _› ‹arity(φ)≤ 2 +⇩_{ω}length(env)› ultimately obtain q where "q∈G" "q ⊩ φ ([ρ,σ]@nenv)" "q∈ℙ" using truth_lemma[OF ‹φ∈_›,of "[ρ,σ] @ nenv"] by auto with ‹⟨ρ,p⟩∈π'› ‹⟨ρ,q⟩∈?π ⟹ f(⟨ρ,q⟩)∈Y› have "f(⟨ρ,q⟩)∈Y" using generic by blast let ?α="succ(rank(σ))" note ‹σ∈M› moreover from this have "?α ∈ M" "σ ∈ Vset(?α)" using rank_closed cons_closed Vset_Ord_rank_iff by (simp_all flip: setclass_iff) 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 ‹φ∈_›, 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 𝟭 "{𝟭}" "{x∈Vset(?sup). x ∈ M}" ] def_val[of G ?big_name] one_in_G one_in_P by (auto simp del: Vset_rank_iff) with ‹v=val(G,τ)› show "v ∈ val(G,?big_name)" by simp qed from ‹?big_name∈M› have "?repl = {v∈?big. ∃x∈c. 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 ?ψ = "(⋅∃⋅⋅0 ∈ 2 +⇩_{ω}length(env) ⋅ ∧ φ⋅⋅)" from ‹φ∈_› have "?ψ∈formula" "arity(?ψ) ≤ 2 +⇩_{ω}length(env)" using pred_mono[OF _ ‹arity(φ)≤2+⇩_{ω}length(env)›] lt_trans[OF _ le_refl] by (auto simp add:ord_simp_union arity) moreover from ‹φ∈_› ‹arity(φ)≤2+⇩_{ω}length(env)› ‹c∈M[G]› ‹env∈_› have "(∃x∈c. M[G], [x,v] @ env ⊨ φ) ⟷ M[G], [v] @ env @ [c] ⊨ ?ψ" if "v∈M[G]" for v using that nth_concat transitivity_MG[OF _ ‹c∈M[G]›] arity_sats_iff[of φ "[c]" _ "[_,v]@env"] by auto 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])" and ground_replacement: "⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)" shows "strong_replacement(##M[G],λx v. 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)" "univalent(##M[G], A, ?R)" with assms have "(##M[G])(?Y)" using Replace_sats_in_MG ground_replacement 1 unfolding ground_replacement_assm_def by auto have "b ∈ ?Y ⟷ (∃x[##M[G]]. x ∈ A ∧ ?R(x,b))" if "(##M[G])(b)" for b proof(rule) from ‹(##M[G])(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 unfolding univalent_def by auto ultimately show ?thesis using ReplaceI[of "λ x y. y∈M[G] ∧ ?R(x,y)"] by blast 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 by simp qed lemma replacement_assm_MG: assumes ground_replacement: "⋀nenv. ground_replacement_assm(M,[ℙ,leq,𝟭] @ nenv, φ)" shows "replacement_assm(M[G],env,φ)" using assms strong_replacement_in_MG unfolding replacement_assm_def by simp end ― ‹\<^locale>‹G_generic1›› end