Theory Soundness

theory Soundness
  imports Calculus Semantics
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 ‹Abstract soundness (BKK Theorem 7.3)›

text ‹Soundness over the abstract ‹Σ›-models of theory ‹Semantics›, 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 route them through
  Theorem 4.3 and Lemma 3.48).›

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).›

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 ‹Every general model is a BKK model›

text ‹The ‹Σ›-model predicate of a general model --- the frame-based construction with the
  recursive denotation as evaluation --- exported from the sublocale
  ‹general_model ⊆ bkk_model› of theory ‹Semantics›.›

lemma (in general_model) bkk_model_pred:
  "bkk_model Dm Ap (λξ A. ⦇A⦈⇘ξ⇙) (λa. a = Tv)" by intro_locales

text ‹Consistency from a single model: a general model that satisfies every member of ‹Φ›
  under some total assignment certifies ‹Φ› consistent --- a derivation of ‹❙⊥› would, by
  soundness, make ‹❙⊥› denote ‹Tv›.  Every concrete consistency proof of this development
  is an instance.›

lemma (in general_model) model_con:
  assumes xi: "bkkA.asg ξ"
      and sat: "∀B ∈ Φ. wff⇘𝗈⇙(B) ∧ ⦇B⦈⇘ξ⇙ = Tv"
  shows "con Φ"
proof (rule con_I)
  assume d: "Φ ⊢ ❙⊥"
  have "⦇❙⊥⦈⇘ξ⇙ = Tv"
    by (rule soundness_bkk[OF d bkk_model_pred xi]) (use sat in auto)
  thus False using bkk.vl_TF[OF xi] by simp
qed


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

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])

text ‹Soundness for the hypothesis relation ‹⊩›: the witnessing finite sub-context is
  sound, and consequence is monotone in the hypotheses.›

theorem soundness_fprov:
  assumes "Φ ⊩ C" shows "Φ ⊨('u) C"
proof -
  from assms obtain Φ⇩0 where "Φ⇩0 ⊆ Φ" and "Φ⇩0 ⊢ C"
    by (auto simp: fprov_def)
  from soundness_sat[OF this(2)] this(1) show ?thesis
    by (rule bkk_consequence_mono)
qed

end