Theory Separation_Axiom

section‹The Axiom of Separation in $M[G]$›
theory Separation_Axiom
  imports Forcing_Theorems Separation_Rename
begin

context G_generic1
begin

lemma map_val :
  assumes "envlist(M[G])"
  shows "nenvlist(M). env = map(val(G),nenv)"
  using assms
proof(induct env)
  case Nil
  have "map(val(G),Nil) = Nil" by simp
  then show ?case by force
next
  case (Cons a l)
  then obtain a' l' where
    "l'  list(M)" "l=map(val(G),l')" "a = val(G,a')"
    "Cons(a,l) = map(val(G),Cons(a',l'))" "Cons(a',l')  list(M)"
    using GenExtD
    by force
  then show ?case by force
qed

lemma Collect_sats_in_MG :
  assumes
    "AM[G]"
    "φ  formula" "envlist(M[G])" "arity(φ)  1 +ω length(env)"
  shows
    "{x  A . (M[G], [x] @ env  φ)}  M[G]"
proof -
  from AM[G]
  obtain π where "π  M" "val(G, π) = A"
    using GenExt_def by auto
  then
  have "domain(π)M" "domain(π) ×   M"
    using cartprod_closed[of _ ,simplified]
    by (simp_all flip:setclass_iff)
  let =" 0  (1 +ω length(env))   φ "
  let ?new_form="sep_ren(length(env),forces())"
  let ="(⋅∃(⋅∃⋅⟨0,1 is 2   ?new_form  ⋅)⋅)"
  note phi = φformula arity(φ)  1 +ω length(env)
  then
  have "formula" "forces()  formula" "arity(φ)  2+ω length(env)"
    using definability le_trans[OF arity(φ)_] add_le_mono[of 1 2,OF _ le_refl]
    by simp_all
  with env_ phi
  have "arity()  2+ωlength(env)"
    using ord_simp_union leI FOL_arities by simp
  with envlist(_) phi
  have "arity(forces())  6 +ω length(env)"
    using  arity_forces_le by simp
  then
  have "arity(forces())  7 +ω length(env)"
    using ord_simp_union arity_forces leI by simp
  with arity(forces()) 7 +ω _ env  _ φ  formula
  have "arity(?new_form)  7 +ω length(env)" "?new_form  formula" "formula"
    using arity_rensep[OF definability[of ""]]
    by auto
  then
  have "arity()  5 +ω length(env)"
    using ord_simp_union arity_forces pred_mono[OF _ pred_mono[OF _ arity(?new_form)  _]]
    by (auto simp:arity)
  from env  _
  obtain nenv where "nenvlist(M)" "env = map(val(G),nenv)" "length(nenv) = length(env)"
    using map_val by auto
  from phi nenv_ env_ πM φ_ length(nenv) = length(env)
  have "arity()  length([θ] @ nenv @ [π])" for θ
    using union_abs2[OF arity(φ)  2+ω _] ord_simp_union FOL_arities
    by simp
  note in_M = πM domain(π) ×   M
  have Equivalence: "
       (M, [u,,leq,𝟭,π] @ nenv  ) 
         (θM. p. u =θ,p 
          (F. M_generic(F)  p  F  M[F],  map(val(F), [θ] @ nenv @[π])   ))"
    if "u  domain(π) × "
    for u
  proof -
    from u  domain(π) ×  domain(π) ×   M
    have "uM" by (simp add:transitivity)
    have "(M, [θ,p,u,,leq,𝟭,π]@nenv  ?new_form) 
          (F. M_generic(F)  p  F  (M[F],  map(val(F), [θ] @ nenv@[π])   ))"
      if "θM" "p"
      for θ p
    proof -
      from p
      have "pM" by (simp add: transitivity)
      let ?env="[p,,leq,𝟭,θ] @ nenv @ [π,u]"
      let ?new_env=" [θ,p,u,,leq,𝟭,π] @ nenv"
      note types = in_M θ  M pM u  domain(π) ×  u  M nenv_
      then
      have tyenv:"?env  list(M)" "?new_env  list(M)"
        by simp_all
      from types
      have eq_env:"[p, , leq, 𝟭] @ ([θ] @ nenv @ [π,u]) = 
                  ([p, , leq, 𝟭] @ ([θ] @ nenv @ [π])) @ [u]"
        using app_assoc by simp
      then
      have "(M, [θ,p,u,,leq,𝟭,π] @ nenv  ?new_form)  (M, ?new_env  ?new_form)"
        by simp
      from tyenv length(nenv) = length(env) arity(forces())  7 +ω length(env) forces()  formula
      have "...  p   ([θ] @ nenv @ [π,u])"
        using sepren_action[of "forces()"  "nenv",OF _ _ nenvlist(M)]
        by simp
      also from types phi env_ length(nenv) = length(env) arity(forces())  6 +ω length(env)
      have "...  p    ([θ] @ nenv @ [π])"
        by (subst eq_env,rule_tac arity_sats_iff,auto)
      also from types phi p arity(forces())  6 +ω length(env) arity()  length([θ] @ nenv @ [π])
      have " ...  (F . M_generic(F)  p  F 
                           M[F],  map(val(F), [θ] @ nenv @ [π])   )"
        using definition_of_forcing[where φ=" 0  (1 +ω length(env))   φ "]
        by auto
      finally
      show ?thesis
        by simp
    qed
    with in_M ?new_form  formula formula nenv  _ u  domain(π)×
    show ?thesis
      by (auto simp add: transitivity)
  qed
  moreover from env = _ πM nenvlist(M)
  have map_nenv:"map(val(G), nenv @ [π]) = env @ [val(G,π)]"
    using map_app_distrib append1_eq_iff by auto
  ultimately
  have aux:"(θM. p. u =θ,p  (pG  M[G], [val(G,θ)] @ env @ [val(G,π)]  ))"
    (is "(θM. p. _ ( _  M[G] , ?vals(θ)  _))")
    if "u  domain(π) × " "M, [u,,leq,𝟭,π] @ nenv  " for u
    using Equivalence[THEN iffD1, OF that] generic by force
  moreover
  have "[val(G, θ)] @ env @ [val(G, π)]  list(M[G])" if "θM" for θ
    using πM env  list(M[G]) GenExtI that by force
  ultimately
  have "(θM. p. u=θ,p  (pG  val(G,θ)nth(1 +ω length(env),[val(G, θ)] @ env @ [val(G, π)])
         (M[G], ?vals(θ)  φ)))"
    if "u  domain(π) × " "M, [u,,leq,𝟭,π] @ nenv  " for u
    using aux[OF that] by simp
  moreover from env  _ πM
  have nth:"nth(1 +ω length(env),[val(G, θ)] @ env @ [val(G, π)]) = val(G,π)"
    if "θM" for θ
    using nth_concat[of "val(G,θ)" "val(G,π)" "M[G]"] that GenExtI by simp
  ultimately
  have "(θM. p. u=θ,p  (pG  val(G,θ)val(G,π)  (M[G],?vals(θ)   φ)))"
    if "u  domain(π) × " "M, [u,,leq,𝟭,π] @ nenv  " for u
    using that πM env  _ by simp
  with domain(π)×M
  have "udomain(π)× . (M, [u,,leq,𝟭,π] @ nenv  )  (θM. p. u =θ,p 
        (p  G  val(G, θ)val(G, π)  (M[G],?vals(θ)   φ)))"
    by (simp add:transitivity)
  then
  have "{udomain(π)× . (M,[u,,leq,𝟭,π] @ nenv  ) } 
     {udomain(π)× . θM. p. u =θ,p 
       (p  G  val(G, θ)val(G, π)  (M[G], ?vals(θ)  φ))}"
    (is "?n?m")
    by auto
  then
  have first_incl: "val(G,?n)  val(G,?m)"
    using val_mono by simp
  note  val(G,π) = A (* from the assumptions *)
  with formula  arity()  _ in_M nenv  _ env  _ length(nenv) = _
  have "?nM"
    using separation_ax leI separation_iff by auto
  from generic
  have "filter(G)" "G"
    by auto
  from val(G,π) = A
  have "val(G,?m) =
               {z . tdomain(π) , (q .
                    (θM. p. t,q = θ, p 
            (p  G  val(G, θ)  A  (M[G],  [val(G, θ)] @ env @ [A]   φ))  q  G)) 
           z=val(G,t)}"
    using val_of_name by auto
  also
  have "... =  {z . tdomain(π) , (q.
                   val(G, t)  A  (M[G],  [val(G, t)] @ env @ [A]   φ)  q  G)  z=val(G,t)}"
    using domain(π)M by (auto simp add:transitivity)
  also
  have "... =  {xA . q. x  A  (M[G],  [x] @ env @ [A]   φ)  q  G}"
  proof(intro equalityI, auto)
    (* Now we show the other inclusion:
      {x .. x ∈ A , ∃q∈ℙ. x ∈ A ∧ (M[G],  [x, w, c] ⊨  φ) ∧ q ∈ G}
      ⊆
      {val(G,t)..t∈domain(π),∃q∈ℙ.val(G,t)∈ A∧(M[G], [val(G,t),w] ⊨ φ)∧q∈G}
    *)
    {
      fix x q
      assume "M[G], Cons(x, env @ [A])  φ" "xA" "q  " "q  G"
      from this val(G,π) = A
      show "x  {y . x  domain(π), val(G, x)  A  (M[G], Cons(val(G, x), env @ [A])  φ)  (q. q  G)  y = val(G, x)}"
        using elem_of_val by force
    }
  qed
  also
  have " ... = {x  A. (M[G], [x] @ env @ [A]  φ)}"
    using G G_nonempty by force
  finally
  have val_m: "val(G,?m) = {x  A. (M[G], [x] @ env @ [A]  φ)}" by simp
  have "val(G,?m)  val(G,?n)"
  proof
    fix x
    assume "x  val(G,?m)"
    with val_m
    have "x  {x  A. (M[G], [x] @ env @ [A]  φ)}" by simp
    with val(G,π) = A
    have "x  val(G,π)" by simp
    then
    obtain θ q where "θ,qπ" "qG" "val(G,θ)=x" "θM"
      using elem_of_val_pair domain_trans[OF trans_M π_]
      by force
    with πM nenv  _ env = _
    have "[val(G,θ), val(G,π)] @ env  list(M[G])" "[θ] @ nenv @ [π]list(M)"
      using GenExt_def by auto
    with val(G,θ)=x val(G,π) = A x  val(G,π) nth θM x {x  A . _}
    have "M[G],  [val(G,θ)] @ env @ [val(G,π)]   0  (1 +ω length(env))   φ "
      by auto
        ― ‹Recall term = And(Member(0,1 +ω length(env)),φ)
    with [_] @ nenv @ [_]  _ map_nenv arity()  length(_) length(nenv) = _
    obtain r where "rG" "r   ([θ] @ nenv @ [π])"
      using truth_lemma[OF _,of "[θ] @ nenv @ [π]"]
      by auto
    with filter(G) and qG
    obtain p where "pG" "pq" "pr"
      unfolding filter_def compat_in_def by force
    with rG qG G
    have "p" "r" "q" "pM"
      using transitivity[OF _ P_in_M] subsetD
      by simp_all
    with φformula θM πM pr nenv  _ arity()  length(_) r   _ env_
    have "p   ([θ] @ nenv @ [π])"
      using strengthening_lemma
      by simp
    with p φformula θM πM nenv  _ arity()  length(_)
    have "F. M_generic(F)  p  F 
                 M[F],   map(val(F), [θ] @ nenv @ [π])   "
      using definition_of_forcing[where φ=" 0  (1 +ω length(env))   φ "]
      by simp
    with p θM
    have Eq6: "θ'M. p'.  θ,p = θ',p'  (F. M_generic(F)  p'  F 
                 M[F],   map(val(F), [θ'] @ nenv @ [π])   )" by auto
    from πM θ,qπ θM p pM
    have "θ,q  M" "θ,pM" "θ,pdomain(π)×"
      using pair_in_M_iff transitivity
      by auto
    with θM Eq6 p
    have "M, [θ,p,,leq,𝟭,π] @ nenv  "
      using Equivalence by auto
    with θ,pdomain(π)×
    have "θ,p?n" by simp
    with pG p
    have "val(G,θ)val(G,?n)"
      using val_of_elem[of θ p] by simp
    with val(G,θ)=x
    show "xval(G,?n)" by simp
  qed (* proof of "val(G,?m) ⊆ val(G,?n)" *)
  with val_m first_incl
  have "val(G,?n) = {x  A. (M[G], [x] @ env @ [A]  φ)}" by auto
  also from A_ phi env  _
  have " ... = {x  A. (M[G], [x] @ env  φ)}"
    using arity_sats_iff[where env="[_]@env"] transitivity_MG
    by auto
  finally
  show "{x  A. (M[G], [x] @ env  φ)} M[G]"
    using ?nM GenExt_def by force
qed

theorem separation_in_MG:
  assumes
    "φformula" and "arity(φ)  1 +ω length(env)" and "envlist(M[G])"
  shows
    "separation(##M[G],λx. (M[G], [x] @ env  φ))"
proof -
  {
    fix A
    assume "AM[G]"
    moreover from env  _
    obtain nenv where "nenvlist(M)""env = map(val(G),nenv)" "length(env) = length(nenv)"
      using GenExt_def map_val[of env] by auto
    moreover note φ  _ arity(φ)  _ env  _
    ultimately
    have "{x  A . (M[G], [x] @ env  φ)}  M[G]"
      using Collect_sats_in_MG by auto
  }
  then
  show ?thesis
    using separation_iff rev_bexI unfolding is_Collect_def by force
qed

end ― ‹localeG_generic1

end