Theory Clausal_Calculus

(*  Title:       Clausal Calculi
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2020
*)

section ‹Clausal Calculi›

theory Clausal_Calculus
  imports
    Ordered_Resolution_Prover.Unordered_Ground_Resolution
    Soundness
    Standard_Redundancy_Criterion
begin

text ‹Various results about consequence relations, counterexample-reducing inference systems, and
the standard redundancy criteria are specialized and customized for clauses as opposed to arbitrary
formulas.›


subsection ‹Setup›

text ‹To avoid confusion, we use the symbol ‹⊫› (with or without subscripts) for the ``models''
and entailment relations on clauses and ‹⊨› for the abstract concept of consequence.›

abbreviation true_lit_thick :: "'a interp ⇒ 'a literal ⇒ bool" (infix ‹⊫l› 50) where
  "I ⊫l L ≡ I ⊨l L"

abbreviation true_cls_thick :: "'a interp ⇒ 'a clause ⇒ bool" (infix ‹⊫› 50) where
  "I ⊫ C ≡ I ⊨ C"

abbreviation true_clss_thick :: "'a interp ⇒ 'a clause set ⇒ bool" (infix ‹⊫s› 50) where
  "I ⊫s 𝒞 ≡ I ⊨s 𝒞"

abbreviation true_cls_mset_thick :: "'a interp ⇒ 'a clause multiset ⇒ bool" (infix ‹⊫m› 50) where
  "I ⊫m 𝒞 ≡ I ⊨m 𝒞"

no_notation true_lit (infix ‹⊨l› 50)
no_notation true_cls (infix ‹⊨› 50)
no_notation true_clss (infix ‹⊨s› 50)
no_notation true_cls_mset (infix ‹⊨m› 50)


subsection ‹Consequence Relation›

abbreviation entails_clss :: "'a clause set ⇒ 'a clause set ⇒ bool" (infix ‹⊫e› 50) where
  "N1 ⊫e N2 ≡ ∀I. I ⊫s N1 ⟶ I ⊫s N2"

lemma entails_iff_unsatisfiable_single:
  "CC ⊫e {E} ⟷ ¬ satisfiable (CC ∪ {{#- L#} |L. L ∈# E})" (is "_ ⟷ _ (_ ∪ ?NegD)")
proof
  assume c_ent_e: "CC ⊫e {E}"
  have "¬ I ⊫s CC ∪ ?NegD" for I
    using c_ent_e[rule_format, of I]
    unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
    by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
  then show "¬ satisfiable (CC ∪ ?NegD)"
    by auto
next
  assume "¬ satisfiable (CC ∪ ?NegD)"
  then have "¬ I ⊫s CC ∪ ?NegD" for I
    by auto
  then show "CC ⊫e {E}"
    unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
    by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
qed

lemma entails_iff_unsatisfiable:
  "CC ⊫e EE ⟷ (∀E ∈ EE. ¬ satisfiable (CC ∪ {{#- L#} |L. L ∈# E}))" (is "?lhs = ?rhs")
proof -
  have "?lhs ⟷ (∀E ∈ EE. CC ⊫e {E})"
    unfolding true_clss_def by auto
  also have "... ⟷ ?rhs"
    unfolding entails_iff_unsatisfiable_single by auto
  finally show ?thesis
    .
qed

interpretation consequence_relation "{{#}}" "(⊫e)"
proof
  fix N2 N1 :: "'a clause set"
  assume "∀C ∈ N2. N1 ⊫e {C}"
  then show "N1 ⊫e N2"
    unfolding true_clss_singleton by (simp add: true_clss_def)
qed (auto intro: true_clss_mono)

interpretation concl_compact_consequence_relation "{{#}} :: ('a :: wellorder) clause set" "(⊫e)"
proof
  fix CC EE :: "'a clause set"
  assume
    fin_e: "finite EE" and
    c_ent_e: "CC ⊫e EE"

  have "∀E ∈ EE. ¬ satisfiable (CC ∪ {{#- L#} |L. L ∈# E})"
    using c_ent_e[unfolded entails_iff_unsatisfiable] .
  then have "∀E ∈ EE. ∃DD ⊆ CC ∪ {{#- L#} |L. L ∈# E}. finite DD ∧ ¬ satisfiable DD"
    by (subst (asm) clausal_logic_compact)
  then obtain DD_of where
    d_of: "∀E ∈ EE. DD_of E ⊆ CC ∪ {{#- L#} |L. L ∈# E} ∧ finite (DD_of E)
      ∧ ¬ satisfiable (DD_of E)"
    by moura

  define CC' where
    "CC' = (⋃E ∈ EE. DD_of E - {{#- L#} |L. L ∈# E})"

  have "CC' ⊆ CC"
    unfolding CC'_def using d_of by auto
  moreover have c'_fin: "finite CC'"
    unfolding CC'_def using d_of fin_e by blast
  moreover have "CC' ⊫e EE"
    unfolding entails_iff_unsatisfiable
  proof
    fix E
    assume e_in: "E ∈ EE"

    have "DD_of E ⊆ CC' ∪ {{#- L#} |L. L ∈# E}"
      using e_in d_of unfolding CC'_def by auto
    moreover have "¬ satisfiable (DD_of E)"
      using e_in d_of by auto
    ultimately show "¬ satisfiable (CC' ∪ {{#- L#} |L. L ∈# E})"
      by (rule unsatisfiable_mono[of "DD_of E"])
  qed
  ultimately show "∃CC' ⊆ CC. finite CC' ∧ CC' ⊫e EE"
    by blast
qed


subsection ‹Counterexample-Reducing Inference Systems›

definition clss_of_interp :: "'a set ⇒ 'a literal multiset set" where
  "clss_of_interp I = {{#(if A ∈ I then Pos else Neg) A#} |A. True}"

lemma true_clss_of_interp_iff_equal[simp]: "J ⊫s clss_of_interp I ⟷ J = I"
  unfolding clss_of_interp_def true_clss_def true_cls_def true_lit_def by force

lemma entails_iff_models[simp]: "clss_of_interp I ⊫e CC ⟷ I ⊫s CC"
  by simp

locale clausal_counterex_reducing_inference_system = inference_system Inf
  for Inf :: "('a :: wellorder) clause inference set" +
  fixes J_of :: "'a clause set ⇒ 'a interp"
  assumes clausal_Inf_counterex_reducing:
    "{#} ∉ N ⟹ D ∈ N ⟹ ¬ J_of N ⊫ D ⟹ (⋀C. C ∈ N ⟹ ¬ J_of N ⊫ C ⟹ D ≤ C) ⟹
     ∃ι ∈ Inf. prems_of ι ≠ [] ∧ main_prem_of ι = D ∧ set (side_prems_of ι) ⊆ N ∧
       J_of N ⊫s set (side_prems_of ι) ∧ ¬ J_of N ⊫ concl_of ι ∧ concl_of ι < D"
begin

abbreviation I_of :: "'a clause set ⇒ 'a clause set" where
  "I_of N ≡ clss_of_interp (J_of N)"

lemma Inf_counterex_reducing:
  assumes
    bot_ni_n: "N ∩ {{#}} = {}" and
    d_in_n: "D ∈ N" and
    n_ent_d: "¬ I_of N ⊫e {D}" and
    d_min: "⋀C. C ∈ N ⟹ ¬ I_of N ⊫e {C} ⟹ D ≤ C"
  shows "∃ι ∈ Inf. prems_of ι ≠ [] ∧ main_prem_of ι = D ∧ set (side_prems_of ι) ⊆ N
    ∧ I_of N ⊫e set (side_prems_of ι) ∧ ¬ I_of N ⊫e {concl_of ι} ∧ concl_of ι < D"
  using bot_ni_n clausal_Inf_counterex_reducing d_in_n d_min n_ent_d by auto

sublocale counterex_reducing_inference_system "{{#}}" "(⊫e)" Inf I_of
  "(<) :: 'a clause ⇒ 'a clause ⇒ bool"
  using Inf_counterex_reducing
  by unfold_locales (simp_all add: less_eq_multiset_def)

end


subsection ‹Counterexample-Reducing Calculi Equipped with a Standard Redundancy Criterion›

locale clausal_counterex_reducing_calculus_with_standard_redundancy =
  calculus_with_standard_redundancy Inf "{{#}}" "(⊫e)" "(<) :: 'a clause ⇒ 'a clause ⇒ bool" +
  clausal_counterex_reducing_inference_system Inf J_of
  for
    Inf :: "('a :: wellorder) clause inference set" and
    J_of :: "'a clause set ⇒ 'a set"
begin

sublocale counterex_reducing_calculus_with_standard_inferance_redundancy "{{#}}" Inf "(⊫e)" Red_I
  Red_F I_of "(<) :: 'a clause ⇒ 'a clause ⇒ bool"
proof unfold_locales
  fix C D :: "'a clause"
  show "C ≠ D ⟹ C < D ∨ D < C"
    by fastforce
qed

lemma clausal_saturated_model: "saturated N ⟹ {#} ∉ N ⟹ J_of N ⊫s N"
  by (simp add: saturated_model[simplified])

corollary clausal_saturated_complete: "saturated N ⟹ (∀I. ¬ I ⊫s N) ⟹ {#} ∈ N"
  using clausal_saturated_model by blast

end

end