Theory Soundness

section "Soundness"

theory Soundness imports Completeness begin

lemma permutation_validS: "mset fs = mset gs ⟹ (validS fs = validS gs)"
  unfolding validS_def evalS_def
  using mset_eq_setD by blast

lemma modelAssigns_vblcase: "φ ∈ modelAssigns M ⟹ x ∈ objects M ⟹ vblcase x φ ∈ modelAssigns M"
  unfolding modelAssigns_def mem_Collect_eq
  by (smt (verit) image_subset_iff mem_Collect_eq range_subsetD vbl_cases
      vblcase_nextX vblcase_zeroX)

lemma soundnessFAll:
    assumes "u ∉ freeVarsFL (FAll Pos A # Gamma)"
    and "validS (instanceF u A # Gamma)"
  shows "validS (FAll Pos A # Gamma)"
unfolding validS_def
proof (intro strip)
  fix M φ
  assume φ: "φ ∈ modelAssigns M"
  have "evalF M (vblcase x φ) A" 
    if x: "x ∈ objects M" and "¬ evalS M φ Gamma" 
    for x
  proof -
    have "evalF M (vblcase x (λy. if y = u then x else φ y)) A"
    proof -
      have "evalF M (vblcase x (λy. if y = u then x else φ y)) A 
           ∨evalS M (λy. if y = u then x else φ y) Gamma"
        using φ assms(2) evalF_instance image_subset_iff validS_def x by fastforce
      then show ?thesis
        using assms(1) equalOn_def evalS_equiv freeVarsFL_cons that(2) by fastforce
    qed
    moreover
    have "equalOn (freeVarsF A) (vblcase x (λy. if y = u then x else φ y))
     (vblcase x φ)"
      by (smt (verit, best) Un_iff assms(1) equalOn_def equalOn_vblcaseI' freeVarsFAll
          freeVarsFL_cons)
    ultimately show ?thesis
      using evalF_equiv by force
  qed 
  then show "evalS M φ (FAll Pos A # Gamma) = True"
    by auto
qed

lemma soundnessFEx: "validS (instanceF x A # Gamma) ⟹ validS (FAll Neg A # Gamma)"
  unfolding validS_def
  by (metis evalF_FEx evalF_instance evalS_cons modelAssigns_iff range_subsetD)

lemma soundnessFCut: "⟦validS (C # Gamma); validS (FNot C # Delta)⟧ ⟹ validS (Gamma @ Delta)"
  using evalF_FNot evalS_append validS_def by auto

lemma soundness: "fs : deductions(PC) ⟹ validS fs"  
proof (induction fs rule: deductions.induct)
  case (inferI conc prems)
  then have vS: "∀x ∈ prems. validS x"
    by auto
  have "validS conc"
    if §: "(conc, prems) ∈ Perms"
  proof -
    obtain Δ where Δ: "prems = {Δ}"
      using § vS by (auto simp: Perms_def)
    then have "mset conc = mset Δ"
      using Perms_def that by fastforce
    with Δ permutation_validS vS show ?thesis
      by blast
  qed
  moreover have "validS conc"
    if "(conc, prems) ∈ Axioms"
    using that by (auto simp add: Axioms_def validS_def)
  moreover have "validS conc"
    if "(conc, prems) ∈ Conjs"
    using that vS inferI apply (simp add: validS_def Conjs_def)
    by (metis evalFConj evalS_append evalS_cons insertCI sign.simps(1))
  moreover have "validS conc"
    if "(conc, prems) ∈ Disjs"
    using that vS inferI by (fastforce simp add: validS_def Disjs_def)
  moreover have "validS conc"
    if "(conc, prems) ∈ Alls"
    using that vS inferI soundnessFAll 
    by (force simp add: validS_def Alls_def subset_iff)
  moreover have "validS conc"
    if "(conc, prems) ∈ Exs"
    using that vS inferI soundnessFEx
    by (force simp add: validS_def Exs_def subset_iff)
  moreover have "validS conc"
    if "(conc, prems) ∈ Weaks"
    using that vS by(force simp: Weaks_def validS_def evalS_def)
  moreover have "validS conc"
    if "(conc, prems) ∈ Contrs"
    using that vS by(fastforce simp add: Contrs_def validS_def evalS_def)
  moreover have "validS conc"
    if "(conc, prems) ∈ Cuts"
    using that vS by (force simp add: Cuts_def soundnessFCut)
  ultimately show ?case
    using inferI.hyps
    by (auto simp: PC_def subset_iff)
qed

theorem completeness: "fs ∈ deductions (PC) ⟷ validS fs"
  using adequacy mono_deductions rulesInPCs(18) soundness by blast

end