Theory Ordered_Resolution_Prover.Inference_System

(*  Title:       Refutational Inference Systems
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2017
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

section ‹Refutational Inference Systems›

theory Inference_System
  imports Herbrand_Interpretation
begin

text ‹
This theory gathers results from Section 2.4 (``Refutational Theorem Proving''), 3 (``Standard
Resolution''), and 4.2 (``Counterexample-Reducing Inference Systems'') of Bachmair and Ganzinger's
chapter.
›


subsection ‹Preliminaries›

text ‹
Inferences have one distinguished main premise, any number of side premises, and a conclusion.
›

datatype 'a inference =
  Infer (side_prems_of: "'a clause multiset") (main_prem_of: "'a clause") (concl_of: "'a clause")

abbreviation prems_of :: "'a inference ⇒ 'a clause multiset" where
  "prems_of γ ≡ side_prems_of γ + {#main_prem_of γ#}"

abbreviation concls_of :: "'a inference set ⇒ 'a clause set" where
  "concls_of Γ ≡ concl_of ` Γ"

definition infer_from :: "'a clause set ⇒ 'a inference ⇒ bool" where
  "infer_from CC γ ⟷ set_mset (prems_of γ) ⊆ CC"

locale inference_system =
  fixes Γ :: "'a inference set"
begin

definition inferences_from :: "'a clause set ⇒ 'a inference set" where
  "inferences_from CC = {γ. γ ∈ Γ ∧ infer_from CC γ}"

definition inferences_between :: "'a clause set ⇒ 'a clause ⇒ 'a inference set" where
  "inferences_between CC C = {γ. γ ∈ Γ ∧ infer_from (CC ∪ {C}) γ ∧ C ∈# prems_of γ}"

lemma inferences_from_mono: "CC ⊆ DD ⟹ inferences_from CC ⊆ inferences_from DD"
  unfolding inferences_from_def infer_from_def by fast

definition saturated :: "'a clause set ⇒ bool" where
  "saturated N ⟷ concls_of (inferences_from N) ⊆ N"

lemma saturatedD:
  assumes
    satur: "saturated N" and
    inf: "Infer CC D E ∈ Γ" and
    cc_subs_n: "set_mset CC ⊆ N" and
    d_in_n: "D ∈ N"
  shows "E ∈ N"
proof -
  have "Infer CC D E ∈ inferences_from N"
    unfolding inferences_from_def infer_from_def using inf cc_subs_n d_in_n by simp
  then have "E ∈ concls_of (inferences_from N)"
    unfolding image_iff by (metis inference.sel(3))
  then show "E ∈ N"
    using satur unfolding saturated_def by blast
qed

end

text ‹
Satisfiability preservation is a weaker requirement than soundness.
›

locale sat_preserving_inference_system = inference_system +
  assumes Γ_sat_preserving: "satisfiable N ⟹ satisfiable (N ∪ concls_of (inferences_from N))"

locale sound_inference_system = inference_system +
  assumes Γ_sound: "Infer CC D E ∈ Γ ⟹ I ⊨m CC ⟹ I ⊨ D ⟹ I ⊨ E"
begin

lemma Γ_sat_preserving:
  assumes sat_n: "satisfiable N"
  shows "satisfiable (N ∪ concls_of (inferences_from N))"
proof -
  obtain I where i: "I ⊨s N"
    using sat_n by blast
  then have "⋀CC D E. Infer CC D E ∈ Γ ⟹ set_mset CC ⊆ N ⟹ D ∈ N ⟹ I ⊨ E"
    using Γ_sound unfolding true_clss_def true_cls_mset_def by (simp add: subset_eq)
  then have "⋀γ. γ ∈ Γ ⟹ infer_from N γ ⟹ I ⊨ concl_of γ"
    unfolding infer_from_def by (case_tac γ) clarsimp
  then have "I ⊨s concls_of (inferences_from N)"
    unfolding inferences_from_def image_def true_clss_def infer_from_def by blast
  then have "I ⊨s N ∪ concls_of (inferences_from N)"
    using i by simp
  then show ?thesis
    by blast
qed

sublocale sat_preserving_inference_system
  by unfold_locales (erule Γ_sat_preserving)

end

locale reductive_inference_system = inference_system Γ for Γ :: "('a :: wellorder) inference set" +
  assumes Γ_reductive: "γ ∈ Γ ⟹ concl_of γ < main_prem_of γ"


subsection ‹Refutational Completeness›

text ‹
Refutational completeness can be established once and for all for counterexample-reducing inference
systems. The material formalized here draws from both the general framework of Section 4.2 and the
concrete instances of Section 3.
›

locale counterex_reducing_inference_system =
  inference_system Γ for Γ :: "('a :: wellorder) inference set" +
  fixes I_of :: "'a clause set ⇒ 'a interp"
  assumes Γ_counterex_reducing:
    "{#} ∉ N ⟹ D ∈ N ⟹ ¬ I_of N ⊨ D ⟹ (⋀C. C ∈ N ⟹ ¬ I_of N ⊨ C ⟹ D ≤ C) ⟹
     ∃CC E. set_mset CC ⊆ N ∧ I_of N ⊨m CC ∧ Infer CC D E ∈ Γ ∧ ¬ I_of N ⊨ E ∧ E < D"
begin

lemma ex_min_counterex:
  fixes N :: "('a :: wellorder) clause set"
  assumes "¬ I ⊨s N"
  shows "∃C ∈ N. ¬ I ⊨ C ∧ (∀D ∈ N. D < C ⟶ I ⊨ D)"
proof -
  obtain C where "C ∈ N" and "¬ I ⊨ C"
    using assms unfolding true_clss_def by auto
  then have c_in: "C ∈ {C ∈ N. ¬ I ⊨ C}"
    by blast
  show ?thesis
    using wf_eq_minimal[THEN iffD1, rule_format, OF wf_less_multiset c_in] by blast
qed

(* Theorem 4.4 (generalizes Theorems 3.9 and 3.16) *)

theorem saturated_model:
  assumes
    satur: "saturated N" and
    ec_ni_n: "{#} ∉ N"
  shows "I_of N ⊨s N"
proof -
  {
    assume "¬ I_of N ⊨s N"
    then obtain D where
      d_in_n: "D ∈ N" and
      d_cex: "¬ I_of N ⊨ D" and
      d_min: "⋀C. C ∈ N ⟹ C < D ⟹ I_of N ⊨ C"
      by (meson ex_min_counterex)
    then obtain CC E where
      cc_subs_n: "set_mset CC ⊆ N" and
      inf_e: "Infer CC D E ∈ Γ" and
      e_cex: "¬ I_of N ⊨ E" and
      e_lt_d: "E < D"
      using Γ_counterex_reducing[OF ec_ni_n] not_less by metis
    from cc_subs_n inf_e have "E ∈ N"
      using d_in_n satur by (blast dest: saturatedD)
    then have False
      using e_cex e_lt_d d_min not_less by blast
  }
  then show ?thesis
    by satx
qed

text ‹
Cf. Corollary 3.10:
›

corollary saturated_complete: "saturated N ⟹ ¬ satisfiable N ⟹ {#} ∈ N"
  using saturated_model by blast

end


subsection ‹Compactness›

text ‹
Bachmair and Ganzinger claim that compactness follows from refutational completeness but leave the
proof to the readers' imagination. Our proof relies on an inductive definition of saturation in
terms of a base set of clauses.
›

context inference_system
begin

inductive_set saturate :: "'a clause set ⇒ 'a clause set" for CC :: "'a clause set" where
  base: "C ∈ CC ⟹ C ∈ saturate CC"
| step: "Infer CC' D E ∈ Γ ⟹ (⋀C'. C' ∈# CC' ⟹ C' ∈ saturate CC) ⟹ D ∈ saturate CC ⟹
    E ∈ saturate CC"

lemma saturate_mono: "C ∈ saturate CC ⟹ CC ⊆ DD ⟹ C ∈ saturate DD"
  by (induct rule: saturate.induct) (auto intro: saturate.intros)

lemma saturated_saturate[simp, intro]: "saturated (saturate N)"
  unfolding saturated_def inferences_from_def infer_from_def image_def
  by clarify (rename_tac x, case_tac x, auto elim!: saturate.step)

lemma saturate_finite: "C ∈ saturate CC ⟹ ∃DD. DD ⊆ CC ∧ finite DD ∧ C ∈ saturate DD"
proof (induct rule: saturate.induct)
  case (base C)
  then have "{C} ⊆ CC" and "finite {C}" and "C ∈ saturate {C}"
    by (auto intro: saturate.intros)
  then show ?case
    by blast
next
  case (step CC' D E)
  obtain DD_of where
    "⋀C. C ∈# CC' ⟹ DD_of C ⊆ CC ∧ finite (DD_of C) ∧ C ∈ saturate (DD_of C)"
    using step(3) by metis
  then have
    "(⋃C ∈ set_mset CC'. DD_of C) ⊆ CC"
    "finite (⋃C ∈ set_mset CC'. DD_of C) ∧ set_mset CC' ⊆ saturate (⋃C ∈ set_mset CC'. DD_of C)"
    by (auto intro: saturate_mono)
  then obtain DD where
    d_sub: "DD ⊆ CC" and d_fin: "finite DD" and in_sat_d: "set_mset CC' ⊆ saturate DD"
    by blast
  obtain EE where
    e_sub: "EE ⊆ CC" and e_fin: "finite EE" and in_sat_ee: "D ∈ saturate EE"
    using step(5) by blast
  have "DD ∪ EE ⊆ CC"
    using d_sub e_sub step(1) by fast
  moreover have "finite (DD ∪ EE)"
    using d_fin e_fin by fast
  moreover have "E ∈ saturate (DD ∪ EE)"
    using in_sat_d in_sat_ee step.hyps(1)
    by (blast intro: inference_system.saturate.step saturate_mono)
  ultimately show ?case
    by blast
qed

end

context sound_inference_system
begin

theorem saturate_sound: "C ∈ saturate CC ⟹ I ⊨s CC ⟹ I ⊨ C"
  by (induct rule: saturate.induct) (auto simp: true_cls_mset_def true_clss_def Γ_sound)

end

context sat_preserving_inference_system
begin

text ‹
This result surely holds, but we have yet to prove it. The challenge is: Every time a new clause is
introduced, we also get a new interpretation (by the definition of
‹sat_preserving_inference_system›). But the interpretation we want here is then the one that
exists "at the limit". Maybe we can use compactness to prove it.
›

theorem saturate_sat_preserving: "satisfiable CC ⟹ satisfiable (saturate CC)"
  oops

end

locale sound_counterex_reducing_inference_system =
  counterex_reducing_inference_system + sound_inference_system
begin

text ‹
Compactness of clausal logic is stated as Theorem 3.12 for the case of unordered ground resolution.
The proof below is a generalization to any sound counterexample-reducing inference system. The
actual theorem will become available once the locale has been instantiated with a concrete inference
system.
›

theorem clausal_logic_compact:
  fixes N :: "('a :: wellorder) clause set"
  shows "¬ satisfiable N ⟷ (∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD)"
proof
  assume "¬ satisfiable N"
  then have "{#} ∈ saturate N"
    using saturated_complete saturated_saturate saturate.base unfolding true_clss_def by meson
  then have "∃DD ⊆ N. finite DD ∧ {#} ∈ saturate DD"
    using saturate_finite by fastforce
  then show "∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD"
    using saturate_sound by auto
next
  assume "∃DD ⊆ N. finite DD ∧ ¬ satisfiable DD"
  then show "¬ satisfiable N"
    by (blast intro: true_clss_mono)
qed

end

end