Theory Replacement_Axiom

sectionThe 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. VM. 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 ― ‹localeforcing_data1

context G_generic1
begin

lemma Replace_sats_in_MG:
  assumes
    "cM[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. xc, vM[G]  (M[G] , [x,v]@env  φ)}  M[G]"
proof -
  let ?R = "λ x v . vM[G]  (M[G] , [x,v]@env  φ)"
  from cM[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 "nenvlist(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. VM. 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 = nenvlist(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 "ρpM" "ρp" "mM" 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. VM. is_Vset(λa. aM, α, 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 "YM"
    "mM. m  Y  (ρpM. ρ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 YM
  have " {yY. Ord(y)}  M" (is "?sup  M")
    using separation_Ord separation_closed Union_closed by simp
  then
  have "{xVset(?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. xc, ?R(x,v)}  val(G,?big_name)" (is "?repl?big")
  proof(intro subsetI)
    fix v
    assume "v?repl"
    moreover from this
    obtain x where "xc" "M[G], [x, v] @ env  φ" "vM[G]"
      by auto
    moreover
    note val(G,π')=c π'M
    moreover
    from calculation
    obtain ρ p where "ρ,pπ'" "val(G,ρ) = x" "pG" "ρM"
      using elem_of_val_pair' by blast
    moreover from this vM[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 "qG" "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 qG ρM nenv_ arity(φ) 2 +ω length(nenv)
    have "M[G], map(val(G),[ρ,τ] @ nenv)  φ"
      using truth_lemma[OF φ_, of "[ρ,τ] @ nenv"] by auto
    moreover from xc cM[G]
    have "xM[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],_,_) xc vM[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 𝟭 "{𝟭}" "{xVset(?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_nameM
  have "?repl = {v?big. xc. M[G], [x,v] @ env   φ}" (is "_ = ?rhs")
  proof(intro equalityI subsetI)
    fix v
    assume "v?repl"
    with ?repl?big
    obtain x where "xc" "M[G], [x, v] @ env  φ" "v?big"
      using subsetD by auto
    with univalent(##M[G],_,_) cM[G]
    show "v  ?rhs"
      unfolding univalent_def
      using transitivity_MG ReplaceI[of "λ x v. xc. M[G], [x, v] @ env  φ"] by blast
  next
    fix v
    assume "v?rhs"
    then
    obtain x where
      "vval(G, ?big_name)" "M[G], [x, v] @ env  φ" "xc"
      by blast
    moreover from this cM[G]
    have "vM[G]" "xM[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) cM[G] env_
  have "(xc. M[G], [x,v] @ env  φ)  M[G], [v] @ env @ [c]  " if "vM[G]" for v
    using that nth_concat transitivity_MG[OF _ cM[G]] arity_sats_iff[of φ "[c]" _ "[_,v]@env"]
    by auto
  moreover from this
  have "{v?big. xc. M[G], [x,v] @ env  φ} = {v?big. M[G], [v] @ env @ [c]   }"
    using transitivity_MG[OF _ GenExtI, OF _ ?big_nameM]
    by simp
  moreover from calculation and env_ c_ ?bigM[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, vM[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 "bM[G]" by simp
        with that
        obtain x where "(##M[G])(x)" "xA" "bM[G]  ?R(x,b)"
          by blast
        moreover from this 1 (##M[G])(b)
        have "xM[G]" "zM[G]  ?R(x,z)  b = z" for z
          unfolding univalent_def
          by auto
        ultimately
        show ?thesis
          using ReplaceI[of "λ x y. yM[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 ― ‹localeG_generic1

end