Theory Forcing_Theorems

section‹The Forcing Theorems›

theory Forcing_Theorems
  imports
    Forces_Definition

begin

context forcing_data
begin

subsection‹The forcing relation in context›

abbreviation Forces :: "[i, i, i] ⇒ o"  ("_ ⊩ _ _" [36,36,36] 60) where
  "p ⊩ φ env   ≡   M, ([p,P,leq,one] @ env) ⊨ forces(φ)"

lemma Collect_forces :
  assumes 
    fty: "φ∈formula" and
    far: "arity(φ)≤length(env)" and
    envty: "env∈list(M)"
  shows
    "{p∈P . p ⊩ φ env} ∈ M"
proof -
  have "z∈P ⟹ z∈M" for z
    using P_in_M transitivity[of z P] by simp
  moreover
  have "separation(##M,λp. (p ⊩ φ env))"
        using separation_ax arity_forces far fty P_in_M leq_in_M one_in_M envty arity_forces_le
    by simp
  then 
  have "Collect(P,λp. (p ⊩ φ env))∈M"
    using separation_closed P_in_M by simp
  then show ?thesis by simp
qed

lemma forces_mem_iff_dense_below:  "p∈P ⟹ forces_mem(p,t1,t2) ⟷ dense_below(
    {q∈P. ∃s. ∃r. r∈P ∧ ⟨s,r⟩ ∈ t2 ∧ q≼r ∧ forces_eq(q,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∈P" "r∈P" "r≼p" "forces_eq(p,t1,t2)"
  shows "forces_eq(r,t1,t2)"
  using assms def_forces_eq[of _ t1 t2] leq_transD by blast
(* Long proof *)
(*
proof -
  {
    fix s q
    assume "q≼ r" "q∈P"
    with assms
    have "q≼p"
      using leq_preord unfolding preorder_on_def trans_on_def by blast
    moreover 
    note ‹q∈P› assms
    moreover
    assume "s∈domain(t1) ∪ domain(t2)" 
    ultimately
    have "forces_mem(q, s, t1) ⟷ forces_mem(q, s, t2)"
      using def_forces_eq[of p t1 t2] by simp
  }
  with ‹r∈P›
  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∈P" "r∈P" "r≼p" "forces_mem(p,t1,t2)"
  shows "forces_mem(r,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∈P"
  shows "forces_mem(p,t1,t2)  ⟷ dense_below({q∈P. forces_mem(q,t1,t2)},p)"
proof
  assume "forces_mem(p,t1,t2)"
  with assms
  show "dense_below({q∈P. forces_mem(q,t1,t2)},p)"
    using forces_mem_iff_dense_below strengthening_mem[of p] ideal_dense_below by auto
next
  assume "dense_below({q ∈ P . forces_mem(q, t1, t2)}, p)"
  with assms
  have "dense_below({q∈P. 
    dense_below({q'∈P. ∃s r. r ∈ P ∧ ⟨s,r⟩∈t2 ∧ q'≼r ∧ forces_eq(q',t1,s)},q)
    },p)"
    using forces_mem_iff_dense_below by simp
  with assms
  show "forces_mem(p,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'∈P. ∀q. q∈P ∧ q≼q' ⟶ forces_mem(q,s,t1) ⟷ forces_mem(q,s,t2)}
    ,p)"
    "forces_mem(q,s,t1)" "q∈P" "p∈P" "q≼p"
  shows
    "dense_below({r∈P. forces_mem(r,s,t2)},q)"
proof
  fix r
  assume "r∈P" "r≼q"
  moreover from this and ‹p∈P› ‹q≼p› ‹q∈P›
  have "r≼p"
    using leq_transD by simp
  moreover
  note ‹forces_mem(q,s,t1)› ‹dense_below(_,p)› ‹q∈P›
  ultimately
  obtain q1 where "q1≼r" "q1∈P" "forces_mem(q1,s,t2)"
    using strengthening_mem[of q _ s t1] refl_leq leq_transD[of _ r q] by blast
  then
  show "∃d∈{r ∈ P . forces_mem(r, s, t2)}. d ∈ P ∧ d≼ r"
    by blast
qed

(* Kunen 2013, Lemma IV.2.37(b) *)
lemma density_eq:
  assumes "p∈P"
  shows "forces_eq(p,t1,t2)  ⟷ dense_below({q∈P. forces_eq(q,t1,t2)},p)"
proof
  assume "forces_eq(p,t1,t2)"
  with ‹p∈P›
  show "dense_below({q∈P. forces_eq(q,t1,t2)},p)"
    using strengthening_eq ideal_dense_below by auto
next
  assume "dense_below({q∈P. forces_eq(q,t1,t2)},p)"
  {
    fix s q 
    let ?D1="{q'∈P. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ P ∧ q≼q' ⟶
           forces_mem(q,s,t1)⟷forces_mem(q,s,t2)}"
    let ?D2="{q'∈P. ∀q. q∈P ∧ q≼q' ⟶ forces_mem(q,s,t1) ⟷ forces_mem(q,s,t2)}"
    assume "s∈domain(t1) ∪ domain(t2)" 
    then
    have "?D1⊆?D2" by blast
    with ‹dense_below(_,p)›
    have "dense_below({q'∈P. ∀s∈domain(t1) ∪ domain(t2). ∀q. q ∈ P ∧ q≼q' ⟶
           forces_mem(q,s,t1)⟷forces_mem(q,s,t2)},p)"
      using dense_below_cong'[OF ‹p∈P› def_forces_eq[of _ t1 t2]] by simp
    with ‹p∈P› ‹?D1⊆?D2›
    have "dense_below({q'∈P. ∀q. q∈P ∧ q≼q' ⟶ 
            forces_mem(q,s,t1) ⟷ forces_mem(q,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'∈P. ∀q. q∈P ∧ q≼q' ⟶ 
            forces_mem(q,s,t2) ⟷ forces_mem(q,s,t1)},p)"
      by blast
    moreover
    assume "q ∈ P" "q≼p"
    moreover
    note ‹p∈P›
    ultimately (*We can omit the next step but it is slower *)
    have "forces_mem(q,s,t1) ⟹ dense_below({r∈P. forces_mem(r,s,t2)},q)"
         "forces_mem(q,s,t2) ⟹ dense_below({r∈P. forces_mem(r,s,t1)},q)" 
      using aux_density_eq by simp_all
    then
    have "forces_mem(q, s, t1) ⟷ forces_mem(q, s, t2)"
      using density_mem[OF ‹q∈P›] by blast
  }
  with ‹p∈P›
  show "forces_eq(p,t1,t2)" using def_forces_eq by blast
qed

subsection‹Kunen 2013, Lemma IV.2.38›
lemma not_forces_neq:
  assumes "p∈P"
  shows "forces_eq(p,t1,t2) ⟷ ¬ (∃q∈P. q≼p ∧ forces_neq(q,t1,t2))"
  using assms density_eq unfolding forces_neq_def by blast


lemma not_forces_nmem:
  assumes "p∈P"
  shows "forces_mem(p,t1,t2) ⟷ ¬ (∃q∈P. q≼p ∧ forces_nmem(q,t1,t2))"
  using assms density_mem unfolding forces_nmem_def by blast


(* Use the newer versions in Forces_Definition! *)
(* (and adequate the rest of the code to them)  *)

lemma sats_forces_Nand':
  assumes
    "p∈P" "φ∈formula" "ψ∈formula" "env ∈ list(M)" 
  shows
    "M, [p,P,leq,one] @ env ⊨ forces(Nand(φ,ψ)) ⟷ 
     ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧ 
           M, [q,P,leq,one] @ env ⊨ forces(φ) ∧ 
           M, [q,P,leq,one] @ env ⊨ forces(ψ))"
  using assms sats_forces_Nand[OF assms(2-4) transitivity[OF ‹p∈P›]]
  P_in_M leq_in_M one_in_M unfolding forces_def
  by simp

lemma sats_forces_Neg':
  assumes
    "p∈P" "env ∈ list(M)" "φ∈formula"
  shows
    "M, [p,P,leq,one] @ env ⊨ forces(Neg(φ))   ⟷ 
     ¬(∃q∈M. q∈P ∧ is_leq(##M,leq,q,p) ∧ 
          M, [q,P,leq,one]@env ⊨ forces(φ))"
  using assms sats_forces_Neg transitivity 
  P_in_M leq_in_M one_in_M  unfolding forces_def
  by (simp, blast)

lemma sats_forces_Forall':
  assumes
    "p∈P" "env ∈ list(M)" "φ∈formula"
  shows
    "M,[p,P,leq,one] @ env ⊨ forces(Forall(φ)) ⟷ 
     (∀x∈M.   M, [p,P,leq,one,x] @ env ⊨ forces(φ))"
  using assms sats_forces_Forall transitivity 
  P_in_M leq_in_M one_in_M sats_ren_forces_forall unfolding forces_def
  by simp

subsection‹The relation of forcing and atomic formulas›
lemma Forces_Equal:
  assumes
    "p∈P" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat" 
  shows
    "(p ⊩ Equal(n,m) env) ⟷ forces_eq(p,t1,t2)"
   using assms sats_forces_Equal forces_eq_abs transitivity P_in_M 
  by simp

lemma Forces_Member:
  assumes
    "p∈P" "t1∈M" "t2∈M" "env∈list(M)" "nth(n,env) = t1" "nth(m,env) = t2" "n∈nat" "m∈nat" 
  shows
    "(p ⊩ Member(n,m) env) ⟷ forces_mem(p,t1,t2)"
   using assms sats_forces_Member forces_mem_abs transitivity P_in_M
  by simp

lemma Forces_Neg:
  assumes
    "p∈P" "env ∈ list(M)" "φ∈formula" 
  shows
    "(p ⊩ Neg(φ) env) ⟷ ¬(∃q∈M. q∈P ∧ q≼p ∧ (q ⊩ φ env))"
    using assms sats_forces_Neg' transitivity 
  P_in_M pair_in_M_iff leq_in_M leq_abs by simp
 
subsection‹The relation of forcing and connectives›

lemma Forces_Nand:
  assumes
    "p∈P" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
  shows
    "(p ⊩ Nand(φ,ψ) env) ⟷ ¬(∃q∈M. q∈P ∧ q≼p ∧ (q ⊩ φ env) ∧ (q ⊩ ψ env))"
   using assms sats_forces_Nand' transitivity 
  P_in_M pair_in_M_iff leq_in_M leq_abs by simp

lemma Forces_And_aux:
  assumes
    "p∈P" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
  shows
    "p ⊩ And(φ,ψ) env   ⟷ 
    (∀q∈M. q∈P ∧ q≼p ⟶ (∃r∈M. r∈P ∧ r≼q ∧ (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∈P" "env ∈ list(M)" "φ∈formula" "ψ∈formula"
  shows
    "(p ⊩ And(φ,ψ) env) ⟷ dense_below({r∈P. (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∈P" "env ∈ list(M)" "φ∈formula"
  shows
    "(p ⊩ Forall(φ) env) ⟷ (∀x∈M. (p ⊩ φ ([x] @ env)))"
   using sats_forces_Forall' assms by simp

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

context 
  includes some_rules
begin

lemma elem_of_valI: "∃θ. ∃p∈P. p∈G ∧ ⟨θ,p⟩∈π ∧ val(P,G,θ) = x ⟹ x∈val(P,G,π)"
  by (subst def_val, auto)

lemma GenExtD: "x∈M[G] ⟷ (∃τ∈M. x = val(P,G,τ))"
  unfolding GenExt_def by simp

lemma left_in_M : "tau∈M ⟹ ⟨a,b⟩∈tau ⟹ a∈M"
  using fst_snd_closed[of "⟨a,b⟩"] transitivity by auto


subsection‹Kunen 2013, Lemma IV.2.29›
lemma generic_inter_dense_below: 
  assumes "D∈M" "M_generic(G)" "dense_below(D,p)" "p∈G"
  shows "D ∩ G ≠ 0"
proof -
  let ?D="{q∈P. p⊥q ∨ q∈D}"
  have "dense(?D)"
  proof
    fix r
    assume "r∈P"
    show "∃d∈{q ∈ P . p ⊥ q ∨ q ∈ D}. d ≼ r"
    proof (cases "p ⊥ r")
      case True
      with ‹r∈P›
        (* 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∈P" "s≼p" "s≼r" by blast
      with assms ‹r∈P›
      show ?thesis
        using dense_belowD[OF assms(3), of s] leq_transD[of _ s r]
        by blast
    qed
  qed
  have "?D⊆P" by auto
  (* D∈M *)
  let ?d_fm="Or(Neg(compat_in_fm(1,2,3,0)),Member(0,4))"
  have 1:"p∈M" 
    using ‹M_generic(G)› M_genericD transitivity[OF _ P_in_M]
          ‹p∈G› by simp
  moreover
  have "?d_fm∈formula" by simp
  moreover
  have "arity(?d_fm) = 5" unfolding compat_in_fm_def pair_fm_def upair_fm_def
    by (simp add: nat_union_abs1 Un_commute)
  moreover
  have "(M, [q,P,leq,p,D] ⊨ ?d_fm) ⟷ (¬ is_compat_in(##M,P,leq,p,q) ∨ q∈D)"
    if "q∈M" for q
    using that sats_compat_in_fm P_in_M leq_in_M 1 ‹D∈M› by simp
  moreover
  have "(¬ is_compat_in(##M,P,leq,p,q) ∨ q∈D) ⟷ p⊥q ∨ q∈D" if "q∈M" for q
    unfolding compat_def using that compat_in_abs P_in_M leq_in_M 1 by simp
  ultimately
  have "?D∈M" using Collect_in_M_4p[of ?d_fm _ _ _ _ _"λx y z w h. w⊥x ∨ x∈h"] 
                    P_in_M leq_in_M ‹D∈M› by simp
  note asm = ‹M_generic(G)› ‹dense(?D)› ‹?D⊆P› ‹?D∈M›
  obtain x where "x∈G" "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 and ‹M_generic(G)›
  have "x∈D"
    using M_generic_compatD[OF _ ‹p∈G›, 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 IV240a_mem_Collect:
  assumes
    "π∈M" "τ∈M"
  shows
    "{q∈P. ∃σ. ∃r. r∈P ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ forces_eq(q,π,σ)}∈M"
proof -
  let ?rel_pred= "λM x a1 a2 a3 a4. ∃σ[M]. ∃r[M]. ∃σr[M]. 
                r∈a1 ∧ pair(M,σ,r,σr) ∧ σr∈a4 ∧ 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(leq_fm(5,3,1),forces_eq_fm(4,5,3,6,2))))))))" 
  have "σ∈M ∧ r∈M" if "⟨σ, r⟩ ∈ τ"  for σ r
    using that ‹τ∈M› pair_in_M_iff transitivity[of "⟨σ,r⟩" τ] by simp
  then
  have "?rel_pred(##M,q,P,leq,π,τ) ⟷ (∃σ. ∃r. r∈P ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ forces_eq(q,π,σ))"
    if "q∈M" for q
    unfolding forces_eq_def using assms that P_in_M leq_in_M leq_abs forces_eq'_abs pair_in_M_iff 
    by auto
  moreover
  have "(M, [q,P,leq,π,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,q,P,leq,π,τ)" if "q∈M" for q
    using assms that sats_forces_eq'_fm sats_leq_fm P_in_M leq_in_M by simp
  moreover
  have "?φ∈formula" by simp
  moreover
  have "arity(?φ)=5" 
    unfolding leq_fm_def pair_fm_def upair_fm_def
    using arity_forces_eq_fm by (simp add:nat_simp_union Un_commute)
  ultimately
  show ?thesis 
    unfolding forces_eq_def using P_in_M leq_in_M assms 
        Collect_in_M_4p[of ?φ _ _ _ _ _ 
            "λq a1 a2 a3 a4. ∃σ. ∃r. r∈a1 ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ forces_eq'(a1,a2,q,a3,σ)"] by simp
qed

(* Lemma IV.2.40(a), membership *)
lemma IV240a_mem:
  assumes
    "M_generic(G)" "p∈G" "π∈M" "τ∈M" "forces_mem(p,π,τ)"
    "⋀q σ. q∈P ⟹ q∈G ⟹ σ∈domain(τ) ⟹ forces_eq(q,π,σ) ⟹ 
      val(P,G,π) = val(P,G,σ)" (* inductive hypothesis *)
  shows
    "val(P,G,π)∈val(P,G,τ)"
proof (intro elem_of_valI)
  let ?D="{q∈P. ∃σ. ∃r. r∈P ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ forces_eq(q,π,σ)}"
  from ‹M_generic(G)› ‹p∈G›
  have "p∈P" by blast
  moreover
  note ‹π∈M› ‹τ∈M›
  ultimately
  have "?D ∈ M" using IV240a_mem_Collect by simp
  moreover from assms ‹p∈P›
  have "dense_below(?D,p)"
    using forces_mem_iff_dense_below by simp
  moreover
  note ‹M_generic(G)› ‹p∈G›
  ultimately
  obtain q where "q∈G" "q∈?D" using generic_inter_dense_below by blast
  then
  obtain σ r where "r∈P" "⟨σ,r⟩ ∈ τ" "q≼r" "forces_eq(q,π,σ)" by blast
  moreover from this and ‹q∈G› assms
  have "r ∈ G" "val(P,G,π) = val(P,G,σ)" by blast+
  ultimately
  show "∃ σ. ∃p∈P. p ∈ G ∧ ⟨σ, p⟩ ∈ τ ∧ val(P,G, σ) = val(P,G, π)" by auto
qed

(* Example IV.2.36 (next two lemmas) *)
lemma refl_forces_eq:"p∈P ⟹ forces_eq(p,x,x)"
  using def_forces_eq by simp

lemma forces_memI: "⟨σ,r⟩∈τ ⟹ p∈P ⟹ r∈P ⟹ p≼r ⟹ forces_mem(p,σ,τ)"
  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:
  assumes
    "M_generic(G)" "p∈G" "forces_eq(p,τ,θ)"
    and
    IH:"⋀q σ. q∈P ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ 
        (forces_mem(q,σ,τ) ⟶ val(P,G,σ) ∈ val(P,G,τ)) ∧
        (forces_mem(q,σ,θ) ⟶ val(P,G,σ) ∈ val(P,G,θ))"
(* Strong enough for this case: *)
(*  IH:"⋀q σ. q∈P ⟹ σ∈domain(τ) ⟹ forces_mem(q,σ,θ) ⟹ 
      val(P,G,σ) ∈ val(P,G,θ)" *)
  shows
    "val(P,G,τ) ⊆ val(P,G,θ)"
proof
  fix x
  assume "x∈val(P,G,τ)"
  then
  obtain σ r where "⟨σ,r⟩∈τ" "r∈G" "val(P,G,σ)=x" by blast
  moreover from this and ‹p∈G› ‹M_generic(G)›
  obtain q where "q∈G" "q≼p" "q≼r" by force
  moreover from this and ‹p∈G› ‹M_generic(G)›
  have "q∈P" "p∈P" by blast+
  moreover from calculation and ‹M_generic(G)›
  have "forces_mem(q,σ,τ)"
    using forces_memI by blast
  moreover
  note ‹forces_eq(p,τ,θ)›
  ultimately
  have "forces_mem(q,σ,θ)"
    using def_forces_eq by blast
  with ‹q∈P› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈τ› ‹val(P,G,σ) = x›
  show "x∈val(P,G,θ)" by (blast)
qed

(* Lemma IV.2.40(a), equality, second inclusion--- COPY-PASTE *)
lemma IV240a_eq_2nd_incl:
  assumes
    "M_generic(G)" "p∈G" "forces_eq(p,τ,θ)"
    and
    IH:"⋀q σ. q∈P ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ 
        (forces_mem(q,σ,τ) ⟶ val(P,G,σ) ∈ val(P,G,τ)) ∧
        (forces_mem(q,σ,θ) ⟶ val(P,G,σ) ∈ val(P,G,θ))"
  shows
    "val(P,G,θ) ⊆ val(P,G,τ)"
proof
  fix x
  assume "x∈val(P,G,θ)"
  then
  obtain σ r where "⟨σ,r⟩∈θ" "r∈G" "val(P,G,σ)=x" by blast
  moreover from this and ‹p∈G› ‹M_generic(G)›
  obtain q where "q∈G" "q≼p" "q≼r" by force
  moreover from this and ‹p∈G› ‹M_generic(G)›
  have "q∈P" "p∈P" by blast+
  moreover from calculation and ‹M_generic(G)›
  have "forces_mem(q,σ,θ)"
    using forces_memI by blast
  moreover
  note ‹forces_eq(p,τ,θ)›
  ultimately
  have "forces_mem(q,σ,τ)"
    using def_forces_eq by blast
  with ‹q∈P› ‹q∈G› IH[of q σ] ‹⟨σ,r⟩∈θ› ‹val(P,G,σ) = x›
  show "x∈val(P,G,τ)" by (blast)
qed

(* Lemma IV.2.40(a), equality, second inclusion--- COPY-PASTE *)
lemma IV240a_eq:
  assumes
    "M_generic(G)" "p∈G" "forces_eq(p,τ,θ)"
    and
    IH:"⋀q σ. q∈P ⟹ q∈G ⟹ σ∈domain(τ) ∪ domain(θ) ⟹ 
        (forces_mem(q,σ,τ) ⟶ val(P,G,σ) ∈ val(P,G,τ)) ∧
        (forces_mem(q,σ,θ) ⟶ val(P,G,σ) ∈ val(P,G,θ))"
  shows
    "val(P,G,τ) = val(P,G,θ)"
  using IV240a_eq_1st_incl[OF assms] IV240a_eq_2nd_incl[OF assms] IH by blast 

subsection‹Induction on names›

lemma core_induction:
  assumes
    "⋀τ θ p. p ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(θ)⟧ ⟹ Q(0,τ,σ,q)⟧ ⟹ Q(1,τ,θ,p)"
    "⋀τ θ p. p ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ Q(1,σ,τ,q) ∧ Q(1,σ,θ,q)⟧ ⟹ Q(0,τ,θ,p)"
    "ft ∈ 2" "p ∈ 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 ∈ P"
    ultimately
    have "⟨ft,τ,θ,p⟩∈ 2×?e×?e×P" (is "?a∈2×?e×?e×P") by simp
    then 
    have "Q(ftype(?a), name1(?a), name2(?a), cond_of(?a))"
      using core_induction_aux[of ?e P 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 forces_induction_with_conds:
  assumes
    "⋀τ θ p. p ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(θ)⟧ ⟹ Q(q,τ,σ)⟧ ⟹ R(p,τ,θ)"
    "⋀τ θ p. p ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ R(q,σ,τ) ∧ R(q,σ,θ)⟧ ⟹ Q(p,τ,θ)"
    "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 ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(θ)⟧ ⟹ ?Q(0,τ,σ,q)⟧ ⟹ ?Q(1,τ,θ,p)"
    by simp
  moreover from assms(2)
  have "⋀τ θ p. p ∈ P ⟹ ⟦⋀q σ. ⟦q∈P ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ ?Q(1,σ,τ,q) ∧ ?Q(1,σ,θ,q)⟧ ⟹ ?Q(0,τ,θ,p)"
    by simp
  moreover
  note ‹p∈P›
  ultimately
  have "?Q(ft,τ,θ,p)" if "ft∈2" for ft
    by (rule core_induction[OF _ _ that, of ?Q])
  then
  show ?thesis by auto
qed

lemma 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 ∈ P ⟹ σ ∈ domain(θ) ⟹ Q(τ, σ)" for q σ
  with assms(1)
  show "R(τ,θ)"
    using one_in_P by simp
next
  fix τ θ p 
    assume "q ∈ P ⟹ σ ∈ 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:
  assumes
    "M_generic(G)"
  shows 
    "(τ∈M ⟶ θ∈M ⟶ (∀p∈G. forces_eq(p,τ,θ) ⟶ val(P,G,τ) = val(P,G,θ))) ∧ 
     (τ∈M ⟶ θ∈M ⟶ (∀p∈G. forces_mem(p,τ,θ) ⟶ val(P,G,τ) ∈ val(P,G,θ)))"
    (is "?Q(τ,θ) ∧ ?R(τ,θ)")
proof (intro forces_induction[of ?Q ?R] impI)
  fix τ θ 
  assume "τ∈M" "θ∈M"  "σ∈domain(θ) ⟹ ?Q(τ,σ)" for σ
  moreover from this
  have "σ∈domain(θ) ⟹ forces_eq(q, τ, σ) ⟹ val(P,G, τ) = val(P,G, σ)" 
    if "q∈P" "q∈G" for q σ
    using that domain_closed[of θ] transitivity by auto
  moreover 
  note assms
  ultimately
  show "∀p∈G. forces_mem(p,τ,θ) ⟶ val(P,G,τ) ∈ val(P,G,θ)"
    using IV240a_mem domain_closed transitivity by (simp)
next
  fix τ θ 
  assume "τ∈M" "θ∈M" "σ ∈ domain(τ) ∪ domain(θ) ⟹ ?R(σ,τ) ∧ ?R(σ,θ)" for σ
  moreover from this
  have IH':"σ ∈ domain(τ) ∪ domain(θ) ⟹ q∈G ⟹
            (forces_mem(q, σ, τ) ⟶ val(P,G, σ) ∈ val(P,G, τ)) ∧ 
            (forces_mem(q, σ, θ) ⟶ val(P,G, σ) ∈ val(P,G, θ))" for q σ 
    by (auto intro:  transitivity[OF _ domain_closed[simplified]])
  ultimately
  show "∀p∈G. forces_eq(p,τ,θ) ⟶ val(P,G,τ) = val(P,G,θ)"
    using IV240a_eq[OF assms(1) _ _ IH'] by (simp)
qed

subsection‹Lemma IV.2.40(b)›
(* Lemma IV.2.40(b), membership *)
lemma IV240b_mem:
  assumes
    "M_generic(G)" "val(P,G,π)∈val(P,G,τ)" "π∈M" "τ∈M"
    and
    IH:"⋀σ. σ∈domain(τ) ⟹ val(P,G,π) = val(P,G,σ) ⟹ 
      ∃p∈G. forces_eq(p,π,σ)" (* inductive hypothesis *)
  shows
    "∃p∈G. forces_mem(p,π,τ)"
proof -
  from ‹val(P,G,π)∈val(P,G,τ)›
  obtain σ r where "r∈G" "⟨σ,r⟩∈τ" "val(P,G,π) = val(P,G,σ)" by auto
  moreover from this and IH
  obtain p' where "p'∈G" "forces_eq(p',π,σ)" by blast
  moreover
  note ‹M_generic(G)›
  ultimately
  obtain p where "p≼r" "p∈G" "forces_eq(p,π,σ)" 
    using M_generic_compatD strengthening_eq[of p'] by blast
  moreover 
  note ‹M_generic(G)›
  moreover from calculation
  have "forces_eq(q,π,σ)" if "q∈P" "q≼p" for q
    using that strengthening_eq by blast
  moreover 
  note ‹⟨σ,r⟩∈τ› ‹r∈G›
  ultimately
  have "r∈P ∧ ⟨σ,r⟩ ∈ τ ∧ q≼r ∧ forces_eq(q,π,σ)" if "q∈P" "q≼p" for q
    using that leq_transD[of _ p r] by blast
  then
  have "dense_below({q∈P. ∃s r. r∈P ∧ ⟨s,r⟩ ∈ τ ∧ q≼r ∧ forces_eq(q,π,s)},p)"
    using refl_leq by blast
  moreover
  note ‹M_generic(G)› ‹p∈G›
  moreover from calculation
  have "forces_mem(p,π,τ)" 
    using forces_mem_iff_dense_below by blast
  ultimately
  show ?thesis by blast
qed

end (* includes *)

lemma Collect_forces_eq_in_M:
  assumes "τ ∈ M" "θ ∈ M"
  shows "{p∈P. forces_eq(p,τ,θ)} ∈ M"
  using assms Collect_in_M_4p[of "forces_eq_fm(1,2,0,3,4)" P leq τ θ 
                                  "λA x p l t1 t2. is_forces_eq(x,t1,t2)"
                                  "λ x p l t1 t2. forces_eq(x,t1,t2)" P] 
        arity_forces_eq_fm P_in_M leq_in_M sats_forces_eq_fm forces_eq_abs forces_eq_fm_type 
  by (simp add: nat_union_abs1 Un_commute)

lemma IV240b_eq_Collects:
  assumes "τ ∈ M" "θ ∈ M"
  shows "{p∈P. ∃σ∈domain(τ) ∪ domain(θ). forces_mem(p,σ,τ) ∧ forces_nmem(p,σ,θ)}∈M" and
        "{p∈P. ∃σ∈domain(τ) ∪ domain(θ). forces_nmem(p,σ,τ) ∧ forces_mem(p,σ,θ)}∈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,P,leq,τ,θ) ⟷ 
        (∃σ∈domain(τ) ∪ domain(θ). forces_mem'(P,leq,p,σ,τ) ∧ forces_nmem'(P,leq,p,σ,θ))" 
        if "p∈M" for p
    unfolding forces_mem_def forces_nmem_def
    using assms that forces_mem'_abs forces_nmem'_abs P_in_M leq_in_M 
      domain_closed Un_closed 
    by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
  have abs2:"?rel_pred(##M,p,P,leq,θ,τ) ⟷ (∃σ∈domain(τ) ∪ domain(θ). 
        forces_nmem'(P,leq,p,σ,τ) ∧ forces_mem'(P,leq,p,σ,θ))" if "p∈M" for p
    unfolding forces_mem_def forces_nmem_def
    using assms that forces_mem'_abs forces_nmem'_abs P_in_M leq_in_M 
      domain_closed Un_closed 
    by (auto simp add:1[of _ _ τ] 1[of _ _ θ])
  have fsats1:"(M,[p,P,leq,τ,θ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,P,leq,τ,θ)" if "p∈M" for p
    using that assms sats_forces_mem'_fm sats_forces_nmem'_fm P_in_M leq_in_M
      domain_closed Un_closed by simp
  have fsats2:"(M,[p,P,leq,θ,τ] ⊨ ?φ) ⟷ ?rel_pred(##M,p,P,leq,θ,τ)" if "p∈M" for p
    using that assms sats_forces_mem'_fm sats_forces_nmem'_fm P_in_M leq_in_M
      domain_closed Un_closed by simp
  have fty:"?φ∈formula" by simp
  have farit:"arity(?φ)=5"
    unfolding forces_nmem_fm_def domain_fm_def pair_fm_def upair_fm_def union_fm_def
    using arity_forces_mem_fm by (simp add:nat_simp_union Un_commute)
    show 
    "{p ∈ P . ∃σ∈domain(τ) ∪ domain(θ). forces_mem(p, σ, τ) ∧ forces_nmem(p, σ, θ)} ∈ M"
    and "{p ∈ P . ∃σ∈domain(τ) ∪ domain(θ). forces_nmem(p, σ, τ) ∧ forces_mem(p, σ, θ)} ∈ M"
    unfolding forces_mem_def
    using abs1 fty fsats1 farit P_in_M leq_in_M assms forces_nmem
          Collect_in_M_4p[of ?φ _ _ _ _ _ 
          "λx p l a1 a2. (∃σ∈domain(a1) ∪ domain(a2). forces_mem'(p,l,x,σ,a1) ∧ 
                                                     forces_nmem'(p,l,x,σ,a2))"]
    using abs2 fty fsats2 farit P_in_M leq_in_M assms forces_nmem domain_closed Un_closed
          Collect_in_M_4p[of ?φ P leq θ τ ?rel_pred 
          "λx p l a2 a1. (∃σ∈domain(a1) ∪ domain(a2). forces_nmem'(p,l,x,σ,a1) ∧ 
                                                     forces_mem'(p,l,x,σ,a2))" P]  
    by simp_all
qed

(* Lemma IV.2.40(b), equality *)
lemma IV240b_eq:
  assumes
    "M_generic(G)" "val(P,G,τ) = val(P,G,θ)" "τ∈M" "θ∈M" 
    and
    IH:"⋀σ. σ∈domain(τ)∪domain(θ) ⟹ 
      (val(P,G,σ)∈val(P,G,τ) ⟶ (∃q∈G. forces_mem(q,σ,τ))) ∧ 
      (val(P,G,σ)∈val(P,G,θ) ⟶ (∃q∈G. forces_mem(q,σ,θ)))"
    (* inductive hypothesis *)
  shows
    "∃p∈G. forces_eq(p,τ,θ)"
proof -
  let ?D1="{p∈P. forces_eq(p,τ,θ)}"
  let ?D2="{p∈P. ∃σ∈domain(τ) ∪ domain(θ). forces_mem(p,σ,τ) ∧ forces_nmem(p,σ,θ)}"
  let ?D3="{p∈P. ∃σ∈domain(τ) ∪ domain(θ). forces_nmem(p,σ,τ) ∧ forces_mem(p,σ,θ)}"
  let ?D="?D1 ∪ ?D2 ∪ ?D3"
  note assms
  moreover from this
  have "domain(τ) ∪ domain(θ)∈M" (is "?B∈M") using domain_closed Un_closed by auto
  moreover from calculation
  have "?D2∈M" and "?D3∈M" using IV240b_eq_Collects by simp_all
  ultimately
  have "?D∈M" using Collect_forces_eq_in_M Un_closed by auto
  moreover
  have "dense(?D)"
  proof
    fix p
    assume "p∈P"
    have "∃d∈P. (forces_eq(d, τ, θ) ∨
            (∃σ∈domain(τ) ∪ domain(θ). forces_mem(d, σ, τ) ∧ forces_nmem(d, σ, θ)) ∨
            (∃σ∈domain(τ) ∪ domain(θ). forces_nmem(d, σ, τ) ∧ forces_mem(d, σ, θ))) ∧
           d ≼ p" 
    proof (cases "forces_eq(p, τ, θ)")
      case True
      with ‹p∈P› 
      show ?thesis using refl_leq by blast
    next
      case False
      moreover note ‹p∈P›
      moreover from calculation
      obtain σ q where "σ∈domain(τ)∪domain(θ)" "q∈P" "q≼p"
        "(forces_mem(q, σ, τ) ∧ ¬ forces_mem(q, σ, θ)) ∨
         (¬ forces_mem(q, σ, τ) ∧ forces_mem(q, σ, θ))"
        using def_forces_eq by blast
      moreover from this
      obtain r where "r≼q" "r∈P"
        "(forces_mem(r, σ, τ) ∧ forces_nmem(r, σ, θ)) ∨
         (forces_nmem(r, σ, τ) ∧ forces_mem(r, σ, θ))"
        using not_forces_nmem strengthening_mem by blast
      ultimately
      show ?thesis using leq_transD by blast
    qed
    then
    show "∃d∈?D1 ∪ ?D2 ∪ ?D3. d ≼ p" by blast
  qed
  moreover
  have "?D ⊆ P"
    by auto
  moreover
  note ‹M_generic(G)›
  ultimately
  obtain p where "p∈G" "p∈?D"
    unfolding M_generic_def by blast
  then 
  consider 
    (1) "forces_eq(p,τ,θ)" | 
    (2) "∃σ∈domain(τ) ∪ domain(θ). forces_mem(p,σ,τ) ∧ forces_nmem(p,σ,θ)" | 
    (3) "∃σ∈domain(τ) ∪ domain(θ). forces_nmem(p,σ,τ) ∧ forces_mem(p,σ,θ)"
    by blast
  then
  show ?thesis
  proof (cases)
    case 1
    with ‹p∈G› 
    show ?thesis by blast
  next
    case 2
    then 
    obtain σ where "σ∈domain(τ) ∪ domain(θ)" "forces_mem(p,σ,τ)" "forces_nmem(p,σ,θ)" 
      by blast
    moreover from this and ‹p∈G› and assms
    have "val(P,G,σ)∈val(P,G,τ)"
      using IV240a[of G σ τ] transitivity[OF _ domain_closed[simplified]] by blast
    moreover note IH ‹val(P,G,τ) = _›
    ultimately
    obtain q where "q∈G" "forces_mem(q, σ, θ)" by auto
    moreover from this and ‹p∈G› ‹M_generic(G)›
    obtain r where "r∈P" "r≼p" "r≼q"
      by blast
    moreover
    note ‹M_generic(G)›
    ultimately
    have "forces_mem(r, σ, θ)"
      using strengthening_mem by blast
    with ‹r≼p› ‹forces_nmem(p,σ,θ)› ‹r∈P›
    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(θ)" "forces_mem(p,σ,θ)" "forces_nmem(p,σ,τ)" 
      by blast
    moreover from this and ‹p∈G› and assms
    have "val(P,G,σ)∈val(P,G,θ)"
      using IV240a[of G σ θ] transitivity[OF _ domain_closed[simplified]] by blast
    moreover note IH ‹val(P,G,τ) = _›
    ultimately
    obtain q where "q∈G" "forces_mem(q, σ, τ)" by auto
    moreover from this and ‹p∈G› ‹M_generic(G)›
    obtain r where "r∈P" "r≼p" "r≼q"
      by blast
    moreover
    note ‹M_generic(G)›
    ultimately
    have "forces_mem(r, σ, τ)"
      using strengthening_mem by blast
    with ‹r≼p› ‹forces_nmem(p,σ,τ)› ‹r∈P›
    have "False"
      unfolding forces_nmem_def by blast
    then
    show ?thesis by simp
  qed
qed

(* Lemma IV.2.40(b), full *)
lemma IV240b:
  assumes
    "M_generic(G)"
  shows 
    "(τ∈M⟶θ∈M⟶val(P,G,τ) = val(P,G,θ) ⟶ (∃p∈G. forces_eq(p,τ,θ))) ∧
     (τ∈M⟶θ∈M⟶val(P,G,τ) ∈ val(P,G,θ) ⟶ (∃p∈G. forces_mem(p,τ,θ)))" 
    (is "?Q(τ,θ) ∧ ?R(τ,θ)")
proof (intro forces_induction)
  fix τ θ p
  assume "σ∈domain(θ) ⟹ ?Q(τ, σ)" for σ
  with assms
  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(P,G, σ) ∈ val(P,G, τ) ⟶ (∃q∈G. forces_mem(q, σ, τ))) ∧
          (val(P,G, σ) ∈ val(P,G, θ) ⟶ (∃q∈G. forces_mem(q, σ, θ)))" for σ 
    by (blast intro:left_in_M) 
  ultimately
  show "?Q(τ,θ)"
    using IV240b_eq[OF assms(1)] by (auto)
qed

lemma map_val_in_MG:
  assumes 
    "env∈list(M)"
  shows 
    "map(val(P,G),env)∈list(M[G])"
  unfolding GenExt_def using assms map_type2 by simp

lemma truth_lemma_mem:
  assumes 
    "env∈list(M)" "M_generic(G)"
    "n∈nat" "m∈nat" "n<length(env)" "m<length(env)"
  shows 
    "(∃p∈G. p ⊩ Member(n,m) env)  ⟷  M[G], map(val(P,G),env) ⊨ Member(n,m)"
  using assms IV240a[OF assms(2), of "nth(n,env)" "nth(m,env)"] 
    IV240b[OF assms(2), of "nth(n,env)" "nth(m,env)"] 
    P_in_M leq_in_M one_in_M 
    Forces_Member[of _  "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
  by (auto)

lemma truth_lemma_eq:
  assumes 
    "env∈list(M)" "M_generic(G)" 
    "n∈nat" "m∈nat" "n<length(env)" "m<length(env)"
  shows 
    "(∃p∈G. p ⊩ Equal(n,m) env)  ⟷  M[G], map(val(P,G),env) ⊨ Equal(n,m)"
  using assms IV240a(1)[OF assms(2), of "nth(n,env)" "nth(m,env)"] 
    IV240b(1)[OF assms(2), of "nth(n,env)" "nth(m,env)"] 
    P_in_M leq_in_M one_in_M 
    Forces_Equal[of _  "nth(n,env)" "nth(m,env)" env n m] map_val_in_MG
  by (auto)

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›

lemma strengthening_lemma:
  assumes 
    "p∈P" "φ∈formula" "r∈P" "r≼p"
  shows
    "⋀env. env∈list(M) ⟹ arity(φ)≤length(env) ⟹ p ⊩ φ env ⟹ r ⊩ φ env"
  using assms(2)
proof (induct)
  case (Member n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "env∈list(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 "env∈list(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 "x∈M" for x
    using that Forces_Forall by simp
  with Forall 
  have "r ⊩ φ ([x] @ env)" if "x∈M" 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)" "env∈list(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∈P" "φ∈formula"
  shows
    "⋀env. env∈list(M) ⟹ arity(φ)≤length(env) ⟹
     dense_below({q∈P. (q ⊩ φ env)},p) ⟹ (p ⊩ φ env)"
  using assms(2)
proof (induct)
  case (Member n m)
  then
  have "n<length(env)" "m<length(env)"
    using arities_at_aux by simp_all
  moreover
  assume "env∈list(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 "env∈list(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 "q∈M" "q∈P" "q≼ p" "q ⊩ φ env"
    moreover 
    note Nand
    moreover from calculation
    obtain d where "d∈P" "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∈P›
  show ?case
    using Forces_Nand[symmetric, OF _ Nand(5,1,3)] by blast
next
  case (Forall φ)
  have "dense_below({q∈P. q ⊩ φ ([a]@env)},p)" if "a∈M" for a
  proof
    fix r
    assume "r∈P" "r≼p"
    with ‹dense_below(_,p)›
    obtain q where "q∈P" "q≼r" "q ⊩ Forall(φ) env"
      by blast
    moreover
    note Forall ‹a∈M›
    moreover from calculation
    have "q ⊩ φ ([a]@env)"
      using Forces_Forall by simp
    ultimately
    show "∃d ∈ {q∈P. q ⊩ φ ([a]@env)}. d ∈ P ∧ d≼r"
      by auto
  qed
  moreover 
  note Forall(2)[of "Cons(_,env)"] Forall(1,3-5)
  ultimately
  have "p ⊩ φ ([a]@env)" if "a∈M" for a
    using that pred_le2 by simp
  with assms Forall
  show ?case using Forces_Forall by simp
qed

lemma density_lemma:
  assumes
    "p∈P" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)"
  shows
    "p ⊩ φ env   ⟷   dense_below({q∈P. (q ⊩ φ env)},p)"
proof
  assume "dense_below({q∈P. (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∈P. q ⊩ φ env},p)"
    using strengthening_lemma refl_leq by auto
qed

subsection‹The Truth Lemma›
lemma Forces_And:
  assumes
    "p∈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 ∈ P . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)"
    using Forces_And_iff_dense_below by simp
  then
  have "dense_below({r ∈ P . (r ⊩ φ env)}, p)" "dense_below({r ∈ P . (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 ∈ P . (r ⊩ φ env) ∧ (r ⊩ ψ env)}, p)"
  proof (intro dense_belowI bexI conjI, assumption)
    fix q
    assume "q∈P" "q≼ p"
    with assms ‹(p ⊩ φ env) ∧ (p ⊩ ψ env)›
    show "q∈{r ∈ P . (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∈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

lemma truth_lemma_Neg:
  assumes 
    "φ∈formula" "M_generic(G)" "env∈list(M)" "arity(φ)≤length(env)" and
    IH: "(∃p∈G. p ⊩ φ env) ⟷ M[G], map(val(P,G),env) ⊨ φ"
  shows
    "(∃p∈G. p ⊩ Neg(φ) env)  ⟷  M[G], map(val(P,G),env) ⊨ Neg(φ)"
proof (intro iffI, elim bexE, rule ccontr) 
  (* Direct implication by contradiction *)
  fix p 
  assume "p∈G" "p ⊩ Neg(φ) env" "¬(M[G],map(val(P,G),env) ⊨ Neg(φ))"
  moreover 
  note assms
  moreover from calculation
  have "M[G], map(val(P,G),env) ⊨ φ"
    using map_val_in_MG by simp
  with IH
  obtain r where "r ⊩ φ env" "r∈G" by blast
  moreover from this and ‹M_generic(G)› ‹p∈G›
  obtain q where "q≼p" "q≼r" "q∈G"
    by blast
  moreover from calculation 
  have "q ⊩ φ env"
    using strengthening_lemma[where φ=φ] by blast
  ultimately
  show "False"
    using Forces_Neg[where φ=φ] transitivity[OF _ P_in_M] by blast
next
  assume "M[G], map(val(P,G),env) ⊨ Neg(φ)"
  with assms 
  have "¬ (M[G], map(val(P,G),env) ⊨ φ)"
    using map_val_in_MG by simp
  let ?D="{p∈P. (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}"
  have "separation(##M,λp. (p ⊩ φ env))" 
      using separation_ax arity_forces assms P_in_M leq_in_M one_in_M arity_forces_le
    by simp
  moreover
  have "separation(##M,λp. (p ⊩ Neg(φ) env))"
      using separation_ax arity_forces assms P_in_M leq_in_M one_in_M arity_forces_le
    by simp
  ultimately
  have "separation(##M,λp. (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env))" 
    using separation_disj by simp
  then 
  have "?D ∈ M" 
    using separation_closed P_in_M by simp
  moreover
  have "?D ⊆ P" by auto
  moreover
  have "dense(?D)"
  proof
    fix q
    assume "q∈P"
    show "∃d∈{p ∈ P . (p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)}. d≼ q"
    proof (cases "q ⊩ Neg(φ) env")
      case True
      with ‹q∈P›
      show ?thesis using refl_leq by blast
    next
      case False
      with ‹q∈P› and assms
      show ?thesis using Forces_Neg by auto
    qed
  qed
  moreover
  note ‹M_generic(G)›
  ultimately
  obtain p where "p∈G" "(p ⊩ φ env) ∨ (p ⊩ Neg(φ) env)"
    by blast
  then
  consider (1) "p ⊩ φ env" | (2) "p ⊩ Neg(φ) env" by blast
  then
  show "∃p∈G. (p ⊩ Neg(φ) env)"
  proof (cases)
    case 1
    with ‹¬ (M[G],map(val(P,G),env) ⊨ φ)› ‹p∈G› IH
    show ?thesis
      by blast
  next
    case 2
    with ‹p∈G› 
    show ?thesis by blast
  qed
qed 

lemma truth_lemma_And:
  assumes 
    "env∈list(M)" "φ∈formula" "ψ∈formula"
    "arity(φ)≤length(env)" "arity(ψ) ≤ length(env)" "M_generic(G)"
    and
    IH: "(∃p∈G. p ⊩ φ env)  ⟷   M[G], map(val(P,G),env) ⊨ φ"
        "(∃p∈G. p ⊩ ψ env)  ⟷   M[G], map(val(P,G),env) ⊨ ψ"
  shows
    "(∃p∈G. (p ⊩ And(φ,ψ) env)) ⟷ M[G] , map(val(P,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 "p∈G" "p ⊩ And(φ,ψ) env"
  with assms
  show "M[G], map(val(P,G),env) ⊨ And(φ,ψ)" 
    using Forces_And[OF M_genericD, of _ _ _ φ ψ] map_val_in_MG by auto
next 
  assume "M[G], map(val(P,G),env) ⊨ And(φ,ψ)"
  moreover
  note assms
  moreover from calculation
  obtain q r where "q ⊩ φ env" "r ⊩ ψ env" "q∈G" "r∈G"
    using map_val_in_MG Forces_And[OF M_genericD assms(1-5)] by auto
  moreover from calculation
  obtain p where "p≼q" "p≼r" "p∈G"
    by blast
  moreover from calculation
  have "(p ⊩ φ env) ∧ (p ⊩ ψ env)" (* can't solve as separate goals *)
    using strengthening_lemma by (blast)
  ultimately
  show "∃p∈G. (p ⊩ And(φ,ψ) env)"
    using Forces_And[OF M_genericD assms(1-5)] by auto
qed 

definition 
  ren_truth_lemma :: "i⇒i" 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 nat_union_abs1 Un_assoc[symmetric] a c nat_union_abs2
        by simp
    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 nat_union_abs1 Un_assoc[symmetric]  nat_union_abs2
        by simp
    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 nat_union_abs1 Un_assoc[symmetric] nat_union_abs2 
      by simp
  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)

lemma truth_lemma' :
  assumes
    "φ∈formula" "env∈list(M)" "arity(φ) ≤ succ(length(env))" 
  shows
    "separation(##M,λd. ∃b∈M. ∀q∈P. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))"
proof -
  let ?rel_pred="λM x a1 a2 a3. ∃b∈M. ∀q∈M. q∈a1 ∧ is_leq(##M,a2,q,x) ⟶ 
                  ¬(M, [q,a1,a2,a3,b] @ env ⊨ forces(φ))" 
  let ?ψ="Exists(Forall(Implies(And(Member(0,3),leq_fm(4,0,2)),
          Neg(ren_truth_lemma(forces(φ))))))"
  have "q∈M" if "q∈P" for q using that transitivity[OF _ P_in_M] by simp
  then
  have 1:"∀q∈M. q∈P ∧ R(q) ⟶ Q(q) ⟹ (∀q∈P. R(q) ⟶ Q(q))" for R Q 
    by auto
  then
  have "⟦b ∈ M; ∀q∈M. q ∈ P ∧ q ≼ d ⟶ ¬(q ⊩ φ ([b]@env))⟧ ⟹
         ∃c∈M. ∀q∈P. q ≼ d ⟶ ¬(q ⊩ φ ([c]@env))" for b d
    by (rule bexI,simp_all)
  then
  have "?rel_pred(M,d,P,leq,one) ⟷ (∃b∈M. ∀q∈P. q≼d ⟶ ¬(q ⊩ φ ([b]@env)))" if "d∈M" for d
    using that leq_abs leq_in_M P_in_M one_in_M assms
    by auto
  moreover
  have "?ψ∈formula" using assms by simp
  moreover
  have "(M, [d,P,leq,one]@env ⊨ ?ψ) ⟷ ?rel_pred(M,d,P,leq,one)" if "d∈M" for d
    using assms that P_in_M leq_in_M one_in_M sats_leq_fm sats_ren_truth_lemma
    by simp
  moreover
  have "arity(?ψ) ≤ 4#+length(env)" 
  proof -
    have eq:"arity(leq_fm(4, 0, 2)) = 5"
      using arity_leq_fm succ_Un_distrib nat_simp_union
      by simp
    with ‹φ∈_›
    have "arity(?ψ) = 3 ∪ (pred^2(arity(ren_truth_lemma(forces(φ)))))"
      using nat_union_abs1 pred_Un_distrib by simp
    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] nat_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]] nat_simp_union by simp
  qed
  ultimately
  show ?thesis using assms P_in_M leq_in_M one_in_M 
       separation_ax[of "?ψ" "[P,leq,one]@env"] 
       separation_cong[of "##M" "λy. (M, [y,P,leq,one]@env ⊨?ψ)"]
    by simp
qed


lemma truth_lemma:
  assumes 
    "φ∈formula" "M_generic(G)"
  shows 
     "⋀env. env∈list(M) ⟹ arity(φ)≤length(env) ⟹ 
      (∃p∈G. p ⊩ φ env)   ⟷   M[G], map(val(P,G),env) ⊨ φ"
  using assms(1)
proof (induct)
  case (Member x y)
  then
  show ?case
    using assms truth_lemma_mem[OF ‹env∈list(M)› assms(2) ‹x∈nat› ‹y∈nat›] 
      arities_at_aux by simp
next
  case (Equal x y)
  then
  show ?case
    using assms truth_lemma_eq[OF ‹env∈list(M)› assms(2) ‹x∈nat› ‹y∈nat›] 
      arities_at_aux by simp
next
  case (Nand φ ψ)
  moreover 
  note ‹M_generic(G)›
  ultimately
  show ?case 
    using truth_lemma_And truth_lemma_Neg Forces_Nand_alt 
      M_genericD map_val_in_MG arity_Nand_le[of φ ψ] by auto
next
  case (Forall φ)
  with ‹M_generic(G)›
  show ?case
  proof (intro iffI)
    assume "∃p∈G. (p ⊩ Forall(φ) env)"
    with ‹M_generic(G)›
    obtain p where "p∈G" "p∈M" "p∈P" "p ⊩ Forall(φ) env"
      using transitivity[OF _ P_in_M] by auto
    with ‹env∈list(M)› ‹φ∈formula›
    have "p ⊩ φ ([x]@env)" if "x∈M" for x
      using that Forces_Forall by simp
    with ‹p∈G› ‹φ∈formula› ‹env∈_› ‹arity(Forall(φ)) ≤ length(env)›
      Forall(2)[of "Cons(_,env)"] 
    show "M[G], map(val(P,G),env) ⊨  Forall(φ)"
      using pred_le2 map_val_in_MG
      by (auto iff:GenExtD)
  next
    assume "M[G], map(val(P,G),env) ⊨ Forall(φ)"
    let ?D1="{d∈P. (d ⊩ Forall(φ) env)}"
    let ?D2="{d∈P. ∃b∈M. ∀q∈P. q≼d ⟶ ¬(q ⊩ φ ([b]@env))}"
    define D where "D ≡ ?D1 ∪ ?D2"
    have arφ:"arity(φ)≤succ(length(env))" 
      using assms ‹arity(Forall(φ)) ≤ length(env)› ‹φ∈formula› ‹env∈list(M)› pred_le2 
      by simp
    then
    have "arity(Forall(φ)) ≤ length(env)" 
      using pred_le ‹φ∈formula› ‹env∈list(M)› by simp
    then
    have "?D1∈M" using Collect_forces arφ ‹φ∈formula› ‹env∈list(M)› by simp
    moreover
    have "?D2∈M" using ‹env∈list(M)› ‹φ∈formula›  truth_lemma' separation_closed arφ
                        P_in_M
      by simp
    ultimately
    have "D∈M" unfolding D_def using Un_closed by simp
    moreover
    have "D ⊆ P" unfolding D_def by auto
    moreover
    have "dense(D)" 
    proof
      fix p
      assume "p∈P"
      show "∃d∈D. d≼ p"
      proof (cases "p ⊩ Forall(φ) env")
        case True
        with ‹p∈P› 
        show ?thesis unfolding D_def using refl_leq by blast
      next
        case False
        with Forall ‹p∈P›
        obtain b where "b∈M" "¬(p ⊩ φ ([b]@env))"
          using Forces_Forall by blast
        moreover from this ‹p∈P› Forall
        have "¬dense_below({q∈P. q ⊩ φ ([b]@env)},p)"
          using density_lemma pred_le2  by auto
        moreover from this
        obtain d where "d≼p" "∀q∈P. q≼d ⟶ ¬(q ⊩ φ ([b] @ env))"
          "d∈P" by blast
        ultimately
        show ?thesis unfolding D_def by auto
      qed
    qed
    moreover
    note ‹M_generic(G)›
    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 "∃p∈G. (p ⊩ Forall(φ) env)"
    proof (cases)
      case 1
      with ‹d∈G›
      show ?thesis by blast
    next
      case 2
      then
      obtain b where "b∈M" "∀q∈P. q≼d ⟶¬(q ⊩ φ ([b] @ env))"
        by blast
      moreover from this(1) and  ‹M[G], _ ⊨  Forall(φ)› and 
        Forall(2)[of "Cons(b,env)"] Forall(1,3-4) ‹M_generic(G)›
      obtain p where "p∈G" "p∈P" "p ⊩ φ ([b] @ env)" 
        using pred_le2 using map_val_in_MG by (auto iff:GenExtD)
      moreover
      note ‹d∈G› ‹M_generic(G)›
      ultimately
      obtain q where "q∈G" "q∈P" "q≼d" "q≼p" by blast
      moreover from this and  ‹p ⊩ φ ([b] @ env)› 
        Forall  ‹b∈M› ‹p∈P›
      have "q ⊩ φ ([b] @ env)"
        using pred_le2 strengthening_lemma by simp
      moreover 
      note ‹∀q∈P. q≼d ⟶¬(q ⊩ φ ([b] @ env))›
      ultimately
      show ?thesis by simp
    qed
  qed
qed
subsection‹The ``Definition of forcing''›
lemma definition_of_forcing:
  assumes
    "p∈P" "φ∈formula" "env∈list(M)" "arity(φ)≤length(env)"
  shows
    "(p ⊩ φ env) ⟷
     (∀G. M_generic(G) ∧ p∈G  ⟶  M[G], map(val(P,G),env) ⊨ φ)"
proof (intro iffI allI impI, elim conjE)
  fix G
  assume "(p ⊩ φ env)" "M_generic(G)" "p ∈ G"
  with assms 
  show "M[G], map(val(P,G),env) ⊨ φ"
    using truth_lemma by blast
next
  assume 1: "∀G.(M_generic(G)∧ p∈G)⟶ M[G] , map(val(P,G),env) ⊨ φ"
  {
    fix r 
    assume 2: "r∈P" "r≼p"
    then 
    obtain G where "r∈G" "M_generic(G)"
      using generic_filter_existence by auto
    moreover from calculation 2 ‹p∈P› 
    have "p∈G" 
      unfolding M_generic_def using filter_leqD by simp
    moreover note 1
    ultimately
    have "M[G], map(val(P,G),env) ⊨ φ"
      by simp
    with assms ‹M_generic(G)› 
    obtain s where "s∈G" "(s ⊩ φ env)"
      using truth_lemma by blast
    moreover from this and  ‹M_generic(G)› ‹r∈G› 
    obtain q where "q∈G" "q≼s" "q≼r"
      by blast
    moreover from calculation ‹s∈G› ‹M_generic(G)› 
    have "s∈P" "q∈P" 
      unfolding M_generic_def filter_def by auto
    moreover 
    note assms
    ultimately 
    have "∃q∈P. q≼r ∧ (q ⊩ φ env)"
      using strengthening_lemma by blast
  }
  then
  have "dense_below({q∈P. (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 (* forcing_data *)

end