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