Theory Ordered_Resolution_Prover.Unordered_Ground_Resolution

(*  Title:       Ground Unordered Resolution Calculus
    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 ‹Ground Unordered Resolution Calculus›

theory Unordered_Ground_Resolution
  imports Inference_System Ground_Resolution_Model
begin

text ‹
Unordered ground resolution is one of the two inference systems studied in Section 3 (``Standard
Resolution'') of Bachmair and Ganzinger's chapter.
›


subsection ‹Inference Rule›

text ‹
Unordered ground resolution consists of a single rule, called unord_resolve› below, which is
sound and counterexample-reducing.
›

locale ground_resolution_without_selection
begin

sublocale ground_resolution_with_selection where S = "λ_. {#}"
  by unfold_locales auto

inductive unord_resolve :: "'a clause  'a clause  'a clause  bool" where
  "unord_resolve (C + replicate_mset (Suc n) (Pos A)) (add_mset (Neg A) D) (C + D)"

lemma unord_resolve_sound: "unord_resolve C D E  I  C  I  D  I  E"
  using unord_resolve.cases by fastforce

text ‹
The following result corresponds to Theorem 3.8, except that the conclusion is strengthened slightly
to make it fit better with the counterexample-reducing inference system framework.
›

theorem unord_resolve_counterex_reducing:
  assumes
    ec_ni_n: "{#}  N" and
    c_in_n: "C  N" and
    c_cex: "¬ INTERP N  C" and
    c_min: "D. D  N  ¬ INTERP N  D  C  D"
  obtains D E where
    "D  N"
    "INTERP N  D"
    "productive N D"
    "unord_resolve D C E"
    "¬ INTERP N  E"
    "E < C"
proof -
  have c_ne: "C  {#}"
    using c_in_n ec_ni_n by blast
  have "A. A  atms_of C  A = Max (atms_of C)"
    using c_ne by (blast intro: Max_in_lits atm_of_Max_lit atm_of_lit_in_atms_of)
  then have "A. Neg A ∈# C"
    using c_ne c_in_n c_cex c_min Max_in_lits Max_lit_eq_pos_or_neg_Max_atm  max_pos_imp_Interp
      Interp_imp_INTERP by metis
  then obtain A where neg_a_in_c: "Neg A ∈# C"
    by blast
  then obtain C' where c: "C = add_mset (Neg A) C'"
    using insert_DiffM by metis
  have "A  INTERP N"
    using neg_a_in_c c_cex[unfolded true_cls_def] by fast
  then obtain D where d0: "produces N D A"
    unfolding INTERP_def by (metis UN_E not_produces_imp_notin_production)
  have prod_d: "productive N D"
    unfolding d0 by simp
  then have d_in_n: "D  N"
    using productive_in_N by fast
  have d_true: "INTERP N  D"
    using prod_d productive_imp_INTERP by blast

  obtain D' AAA where
    d: "D = D' + AAA" and
    d': "D' = {#L ∈# D. L  Pos A#}" and
    aa: "AAA = {#L ∈# D. L = Pos A#}"
    using multiset_partition union_commute by metis
  have d'_subs: "set_mset D'  set_mset D"
    unfolding d' by auto
  have "¬ Neg A ∈# D"
    using d0 by (blast dest: produces_imp_neg_notin_lits)
  then have neg_a_ni_d': "¬ Neg A ∈# D'"
    using d'_subs by auto
  have a_ni_d': "A  atms_of D'"
    using d' neg_a_ni_d' by (auto dest: atm_imp_pos_or_neg_lit)
  have "n. AAA = replicate_mset (Suc n) (Pos A)"
    using aa d0 not0_implies_Suc produces_imp_Pos_in_lits[of N]
    by (simp add: filter_eq_replicate_mset del: replicate_mset_Suc)
  then have res_e: "unord_resolve D C (D' + C')"
    unfolding c d by (fastforce intro: unord_resolve.intros)

  have d'_le_d: "D'  D"
    unfolding d by simp
  have a_max_d: "A = Max (atms_of D)"
    using d0 productive_imp_produces_Max_atom by auto
  then have "D'  {#}  Max (atms_of D')  A"
    using d'_le_d by (blast intro: less_eq_Max_atms_of)
  moreover have "D'  {#}  Max (atms_of D')  A"
    using a_ni_d' Max_in by (blast intro: atms_empty_iff_empty[THEN iffD1])
  ultimately have max_d'_lt_a: "D'  {#}  Max (atms_of D') < A"
    using dual_order.strict_iff_order by blast

  have "¬ interp N D  D"
    using d0 productive_imp_not_interp by blast
  then have "¬ Interp N D  D'"
    unfolding d0 d' Interp_def true_cls_def by (auto simp: true_lit_def simp del: not_gr_zero)
  then have "¬ INTERP N  D'"
    using a_max_d d'_le_d max_d'_lt_a not_Interp_imp_not_INTERP by blast
  moreover have "¬ INTERP N  C'"
    using c_cex unfolding c by simp
  ultimately have e_cex: "¬ INTERP N  D' + C'"
    by simp

  have "B. B  atms_of D'  B  A"
    using d0 d'_subs contra_subsetD lits_subseteq_imp_atms_subseteq produces_imp_atms_leq by metis
  then have "L. L ∈# D'  L < Neg A"
    using neg_a_ni_d' antisym_conv1 atms_less_eq_imp_lit_less_eq_neg by metis
  then have lt_cex: "D' + C' < C"
    by (force intro: add.commute simp: c less_multisetDM intro: exI[of _ "{#Neg A#}"])

  from d_in_n d_true prod_d res_e e_cex lt_cex show ?thesis ..
qed


subsection ‹Inference System›

text ‹
Theorem 3.9 and Corollary 3.10 are subsumed in the counterexample-reducing inference system
framework, which is instantiated below.
›

definition unord_Γ :: "'a inference set" where
  "unord_Γ = {Infer {#C#} D E | C D E. unord_resolve C D E}"

sublocale unord_Γ_sound_counterex_reducing?:
  sound_counterex_reducing_inference_system unord_Γ INTERP
proof unfold_locales
  fix D E and N :: "('b :: wellorder) clause set"
  assume "{#}  N" and "D  N" and "¬ INTERP N  D" and "C. C  N  ¬ INTERP N  C  D  C"
  then obtain C E where
    c_in_n: "C  N" and
    c_true: "INTERP N  C" and
    res_e: "unord_resolve C D E" and
    e_cex: "¬ INTERP N  E" and
    e_lt_d: "E < D"
    using unord_resolve_counterex_reducing by (metis (no_types))
  from c_in_n have "set_mset {#C#}  N"
    by auto
  moreover have "Infer {#C#} D E  unord_Γ"
    unfolding unord_Γ_def using res_e by blast
  ultimately show
    "CC E. set_mset CC  N  INTERP N ⊨m CC  Infer CC D E  unord_Γ  ¬ INTERP N  E  E < D"
    using c_in_n c_true e_cex e_lt_d by blast
next
  fix CC D E and I :: "'b interp"
  assume "Infer CC D E  unord_Γ" and "I ⊨m CC" and "I  D"
  then show "I  E"
    by (clarsimp simp: unord_Γ_def true_cls_mset_def) (erule unord_resolve_sound, auto)
qed

lemmas clausal_logic_compact = unord_Γ_sound_counterex_reducing.clausal_logic_compact

end

text ‹
Theorem 3.12, compactness of clausal logic, has finally been derived for a concrete inference
system:
›

lemmas clausal_logic_compact = ground_resolution_without_selection.clausal_logic_compact

end