Theory Separation_Axiom

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

context G_generic
begin

lemma map_val :
  assumes "env∈list(M[G])"
  shows "∃nenv∈list(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 ‹a∈M[G]› GenExtD
      by force
    then show ?case by force
qed


lemma Collect_sats_in_MG :
  assumes
    "c∈M[G]"
    "φ ∈ formula" "env∈list(M[G])" "arity(φ) ≤ 1 #+ length(env)"
  shows    
    "{x∈c. (M[G], [x] @ env ⊨ φ)}∈ M[G]"
proof -  
  from ‹c∈M[G]›
  obtain π where "π ∈ M" "val(G, π) = c"
    using GenExt_def by auto
  let ?χ="And(Member(0,1 #+ length(env)),φ)" and ?Pl1="[P,leq,one]"
  let ?new_form="sep_ren(length(env),forces(?χ))"
  let ?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
  note phi = ‹φ∈formula› ‹arity(φ) ≤ 1 #+ length(env)› 
  then
  have "?χ∈formula" by simp
  with ‹env∈_› phi
  have "arity(?χ) ≤ 2#+length(env) " 
    using nat_simp_union leI by simp
  with ‹env∈list(_)› phi
  have "arity(forces(?χ)) ≤ 6 #+ length(env)"
    using  arity_forces_le by simp
  then
  have "arity(forces(?χ)) ≤ 7 #+ length(env)"
    using nat_simp_union arity_forces leI by simp
  with ‹arity(forces(?χ)) ≤7 #+ _› ‹env ∈ _› ‹φ ∈ formula›
  have "arity(?new_form) ≤ 7 #+ length(env)" "?new_form ∈ formula"
    using arity_rensep[OF definability[of "?χ"]]  definability[of "?χ"] type_rensep 
    by auto
  then
  have "pred(pred(arity(?new_form))) ≤ 5 #+ length(env)" "?ψ∈formula"
    unfolding pair_fm_def upair_fm_def 
    using nat_simp_union length_type[OF ‹env∈list(M[G])›] 
        pred_mono[OF _ pred_mono[OF _ ‹arity(?new_form) ≤ _›]]
    by auto
  with ‹arity(?new_form) ≤ _› ‹?new_form ∈ formula›
  have "arity(?ψ) ≤ 5 #+ length(env)"
    unfolding pair_fm_def upair_fm_def 
    using nat_simp_union arity_forces
    by auto
  from ‹φ∈formula›
  have "forces(?χ) ∈ formula"
    using definability by simp
  from ‹π∈M› P_in_M 
  have "domain(π)∈M" "domain(π) × P ∈ M"
    by (simp_all flip:setclass_iff)
  from ‹env ∈ _›
  obtain nenv where "nenv∈list(M)" "env = map(val(G),nenv)" "length(nenv) = length(env)"
    using map_val by auto
  from ‹arity(φ) ≤ _› ‹env∈_› ‹φ∈_›
  have "arity(φ) ≤ 2#+ length(env)" 
    using le_trans[OF ‹arity(φ)≤_›] add_le_mono[of 1 2,OF _ le_refl] 
    by auto
  with ‹nenv∈_› ‹env∈_› ‹π∈M› ‹φ∈_› ‹length(nenv) = length(env)›
  have "arity(?χ) ≤ length([θ] @ nenv @ [π])" for θ 
    using nat_union_abs2[OF _ _ ‹arity(φ) ≤ 2#+ _›] nat_simp_union 
    by simp    
  note in_M = ‹π∈M› ‹domain(π) × P ∈ M›  P_in_M one_in_M leq_in_M
  {
    fix u
    assume "u ∈ domain(π) × P" "u ∈ M"
    with in_M ‹?new_form ∈ formula› ‹?ψ∈formula› ‹nenv ∈ _›
    have Eq1: "(M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷ 
                        (∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧ 
                          M, [θ,p,u]@?Pl1@[π] @ nenv ⊨ ?new_form)"
      by (auto simp add: transitivity)
    have Eq3: "θ∈M ⟹ p∈P ⟹
       (M, [θ,p,u]@?Pl1@[π]@nenv ⊨ ?new_form) ⟷
          (∀F. M_generic(F) ∧ p ∈ F ⟶ (M[F],  map(val(F), [θ] @ nenv@[π]) ⊨  ?χ))" 
      for θ p 
    proof -
      fix p θ 
      assume "θ ∈ M" "p∈P"
      then 
      have "p∈M" using P_in_M by (simp add: transitivity)
      note in_M' = in_M ‹θ ∈ M› ‹p∈M› ‹u ∈ domain(π) × P› ‹u ∈ M› ‹nenv∈_›
      then 
      have "[θ,u] ∈ list(M)" by simp
      let ?env="[p]@?Pl1@[θ] @ nenv @ [π,u]"
      let ?new_env=" [θ,p,u,P,leq,one,π] @ nenv"
      let ?ψ="Exists(Exists(And(pair_fm(0,1,2),?new_form)))"
      have "[θ, p, u, π, leq, one, π] ∈ list(M)" 
        using in_M' by simp
      have "?χ ∈ formula" "forces(?χ)∈ formula"  
        using phi by simp_all
      from in_M' 
      have "?Pl1 ∈ list(M)" by simp
      from in_M' have "?env ∈ list(M)" by simp
      have Eq1': "?new_env ∈ list(M)" using in_M'  by simp 
      then 
      have "(M, [θ,p,u]@?Pl1@[π] @ nenv ⊨ ?new_form) ⟷ (M, ?new_env ⊨ ?new_form)"
        by simp
      from in_M' ‹env ∈ _› Eq1' ‹length(nenv) = length(env)› 
        ‹arity(forces(?χ)) ≤ 7 #+ length(env)› ‹forces(?χ)∈ formula›
        ‹[θ, p, u, π, leq, one, π] ∈ list(M)› 
      have "... ⟷ M, ?env ⊨ forces(?χ)"
        using sepren_action[of "forces(?χ)"  "nenv",OF _ _ ‹nenv∈list(M)›] 
        by simp
      also from in_M'
      have "... ⟷ M,  ([p,P, leq, one,θ]@nenv@ [π])@[u] ⊨ forces(?χ)" 
        using app_assoc by simp
      also 
      from in_M' ‹env∈_› phi ‹length(nenv) = length(env)›
        ‹arity(forces(?χ)) ≤ 6 #+ length(env)› ‹forces(?χ)∈formula›
      have "... ⟷ M,  [p,P, leq, one,θ]@ nenv @ [π] ⊨ forces(?χ)"        
        by (rule_tac arity_sats_iff,auto)
      also 
      from ‹arity(forces(?χ)) ≤ 6 #+ length(env)› ‹forces(?χ)∈formula› in_M' phi 
      have " ... ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶ 
                           M[F],  map(val(F), [θ] @ nenv @ [π]) ⊨  ?χ)"
        using  definition_of_forcing 
      proof (intro iffI)
        assume a1: "M,  [p,P, leq, one,θ] @ nenv @ [π] ⊨  forces(?χ)"
        note definition_of_forcing ‹arity(φ)≤ 1#+_›
        with ‹nenv∈_› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])› ‹env∈_›
        have "p ∈ P ⟹ ?χ∈formula ⟹ [θ,π] ∈ list(M) ⟹
                  M, [p,P, leq, one] @ [θ]@ nenv@[π] ⊨ forces(?χ) ⟹ 
              ∀G. M_generic(G) ∧ p ∈ G ⟶ M[G],  map(val(G), [θ] @ nenv @[π]) ⊨  ?χ"
          by auto
        then
        show "∀F. M_generic(F) ∧ p ∈ F ⟶ 
                  M[F],  map(val(F), [θ] @ nenv @ [π]) ⊨  ?χ"
          using  ‹?χ∈formula› ‹p∈P› a1 ‹θ∈M› ‹π∈M› by simp
      next
        assume "∀F. M_generic(F) ∧ p ∈ F ⟶ 
                   M[F],  map(val(F), [θ] @ nenv @[π]) ⊨  ?χ"
        with definition_of_forcing [THEN iffD2] ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
        show "M,  [p, P, leq, one,θ] @ nenv @ [π] ⊨  forces(?χ)"
          using  ‹?χ∈formula› ‹p∈P› in_M' 
          by auto
      qed
      finally 
      show "(M, [θ,p,u]@?Pl1@[π]@nenv ⊨ ?new_form) ⟷ (∀F. M_generic(F) ∧ p ∈ F ⟶ 
                           M[F],  map(val(F), [θ] @ nenv @ [π]) ⊨  ?χ)" 
        by simp
    qed
    with Eq1 
    have "(M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷ 
         (∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧ 
          (∀F. M_generic(F) ∧ p ∈ F ⟶ M[F],  map(val(F), [θ] @ nenv @ [π]) ⊨  ?χ))"
      by auto 
  }
  then 
  have Equivalence: "u∈ domain(π) × P ⟹ u ∈ M ⟹ 
       (M, [u] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ) ⟷ 
         (∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧ 
          (∀F. M_generic(F) ∧ p ∈ F ⟶ M[F],   map(val(F), [θ] @ nenv @[π]) ⊨  ?χ))" 
    for u 
    by simp
  moreover from ‹env = _› ‹π∈M› ‹nenv∈list(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∈P. u =⟨θ,p⟩ ∧ (p∈G ⟶ M[G], [val(G,θ)] @ env @ [val(G,π)] ⊨ ?χ))" 
   (is "(∃θ∈M. ∃p∈P. _ ( _ ⟶ _, ?vals(θ) ⊨ _))")
   if "u ∈ domain(π) × P" "u ∈ M"  "M, [u]@ ?Pl1 @[π] @ nenv ⊨ ?ψ" for u
    using Equivalence[THEN iffD1, OF that] generic by force
  moreover 
  have "θ∈M ⟹ val(G,θ)∈M[G]" for θ
    using GenExt_def by auto
  moreover
  have "θ∈ M ⟹ [val(G, θ)] @ env @ [val(G, π)] ∈ list(M[G])" for θ
  proof -
    from ‹π∈M›
    have "val(G,π)∈ M[G]" using GenExtI by simp
    moreover
    assume "θ ∈ M"
    moreover
    note ‹env ∈ list(M[G])›
    ultimately
    show ?thesis 
      using GenExtI by simp
  qed
  ultimately 
  have "(∃θ∈M. ∃p∈P. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(G,θ)∈nth(1 #+ length(env),[val(G, θ)] @ env @ [val(G, π)]) 
        ∧ M[G],  ?vals(θ) ⊨  φ))"
    if "u ∈ domain(π) × P" "u ∈ M"  "M, [u] @ ?Pl1 @[π] @ 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]"] using that GenExtI by simp
  ultimately
  have "(∃θ∈M. ∃p∈P. u=⟨θ,p⟩ ∧ (p∈G ⟶ val(G,θ)∈val(G,π) ∧ M[G],  ?vals(θ) ⊨  φ))"
    if "u ∈ domain(π) × P" "u ∈ M"  "M, [u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ" for u
    using that ‹π∈M› ‹env ∈ _› by simp
  with ‹domain(π)×P∈M›
  have "∀u∈domain(π)×P . (M, [u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ) ⟶ (∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧
        (p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ M[G],  ?vals(θ) ⊨  φ))"
    by (simp add:transitivity)
  then 
  have "{u∈domain(π)×P . (M,[u] @ ?Pl1 @[π] @ nenv ⊨ ?ψ) } ⊆
     {u∈domain(π)×P . ∃θ∈M. ∃p∈P. u =⟨θ,p⟩ ∧ 
       (p ∈ G ⟶ val(G, θ)∈val(G, π) ∧ (M[G], ?vals(θ) ⊨ φ))}"
    (is "?n⊆?m") 
    by auto
  with val_mono 
  have first_incl: "val(G,?n) ⊆ val(G,?m)" 
    by simp
  note  ‹val(G,π) = c› (* from the assumptions *)
  with ‹?ψ∈formula›  ‹arity(?ψ) ≤ _› in_M ‹nenv ∈ _› ‹env ∈ _› ‹length(nenv) = _› 
  have "?n∈M" 
    using separation_ax leI separation_iff by auto 
  from generic 
  have "filter(G)" "G⊆P" 
    unfolding M_generic_def filter_def by simp_all
  from ‹val(G,π) = c› 
  have "val(G,?m) =
               {val(G,t) .. t∈domain(π) , ∃q∈P .  
                    (∃θ∈M. ∃p∈P. ⟨t,q⟩ = ⟨θ, p⟩ ∧ 
            (p ∈ G ⟶ val(G, θ) ∈ c ∧ (M[G],  [val(G, θ)] @ env @ [c] ⊨  φ)) ∧ q ∈ G)}"
    using val_of_name by auto
  also 
  have "... =  {val(G,t) .. t∈domain(π) , ∃q∈P. 
                   val(G, t) ∈ c ∧ (M[G],  [val(G, t)] @ env @ [c] ⊨  φ) ∧ q ∈ G}" 
  proof -

    have "t∈M ⟹
      (∃q∈P. (∃θ∈M. ∃p∈P. ⟨t,q⟩ = ⟨θ, p⟩ ∧ 
              (p ∈ G ⟶ val(G, θ) ∈ c ∧ (M[G],  [val(G, θ)] @ env @ [c] ⊨  φ)) ∧ q ∈ G)) 
      ⟷ 
      (∃q∈P. val(G, t) ∈ c ∧ ( M[G], [val(G, t)]@env@[c]⊨ φ ) ∧ q ∈ G)" for t
      by auto
    then show ?thesis using ‹domain(π)∈M› by (auto simp add:transitivity)
  qed
  also 
  have "... =  {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G],  [x] @ env @ [c] ⊨  φ) ∧ q ∈ G}"
  proof

    show "... ⊆ {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G],  [x] @ env @ [c] ⊨  φ) ∧ q ∈ G}"
      by auto
  next 
    (* Now we show the other inclusion:
      {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G],  [x, w, c] ⊨  φ) ∧ q ∈ G}
      ⊆
      {val(G,t)..t∈domain(π),∃q∈P.val(G,t)∈c∧(M[G], [val(G,t),w] ⊨ φ)∧q∈G}
    *)
    {
      fix x
      assume "x∈{x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G],  [x] @ env @ [c] ⊨  φ) ∧ q ∈ G}"
      then 
      have "∃q∈P. x ∈ c ∧ (M[G],  [x] @ env @ [c] ⊨  φ) ∧ q ∈ G"
        by simp
      with ‹val(G,π) = c›  
      have "∃q∈P. ∃t∈domain(π). val(G,t) =x ∧ (M[G],  [val(G,t)] @ env @ [c] ⊨  φ) ∧ q ∈ G" 
        using Sep_and_Replace elem_of_val by auto
    }
    then 
    show " {x .. x∈c , ∃q∈P. x ∈ c ∧ (M[G],  [x] @ env @ [c] ⊨  φ) ∧ q ∈ G} ⊆ ..."
      using SepReplace_iff by force
  qed
  also 
  have " ... = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}"
    using ‹G⊆P› G_nonempty by force
  finally 
  have val_m: "val(G,?m) = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by simp
  have "val(G,?m) ⊆ val(G,?n)" 
  proof
    fix x
    assume "x ∈ val(G,?m)"
    with val_m 
    have Eq4: "x ∈ {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by simp
    with ‹val(G,π) = c›
    have "x ∈ val(G,π)" by simp
    then 
    have "∃θ. ∃q∈G. ⟨θ,q⟩∈π ∧ val(G,θ) =x" 
      using elem_of_val_pair by auto
    then obtain θ q where
      "⟨θ,q⟩∈π" "q∈G" "val(G,θ)=x" by auto
    from ‹⟨θ,q⟩∈π›
    have "θ∈M"
      using domain_trans[OF trans_M ‹π∈_›] by auto
    with ‹π∈M› ‹nenv ∈ _› ‹env = _›
    have "[val(G,θ), val(G,π)] @ env ∈list(M[G])" 
      using GenExt_def by auto
    with  Eq4 ‹val(G,θ)=x› ‹val(G,π) = c› ‹x ∈ val(G,π)› nth ‹θ∈M›
    have Eq5: "M[G],  [val(G,θ)] @ env @[val(G,π)] ⊨ And(Member(0,1 #+ length(env)),φ)" 
      by auto
        (* Recall ?χ = And(Member(0,1 #+ length(env)),φ) *)
    with ‹θ∈M› ‹π∈M›  Eq5 ‹M_generic(G)› ‹φ∈formula› ‹nenv ∈ _ › ‹env = _ › map_nenv 
      ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
    have "(∃r∈G. M,  [r,P,leq,one,θ] @ nenv @[π] ⊨ forces(?χ))"
      using truth_lemma  
      by auto
    then obtain r where      (* I can't "obtain" this directly *)
      "r∈G" "M,  [r,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)" by auto
    with ‹filter(G)› and ‹q∈G› obtain p where
      "p∈G" "p≼q" "p≼r" 
      unfolding filter_def compat_in_def by force
    with ‹r∈G›  ‹q∈G› ‹G⊆P› 
    have "p∈P" "r∈P" "q∈P" "p∈M"
      using  P_in_M  by (auto simp add:transitivity)
    with ‹φ∈formula› ‹θ∈M› ‹π∈M›  ‹p≼r› ‹nenv ∈ _› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
      ‹M, [r,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)› ‹env∈_›
    have "M,  [p,P,leq,one,θ] @ nenv @ [π] ⊨ forces(?χ)"
      using strengthening_lemma 
      by simp
    with ‹p∈P› ‹φ∈formula› ‹θ∈M› ‹π∈M› ‹nenv ∈ _› ‹arity(?χ) ≤ length([θ] @ nenv @ [π])›
    have "∀F. M_generic(F) ∧ p ∈ F ⟶ 
                 M[F],   map(val(F), [θ] @ nenv @[π]) ⊨  ?χ"
      using definition_of_forcing
      by simp
    with ‹p∈P› ‹θ∈M›  
    have Eq6: "∃θ'∈M. ∃p'∈P.  ⟨θ,p⟩ = <θ',p'> ∧ (∀F. M_generic(F) ∧ p' ∈ F ⟶ 
                 M[F],   map(val(F), [θ'] @ nenv @ [π]) ⊨  ?χ)" by auto
    from ‹π∈M› ‹⟨θ,q⟩∈π› 
    have "⟨θ,q⟩ ∈ M" by (simp add:transitivity)
    from ‹⟨θ,q⟩∈π› ‹θ∈M› ‹p∈P›  ‹p∈M› 
    have "⟨θ,p⟩∈M" "⟨θ,p⟩∈domain(π)×P" 
      using tuples_in_M by auto
    with ‹θ∈M› Eq6 ‹p∈P›
    have "M, [⟨θ,p⟩] @ ?Pl1 @ [π] @ nenv ⊨ ?ψ"
      using Equivalence  by auto
    with ‹⟨θ,p⟩∈domain(π)×P› 
    have "⟨θ,p⟩∈?n" by simp
    with ‹p∈G› ‹p∈P› 
    have "val(G,θ)∈val(G,?n)" 
      using  val_of_elem[of θ p] by simp
    with ‹val(G,θ)=x› 
    show "x∈val(G,?n)" by simp
  qed (* proof of "val(G,?m) ⊆ val(G,?n)" *)
  with val_m first_incl 
  have "val(G,?n) = {x∈c. (M[G], [x] @ env @ [c] ⊨ φ)}" by auto
  also 
  have " ... = {x∈c. (M[G], [x] @ env ⊨ φ)}" 
  proof -
    {
      fix x
      assume "x∈c"
      moreover from assms 
      have "c∈M[G]"
        unfolding GenExt_def by auto
      moreover from this and ‹x∈c› 
      have "x∈M[G]"
        using transitivity_MG
        by simp
      ultimately 
      have "(M[G],  ([x] @ env) @[c] ⊨  φ) ⟷ (M[G],  [x] @ env ⊨  φ)" 
        using phi ‹env ∈ _› by (rule_tac arity_sats_iff, simp_all)   (* Enhance this *)
    }
    then show ?thesis by auto
  qed      
  finally 
  show "{x∈c. (M[G], [x] @ env ⊨ φ)}∈ M[G]" 
    using ‹?n∈M› GenExt_def by force
qed

theorem separation_in_MG:
  assumes 
    "φ∈formula" and "arity(φ) ≤ 1 #+ length(env)" and "env∈list(M[G])"
  shows  
    "separation(##M[G],λx. (M[G], [x] @ env ⊨ φ))"
proof -
  { 
    fix c
    assume "c∈M[G]" 
    moreover from ‹env ∈ _›
    obtain nenv where  "nenv∈list(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 Eq1: "{x∈c. (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 (* context: G_generic *)

end