Theory Soundness

theory Soundness
  imports Calculus
begin

section ‹Soundness›

text ‹This section proves ‹NK› sound for the model class ‹ℳ⇘βfb⇙›
  (BKK Theorem 7.3, including BKK's evaluation-variant argument).›

subsection ‹The canonical construction respects ‹β›-conversion (BKK Remark 3.19)›

text ‹In a ‹Σ›-Henkin model, ‹β›-convertible terms denote the same object under any total
  assignment; the abstraction-congruence case uses functionality (property f).›

context general_model
begin

lemma beq_den: "s ≈⇘ρ⇙ t ⟹ (∀n τ. 𝒟⇘τ⇙ (ξ n τ)) ⟹ ⦇s⦈⇘ξ⇙ = ⦇t⦈⇘ξ⇙"
proof (induction arbitrary: ξ rule: beq.induct)
  case beta thus ?case using den_App_Abs resp_def by auto
next
  case (abs L b σ τ b')
  define x where "x = fresh (L ∪ fvs b ∪ fvs b')"
  have xL: "x ∉ L" and xb: "x ∉ fvs b" and xb': "x ∉ fvs b'"           
    using fresh_notin[of "L ∪ fvs b ∪ fvs b'"] abs unfolding x_def by auto
  have wb: "wff⇘τ⇙(b❙⟨x⇧f⇘σ⇙❙⟩)" and wb': "wff⇘τ⇙(b'❙⟨x⇧f⇘σ⇙❙⟩)"
    using beq_wffL beq_wffR abs xL by blast+
  {
    fix a
    assume a: "𝒟⇘σ⇙ a"
    hence tot: "∀n γ. 𝒟⇘γ⇙ (ξ(x⇘σ⇙ := a) n γ)"
      using abs.prems by (auto simp: upd_def)
    have "⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ ❙@ a = ⦇b❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
        by (rule gm_beta[OF wb xb abs.prems a])
    also have "… = ⦇b'❙⟨x⇧f⇘σ⇙❙⟩⦈⇘ξ(x⇘σ⇙ := a)⇙"
      using abs.IH[OF xL, of "ξ(x⇘σ⇙ := a)"] tot by blast
    also have "… = ⦇❙Λ⇘σ⇙ b'⦈⇘ξ⇙ ❙@ a"
      using gm_beta wb' xb' abs.prems a by simp
    finally have "⦇❙Λ⇘σ⇙ b⦈⇘ξ⇙ ❙@ a = ⦇❙Λ⇘σ⇙ b'⦈⇘ξ⇙ ❙@ a".
  }
  thus ?case
    using gm_funct gm_lamTy wff_Abs_open_rev wb xb abs.prems wb' xb' by blast
qed(auto simp: den.simps(8))

end

subsection ‹Abstract soundness (BKK Theorem 7.3)›

text ‹Soundness over the abstract ‹Σ›-models of Section 2, following BKK's
  proof of Theorem 7.3 case by case.  The ‹NK(ΠI)› case uses BKK's device verbatim:
  ``from the evaluation function ‹E›, one can define another evaluation function ‹E'›
  such that ‹E'(w) ≡ a› and ‹E'⇘φ⇙(A) ≡ E⇘φ⇙(A)› if ‹w› does not occur in ‹A›'' ---
  realised below by reading the parameter as a fresh variable after an injective shift
  of all free variables.  The extensionality cases ‹NK(f)› and ‹NK(b)› rest on BKK's
  Lemma 4.2 on Leibniz equality, proven here abstractly (BKK themselves route them
  through Theorem 4.3(3) and Lemma 3.48/Theorem 4.3(4), which rest on Lemma 4.2).›

subsubsection ‹The variable shift›

text ‹‹vshift› renames every free variable ‹n› to ‹n + 1›, freeing the name ‹0› at every
  type; ‹β›-equality and typing are stable under it and under the parameter-to-variable
  rename ‹pvar›.›

definition vshift :: "'p tm ⇒ 'p tm" where "vshift = msub (λn τ. (Suc n)⇧f⇘τ⇙)"
lemma occ_vshift: "occ (vshift t) = (λ(n, τ). (Suc n, τ)) ` occ t"
  unfolding vshift_def by (induction t) (auto simp: image_Un)
lemma pars_vshift: "pars (vshift t) = pars t"
  unfolding vshift_def by (induction t) auto
lemma wff_vshift: "wff⇘τ⇙(t) ⟹ wff⇘τ⇙(vshift t)"
  by (auto elim: wff_msub intro: wff_Fre simp: vshift_def)
lemma vshift_opn: "vshift (t❙⟨x⇧f⇘σ⇙❙⟩) = (vshift t)❙⟨(Suc x)⇧f⇘σ⇙❙⟩"
  unfolding vshift_def by (subst msub_opn) auto
lemma beq_vshift: "s ≈⇘ρ⇙ t ⟹ vshift s ≈⇘ρ⇙ vshift t"
proof (induction rule: beq.induct)
  case (beta σ ρ b a)
  moreover have "vshift ((❙Λ⇘σ⇙ b) ❙⋅ a) = (❙Λ⇘σ⇙ (vshift b)) ❙⋅ (vshift a)"
    by (simp add: vshift_def)
  moreover have "vshift (b❙⟨a❙⟩) = (vshift b)❙⟨vshift a❙⟩"
    unfolding vshift_def by (subst msub_opn) auto
  moreover have "wff⇘σ❙⇒ρ⇙(❙Λ⇘σ⇙ (vshift b))"
    using wff_vshift beta unfolding vshift_def by force
  ultimately show ?case using beq.beta wff_vshift by metis
next case appL thus ?case by (metis beq.appL msub.simps(9) vshift_def wff_vshift)
next case appR thus ?case by (metis beq.appR msub.simps(9) vshift_def wff_vshift)
next case (abs L b σ τ b')
  have "❙Λ⇘σ⇙ (vshift b) ≈⇘σ❙⇒τ⇙ ❙Λ⇘σ⇙ (vshift b')" 
  proof (rule beq.abs[of "{0} ∪ Suc ` L"])
    show "finite ({0} ∪ Suc ` L)" using abs.hyps(1) by simp
    fix y assume y: "y ∉ {0} ∪ Suc ` L"
    then obtain x where x: "y = Suc x" "x ∉ L" by (cases y) auto
    show "(vshift b)❙⟨y⇧f⇘σ⇙❙⟩ ≈⇘τ⇙ (vshift b')❙⟨y⇧f⇘σ⇙❙⟩" using abs.IH[OF x(2)]
      by (simp add: x(1) vshift_opn[symmetric])
  qed
  thus ?case by (simp add: vshift_def)
qed(auto simp: wff_vshift intro: beq.intros)

lemma beq_pvar: "s ≈⇘ρ⇙ t ⟹ pvar w σw x s ≈⇘ρ⇙ pvar w σw x t"
proof (induction rule: beq.induct)
  case beta thus ?case by (smt (verit, best) beq.simps pvar.simps(10,9) pvar_opn wff_pvar)
qed(auto simp: wff_pvar beq.abs pvar_opn intro: beq.intros)

lemma occ_pvar: "occ (pvar w σw x t) ⊆ occ t ∪ {(x, σw)}"
  by (induction t) auto

subsubsection ‹Satisfaction of Leibniz equality (BKK Lemma 4.2)›

text ‹Leibniz equality ‹β›-reduces to its ‹∀›-form (the syntactic prelude to Lemma 4.2).›

lemma Leib_beq: assumes wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)"
  shows "(A ❙≐⇘α⇙ B) ≈⇘𝗈⇙ ❙Π⇘α❙⇒𝗈⇙ ((Bnd 0 ❙⋅ A) ❙⊃ (Bnd 0 ❙⋅ B))"
proof -
  have lcA: "lc A" and lcB: "lc B" using wA wB by (auto intro: wff_lc)
  let ?inner = "❙Λ⇘α⇙ (❙Π⇘α❙⇒𝗈⇙ ((Bnd 0 ❙⋅ A) ❙⊃ (Bnd 0 ❙⋅ Bnd 1)))"
  have "(Leib α ❙⋅ A) ≈⇘α❙⇒𝗈⇙ ?inner"
    using beq.beta[OF wff_Leib[unfolded Leib_def] wA]
    unfolding Leib_def by (simp add: opn_lc[OF lcA])
  moreover {
    have "wff⇘α❙⇒𝗈⇙(?inner)" using beq_wffR calculation by blast
    with beq.beta[OF this wB]
    have "(?inner ❙⋅ B) ≈⇘𝗈⇙ ❙Π⇘α❙⇒𝗈⇙ ((Bnd 0 ❙⋅ A) ❙⊃ (Bnd 0 ❙⋅ B))"
      using opn_lc[OF lcA] opn_lc[OF lcB] by simp
  }
  ultimately show ?thesis using beq.trans beq.appL wB by blast
qed

context sigma_model
begin

lemma sat_Leib: assumes wA: "wff⇘α⇙(A)" and wB: "wff⇘α⇙(B)" and xi: "asg ξ"
  shows "vl (Ee ξ (A ❙≐⇘α⇙ B)) ⟷ Ee ξ A = Ee ξ B"
proof -
  have lcA: "lc A" and lcB: "lc B" using wA wB by (auto intro: wff_lc)
  define p where "p = fresh (fvs A ∪ fvs B)"
  have p: "p ∉ fvs A" "p ∉ fvs B"
    unfolding p_def using fresh_notin[of "fvs A ∪ fvs B"] by auto
  let ?b = "(Bnd 0 ❙⋅ A) ❙⊃ (Bnd 0 ❙⋅ B)"
  have wI: "wff⇘(α❙⇒𝗈)❙⇒𝗈⇙(❙Λ⇘α❙⇒𝗈⇙ ?b)"
    by (smt (verit, del_insts) ImpB_def lcA lcB opn.simps(1,4,5,9) opn_lc wA wB
        wff_AbsI wff_App wff_Fre wff_ImpB)
  have pf: "p ∉ fvs ?b" using p by (auto simp: ImpB_def)
  have unf: "vl (Ee ξ (A ❙≐⇘α⇙ B)) ⟷ (∀r. Dm (α ❙⇒ 𝗈) r
      ⟶ (vl (Ap r (Ee ξ A)) ⟶ vl (Ap r (Ee ξ B))))"
  proof -
    have inner: "vl (Ee (ξ(p⇘α ❙⇒ 𝗈⇙ := r)) (?b❙⟨p⇧f⇘α ❙⇒ 𝗈⇙❙⟩))
        ⟷ (vl (Ap r (Ee ξ A)) ⟶ vl (Ap r (Ee ξ B)))"
      if r: "Dm (α ❙⇒ 𝗈) r" for r 
    proof -
      let ?ξ = "ξ(p⇘α ❙⇒ 𝗈⇙ := r)"
      have ob: "?b❙⟨p⇧f⇘α ❙⇒ 𝗈⇙❙⟩ = (p⇧f⇘α ❙⇒ 𝗈⇙ ❙⋅ A) ❙⊃ (p⇧f⇘α ❙⇒ 𝗈⇙ ❙⋅ B)"
        by (simp add: opn_lc[OF lcA] opn_lc[OF lcB])
      have cA: "Ee ?ξ A = Ee ξ A"
        using p ev_coin[OF wA asg_upd[OF xi r] xi]
        unfolding upd_def fvs_eq_fst_occ image_iff by force
      have cB: "Ee ?ξ B = Ee ξ B"
        using p ev_coin[OF wB asg_upd[OF xi r] xi]
        unfolding upd_def fvs_eq_fst_occ image_iff by force
      show ?thesis unfolding ob
        by (smt (verit, del_insts) asg_upd cA cB ev_app ev_var sat_ImpB that upd_same wA wB
            wff_App wff_AppE wff_App_FreFre wff_FreE xi)
    qed
    show ?thesis
      unfolding ev_beta[OF Leib_beq[OF wA wB] xi] sat_Forall[OF wI pf xi]
      using inner by blast
  qed
  show ?thesis 
  proof
    assume L: "vl (Ee ξ (A ❙≐⇘α⇙ B))"
    let ?r = "Ap (Ee ξ (Eq α)) (Ee ξ A)"
    have rA: "vl (Ap ?r (Ee ξ A))"
      using vl_eq[OF xi ev_type[OF wA xi] ev_type[OF wA xi]] by simp
    have "vl (Ap ?r (Ee ξ B))"
      using unf L as_appTy[OF ev_type[OF wff_Eq xi] ev_type[OF wA xi]] rA by blast
    thus "Ee ξ A = Ee ξ B"
      using vl_eq[OF xi ev_type[OF wA xi] ev_type[OF wB xi]] by simp
  qed(simp add: unf)
qed

end

subsubsection ‹The evaluation variant at a parameter›

context bkk_model
begin

text ‹Agreement under the variable shift: shifting all free variables and the
  assignment in step leaves denotations unchanged (property f resolves the
  abstraction case applicatively).›

lemma Ee_vshift:
  assumes ‹wff⇘τ⇙(A)› ‹asg ξ› ‹asg ξ'› ‹⋀n τ'. (n, τ') ∈ occ A ⟹ ξ' (Suc n) τ' = ξ n τ'›
  shows ‹Ee ξ' (vshift A) = Ee ξ A›
using assms proof (induction A arbitrary: τ ξ ξ' rule: size_induct)
  case (App s u)
  then obtain σ where ws: "wff⇘σ❙⇒τ⇙(s)" and wu: "wff⇘σ⇙(u)"
      using App by auto
  have IHs: "Ee ξ' (vshift s) = Ee ξ s"
    using App wf by auto
  have IHu: "Ee ξ' (vshift u) = Ee ξ u"
    using App by auto
  have "Ee ξ' (vshift (s ❙⋅ u)) = Ee ξ' (vshift s ❙⋅ vshift u)"
    by (simp add: vshift_def)
  also have "… = Ap (Ee ξ' (vshift s)) (Ee ξ' (vshift u))"
    by (meson ev_app App.prems(3) wff_vshift ws wu) 
  also have "… = Ap (Ee ξ s) (Ee ξ u)" by (simp add: IHs IHu)
  also have "… = Ee ξ (s ❙⋅ u)"
    by (simp add: ev_app[OF ws wu App.prems(2)])
  finally show ?case using App by simp
next
  case (Abs σ b)
  then obtain τ' where t: "τ = σ ❙⇒ τ'" and wA: "wff⇘σ❙⇒τ'⇙(❙Λ⇘σ⇙ b)"
    by (metis wff_AbsE)
  have wS: "wff⇘σ❙⇒τ'⇙(❙Λ⇘σ⇙ (vshift b))"
    using wff_vshift[OF wA] by (simp add: vshift_def)
  define y where "y = fresh (fvs b)"
  have y: "y ∉ fvs b" unfolding y_def by (simp add: fresh_notin)
  have y': "Suc y ∉ fvs (vshift b)"
    using y by (force simp: occ_vshift fvs_eq_fst_occ)
  {
    fix d
    assume d: "Dm σ d"
    have IH: "Ee (ξ'(Suc y⇘σ⇙ := d)) (vshift (b❙⟨y⇧f⇘σ⇙❙⟩)) = Ee (ξ(y⇘σ⇙ := d)) (b❙⟨y⇧f⇘σ⇙❙⟩)"
    proof (rule Abs.IH)
      show "size (b❙⟨y⇧f⇘σ⇙❙⟩) ≤ size b" using Abs by simp
    next
      fix n τ''
      assume o: "(n, τ'') ∈ occ (b❙⟨y⇧f⇘σ⇙❙⟩)"
      hence "(n, τ'') ∈ occ b ∨ (n, τ'') = (y, σ)"
          using occ_opn[of 0 "y⇧f⇘σ⇙" b] by auto
      thus "(ξ'(Suc y⇘σ⇙ := d)) (Suc n) τ'' = (ξ(y⇘σ⇙ := d)) n τ''"
        using Abs by (auto simp: upd_def)
    qed(auto intro: wff_Abs_open[OF wA y] asg_upd[OF Abs.prems(2) d] asg_upd[OF Abs.prems(3) d])
    hence "Ap (Ee ξ' (❙Λ⇘σ⇙ (vshift b))) d = Ap (Ee ξ (❙Λ⇘σ⇙ b)) d"
      using ev_abs_app[OF wS Abs.prems(3) y', OF d] ev_abs_app[OF wA Abs.prems(2) y, OF d]
      by (simp add: vshift_opn)
  }
  hence "Ee ξ' (❙Λ⇘σ⇙ (vshift b)) = Ee ξ (❙Λ⇘σ⇙ b)"
      using prop_f ev_type[OF wS Abs.prems(3)] ev_type[OF wA
      Abs.prems(2)] unfolding functional_def by blast
  thus ?case using Abs by (simp add: vshift_def)
qed(auto simp: Ee_closed vshift_def ev_var)

text ‹BKK's ‹E'› (the ‹NK(ΠI)› case of Theorem 7.3): the parameter ‹w› is read as the
  freshly freed variable ‹0›, assigned ‹a›.›

definition upshift :: "(nat ⇒ ty ⇒ 'u) ⇒ ty ⇒ 'u ⇒ nat ⇒ ty ⇒ 'u" where
  "upshift ξ σ a = (λn τ. case n of 0 ⇒ (if τ = σ then a else ξ 0 τ) | Suc m ⇒ ξ m τ)"
definition Evar :: "'p ⇒ ty ⇒ 'u ⇒ (nat ⇒ ty ⇒ 'u) ⇒ 'p tm ⇒ 'u" where
  "Evar w σ a ξ A = Ee (upshift ξ σ a) (pvar w σ 0 (vshift A))"
lemma asg_upshift: "asg ξ ⟹ Dm σ a ⟹ asg (upshift ξ σ a)"
  by (auto simp: asg_def upshift_def split: nat.splits)
lemma Evar_par: "asg ξ ⟹ Dm σ a ⟹ Evar w σ a ξ (w⇧p⇘σ⇙) = a"
  by (smt (verit, del_insts) Evar_def asg_upshift bkk_model.upshift_def
      bkk_model_axioms ev_var msub.simps(3) old.nat.simps(4) pvar.simps(3) vshift_def)
lemma Evar_agree: "wff⇘τ⇙(A) ⟹ asg ξ ⟹ Dm σ a ⟹ w ∉ pars A ⟹ Evar w σ a ξ A = Ee ξ A" 
  using Evar_def asg_upshift bkk_model.Ee_vshift bkk_model_axioms
        pars_vshift upshift_def by fastforce
lemma Evar_bkk: assumes a: "Dm σ a" shows "bkk_model Dm Ap (Evar w σ a) vl"
proof (unfold_locales, goal_cases)
  case 1 thus ?case
    by (simp add: Evar_def asg_upshift assms ev_type wff_pvar wff_vshift)
next
  case 2 thus ?case
    by (metis Evar_agree assms emptyE ev_var tm.simps(230) wff_Fre)
next
  case 3 thus ?case
    by (simp add: Evar_def vshift_def)
       (metis asg_upshift assms ev_app vshift_def wff_pvar wff_vshift)
next
  case (4 τ A ξ ξ')
  have ag: "upshift ξ σ a n τ' = upshift ξ' σ a n τ'"
    if o: "(n, τ') ∈ occ (pvar w σ 0 (vshift A))" for n τ'
  proof -
    from o have "(n, τ') ∈ occ (vshift A) ∪ {(0, σ)}"
        using occ_pvar[of w σ 0 "vshift A"] by blast
    then consider (sh) m where "n = Suc m" "(m, τ') ∈ occ A" |
        (zero) "n = 0" "τ' = σ" by (auto simp: occ_vshift)
    thus ?thesis using "4"(4) upshift_def by fastforce
  qed
  show ?case unfolding Evar_def 
    by (rule ev_coin[OF wff_pvar[OF wff_vshift[OF 4(1)]]
        asg_upshift[OF 4(2) a] asg_upshift[OF 4(3) a] ag])
next
  case 5 thus ?case
    by (metis (full_types) Evar_def asg_upshift assms beq_pvar beq_vshift ev_beta)
qed(auto simp: Evar_def asg_upshift assms vl_eq vl_pi vl_dis vl_neg vl_iota
               vshift_def prop_b prop_f)

end

subsubsection ‹Soundness›

text ‹BKK Theorem 7.3, for the class ‹ℳ⇘βfb⇙› (with primitive equality and description):
  each case mirrors BKK's proof text.›

theorem soundness_bkk:
  assumes "Φ ⊢ C" "bkk_model Dm Ap Ee vl" "app_struct.asg Dm ξ"
          "∀A ∈ Φ. wff⇘𝗈⇙(A)" "∀A ∈ Φ. vl (Ee ξ A)"
    shows "vl (Ee ξ C)"
using assms proof (induction arbitrary: Dm Ap Ee vl ξ rule: bprov.induct)
  case Hyp thus ?case by blast
next
  case Beta thus ?case
    by (metis bkk_model_def sigma_eval.ev_beta sigma_model.axioms(1))
next 
  case NegI thus ?case
    by (metis UnE bkk_model_def sigma_model.sat_Neg sigma_model.vl_TF singleton_iff)
next
  case NegE thus ?case
    using bkk_model.axioms(1) bprov_wff sigma_model.sat_Neg by fastforce
next
  case DisIL thus ?case
    by (metis Hyp bprov_wff bkk_model.axioms(1) sigma_model.sat_Dis)
next
  case DisIR thus ?case
    by (metis bprov_wff sigma_model.sat_Dis bkk_model.axioms(1))
next
  case DisE thus ?case
    by (metis UnE bkk_model.axioms(1) sigma_model.sat_Dis singleton_iff)
next
  case (PiI Φ G w α)
  interpret M: bkk_model Dm Ap Ee vl by (rule PiI.prems(1))
  have wGw: "wff⇘𝗈⇙(G ❙⋅ (w⇧p⇘α⇙))"
    using bprov_wff[OF PiI.hyps(1)] PiI.prems(3) by blast
  have "vl (Ap (Ee ξ G) a)" if a: "Dm α a" for a 
  proof -
    let ?E = "M.Evar w α a"
    interpret V: bkk_model Dm Ap ?E vl by (rule M.Evar_bkk[OF a])
    have sat: "∀A ∈ Φ. vl (?E ξ A)" using PiI.prems(3,4) PiI.hyps(4)
        by (auto simp: M.Evar_agree[OF _ PiI.prems(2) a])
    have "vl (?E ξ (G ❙⋅ (w⇧p⇘α⇙)))" by (rule PiI.IH[OF M.Evar_bkk[OF a]
        PiI.prems(2) PiI.prems(3) sat])
    moreover have "?E ξ (G ❙⋅ (w⇧p⇘α⇙)) = Ap (Ee ξ G) a"
        by (simp add: V.ev_app[OF PiI.hyps(2) wff_Par PiI.prems(2)]
          M.Evar_agree[OF PiI.hyps(2) PiI.prems(2) a PiI.hyps(3)]
              M.Evar_par[OF PiI.prems(2) a])
    ultimately show ?thesis by simp
  qed
  thus ?case by (simp add: M.sat_Pi[OF PiI.hyps(2) PiI.prems(2)])
next
  case (PiE Φ α G A)
  interpret M: bkk_model Dm Ap Ee vl by (rule PiE.prems(1))
  have wPiG: "wff⇘𝗈⇙(Pi α ❙⋅ G)" using bprov_wff[OF PiE.hyps(1)]
      PiE.prems(3) by blast
  have wG: "wff⇘α❙⇒𝗈⇙(G)" using wPiG by (auto dest: wff_unique)
  have "vl (Ap (Ee ξ G) (Ee ξ A))" using PiE.IH[OF PiE.prems]
      M.sat_Pi[OF wG PiE.prems(2)]
      M.ev_type[OF PiE.hyps(2) PiE.prems(2)] by simp
  thus ?case by (simp add: M.ev_app[OF wG PiE.hyps(2) PiE.prems(2)])
next
  case Contr thus ?case
    using bkk_model.axioms(1) sigma_model.sat_Neg sigma_model.vl_TF by fastforce
next
  case (FuncE Φ α G β H)
  interpret M: bkk_model Dm Ap Ee vl by (rule FuncE.prems(1))
  have lcG: "lc G" and lcH: "lc H" using FuncE.hyps(2,3)
    by (auto intro: wff_lc)
  define y where "y = fresh (fvs G ∪ fvs H)"
  have y: "y ∉ fvs G" "y ∉ fvs H" unfolding y_def
    using fresh_notin[of "fvs G ∪ fvs H"] by auto
  let ?b = "G ❙⋅ Bnd 0 ❙≐⇘β⇙ H ❙⋅ Bnd 0"
  have wI: "wff⇘α❙⇒𝗈⇙(❙Λ⇘α⇙ ?b)"
    by (auto intro!: wff_AbsI wff_App[OF FuncE.hyps(2) wff_Fre] wff_App[OF FuncE.hyps(3) wff_Fre]
             simp: opn_lc[OF lcG] opn_lc[OF lcH])
  have yb: "y ∉ fvs ?b" using y by (auto simp: Leib_def Forall_def ImpB_def)
  have pointwise: "Ap (Ee ξ G) d = Ap (Ee ξ H) d" if d: "Dm α d" for d
  proof -
    let ?ξ = "ξ(y⇘α⇙ := d)"
    have "vl (Ee ξ (❙Π⇘α⇙ ?b))" using FuncE.IH[OF FuncE.prems] .
    hence "vl (Ee ?ξ (?b❙⟨y⇧f⇘α⇙❙⟩))"
      using FuncE.prems(2) M.sat_Forall that wI yb by blast
    hence "vl (Ee ?ξ (G ❙⋅ (y⇧f⇘α⇙) ❙≐⇘β⇙ H ❙⋅ (y⇧f⇘α⇙)))"
        by (simp add: opn_lc[OF lcG] opn_lc[OF lcH])
    hence "Ee ?ξ (G ❙⋅ (y⇧f⇘α⇙)) = Ee ?ξ (H ❙⋅ (y⇧f⇘α⇙))"
      by (meson FuncE.hyps(2,3) FuncE.prems(2) M.sat_Leib M.sigma_model_axioms app_struct.asg_upd
                sigma_eval_def sigma_model_def that wff_App wff_Fre)
    moreover have "Ee ?ξ G = Ee ξ G"
      by (metis (mono_tags, lifting) FuncE.hyps(2) FuncE.prems(2) M.asg_upd M.ev_coin fst_conv
                fvs_eq_fst_occ image_eqI that upd_def y(1))
    moreover have "Ee ?ξ H = Ee ξ H"
      by (metis (mono_tags, lifting) FuncE.hyps(3) FuncE.prems(2) M.asg_upd M.ev_coin fst_conv
                fvs_eq_fst_occ image_eqI that upd_def y(2))
    ultimately show ?thesis
      by (metis FuncE.hyps(2,3) FuncE.prems(2) M.asg_upd M.ev_app M.ev_var that upd_same wff_Fre)
  qed
  have "Ee ξ G = Ee ξ H"
    using FuncE.hyps(2,3) FuncE.prems(2) M.ev_type M.functional_def M.prop_f pointwise by blast
  thus ?case by (simp add: M.sat_Leib[OF FuncE.hyps(2,3) FuncE.prems(2)])
next
  case (BoolE Φ A B)
  interpret M: bkk_model Dm Ap Ee vl by (rule BoolE.prems(1))
  have "vl (Ee ξ A) ⟷ vl (Ee ξ B)"
    using BoolE by fast
  hence "Ee ξ A = Ee ξ B"
    by (simp add: BoolE.hyps(3,4) BoolE.prems(2) M.ev_type M.prop_b)
  thus ?case
    by (simp add: M.sat_Leib[OF BoolE.hyps(3,4) BoolE.prems(2)])
next case (Desc α A Φ)
  interpret M: bkk_model Dm Ap Ee vl by (rule Desc.prems(1))
  define y where "y = fresh (fvs A)"
  have y: "y ∉ fvs A" unfolding y_def by (simp add: fresh_notin)
  let ?f = "Ee ξ (Leib α ❙⋅ A)"
  have sing: "vl (Ap ?f b) ⟷ b = Ee ξ A" if b: "Dm α b" for b 
  proof -
    let ?ξ = "ξ(y⇘α⇙ := b)"
    have c: "Ee ?ξ (Leib α ❙⋅ A) = ?f"
      using y
      by (safe intro!: M.ev_coin[OF wff_App[OF wff_Leib Desc.hyps]
                                    M.asg_upd[OF Desc.prems(2) b] Desc.prems(2)])
         (auto simp add: Forall_def ImpB_def Leib_def upd_def fvs_eq_fst_occ image_iff)
    have cA: "Ee ?ξ A = Ee ξ A"
      by (metis (mono_tags, lifting) Desc.hyps Desc.prems(2) M.asg_upd M.ev_coin fst_conv
                fvs_eq_fst_occ image_eqI that upd_def y)
    have "Ap ?f b = Ee ?ξ (A ❙≐⇘α⇙ (y⇧f⇘α⇙))"
      by (simp add: M.ev_app[OF wff_App[OF wff_Leib Desc.hyps]
            wff_Fre M.asg_upd[OF Desc.prems(2) b]]
            M.ev_var[OF M.asg_upd[OF Desc.prems(2) b]] c)
    thus ?thesis
      by (metis Desc.hyps that cA Desc.prems(2) wff_Fre M.sat_Leib M.ev_var app_struct.asg_upd
                upd_same M.app_struct_axioms)
  qed
  have "Ee ξ (Iota α ❙⋅ (Leib α ❙⋅ A)) = Ee ξ A"
    using M.vl_iota[OF Desc.prems(2) M.ev_type[OF wff_App[OF wff_Leib Desc.hyps] Desc.prems(2)]
                    M.ev_type[OF Desc.hyps Desc.prems(2)]] sing 
    by (simp add: M.ev_app[OF wff_Iota wff_App[OF wff_Leib Desc.hyps]
        Desc.prems(2)])
  thus ?case 
    by (simp add: M.sat_Leib[OF wff_App[OF wff_Iota wff_App[OF wff_Leib Desc.hyps]]
                  Desc.hyps Desc.prems(2)])
next
  case (EqR α A Φ)
  interpret M: bkk_model Dm Ap Ee vl by (rule EqR.prems(1))
  show ?case
    by (simp add: M.ev_app[OF wff_App[OF wff_Eq EqR.hyps] EqR.hyps EqR.prems(2)]
        M.ev_app[OF wff_Eq EqR.hyps EqR.prems(2)]
        M.vl_eq[OF EqR.prems(2) M.ev_type[OF EqR.hyps EqR.prems(2)]
                    M.ev_type[OF EqR.hyps EqR.prems(2)]])
next case (EqL Φ C α D)
  interpret M: bkk_model Dm Ap Ee vl by (rule EqL.prems(1))
  have wCD: "wff⇘𝗈⇙(C ❙=⇘α⇙ D)" using bprov_wff[OF EqL.hyps(1)] EqL.prems(3)
    by blast
  have wC: "wff⇘α⇙(C)" and wD: "wff⇘α⇙(D)" using wCD
    by (auto dest: wff_unique)
  have "vl (Ee ξ (C ❙=⇘α⇙ D))" using EqL.IH[OF EqL.prems] .
  hence "Ee ξ C = Ee ξ D"
    by (simp add: M.ev_app[OF wff_App[OF wff_Eq wC] wD EqL.prems(2)]
        M.ev_app[OF wff_Eq wC EqL.prems(2)]
        M.vl_eq[OF EqL.prems(2) M.ev_type[OF wC EqL.prems(2)] M.ev_type[OF wD EqL.prems(2)]])
  thus ?case by (simp add: M.sat_Leib[OF wC wD EqL.prems(2)])
qed


subsubsection ‹The canonical construction is a BKK model›

text ‹Every ‹Σ›-Henkin general model in the sense of Section 2 --- the
  frame-based canonical construction --- is a BKK model: take ‹E := den› and
  ‹υ := (λa. a = Tv)›.  The four evaluation conditions are the denotation lemmas,
  and the ‹L›-properties are the ‹gm›-conditions.›

sublocale general_model ⊆ bkkA: app_struct Dm Ap
  by unfold_locales (use gm_nonempty gm_appTy in blast)+

sublocale general_model ⊆ bkk: bkk_model Dm Ap "λξ A. ⦇A⦈⇘ξ⇙" "λa. a = Tv"
  by (unfold_locales;
      auto simp: bkkA.functional_def general_model_axioms[unfolded general_model_def]
                 bkkA.asg_def frame_sig.den.simps(8) resp_def
         intro: beq_den den_coincidence den_dom)


subsubsection ‹Derived rules for the defined quantifiers›

text ‹‹NK(ΠE)› and ‹NK(ΠI)› for the folded quantifier ‹❙Π⇘σ⇙›.›

lemma PiE_Forall: "Φ ⊢ ❙Π⇘α⇙ b ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ (❙Λ⇘α⇙ b) ❙⋅ A"
  unfolding Forall_def by (rule bprov.PiE)
lemma PiI_Forall: "Φ ⊢ (❙Λ⇘α⇙ b) ❙⋅ (w⇧p⇘α⇙) ⟹ wff⇘α ❙⇒ 𝗈⇙(❙Λ⇘α⇙ b) ⟹ w ∉ pars (❙Λ⇘α⇙ b)
                   ⟹ (∀D ∈ Φ. w ∉ pars D)  ⟹ Φ ⊢ ❙Π⇘α⇙ b"
  unfolding Forall_def by (rule bprov.PiI)

text ‹Existential elimination at a fresh eigen-parameter, for the defined quantifier
  ‹❙∃ = ❙¬❙Π❙¬›: the derived counterpart of the paper-style step ``obtain a witness''.›

lemma ExE: assumes ex: "Φ ⊢ ❙∃⇘σ⇙ b" and step: "Φ ∪ {b❙⟨w⇧p⇘σ⇙❙⟩} ⊢ C"
    and wb: "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ b)" 
  and wC: "wff⇘𝗈⇙(C)" and wpb: "w ∉ pars b" and wpC: "w ∉ pars C"
      and wpΦ: "∀D ∈ Φ. w ∉ pars D" and fp: "freep Φ" 
  shows "Φ ⊢ C"
proof -
  have wNb: "wff⇘σ ❙⇒ 𝗈⇙(❙Λ⇘σ⇙ (❙¬ b))"
    by (auto intro!: wff_opn[OF wb] wff_Fre wff_AbsI)
  have fp1: "freep (Φ ∪ {❙¬ C})" using freep_add[OF fp] by simp
  have fp2: "freep (Φ ∪ {❙¬ C} ∪ {b❙⟨w⇧p⇘σ⇙❙⟩})"
      using freep_add[OF freep_add[OF fp]] by simp
  have s1: "Φ ∪ {❙¬ C} ∪ {b❙⟨w⇧p⇘σ⇙❙⟩} ⊢ C"
    by (rule bprov_weaken[OF step _ fp2]) auto
  have s2: "Φ ∪ {❙¬ C} ∪ {b❙⟨w⇧p⇘σ⇙❙⟩} ⊢ ❙¬ C" by (auto intro: bprov.Hyp)
  have bq: "(❙Λ⇘σ⇙ (❙¬ b)) ❙⋅ (w⇧p⇘σ⇙) ≈⇘𝗈⇙ ❙¬ (b❙⟨w⇧p⇘σ⇙❙⟩)"
      using beq.beta[OF wNb wff_Par] by simp
    have s5: "Φ ∪ {❙¬ C} ⊢ ❙Π⇘σ⇙ (❙¬ b)"
      using wpb wpC wpΦ
      by (safe intro!:
          PiI_Forall[OF bprov.Beta[OF beq.sym[OF bq] bprov.NegI[OF
                bprov.NegE[OF s2 s1 wff_FalseB] wff_opn[OF wb wff_Par]]] wNb]) auto
  have s6: "Φ ∪ {❙¬ C} ⊢ ❙¬ (❙Π⇘σ⇙ (❙¬ b))" by (rule bprov_weaken[OF ex _ fp1]) auto
  show ?thesis by (rule bprov.Contr[OF bprov.NegE[OF s6 s5 wff_FalseB] wC])
qed

text ‹Universal instantiation directly at the ‹β›-reduced instance.›

lemma PiE_open: "Φ ⊢ ❙Π⇘α⇙ b ⟹ wff⇘α ❙⇒ 𝗈⇙(❙Λ⇘α⇙ b) ⟹ wff⇘α⇙(A) ⟹ Φ ⊢ b❙⟨A❙⟩" 
  by (metis PiE_Forall beq.beta bprov.Beta)

text ‹Soundness, repackaged in the validity and satisfaction notation: the two
  forms used by the closing summary.›

theorem soundness_sat:
  "Φ ⊢ C ⟹ Φ ⊨('u) C"
  by (simp add: bkk_consequence_def rel_truth_def soundness_bkk)

theorem soundness_valid: "⊢ A ⟹ ⊨('u) A"
  unfolding bkk_valid_def rel_truth_def
  by (auto intro: soundness_bkk[of "{}" A])

end