Theory Ground_Resolution_Model

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

section ‹Candidate Models for Ground Resolution›

theory Ground_Resolution_Model
  imports Herbrand_Interpretation
begin

text ‹
The proofs of refutational completeness for the two resolution inference systems presented in
Section 3 (``Standard Resolution'') of Bachmair and Ganzinger's chapter share mostly the same
candidate model construction. The literal selection capability needed for the second system is
ignored by the first one, by taking @{term "λ_. {}"} as instantiation for the ‹S›
parameter.
›

locale selection =
  fixes S :: "'a clause ⇒ 'a clause"
  assumes
    S_selects_subseteq: "S C ⊆# C" and
    S_selects_neg_lits: "L ∈# S C ⟹ is_neg L"

locale ground_resolution_with_selection = selection S
  for S :: "('a :: wellorder) clause ⇒ 'a clause"
begin

text ‹
The following commands corresponds to Definition 3.14, which generalizes Definition 3.1.
‹production C› is denoted $\varepsilon_C$ in the chapter; ‹interp C› is denoted
$I_C$; ‹Interp C› is denoted $I^C$; and ‹Interp_N› is denoted $I_N$. The mutually
recursive definition from the chapter is massaged to simplify the termination argument. The
‹production_unfold› lemma below gives the intended characterization.
›

context
  fixes N :: "'a clause set"
begin

function production :: "'a clause ⇒ 'a interp" where
  "production C =
   {A. C ∈ N ∧ C ≠ {#} ∧ Max_mset C = Pos A ∧ ¬ (⋃D ∈ {D. D < C}. production D) ⊨ C ∧ S C = {#}}"
  by auto
termination by (rule "termination"[OF wf, simplified])

declare production.simps [simp del]

definition interp :: "'a clause ⇒ 'a interp" where
  "interp C = (⋃D ∈ {D. D < C}. production D)"

lemma production_unfold:
  "production C = {A. C ∈ N ∧ C ≠ {#} ∧ Max_mset C = Pos A ∧ ¬ interp C ⊨ C ∧ S C = {#}}"
  unfolding interp_def by (rule production.simps)

abbreviation productive :: "'a clause ⇒ bool" where
  "productive C ≡ production C ≠ {}"

abbreviation produces :: "'a clause ⇒ 'a ⇒ bool" where
  "produces C A ≡ production C = {A}"

lemma producesD: "produces C A ⟹ C ∈ N ∧ C ≠ {#} ∧ Pos A = Max_mset C ∧ ¬ interp C ⊨ C ∧ S C = {#}"
  unfolding production_unfold by auto

definition Interp :: "'a clause ⇒ 'a interp" where
  "Interp C = interp C ∪ production C"

lemma interp_subseteq_Interp[simp]: "interp C ⊆ Interp C"
  by (simp add: Interp_def)

lemma Interp_as_UNION: "Interp C = (⋃D ∈ {D. D ≤ C}. production D)"
  unfolding Interp_def interp_def less_eq_multiset_def by fast

lemma productive_not_empty: "productive C ⟹ C ≠ {#}"
  unfolding production_unfold by simp

lemma productive_imp_produces_Max_literal: "productive C ⟹ produces C (atm_of (Max_mset C))"
  unfolding production_unfold by (auto simp del: atm_of_Max_lit)

lemma productive_imp_produces_Max_atom: "productive C ⟹ produces C (Max (atms_of C))"
  unfolding atms_of_def Max_atm_of_set_mset_commute[OF productive_not_empty]
  by (rule productive_imp_produces_Max_literal)

lemma produces_imp_Max_literal: "produces C A ⟹ A = atm_of (Max_mset C)"
  using productive_imp_produces_Max_literal by auto

lemma produces_imp_Max_atom: "produces C A ⟹ A = Max (atms_of C)"
  using producesD produces_imp_Max_literal by auto

lemma produces_imp_Pos_in_lits: "produces C A ⟹ Pos A ∈# C"
  by (simp add: producesD)

lemma productive_in_N: "productive C ⟹ C ∈ N"
  unfolding production_unfold by simp

lemma produces_imp_atms_leq: "produces C A ⟹ B ∈ atms_of C ⟹ B ≤ A"
  using Max.coboundedI produces_imp_Max_atom by blast

lemma produces_imp_neg_notin_lits: "produces C A ⟹ ¬ Neg A ∈# C"
  by (simp add: pos_Max_imp_neg_notin producesD)

lemma less_eq_imp_interp_subseteq_interp: "C ≤ D ⟹ interp C ⊆ interp D"
  unfolding interp_def by auto (metis order.strict_trans2)

lemma less_eq_imp_interp_subseteq_Interp: "C ≤ D ⟹ interp C ⊆ Interp D"
  unfolding Interp_def using less_eq_imp_interp_subseteq_interp by blast

lemma less_imp_production_subseteq_interp: "C < D ⟹ production C ⊆ interp D"
  unfolding interp_def by fast

lemma less_eq_imp_production_subseteq_Interp: "C ≤ D ⟹ production C ⊆ Interp D"
  unfolding Interp_def using less_imp_production_subseteq_interp
  by (metis le_imp_less_or_eq le_supI1 sup_ge2)

lemma less_imp_Interp_subseteq_interp: "C < D ⟹ Interp C ⊆ interp D"
  by (simp add: Interp_def less_eq_imp_interp_subseteq_interp less_imp_production_subseteq_interp)

lemma less_eq_imp_Interp_subseteq_Interp: "C ≤ D ⟹ Interp C ⊆ Interp D"
  using Interp_def less_eq_imp_interp_subseteq_Interp less_eq_imp_production_subseteq_Interp by auto

lemma not_Interp_to_interp_imp_less: "A ∉ Interp C ⟹ A ∈ interp D ⟹ C < D"
  using less_eq_imp_interp_subseteq_Interp not_less by blast

lemma not_interp_to_interp_imp_less: "A ∉ interp C ⟹ A ∈ interp D ⟹ C < D"
  using less_eq_imp_interp_subseteq_interp not_less by blast

lemma not_Interp_to_Interp_imp_less: "A ∉ Interp C ⟹ A ∈ Interp D ⟹ C < D"
  using less_eq_imp_Interp_subseteq_Interp not_less by blast

lemma not_interp_to_Interp_imp_le: "A ∉ interp C ⟹ A ∈ Interp D ⟹ C ≤ D"
  using less_imp_Interp_subseteq_interp not_less by blast

definition INTERP :: "'a interp" where
  "INTERP = (⋃C ∈ N. production C)"

lemma interp_subseteq_INTERP: "interp C ⊆ INTERP"
  unfolding interp_def INTERP_def by (auto simp: production_unfold)

lemma production_subseteq_INTERP: "production C ⊆ INTERP"
  unfolding INTERP_def using production_unfold by blast

lemma Interp_subseteq_INTERP: "Interp C ⊆ INTERP"
  by (simp add: Interp_def interp_subseteq_INTERP production_subseteq_INTERP)

lemma produces_imp_in_interp:
  assumes a_in_c: "Neg A ∈# C" and d: "produces D A"
  shows "A ∈ interp C"
  by (metis Interp_def Max_pos_neg_less_multiset UnCI a_in_c d
      not_interp_to_Interp_imp_le not_less producesD singletonI)

lemma neg_notin_Interp_not_produce: "Neg A ∈# C ⟹ A ∉ Interp D ⟹ C ≤ D ⟹ ¬ produces D'' A"
  using less_eq_imp_interp_subseteq_Interp produces_imp_in_interp by blast

lemma in_production_imp_produces: "A ∈ production C ⟹ produces C A"
  using productive_imp_produces_Max_atom by fastforce

lemma not_produces_imp_notin_production: "¬ produces C A ⟹ A ∉ production C"
  using in_production_imp_produces by blast

lemma not_produces_imp_notin_interp: "(⋀D. ¬ produces D A) ⟹ A ∉ interp C"
  unfolding interp_def by (fast intro!: in_production_imp_produces)

text ‹
The results below corresponds to Lemma 3.4.
›

lemma Interp_imp_general:
  assumes
    c_le_d: "C ≤ D" and
    d_lt_d': "D < D'" and
    c_at_d: "Interp D ⊨ C" and
    subs: "interp D' ⊆ (⋃C ∈ CC. production C)"
  shows "(⋃C ∈ CC. production C) ⊨ C"
proof (cases "∃A. Pos A ∈# C ∧ A ∈ Interp D")
  case True
  then obtain A where a_in_c: "Pos A ∈# C" and a_at_d: "A ∈ Interp D"
    by blast
  from a_at_d have "A ∈ interp D'"
    using d_lt_d' less_imp_Interp_subseteq_interp by blast
  then show ?thesis
    using subs a_in_c by (blast dest: contra_subsetD)
next
  case False
  then obtain A where a_in_c: "Neg A ∈# C" and "A ∉ Interp D"
    using c_at_d unfolding true_cls_def by blast
  then have "⋀D''. ¬ produces D'' A"
    using c_le_d neg_notin_Interp_not_produce by simp
  then show ?thesis
    using a_in_c subs not_produces_imp_notin_production by auto
qed

lemma Interp_imp_interp: "C ≤ D ⟹ D < D' ⟹ Interp D ⊨ C ⟹ interp D' ⊨ C"
  using interp_def Interp_imp_general by simp

lemma Interp_imp_Interp: "C ≤ D ⟹ D ≤ D' ⟹ Interp D ⊨ C ⟹ Interp D' ⊨ C"
  using Interp_as_UNION interp_subseteq_Interp Interp_imp_general by (metis antisym_conv2)

lemma Interp_imp_INTERP: "C ≤ D ⟹ Interp D ⊨ C ⟹ INTERP ⊨ C"
  using INTERP_def interp_subseteq_INTERP Interp_imp_general[OF _ le_multiset_right_total] by simp

lemma interp_imp_general:
  assumes
    c_le_d: "C ≤ D" and
    d_le_d': "D ≤ D'" and
    c_at_d: "interp D ⊨ C" and
    subs: "interp D' ⊆ (⋃C ∈ CC. production C)"
  shows "(⋃C ∈ CC. production C) ⊨ C"
proof (cases "∃A. Pos A ∈# C ∧ A ∈ interp D")
  case True
  then obtain A where a_in_c: "Pos A ∈# C" and a_at_d: "A ∈ interp D"
    by blast
  from a_at_d have "A ∈ interp D'"
    using d_le_d' less_eq_imp_interp_subseteq_interp by blast
  then show ?thesis
    using subs a_in_c by (blast dest: contra_subsetD)
next
  case False
  then obtain A where a_in_c: "Neg A ∈# C" and "A ∉ interp D"
    using c_at_d unfolding true_cls_def by blast
  then have "⋀D''. ¬ produces D'' A"
    using c_le_d by (auto dest: produces_imp_in_interp less_eq_imp_interp_subseteq_interp)
  then show ?thesis
    using a_in_c subs not_produces_imp_notin_production by auto
qed

lemma interp_imp_interp: "C ≤ D ⟹ D ≤ D' ⟹ interp D ⊨ C ⟹ interp D' ⊨ C"
  using interp_def interp_imp_general by simp

lemma interp_imp_Interp: "C ≤ D ⟹ D ≤ D' ⟹ interp D ⊨ C ⟹ Interp D' ⊨ C"
  using Interp_as_UNION interp_subseteq_Interp[of D'] interp_imp_general by simp

lemma interp_imp_INTERP: "C ≤ D ⟹ interp D ⊨ C ⟹ INTERP ⊨ C"
  using INTERP_def interp_subseteq_INTERP interp_imp_general linear by metis

lemma productive_imp_not_interp: "productive C ⟹ ¬ interp C ⊨ C"
  unfolding production_unfold by simp

text ‹
This corresponds to Lemma 3.3:
›

lemma productive_imp_Interp:
  assumes "productive C"
  shows "Interp C ⊨ C"
proof -
  obtain A where a: "produces C A"
    using assms productive_imp_produces_Max_atom by blast
  then have a_in_c: "Pos A ∈# C"
    by (rule produces_imp_Pos_in_lits)
  moreover have "A ∈ Interp C"
    using a less_eq_imp_production_subseteq_Interp by blast
  ultimately show ?thesis
    by fast
qed

lemma productive_imp_INTERP: "productive C ⟹ INTERP ⊨ C"
  by (fast intro: productive_imp_Interp Interp_imp_INTERP)

text ‹
This corresponds to Lemma 3.5:
›

lemma max_pos_imp_Interp:
  assumes "C ∈ N" and "C ≠ {#}" and "Max_mset C = Pos A" and "S C = {#}"
  shows "Interp C ⊨ C"
proof (cases "productive C")
  case True
  then show ?thesis
    by (fast intro: productive_imp_Interp)
next
  case False
  then have "interp C ⊨ C"
    using assms unfolding production_unfold by simp
  then show ?thesis
    unfolding Interp_def using False by auto
qed

text ‹
The following results correspond to Lemma 3.6:
›

lemma max_atm_imp_Interp:
  assumes
    c_in_n: "C ∈ N" and
    pos_in: "Pos A ∈# C" and
    max_atm: "A = Max (atms_of C)" and
    s_c_e: "S C = {#}"
  shows "Interp C ⊨ C"
proof (cases "Neg A ∈# C")
  case True
  then show ?thesis
    using pos_in pos_neg_in_imp_true by metis
next
  case False
  moreover have ne: "C ≠ {#}"
    using pos_in by auto
  ultimately have "Max_mset C = Pos A"
    using max_atm using Max_in_lits Max_lit_eq_pos_or_neg_Max_atm by metis
  then show ?thesis
    using ne c_in_n s_c_e by (blast intro: max_pos_imp_Interp)
qed

lemma not_Interp_imp_general:
  assumes
    d'_le_d: "D' ≤ D" and
    in_n_or_max_gt: "D' ∈ N ∧ S D' = {#} ∨ Max (atms_of D') < Max (atms_of D)" and
    d'_at_d: "¬ Interp D ⊨ D'" and
    d_lt_c: "D < C" and
    subs: "interp C ⊆ (⋃C ∈ CC. production C)"
  shows "¬ (⋃C ∈ CC. production C) ⊨ D'"
proof -
  {
    assume cc_blw_d': "(⋃C ∈ CC. production C) ⊨ D'"
    have "Interp D ⊆ (⋃C ∈ CC. production C)"
      using less_imp_Interp_subseteq_interp d_lt_c subs by blast
    then obtain A where a_in_d': "Pos A ∈# D'" and a_blw_cc: "A ∈ (⋃C ∈ CC. production C)"
      using cc_blw_d' d'_at_d false_to_true_imp_ex_pos by metis
    from a_in_d' have a_at_d: "A ∉ Interp D"
      using d'_at_d by fast
    from a_blw_cc obtain C' where prod_c': "production C' = {A}"
      by (fast intro!: in_production_imp_produces)
    have max_c': "Max (atms_of C') = A"
      using prod_c' productive_imp_produces_Max_atom by force
    have leq_dc': "D ≤ C'"
      using a_at_d d'_at_d prod_c' by (auto simp: Interp_def intro: not_interp_to_Interp_imp_le)
    then have "D' ≤ C'"
      using d'_le_d order_trans by blast
    then have max_d': "Max (atms_of D') = A"
      using a_in_d' max_c' by (fast intro: pos_lit_in_atms_of le_multiset_Max_in_imp_Max)

    {
      assume "D' ∈ N ∧ S D' = {#}"
      then have "Interp D' ⊨ D'"
        using a_in_d' max_d' by (blast intro: max_atm_imp_Interp)
      then have "Interp D ⊨ D'"
        using d'_le_d by (auto intro: Interp_imp_Interp simp: less_eq_multiset_def)
      then have False
        using d'_at_d by satx
    }
    moreover
    {
      assume "Max (atms_of D') < Max (atms_of D)"
      then have False
        using max_d' leq_dc' max_c' d'_le_d
        by (metis le_imp_less_or_eq le_multiset_empty_right less_eq_Max_atms_of less_imp_not_less)
    }
    ultimately have False
      using in_n_or_max_gt by satx
  }
  then show ?thesis
    by satx
qed

lemma not_Interp_imp_not_interp:
  "D' ≤ D ⟹ D' ∈ N ∧ S D' = {#} ∨ Max (atms_of D') < Max (atms_of D) ⟹ ¬ Interp D ⊨ D' ⟹
   D < C ⟹ ¬ interp C ⊨ D'"
  using interp_def not_Interp_imp_general by simp

lemma not_Interp_imp_not_Interp:
  "D' ≤ D ⟹ D' ∈ N ∧ S D' = {#} ∨ Max (atms_of D') < Max (atms_of D) ⟹ ¬ Interp D ⊨ D' ⟹
   D < C ⟹ ¬ Interp C ⊨ D'"
  using Interp_as_UNION interp_subseteq_Interp not_Interp_imp_general by metis

lemma not_Interp_imp_not_INTERP:
  "D' ≤ D ⟹ D' ∈ N ∧ S D' = {#} ∨ Max (atms_of D') < Max (atms_of D) ⟹ ¬ Interp D ⊨ D' ⟹
   ¬ INTERP ⊨ D'"
  using INTERP_def interp_subseteq_INTERP not_Interp_imp_general[OF _ _ _ le_multiset_right_total]
  by simp

text ‹
Lemma 3.7 is a problem child. It is stated below but not proved; instead, a counterexample is
displayed. This is not much of a problem, because it is not invoked in the rest of the chapter.
›

lemma
  assumes "D ∈ N" and "⋀D'. D' < D ⟹ Interp D' ⊨ C"
  shows "interp D ⊨ C"
  oops

lemma
  assumes d: "D = {#}" and n: "N = {D, C}" and c: "C = {#Pos A#}"
  shows "D ∈ N" and "⋀D'. D' < D ⟹ Interp D' ⊨ C" and "¬ interp D ⊨ C"
  using n unfolding d c interp_def by auto

end

end

end