Theory Forcing_Theorems

section‹The Forcing Theorems›

theory Forcing_Theorems
  imports
    Cohen_Posets_Relative
    Forces_Definition
    Names

begin

context forcing_data1
begin

subsection‹The forcing relation in context›

lemma separation_forces :
  assumes
    fty: "φformula" and
    far: "arity(φ)length(env)" and
    envty: "envlist(M)"
  shows
    "separation(##M,λp. (p  φ env))"
  using separation_ax arity_forces far fty envty arity_forces_le
    transitivity[of _ ]
  by simp

lemma Collect_forces :
  assumes
    "φformula" and
    "arity(φ)length(env)" and
    "envlist(M)"
  shows
    "{p . p  φ env}  M"
  using assms separation_forces separation_closed
  by simp

lemma forces_mem_iff_dense_below:  "p  p forcesa (t1  t2)  dense_below(
    {q. s. r. r  s,r  t2  qr  q forcesa (t1 = s)}
    ,p)"
  using def_forces_mem[of p t1 t2] by blast

subsection‹Kunen 2013, Lemma IV.2.37(a)›

lemma strengthening_eq:
  assumes "p" "r" "rp" "p forcesa (t1 = t2)"
  shows "r forcesa (t1 = t2)"
  using assms def_forces_eq[of _ t1 t2] leq_transD by blast
    (* Long proof *)
    (*
proof -
  {
    fix s q
    assume "q≼ r" "q∈ℙ"
    with assms
    have "q≼p"
      using leq_preord unfolding preorder_on_def trans_on_def by blast
    moreover
    note ‹q∈ℙ› assms
    moreover
    assume "s∈domain(t1) ∪ domain(t2)"
    ultimately
    have "q forcesa ( s ∈  t1) ⟷ q forcesa ( s ∈  t2)"
      using def_forces_eq[of p t1 t2] by simp
  }
  with ‹r∈ℙ›
  show ?thesis using def_forces_eq[of r t1 t2] by blast
qed
*)

subsection‹Kunen 2013, Lemma IV.2.37(a)›
lemma strengthening_mem:
  assumes "p" "r" "rp" "p forcesa (t1  t2)"
  shows "r forcesa (t1  t2)"
  using assms forces_mem_iff_dense_below dense_below_under by auto

subsection‹Kunen 2013, Lemma IV.2.37(b)›
lemma density_mem:
  assumes "p"
  shows "p forcesa (t1  t2)   dense_below({q. q forcesa (t1  t2)},p)"
proof
  assume "p forcesa (t1  t2)"
  with assms
  show "dense_below({q. q forcesa (t1  t2)},p)"
    using forces_mem_iff_dense_below strengthening_mem[of p] ideal_dense_below by auto
next
  assume "dense_below({q   . q forcesa ( t1   t2)}, p)"
  with assms
  have "dense_below({q.
    dense_below({q'. s r. r    s,rt2  q'r  q' forcesa (t1 = s)},q)
    },p)"
    using forces_mem_iff_dense_below by simp
  with assms
  show "p forcesa (t1  t2)"
    using dense_below_dense_below forces_mem_iff_dense_below[of p t1 t2] by blast
qed

lemma aux_density_eq:
  assumes
    "dense_below(
    {q'. q. q  qq'  q forcesa (s  t1)  q forcesa (s  t2)}
    ,p)"
    "q forcesa (s  t1)" "q" "p" "qp"
  shows
    "dense_below({r. r forcesa (s  t2)},q)"
proof
  fix r
  assume "r" "rq"
  moreover from this and p qp q
  have "rp"
    using leq_transD by simp
  moreover
  note q forcesa (s  t1) dense_below(_,p) q
  ultimately
  obtain q1 where "q1r" "q1" "q1 forcesa (s  t2)"
    using strengthening_mem[of q _ s t1] refl_leq leq_transD[of _ r q] by blast
  then
  show "d{r   . r forcesa ( s   t2)}. d    d r"
    by blast
qed

(* Kunen 2013, Lemma IV.2.37(b) *)
lemma density_eq:
  assumes "p"
  shows "p forcesa (t1 = t2)   dense_below({q. q forcesa (t1 = t2)},p)"
proof
  assume "p forcesa (t1 = t2)"
  with p
  show "dense_below({q. q forcesa (t1 = t2)},p)"
    using strengthening_eq ideal_dense_below by auto
next
  assume "dense_below({q. q forcesa (t1 = t2)},p)"
  {
    fix s q
    let ?D1="{q'. sdomain(t1)  domain(t2). q. q    qq' 
           q forcesa (s  t1)q forcesa (s  t2)}"
    let ?D2="{q'. q. q  qq'  q forcesa (s  t1)  q forcesa (s  t2)}"
    assume "sdomain(t1)  domain(t2)"
    then
    have "?D1?D2" by blast
    with dense_below(_,p)
    have "dense_below({q'. sdomain(t1)  domain(t2). q. q    qq' 
           q forcesa (s  t1)q forcesa (s  t2)},p)"
      using dense_below_cong'[OF p def_forces_eq[of _ t1 t2]] by simp
    with p ?D1?D2
    have "dense_below({q'. q. q  qq' 
            q forcesa (s  t1)  q forcesa (s  t2)},p)"
      using dense_below_mono by simp
    moreover from this (* Automatic tools can't handle this symmetry
                          in order to apply aux_density_eq below *)
    have  "dense_below({q'. q. q  qq' 
            q forcesa (s  t2)  q forcesa (s  t1)},p)"
      by blast
    moreover
    assume "q  " "qp"
    moreover
    note p
    ultimately (*We can omit the next step but it is slower *)
    have "q forcesa (s  t1)  dense_below({r. r forcesa (s  t2)},q)"
      "q forcesa (s  t2)  dense_below({r. r forcesa (s  t1)},q)"
      using aux_density_eq by simp_all
    then
    have "q forcesa ( s   t1)  q forcesa ( s   t2)"
      using density_mem[OF q] by blast
  }
  with p
  show "p forcesa (t1 = t2)" using def_forces_eq by blast
qed

subsection‹Kunen 2013, Lemma IV.2.38›
lemma not_forces_neq:
  assumes "p"
  shows "p forcesa (t1 = t2)  ¬ (q. qp  q forcesa (t1  t2))"
  using assms density_eq unfolding forces_neq_def by blast

lemma not_forces_nmem:
  assumes "p"
  shows "p forcesa (t1  t2)  ¬ (q. qp  q forcesa (t1  t2))"
  using assms density_mem unfolding forces_nmem_def by blast

subsection‹The relation of forcing and atomic formulas›
lemma Forces_Equal:
  assumes
    "p" "t1M" "t2M" "envlist(M)" "nth(n,env) = t1" "nth(m,env) = t2" "nnat" "mnat"
  shows
    "(p  Equal(n,m) env)  p forcesa (t1 = t2)"
  using assms sats_forces_Equal forces_eq_abs transitivity
  by simp

lemma Forces_Member:
  assumes
    "p" "t1M" "t2M" "envlist(M)" "nth(n,env) = t1" "nth(m,env) = t2" "nnat" "mnat"
  shows
    "(p  Member(n,m) env)  p forcesa (t1  t2)"
  using assms sats_forces_Member forces_mem_abs transitivity
  by simp

lemma Forces_Neg:
  assumes
    "p" "env  list(M)" "φformula"
  shows
    "(p  Neg(φ) env)  ¬(qM. q  qp  (q  φ env))"
  using assms sats_forces_Neg transitivity pair_in_M_iff leq_abs
  by simp

subsection‹The relation of forcing and connectives›

lemma Forces_Nand:
  assumes
    "p" "env  list(M)" "φformula" "ψformula"
  shows
    "(p  Nand(φ,ψ) env)  ¬(qM. q  qp  (q  φ env)  (q  ψ env))"
  using assms sats_forces_Nand transitivity pair_in_M_iff leq_abs by simp

lemma Forces_And_aux:
  assumes
    "p" "env  list(M)" "φformula" "ψformula"
  shows
    "p  And(φ,ψ) env   
    (qM. q  qp  (rM. r  rq  (r  φ env)  (r  ψ env)))"
  unfolding And_def using assms Forces_Neg Forces_Nand by (auto simp only:)

lemma Forces_And_iff_dense_below:
  assumes
    "p" "env  list(M)" "φformula" "ψformula"
  shows
    "(p  And(φ,ψ) env)  dense_below({r. (r  φ env)  (r  ψ env) },p)"
  unfolding dense_below_def using Forces_And_aux assms
  by (auto dest:transitivity[OF _ P_in_M]; rename_tac q; drule_tac x=q in bspec)+

lemma Forces_Forall:
  assumes
    "p" "env  list(M)" "φformula"
  shows
    "(p  Forall(φ) env)  (xM. (p  φ ([x] @ env)))"
  using sats_forces_Forall assms transitivity[OF _ P_in_M]
  by simp

(* "x∈val(G,π) ⟹ ∃θ. ∃p∈G.  ⟨θ,p⟩∈π ∧ val(G,θ) = x" *)
bundle some_rules =  elem_of_val_pair [dest]

context
  includes some_rules
begin

lemma elem_of_valI: "θ. p. pG  θ,pπ  val(G,θ) = x  xval(G,π)"
  by (subst def_val, auto)

lemma GenExt_iff: "xM[G]  (τM. x = val(G,τ))"
  unfolding GenExt_def by simp
end

end
context G_generic1
  
begin

subsection‹Kunen 2013, Lemma IV.2.29›
lemma generic_inter_dense_below:
  assumes "DM" "dense_below(D,p)" "pG"
  shows "D  G  0"
proof -
  let ?D="{q. pq  qD}"
  have "dense(?D)"
  proof
    fix r
    assume "r"
    show "d{q   . p  q  q  D}. d  r"
    proof (cases "p  r")
      case True
      with r
        (* Automatic tools can't handle this case for some reason... *)
      show ?thesis using refl_leq[of r] by (intro bexI) (blast+)
    next
      case False
      then
      obtain s where "s" "sp" "sr" by blast
      with assms r
      show ?thesis
        using dense_belowD[OF assms(2), of s] leq_transD[of _ s r]
        by blast
    qed
  qed
  have "?D" by auto
  let ?d_fm="⋅¬compat_in_fm(1, 2, 3, 0)   0  4"
  from pG
  have "pM"
    using G_subset_M subsetD by simp
  moreover
  have "?d_fmformula" by simp
  moreover
  have "arity(?d_fm) = 5"
    by (auto simp add: arity)
  moreover from DM pM
  have "(M, [q,,leq,p,D]  ?d_fm)  (¬ is_compat_in(##M,,leq,p,q)  qD)"
    if "qM" for q
    using that sats_compat_in_fm zero_in_M
    by simp
  moreover from pM
  have "(¬ is_compat_in(##M,,leq,p,q)  qD)  pq  qD" if "qM" for q
    unfolding compat_def
    using that compat_in_abs
    by simp
  ultimately
  have "?DM"
    using Collect_in_M[of ?d_fm "[,leq,p,D]"] DM
    by simp
  note asm = dense(?D) ?D ?DM
  obtain x where "xG" "x?D" 
    using M_generic_denseD[OF asm]
    by force (* by (erule bexE) does it, but the other automatic tools don't *)
  moreover from this
  have "xD"
    using M_generic_compatD[OF _ pG, of x] refl_leq compatI[of _ p x]
    by force
  ultimately
  show ?thesis by auto
qed

subsection‹Auxiliary results for Lemma IV.2.40(a)›
lemma (in forcing_data1) IV240a_mem_Collect:
  assumes
    "πM" "τM"
  shows
    "{q. σ. r. r  σ,r  τ  qr  q forcesa (π = σ)}M"
proof -
  let ?rel_pred= "λM x a1 a2 a3 a4. σ[M]. r[M]. σr[M].
                ra1  pair(M,σ,r,σr)  σra4  is_leq(M,a2,x,r)  is_forces_eq'(M,a1,a2,x,a3,σ)"
  let ="Exists(Exists(Exists(And(Member(1,4),And(pair_fm(2,1,0),
          And(Member(0,7),And(is_leq_fm(5,3,1),forces_eq_fm(4,5,3,6,2))))))))"
  have "σM  rM" if "σ, r  τ"  for σ r
    using that τM pair_in_M_iff transitivity[of "σ,r" τ] by simp
  then
  have "?rel_pred(##M,q,,leq,π,τ)  (σ. r. r  σ,r  τ  qr  q forcesa (π = σ))"
    if "qM" for q
    unfolding forces_eq_def
    using assms that leq_abs forces_eq'_abs pair_in_M_iff
    by auto
  moreover
  have "(M, [q,,leq,π,τ]  )  ?rel_pred(##M,q,,leq,π,τ)" if "qM" for q
    using assms that sats_forces_eq_fm sats_is_leq_fm zero_in_M
    by simp
  moreover
  have "formula" by simp
  moreover
  have "arity()=5"
    using arity_forces_eq_fm
    by (simp add:ord_simp_union arity)
  ultimately
  show ?thesis
    unfolding forces_eq_def using assms Collect_in_M[of  "[,leq,π,τ]"]
    by simp
qed

(* Lemma IV.2.40(a), membership *)
lemma IV240a_mem:
  assumes
    "pG" "πM" "τM" "p forcesa (π  τ)"
    "q σ. q  qG  σdomain(τ)  q forcesa (π = σ) 
      val(G,π) = val(G,σ)" (* inductive hypothesis *)
  shows
    "val(G,π)val(G,τ)"
proof (intro elem_of_valI)
  let ?D="{q. σ. r. r  σ,r  τ  qr  q forcesa (π = σ)}"
  from pG
  have "p" by blast
  moreover
  note πM τM
  ultimately
  have "?D  M" using IV240a_mem_Collect by simp
  moreover from assms p
  have "dense_below(?D,p)"
    using forces_mem_iff_dense_below by simp
  moreover
  note pG
  ultimately
  obtain q where "qG" "q?D" 
    using generic_inter_dense_below[of ?D p] by blast
  then
  obtain σ r where "r" "σ,r  τ" "qr" "q forcesa (π = σ)" by blast
  moreover from this and qG assms
  have "r  G" "val(G,π) = val(G,σ)" by blast+
  ultimately
  show " σ. p. p  G  σ, p  τ  val(G, σ) = val(G, π)" by auto
qed

(* Example IV.2.36 (next two lemmas) *)
lemma refl_forces_eq:"p  p forcesa (x = x)"
  using def_forces_eq by simp

lemma forces_memI: "σ,rτ  p  r  pr  p forcesa (σ  τ)"
  using refl_forces_eq[of _ σ] leq_transD refl_leq
  by (blast intro:forces_mem_iff_dense_below[THEN iffD2])

(* Lemma IV.2.40(a), equality, first inclusion *)
lemma IV240a_eq_1st_incl:
  includes some_rules
  assumes
    "pG" "p forcesa (τ = θ)"
    and
    IH:"q σ. q  qG  σdomain(τ)  domain(θ) 
        (q forcesa (σ  τ)  val(G,σ)  val(G,τ)) 
        (q forcesa (σ  θ)  val(G,σ)  val(G,θ))"
    (* Strong enough for this case: *)
    (*  IH:"⋀q σ. q∈ℙ ⟹ σ∈domain(τ) ⟹ q forcesa (σ ∈ θ) ⟹
      val(G,σ) ∈ val(G,θ)" *)
  shows
    "val(G,τ)  val(G,θ)"
proof
  fix x
  assume "xval(G,τ)"
  then
  obtain σ r where "σ,rτ" "rG" "val(G,σ)=x" by blast
  moreover from this and pG
  obtain q where "qG" "qp" "qr" by force
  moreover from this and pG
  have "q" "p" by blast+
  moreover from calculation
  have "q forcesa (σ  τ)"
    using forces_memI by auto
  moreover
  note p forcesa (τ = θ)
  ultimately
  have "q forcesa (σ  θ)"
    using def_forces_eq by auto
  with q qG IH[of q σ] σ,rτ val(G,σ) = x
  show "xval(G,θ)" by blast
qed

(* Lemma IV.2.40(a), equality, second inclusion--- COℙY-ℙASTE *)
lemma IV240a_eq_2nd_incl:
  includes some_rules
  assumes
    "pG" "p forcesa (τ = θ)"
    and
    IH:"q σ. q  qG  σdomain(τ)  domain(θ) 
        (q forcesa (σ  τ)  val(G,σ)  val(G,τ)) 
        (q forcesa (σ  θ)  val(G,σ)  val(G,θ))"
  shows
    "val(G,θ)  val(G,τ)"
proof
  fix x
  assume "xval(G,θ)"
  then
  obtain σ r where "σ,rθ" "rG" "val(G,σ)=x" by blast
  moreover from this and pG
  obtain q where "qG" "qp" "qr" by force
  moreover from this and pG
  have "q" "p" by blast+
  moreover from calculation
  have "q forcesa (σ  θ)"
    using forces_memI by auto
  moreover
  note p forcesa (τ = θ)
  ultimately
  have "q forcesa (σ  τ)"
    using def_forces_eq by auto
  with q qG IH[of q σ] σ,rθ val(G,σ) = x
  show "xval(G,τ)" by blast
qed

(* Lemma IV.2.40(a), equality, second inclusion--- COℙY-ℙASTE *)
lemma IV240a_eq:
  includes some_rules
  assumes
    "pG" "p forcesa (τ = θ)"
    and
    IH:"q σ. q  qG  σdomain(τ)  domain(θ) 
        (q forcesa (σ  τ)  val(G,σ)  val(G,τ)) 
        (q forcesa (σ  θ)  val(G,σ)  val(G,θ))"
  shows
    "val(G,τ) = val(G,θ)"
  using IV240a_eq_1st_incl[OF assms] IV240a_eq_2nd_incl[OF assms] IH by blast

subsection‹Induction on names›

lemma (in forcing_data1) core_induction:
  assumes
    "τ θ p. p    q σ. q ; σdomain(θ)  Q(0,τ,σ,q)  Q(1,τ,θ,p)"
    "τ θ p. p    q σ. q ; σdomain(τ)  domain(θ)  Q(1,σ,τ,q)  Q(1,σ,θ,q)  Q(0,τ,θ,p)"
    "ft  2" "p  "
  shows
    "Q(ft,τ,θ,p)"
proof -
  {
    fix ft p τ θ
    have "Transset(eclose({τ,θ}))" (is "Transset(?e)")
      using Transset_eclose by simp
    have "τ  ?e" "θ  ?e"
      using arg_into_eclose by simp_all
    moreover
    assume "ft  2" "p  "
    ultimately
    have "ft,τ,θ,p 2×?e×?e×" (is "?a2×?e×?e×") by simp
    then
    have "Q(ftype(?a), name1(?a), name2(?a), cond_of(?a))"
      using core_induction_aux[of ?e  Q ?a,OF Transset(?e) assms(1,2) ?a_]
      by (clarify) (blast)
    then have "Q(ft,τ,θ,p)" by (simp add:components_simp)
  }
  then show ?thesis using assms by simp
qed

lemma (in forcing_data1) forces_induction_with_conds:
  assumes
    "τ θ p. p    q σ. q ; σdomain(θ)  Q(q,τ,σ)  R(p,τ,θ)"
    "τ θ p. p    q σ. q ; σdomain(τ)  domain(θ)  R(q,σ,τ)  R(q,σ,θ)  Q(p,τ,θ)"
    "p  "
  shows
    "Q(p,τ,θ)  R(p,τ,θ)"
proof -
  let ?Q="λft τ θ p. (ft = 0  Q(p,τ,θ))  (ft = 1  R(p,τ,θ))"
  from assms(1)
  have "τ θ p. p    q σ. q ; σdomain(θ)  ?Q(0,τ,σ,q)  ?Q(1,τ,θ,p)"
    by simp
  moreover from assms(2)
  have "τ θ p. p    q σ. q ; σdomain(τ)  domain(θ)  ?Q(1,σ,τ,q)  ?Q(1,σ,θ,q)  ?Q(0,τ,θ,p)"
    by simp
  moreover
  note p
  ultimately
  have "?Q(ft,τ,θ,p)" if "ft2" for ft
    by (rule core_induction[OF _ _ that, of ?Q])
  then
  show ?thesis by auto
qed

lemma (in forcing_data1) forces_induction:
  assumes
    "τ θ. σ. σdomain(θ)  Q(τ,σ)  R(τ,θ)"
    "τ θ. σ. σdomain(τ)  domain(θ)  R(σ,τ)  R(σ,θ)  Q(τ,θ)"
  shows
    "Q(τ,θ)  R(τ,θ)"
proof (intro forces_induction_with_conds[OF _ _ one_in_P ])
  fix τ θ p
  assume "q    σ  domain(θ)  Q(τ, σ)" for q σ
  with assms(1)
  show "R(τ,θ)"
    using one_in_P by simp
next
  fix τ θ p
  assume "q    σ  domain(τ)  domain(θ)  R(σ,τ)  R(σ,θ)" for q σ
  with assms(2)
  show "Q(τ,θ)"
    using one_in_P by simp
qed

subsection‹Lemma IV.2.40(a), in full›
lemma IV240a:
  shows
    "(τM  θM  (pG. p forcesa (τ = θ)  val(G,τ) = val(G,θ))) 
     (τM  θM  (pG. p forcesa (τ  θ)  val(G,τ)  val(G,θ)))"
    (is "?Q(τ,θ)  ?R(τ,θ)")
proof (intro forces_induction[of ?Q ?R] impI)
  fix τ θ
  assume "τM" "θM"  "σdomain(θ)  ?Q(τ,σ)" for σ
  moreover from this
  have "σdomain(θ)  q forcesa (τ = σ)  val(G, τ) = val(G, σ)"
    if "q" "qG" for q σ
    using that domain_closed[of θ] transitivity by auto
  ultimately
  show "pG. p forcesa (τ  θ)  val(G,τ)  val(G,θ)"
    using IV240a_mem domain_closed transitivity by simp
next
  fix τ θ
  assume "τM" "θM" and d:"σ  domain(τ)  domain(θ)  ?R(σ,τ)  ?R(σ,θ)" for σ
  moreover from this
  have IH':"(q forcesa (σ  τ)  val(G, σ)  val(G, τ)) 
            (q forcesa (σ  θ)  val(G, σ)  val(G, θ))" 
    if "σ  domain(τ)  domain(θ)" "qG" for q σ
  proof -
    from d that
    have A:"?R(σ,τ)" "?R(σ,θ)"
      by auto
    from τ_ θM qG σ_
     show ?thesis
      using transitivity[of σ] domain_closed A[rule_format,of q]
      by auto
  qed
  show "pG. p forcesa (τ = θ)  val(G,τ) = val(G,θ)"
    using IV240a_eq[OF _ _ IH'] by simp
qed

subsection‹Lemma IV.2.40(b)›
  (* Lemma IV.2.40(b), membership *)
lemma IV240b_mem:
  includes some_rules
  assumes
    "val(G,π)val(G,τ)" "πM" "τM"
    and
    IH:"σ. σdomain(τ)  val(G,π) = val(G,σ) 
      pG. p forcesa (π = σ)" (* inductive hypothesis *)
  shows
    "pG. p forcesa (π  τ)"
proof -
  from val(G,π)val(G,τ)
  obtain σ r where "rG" "σ,rτ" "val(G,π) = val(G,σ)" by auto
  moreover from this and IH
  obtain p' where "p'G" "p' forcesa (π = σ)" by blast
  ultimately
  obtain p where "pr" "pp'" "pG" "p forcesa (π = σ)"
    using M_generic_compatD strengthening_eq[of p'] M_genericD by auto
  moreover from calculation
  have "q forcesa (π = σ)" if "q" "qp" for q
    using that strengthening_eq by blast
  moreover
  note σ,rτ rG
  ultimately
  have "r  σ,r  τ  qr  q forcesa (π = σ)" if "q" "qp" for q
    using that leq_transD[of _ p r] by blast
  then
  have "dense_below({q. s r. r  s,r  τ  qr  q forcesa (π = s)},p)"
    using refl_leq by blast
  moreover
  note pG
  moreover from calculation
  have "p forcesa (π  τ)"
    using forces_mem_iff_dense_below by blast
  ultimately
  show ?thesis by blast
qed

end ― ‹localeG_generic1

context forcing_data1
begin

lemma Collect_forces_eq_in_M:
  assumes "τ  M" "θ  M"
  shows "{p. p forcesa (τ = θ)}  M"
  using assms Collect_in_M[of "forces_eq_fm(1,2,0,3,4)" "[,leq,τ,θ]"]
    arity_forces_eq_fm sats_forces_eq_fm forces_eq_abs forces_eq_fm_type
  by (simp add: union_abs1 Un_commute)

lemma IV240b_eq_Collects:
  assumes "τ  M" "θ  M"
  shows "{p. σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}M" and
    "{p. σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}M"
proof -
  let ?rel_pred="λM x a1 a2 a3 a4.
        σ[M]. u[M]. da3[M]. da4[M]. is_domain(M,a3,da3)  is_domain(M,a4,da4) 
          union(M,da3,da4,u)  σu  is_forces_mem'(M,a1,a2,x,σ,a3) 
          is_forces_nmem'(M,a1,a2,x,σ,a4)"
  let ="Exists(Exists(Exists(Exists(And(domain_fm(7,1),And(domain_fm(8,0),
          And(union_fm(1,0,2),And(Member(3,2),And(forces_mem_fm(5,6,4,3,7),
                              forces_nmem_fm(5,6,4,3,8))))))))))"
  have 1:"σM" if "σ,yδ" "δM" for σ δ y
    using that pair_in_M_iff transitivity[of "σ,y" δ] by simp
  have abs1:"?rel_pred(##M,p,,leq,τ,θ) 
        (σdomain(τ)  domain(θ). forces_mem'(,leq,p,σ,τ)  forces_nmem'(,leq,p,σ,θ))"
    if "pM" for p
    unfolding forces_mem_def forces_nmem_def
    using assms that forces_mem'_abs forces_nmem'_abs
      domain_closed Un_closed
    by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
  have abs2:"?rel_pred(##M,p,,leq,θ,τ)  (σdomain(τ)  domain(θ).
        forces_nmem'(,leq,p,σ,τ)  forces_mem'(,leq,p,σ,θ))" if "pM" for p
    unfolding forces_mem_def forces_nmem_def
    using assms that forces_mem'_abs forces_nmem'_abs
      domain_closed Un_closed
    by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
  have fsats1:"(M,[p,,leq,τ,θ]  )  ?rel_pred(##M,p,,leq,τ,θ)" if "pM" for p
    using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M
      domain_closed Un_closed by simp
  have fsats2:"(M,[p,,leq,θ,τ]  )  ?rel_pred(##M,p,,leq,θ,τ)" if "pM" for p
    using that assms sats_forces_mem_fm sats_forces_nmem_fm zero_in_M
      domain_closed Un_closed by simp
  have fty:"formula" by simp
  have farit:"arity()=5"
    by (simp add:ord_simp_union arity)
  show
    "{p   . σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}  M"
    and "{p   . σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}  M"
    unfolding forces_mem_def
    using abs1 fty fsats1 farit assms forces_nmem
      Collect_in_M[of  "[,leq,τ,θ]"]
    using abs2 fty fsats2 farit assms forces_nmem domain_closed Un_closed
      Collect_in_M[of  "[,leq,θ,τ]"]
    by simp_all
qed

end ― ‹localeforcing_data1

context G_generic1
begin

(* Lemma IV.2.40(b), equality *)
lemma IV240b_eq:
  includes some_rules
  assumes
    "val(G,τ) = val(G,θ)" "τM" "θM"
    and
    IH:"σ. σdomain(τ)domain(θ) 
      (val(G,σ)val(G,τ)  (qG. q forcesa (σ  τ))) 
      (val(G,σ)val(G,θ)  (qG. q forcesa (σ  θ)))"
    (* inductive hypothesis *)
  shows
    "pG. p forcesa (τ = θ)"
proof -
  let ?D1="{p. p forcesa (τ = θ)}"
  let ?D2="{p. σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}"
  let ?D3="{p. σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)}"
  let ?D="?D1  ?D2  ?D3"
  note assms
  moreover from this
  have "domain(τ)  domain(θ)M" (is "?BM") using domain_closed Un_closed by auto
  moreover from calculation
  have "?D2M" and "?D3M" using IV240b_eq_Collects by simp_all
  ultimately
  have "?DM" using Collect_forces_eq_in_M Un_closed by auto
  moreover
  have "dense(?D)"
  proof
    fix p
    assume "p"
    have "d. (d forcesa (τ = θ) 
            (σdomain(τ)  domain(θ). d forcesa (σ  τ)  d forcesa (σ  θ)) 
            (σdomain(τ)  domain(θ). d forcesa (σ  τ)  d forcesa (σ  θ))) 
           d  p"
    proof (cases "p forcesa (τ = θ)")
      case True
      with p
      show ?thesis using refl_leq by blast
    next
      case False
      moreover note p
      moreover from calculation
      obtain σ q where "σdomain(τ)domain(θ)" "q" "qp"
        "(q forcesa (σ  τ)  ¬ q forcesa (σ  θ)) 
         (¬ q forcesa (σ  τ)  q forcesa (σ  θ))"
        using def_forces_eq by blast
      moreover from this
      obtain r where "rq" "r"
        "(r forcesa (σ  τ)  r forcesa (σ  θ)) 
         (r forcesa (σ  τ)  r forcesa (σ  θ))"
        using not_forces_nmem strengthening_mem by blast
      ultimately
      show ?thesis using leq_transD by blast
    qed
    then
    show "d?D . d  p" by blast
  qed
  moreover
  have "?D  "
    by auto
  ultimately
  obtain p where "pG" "p?D"
    using M_generic_denseD[of ?D] by blast
  then
  consider
    (1) "p forcesa (τ = θ)" |
    (2) "σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)" |
    (3) "σdomain(τ)  domain(θ). p forcesa (σ  τ)  p forcesa (σ  θ)"
    by blast
  then
  show ?thesis
  proof (cases)
    case 1
    with pG
    show ?thesis by blast
  next
    case 2
    then
    obtain σ where "σdomain(τ)  domain(θ)" "p forcesa (σ  τ)" "p forcesa (σ  θ)"
      by blast
    moreover from this and pG and assms
    have "val(G,σ)val(G,τ)"
      using IV240a[of σ τ] transitivity[OF _ domain_closed[simplified]] by force
    moreover note val(G,τ) = _
    ultimately
    obtain q where "qG" "q forcesa (σ  θ)" 
      using IH[OF σ_]
      by auto
    moreover from this and pG
    obtain r where "r" "rp" "rq"
      by blast
    ultimately
    have "r forcesa (σ  θ)"
      using strengthening_mem by blast
    with rp p forcesa (σ  θ) r
    have "False"
      unfolding forces_nmem_def by blast
    then
    show ?thesis by simp
  next (* copy-paste from case 2 mutatis mutandis*)
    case 3
    then
    obtain σ where "σdomain(τ)  domain(θ)" "p forcesa (σ  θ)" "p forcesa (σ  τ)"
      by blast
    moreover from this and pG and assms
    have "val(G,σ)val(G,θ)"
      using IV240a[of σ θ] transitivity[OF _ domain_closed[simplified]] by force
    moreover note val(G,τ) = _
    ultimately
    obtain q where "qG" "q forcesa (σ  τ)" 
      using IH[OF σ_]
      by auto
    moreover from this and pG
    obtain r where "r" "rp" "rq"
      by blast
    ultimately
    have "r forcesa (σ  τ)"
      using strengthening_mem by blast
    with rp p forcesa (σ  τ) r
    have "False"
      unfolding forces_nmem_def by blast
    then
    show ?thesis by simp
  qed
qed

(* Lemma IV.2.40(b), full *)
lemma IV240b:
    "(τMθMval(G,τ) = val(G,θ)  (pG. p forcesa (τ = θ))) 
     (τMθMval(G,τ)  val(G,θ)  (pG. p forcesa (τ  θ)))"
    (is "?Q(τ,θ)  ?R(τ,θ)")
proof (intro forces_induction)
  fix τ θ p
  assume "σdomain(θ)  ?Q(τ, σ)" for σ
  then  show "?R(τ, θ)"
    using IV240b_mem domain_closed transitivity by simp
next
  fix τ θ p
  assume "σ  domain(τ)  domain(θ)  ?R(σ,τ)  ?R(σ,θ)" for σ
  moreover from this
  have IH':"τM  θM  σ  domain(τ)  domain(θ) 
          (val(G, σ)  val(G, τ)  (qG. q forcesa (σ  τ))) 
          (val(G, σ)  val(G, θ)  (qG. q forcesa (σ  θ)))" for σ
    using domain_trans[OF trans_M]
    by blast
  ultimately
  show "?Q(τ,θ)"
    using IV240b_eq by auto
qed

lemma truth_lemma_mem:
  assumes
    "envlist(M)"
    "nnat" "mnat" "n<length(env)" "m<length(env)"
  shows
    "(pG. p  Member(n,m) env)    M[G], map(val(G),env)  Member(n,m)"
  using assms IV240a[of "nth(n,env)" "nth(m,env)"]
    IV240b[of "nth(n,env)" "nth(m,env)"]
    M_genericD
    Forces_Member[of _  "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
  by auto

lemma truth_lemma_eq:
  assumes
    "envlist(M)"
    "nnat" "mnat" "n<length(env)" "m<length(env)"
  shows
    "(pG. p  Equal(n,m) env)    M[G], map(val(G),env)  Equal(n,m)"
  using assms IV240a(1)[of "nth(n,env)" "nth(m,env)"]
    IV240b(1)[of "nth(n,env)" "nth(m,env)"]
    M_genericD
    Forces_Equal[of _  "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
  by auto

end ― ‹localeG_generic1

lemma arities_at_aux:
  assumes
    "n  nat" "m  nat" "env  list(M)" "succ(n)  succ(m)  length(env)"
  shows
    "n < length(env)" "m < length(env)"
  using assms succ_leE[OF Un_leD1, of n "succ(m)" "length(env)"]
    succ_leE[OF Un_leD2, of "succ(n)" m "length(env)"] by auto

subsection‹The Strenghtening Lemma›

context forcing_data1
begin

lemma strengthening_lemma:
  assumes
    "p" "φformula" "r" "rp"
    "envlist(M)" "arity(φ)length(env)"
  shows
    "p  φ env  r  φ env"
  using assms(2-)
proof (induct arbitrary:env)
  case (Member n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "envlist(M)"
  moreover
  note assms Member
  ultimately
  show ?case
    using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m]
      strengthening_mem[of p r "nth(n,env)" "nth(m,env)"] by simp
next
  case (Equal n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "envlist(M)"
  moreover
  note assms Equal
  ultimately
  show ?case
    using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m]
      strengthening_eq[of p r "nth(n,env)" "nth(m,env)"] by simp
next
  case (Nand φ ψ)
  with assms
  show ?case
    using Forces_Nand transitivity[OF _ P_in_M] pair_in_M_iff
      transitivity[OF _ leq_in_M] leq_transD by auto
next
  case (Forall φ)
  with assms
  have "p  φ ([x] @ env)" if "xM" for x
    using that Forces_Forall by simp
  with Forall
  have "r  φ ([x] @ env)" if "xM" for x
    using that pred_le2 by (simp)
  with assms Forall
  show ?case
    using Forces_Forall by simp
qed

subsection‹The Density Lemma›

lemma arity_Nand_le:
  assumes "φ  formula" "ψ  formula" "arity(Nand(φ, ψ))  length(env)" "envlist(A)"
  shows "arity(φ)  length(env)" "arity(ψ)  length(env)"
  using assms
  by (rule_tac Un_leD1, rule_tac [5] Un_leD2, auto)

lemma dense_below_imp_forces:
  assumes
    "p" "φformula"
    "envlist(M)" "arity(φ)length(env)"
  shows
    "dense_below({q. (q  φ env)},p)  (p  φ env)"
  using assms(2-)
proof (induct arbitrary:env)
  case (Member n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "envlist(M)"
  moreover
  note assms Member
  ultimately
  show ?case
    using Forces_Member[of _ "nth(n,env)" "nth(m,env)" env n m]
      density_mem[of p "nth(n,env)" "nth(m,env)"] by simp
next
  case (Equal n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "envlist(M)"
  moreover
  note assms Equal
  ultimately
  show ?case
    using Forces_Equal[of _ "nth(n,env)" "nth(m,env)" env n m]
      density_eq[of p "nth(n,env)" "nth(m,env)"] by simp
next
  case (Nand φ ψ)
  {
    fix q
    assume "qM" "q" "q p" "q  φ env"
    moreover
    note Nand
    moreover from calculation
    obtain d where "d" "d  Nand(φ, ψ) env" "d q"
      using dense_belowI by auto
    moreover from calculation
    have "¬(d ψ env)" if "d  φ env"
      using that Forces_Nand refl_leq transitivity[OF _ P_in_M, of d] by auto
    moreover
    note arity_Nand_le[of φ ψ]
    moreover from calculation
    have "d  φ env"
      using strengthening_lemma[of q φ d env] Un_leD1 by auto
    ultimately
    have "¬ (q  ψ env)"
      using strengthening_lemma[of q ψ d env] by auto
  }
  with p
  show ?case
    using Forces_Nand[symmetric, OF _ Nand(6,1,3)] by blast
next
  case (Forall φ)
  have "dense_below({q. q  φ ([a]@env)},p)" if "aM" for a
  proof
    fix r
    assume "r" "rp"
    with dense_below(_,p)
    obtain q where "q" "qr" "q  Forall(φ) env"
      by blast
    moreover
    note Forall aM
    moreover from calculation
    have "q  φ ([a]@env)"
      using Forces_Forall by simp
    ultimately
    show "d  {q. q  φ ([a]@env)}. d    dr"
      by auto
  qed
  moreover
  note Forall(2)[of "Cons(_,env)"] Forall(1,3-5)
  ultimately
  have "p  φ ([a]@env)" if "aM" for a
    using that pred_le2 by simp
  with assms Forall
  show ?case using Forces_Forall by simp
qed

lemma density_lemma:
  assumes
    "p" "φformula" "envlist(M)" "arity(φ)length(env)"
  shows
    "p  φ env      dense_below({q. (q  φ env)},p)"
proof
  assume "dense_below({q. (q  φ env)},p)"
  with assms
  show  "(p  φ env)"
    using dense_below_imp_forces by simp
next
  assume "p  φ env"
  with assms
  show "dense_below({q. q  φ env},p)"
    using strengthening_lemma refl_leq by auto
qed

subsection‹The Truth Lemma›

lemma Forces_And:
  assumes
    "p" "env  list(M)" "φformula" "ψformula"
    "arity(φ)  length(env)" "arity(ψ)  length(env)"
  shows
    "p  And(φ,ψ) env     (p  φ env)  (p  ψ env)"
proof
  assume "p  And(φ, ψ) env"
  with assms
  have "dense_below({r   . (r  φ env)  (r  ψ env)}, p)"
    using Forces_And_iff_dense_below by simp
  then
  have "dense_below({r   . (r  φ env)}, p)" "dense_below({r   . (r  ψ env)}, p)"
    by blast+
  with assms
  show "(p  φ env)  (p  ψ env)"
    using density_lemma[symmetric] by simp
next
  assume "(p  φ env)  (p  ψ env)"
  have "dense_below({r   . (r  φ env)  (r  ψ env)}, p)"
  proof (intro dense_belowI bexI conjI, assumption)
    fix q
    assume "q" "q p"
    with assms (p  φ env)  (p  ψ env)
    show "q{r   . (r  φ env)  (r  ψ env)}" "q q"
      using strengthening_lemma refl_leq by auto
  qed
  with assms
  show "p  And(φ,ψ) env"
    using Forces_And_iff_dense_below by simp
qed

lemma Forces_Nand_alt:
  assumes
    "p" "env  list(M)" "φformula" "ψformula"
    "arity(φ)  length(env)" "arity(ψ)  length(env)"
  shows
    "(p  Nand(φ,ψ) env)  (p  Neg(And(φ,ψ)) env)"
  using assms Forces_Nand Forces_And Forces_Neg by auto

end

context G_generic1
begin

lemma  truth_lemma_Neg:
  assumes
    "φformula" "envlist(M)" "arity(φ)length(env)" and
    IH: "(pG. p  φ env)  M[G], map(val(G),env)  φ"
  shows
    "(pG. p  Neg(φ) env)    M[G], map(val(G),env)  Neg(φ)"
proof (intro iffI, elim bexE, rule ccontr)
  (* Direct implication by contradiction *)
  fix p
  assume "pG" "p  Neg(φ) env" "¬(M[G],map(val(G),env)  Neg(φ))"
  moreover
  note assms
  moreover from calculation
  have "M[G], map(val(G),env)  φ" "p"
    using map_val_in_MG by auto
  with IH
  obtain r where "r  φ env" "rG" "r" by blast
  moreover from this and pG
  obtain q where "qp" "qr" "qG" "q" "qM"
    using transitivity[OF _ P_in_M]
    by blast
  moreover from calculation
  have "q  φ env"
    using strengthening_lemma
    by simp
  with assms p  _ _ qp qM p q
   show "False"
    using Forces_Neg
    by auto
next
  assume "M[G], map(val(G),env)  Neg(φ)"
  with assms
  have "¬ (M[G], map(val(G),env)  φ)"
    using map_val_in_MG by simp
  let ?D="{p. (p  φ env)  (p  Neg(φ) env)}"
  from assms
  have "?D  M"
    using separation_disj separation_closed separation_forces by simp
  moreover
  have "?D  " by auto
  moreover
  have "dense(?D)"
  proof
    fix q
    assume "q"
    with assms
    show "d{p   . (p  φ env)  (p  Neg(φ) env)}. d q"
      using refl_leq Forces_Neg by (cases "q  Neg(φ) env", auto)
  qed
  ultimately
  obtain p where "pG" "(p  φ env)  (p  Neg(φ) env)"
    by blast
  then
  consider (1) "p  φ env" | (2) "p  Neg(φ) env" by blast
  then
  show "pG. (p  Neg(φ) env)"
  proof (cases)
    case 1
    with ¬ (M[G],map(val(G),env)  φ) pG IH
    show ?thesis
      by blast
  next
    case 2
    with pG
    show ?thesis by blast
  qed
qed

lemma truth_lemma_And:
  assumes
    "envlist(M)" "φformula" "ψformula"
    "arity(φ)length(env)" "arity(ψ)  length(env)"
    and
    IH: "(pG. p  φ env)     M[G], map(val(G),env)  φ"
    "(pG. p  ψ env)     M[G], map(val(G),env)  ψ"
  shows
    "(pG. (p  And(φ,ψ) env))  M[G] , map(val(G),env)  And(φ,ψ)"
  using assms map_val_in_MG Forces_And[OF M_genericD assms(1-5)]
proof (intro iffI, elim bexE)
  fix p
  assume "pG" "p  And(φ,ψ) env"
  with assms
  show "M[G], map(val(G),env)  And(φ,ψ)"
    using Forces_And[of  _ _ φ ψ] map_val_in_MG M_genericD by auto
next
  assume "M[G], map(val(G),env)  And(φ,ψ)"
  moreover
  note assms
  moreover from calculation
  obtain q r where "q  φ env" "r  ψ env" "qG" "rG" "r" "q"
    using map_val_in_MG Forces_And[OF M_genericD assms(1-5)] M_genericD by auto
  moreover from calculation
  obtain p where "pq" "pr" "pG"
    by auto
  moreover from calculation
  have "(p  φ env)  (p  ψ env)" (* can't solve as separate goals *)
    using strengthening_lemma[OF M_genericD] by force
  ultimately
  show "pG. (p  And(φ,ψ) env)"
    using Forces_And[OF M_genericD assms(1-5)] by auto
qed

end

definition
  ren_truth_lemma :: "ii" where
  "ren_truth_lemma(φ) 
    Exists(Exists(Exists(Exists(Exists(
    And(Equal(0,5),And(Equal(1,8),And(Equal(2,9),And(Equal(3,10),And(Equal(4,6),
    iterates(λp. incr_bv(p)`5 , 6, φ)))))))))))"

lemma ren_truth_lemma_type[TC] :
  "φformula  ren_truth_lemma(φ) formula"
  unfolding ren_truth_lemma_def
  by simp

lemma arity_ren_truth :
  assumes "φformula"
  shows "arity(ren_truth_lemma(φ))  6  succ(arity(φ))"
proof -
  consider (lt) "5 <arity(φ)" | (ge) "¬ 5 < arity(φ)"
    by auto
  then
  show ?thesis
  proof cases
    case lt
    consider (a) "5<arity(φ)+ω5"  | (b) "arity(φ)+ω5  5"
      using not_lt_iff_le φ_ by force
    then
    show ?thesis
    proof cases
      case a
      with φ_ lt
      have "5 < succ(arity(φ))" "5<arity(φ)+ω2"  "5<arity(φ)+ω3"  "5<arity(φ)+ω4"
        using succ_ltI by auto
      with φ_
      have c:"arity(iterates(λp. incr_bv(p)`5,5,φ)) = 5+ωarity(φ)" (is "arity(?φ') = _")
        using arity_incr_bv_lemma lt a
        by simp
      with φ_
      have "arity(incr_bv(?φ')`5) = 6+ωarity(φ)"
        using arity_incr_bv_lemma[of ?φ' 5] a by auto
      with φ_
      show ?thesis
        unfolding ren_truth_lemma_def
        using pred_Un_distrib union_abs1 Un_assoc[symmetric] a c union_abs2
        by (simp add:arity)
    next
      case b
      with φ_ lt
      have "5 < succ(arity(φ))" "5<arity(φ)+ω2"  "5<arity(φ)+ω3"  "5<arity(φ)+ω4" "5<arity(φ)+ω5"
        using succ_ltI by auto
      with φ_
      have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = 6+ωarity(φ)" (is "arity(?φ') = _")
        using arity_incr_bv_lemma lt
        by simp
      with φ_
      show ?thesis
        unfolding ren_truth_lemma_def
        using pred_Un_distrib union_abs1 Un_assoc[symmetric]  union_abs2
        by (simp add:arity)
    qed
  next
    case ge
    with φ_
    have "arity(φ)  5" "pred^5(arity(φ))  5"
      using not_lt_iff_le le_trans[OF le_pred]
      by auto
    with φ_
    have "arity(iterates(λp. incr_bv(p)`5,6,φ)) = arity(φ)" "arity(φ)6" "pred^5(arity(φ))  6"
      using arity_incr_bv_lemma ge le_trans[OF arity(φ)5] le_trans[OF pred^5(arity(φ))5]
      by auto
    with arity(φ)  5 φ_ pred^5(_)  5
    show ?thesis
      unfolding ren_truth_lemma_def
      using  pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2
      by (simp add:arity)
  qed
qed

lemma sats_ren_truth_lemma:
  "[q,b,d,a1,a2,a3] @ env  list(M)  φ  formula 
   (M, [q,b,d,a1,a2,a3] @ env  ren_truth_lemma(φ) ) 
   (M, [q,a1,a2,a3,b] @ env  φ)"
  unfolding ren_truth_lemma_def
  by (insert sats_incr_bv_iff [of _ _ M _ "[q,a1,a2,a3,b]"], simp)

context forcing_data1
begin

lemma truth_lemma' :
  assumes
    "φformula" "envlist(M)" "arity(φ)  succ(length(env))"
  shows
    "separation(##M,λd. bM. q. qd  ¬(q  φ ([b]@env)))"
proof -
  let ?rel_pred="λM x a1 a2 a3. bM. qM. qa1  is_leq(##M,a2,q,x) 
                  ¬(M, [q,a1,a2,a3,b] @ env  forces(φ))"
  let ="Exists(Forall(Implies(And(Member(0,3),is_leq_fm(4,0,2)),
          Neg(ren_truth_lemma(forces(φ))))))"
  have "qM" if "q" for q using that transitivity[OF _ P_in_M] by simp
  then
  have 1:"qM. q  R(q)  Q(q)  (q. R(q)  Q(q))" for R Q
    by auto
  then
  have "b  M; qM. q    q  d  ¬(q  φ ([b]@env)) 
         cM. q. q  d  ¬(q  φ ([c]@env))" for b d
    by (rule bexI,simp_all)
  then
  have "?rel_pred(M,d,,leq,𝟭)  (bM. q. qd  ¬(q  φ ([b]@env)))" if "dM" for d
    using that leq_abs assms
    by auto
  moreover
  have "formula" using assms by simp
  moreover
  have "(M, [d,,leq,𝟭]@env  )  ?rel_pred(M,d,,leq,𝟭)" if "dM" for d
    using assms that sats_is_leq_fm sats_ren_truth_lemma zero_in_M
    by simp
  moreover
  have "arity()  4+ωlength(env)"
  proof -
    have eq:"arity(is_leq_fm(4, 0, 2)) = 5"
      using arity_is_leq_fm succ_Un_distrib ord_simp_union
      by simp
    with φ_
    have "arity() = 3  (pred^2(arity(ren_truth_lemma(forces(φ)))))"
      using union_abs1 pred_Un_distrib by (simp add:arity)
    moreover
    have "...  3  (pred(pred(6  succ(arity(forces(φ))))))" (is "_  ?r")
      using  φ_ Un_le_compat[OF le_refl[of 3]]
        le_imp_subset arity_ren_truth[of "forces(φ)"]
        pred_mono
      by auto
    finally
    have "arity()  ?r" by simp
    have i:"?r  4  pred(arity(forces(φ)))"
      using pred_Un_distrib pred_succ_eq φ_ Un_assoc[symmetric] union_abs1 by simp
    have h:"4  pred(arity(forces(φ)))  4  (4+ωlength(env))"
      using  env_ add_commute φ_
        Un_le_compat[of 4 4,OF _ pred_mono[OF _ arity_forces_le[OF _ _ arity(φ)_]] ]
        env_ by auto
    with φ_ env_
    show ?thesis
      using le_trans[OF  arity()  ?r  le_trans[OF i h]] ord_simp_union by simp
  qed
  ultimately
  show ?thesis using assms
      separation_ax[of "" "[,leq,𝟭]@env"]
      separation_cong[of "##M" "λy. (M, [y,,leq,𝟭]@env )"]
    by simp
qed

end

context G_generic1
begin

lemma truth_lemma:
  assumes
    "φformula"
    "envlist(M)" "arity(φ)length(env)"
  shows
    "(pG. p  φ env)      M[G], map(val(G),env)  φ"
  using assms
proof (induct arbitrary:env)
  case (Member x y)
  then
  show ?case
    using truth_lemma_mem[OF envlist(M) xnat ynat] arities_at_aux 
    by simp
next
  case (Equal x y)
  then
  show ?case
    using truth_lemma_eq[OF envlist(M) xnat ynat] arities_at_aux by simp
next
  case (Nand φ ψ)
  then
  show ?case
    using truth_lemma_And truth_lemma_Neg[of "φ  ψ"] Forces_Nand_alt
      M_genericD map_val_in_MG arity_Nand_le[of φ ψ] FOL_arities by auto
next
  case (Forall φ)
  then
  show ?case
  proof (intro iffI)
    assume "pG. (p  Forall(φ) env)"
    then
    obtain p where "pG" "pM" "p" "p  Forall(φ) env"
      using transitivity[OF _ P_in_M] by auto
    with envlist(M) φformula
    have "p  φ ([x]@env)" if "xM" for x
      using that Forces_Forall by simp
    with pG φformula env_ arity(Forall(φ))  length(env)
      Forall(2)[of "Cons(_,env)"]
    show "M[G], map(val(G),env)   Forall(φ)"
      using pred_le2 map_val_in_MG
      by (auto iff:GenExt_iff)
  next
    assume "M[G], map(val(G),env)  Forall(φ)"
    let ?D1="{d. (d  Forall(φ) env)}"
    let ?D2="{d. bM. q. qd  ¬(q  φ ([b]@env))}"
    define D where "D  ?D1  ?D2"
    note arity(Forall(φ))  length(env) φformula envlist(M)
    moreover from this
    have arφ:"arity(φ)succ(length(env))"
      using pred_le2 by simp
    moreover from calculation
    have "?D1M" using Collect_forces  by simp
    moreover from envlist(M) φformula
    have "?D2M"
      using truth_lemma'[of φ] separation_closed arφ
      by simp
    ultimately
    have "DM" unfolding D_def using Un_closed by simp
    moreover
    have "D  " unfolding D_def by auto
    moreover
    have "dense(D)"
    proof
      fix p
      assume "p"
      show "dD. d p"
      proof (cases "p  Forall(φ) env")
        case True
        with p
        show ?thesis unfolding D_def using refl_leq by blast
      next
        case False
        with Forall p
        obtain b where "bM" "¬(p  φ ([b]@env))"
          using Forces_Forall by blast
        moreover from this p Forall
        have "¬dense_below({q. q  φ ([b]@env)},p)"
          using density_lemma pred_le2  by auto
        moreover from this
        obtain d where "dp" "q. qd  ¬(q  φ ([b] @ env))"
          "d" by blast
        ultimately
        show ?thesis unfolding D_def by auto
      qed
    qed
    moreover
    note generic
    ultimately
    obtain d where "d  D" "d  G" by blast
    then
    consider (1) "d?D1" | (2) "d?D2" unfolding D_def by blast
    then
    show "pG. (p  Forall(φ) env)"
    proof (cases)
      case 1
      with dG
      show ?thesis by blast
    next
      case 2
      then
      obtain b where "bM" "q. qd ¬(q  φ ([b] @ env))"
        by blast
      moreover from this(1) and  M[G], _   Forall(φ) and
        Forall(2)[of "Cons(b,env)"] Forall(1,3-)
      obtain p where "pG" "p" "p  φ ([b] @ env)"
        using pred_le2 map_val_in_MG M_genericD by (auto iff:GenExt_iff)
      moreover
      note dG
      ultimately
      obtain q where "qG" "q" "qd" "qp"
        using M_genericD by force
      moreover from this and  p  φ ([b] @ env)
        Forall  bM p
      have "q  φ ([b] @ env)"
        using pred_le2 strengthening_lemma by simp
      moreover
      note q. qd ¬(q  φ ([b] @ env))
      ultimately
      show ?thesis by simp
    qed
  qed
qed

end

context forcing_data1
begin

subsection‹The ``Definition of forcing''›
lemma definition_of_forcing:
  assumes
    "p" "φformula" "envlist(M)" "arity(φ)length(env)"
  shows
    "(p  φ env) 
     (G. M_generic(G)  pG  M[G], map(val(G),env)  φ)"
proof (intro iffI allI impI, elim conjE)
  fix G
  assume "(p  φ env)" "M_generic(G)" "p  G"
  moreover from this
  interpret G_generic1  leq 𝟭 M enum G 
    by (unfold_locales,simp)
  from calculation assms
  show "M[G], map(val(G),env)  φ"
    using truth_lemma[of φ] by auto
next
  assume 1: "G.(M_generic(G) pG)  M[G] , map(val(G),env)  φ"
  {
    fix r
    assume 2: "r" "rp"
    then
    obtain G where "rG" "M_generic(G)"
      text‹Here we're using countability (via the existence of
        generic filters) of termM as a shortcut.›
      using generic_filter_existence by auto
    moreover from this
    interpret G_generic1  leq 𝟭 M enum G 
      by (unfold_locales,simp)
    from calculation 2 p
    have "pG"
      using filter_leqD by auto
    moreover note 1
    ultimately
    have "M[G], map(val(G),env)  φ"
      by simp
    moreover
    note assms
    moreover from calculation
    obtain s where "sG" "(s  φ env)"
      using truth_lemma[of φ] by blast
    moreover from this rG
    obtain q where "qG" "qs" "qr" "s" "q"
      by blast
    ultimately
    have "q. qr  (q  φ env)"
      using strengthening_lemma[of s] by auto
  }
  then
  have "dense_below({q. (q  φ env)},p)"
    unfolding dense_below_def by blast
  with assms
  show "(p  φ env)"
    using density_lemma by blast
qed

lemmas definability = forces_type

end ― ‹localeforcing_data1

end