Theory Ground_Ordered_Resolution

theory Ground_Ordered_Resolution
  imports
    First_Order_Clause.Selection_Function
    First_Order_Clause.Ground_Order
    First_Order_Clause.Literal_Functor
begin

section ‹Resolution Calculus›

locale ground_ordered_resolution_calculus =
  ground_order where less⇩t = less⇩t +
  selection_function select
for
  less⇩t :: "'t ⇒ 't ⇒ bool" and
  select :: "'t clause ⇒ 't clause"
begin

subsection ‹Resolution Calculus›

inductive resolution :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
  resolutionI: 
  "E = add_mset l⇩1 E' ⟹
   D = add_mset l⇩2 D' ⟹
   l⇩1 = Neg t ⟹
   l⇩2 = Pos t ⟹
   C = (E' + D') ⟹
   resolution D E C"
if 
 "D ≺⇩c E"
 "select E = {#} ∧ is_maximal l⇩1 E ∨ is_maximal l⇩1 (select E)"
 "select D = {#}"
 "is_strictly_maximal l⇩2 D"

inductive factoring :: "'t clause ⇒ 't clause ⇒ bool" where
  factoringI: 
  "D = add_mset l (add_mset l D') ⟹
   l = Pos t ⟹
   C = add_mset l D' ⟹
   factoring D C"
if
  "select D = {#}"
  "is_maximal l D"

subsection ‹Ground Layer›

abbreviation resolution_inferences where
  "resolution_inferences ≡ {Infer [D, E] C | D E C. resolution D E C}"

abbreviation factoring_inferences where
  "factoring_inferences ≡ {Infer [D] C | D C. factoring D C}"

definition G_Inf :: "'t clause inference set" where
  "G_Inf =
    {Infer [D, E] C | D E C. resolution D E C} ∪
    {Infer [D] C | D C. factoring D C}"

abbreviation G_Bot :: "'t clause set" where
  "G_Bot ≡ {{#}}"

definition G_entails :: "'t clause set ⇒ 't clause set ⇒ bool" where
  "G_entails N⇩1 N⇩2 ⟷ (∀ I. I ⊫s N⇩1 ⟶ I ⊫s N⇩2)"

subsection ‹Smaller Conclussions›

lemma ground_resolution_smaller_conclusion:
  assumes
    step: "resolution D E C"
  shows "C ≺⇩c E"
  using step
proof (cases D E C rule: resolution.cases)
  case (resolutionI l⇩1 l⇩2 E' D' t)

  have "∀k∈#D'. k ≺⇩l Pos t"
    using ‹is_strictly_maximal l⇩2 D› ‹D = add_mset l⇩2 D'›
    using is_strictly_maximal_def resolutionI(8)
    by fastforce

  moreover have "⋀A. Pos A ≺⇩l Neg A"
    unfolding literal.order.multiset_extension_def
    by auto

  ultimately have "∀k∈#D'. k ≺⇩l Neg t"
    using literal.order.order.strict_trans
    by blast

  hence "D' ≺⇩c {#Neg t#}"
    using one_step_implies_multp[of "{#Neg t#}" D' "(≺⇩l)" "{#}"]
    by (simp add: less⇩c_def)

  hence "D' + E' ≺⇩c add_mset (Neg t) E'"
    using multp_cancel[of "(≺⇩l)" E' D' "{#Neg t#}"] less⇩c_def 
    by force

  thus ?thesis
    unfolding resolutionI
    by (simp only: add.commute)
qed

lemma ground_factoring_smaller_conclusion:
  assumes step: "factoring D C"
  shows "C ≺⇩c D"
  using step
proof (cases D C rule: factoring.cases)
  case (factoringI l D' t)
 
  have "C = add_mset l D'"
    using factoringI
    by argo

  then show ?thesis
    by (metis (lifting) add.comm_neutral add_mset_add_single add_mset_not_empty 
        clause.order.multiset_extension_def empty_iff local.factoringI(3)
        one_step_implies_multp set_mset_empty)
qed

end

subsection ‹Redundancy Criterion›

sublocale ground_ordered_resolution_calculus ⊆ consequence_relation where
  Bot = G_Bot and
  entails = G_entails
proof unfold_locales

  show "G_Bot ≠ {}"
    by simp
next

  show "⋀B N. B ∈ G_Bot ⟹ G_entails {B} N"
    by (simp add: G_entails_def)
next

  show "⋀N2 N1. N2 ⊆ N1 ⟹ G_entails N1 N2"
    by (auto simp: G_entails_def elim!: true_clss_mono[rotated])
next
  fix N1 N2 
  assume ball_G_entails: "∀C ∈ N2. G_entails N1 {C}"

  show "G_entails N1 N2"
    unfolding G_entails_def
  proof (intro allI impI)
    fix I :: "'t set"
    assume "I ⊫s N1"

    hence "∀C ∈ N2. I ⊫s {C}"
      using ball_G_entails 
      by (simp add: G_entails_def)

    then show "I ⊫s N2"
      by (simp add: true_clss_def)
  qed
next

  show "⋀N1 N2 N3. G_entails N1 N2 ⟹ G_entails N2 N3 ⟹ G_entails N1 N3"
    using G_entails_def 
    by simp
qed

sublocale ground_ordered_resolution_calculus ⊆ calculus_with_finitary_standard_redundancy where
  Inf = G_Inf and
  Bot = G_Bot and
  entails = G_entails and
  less = "(≺⇩c)"
  defines GRed_I = Red_I and GRed_F = Red_F
proof unfold_locales

  show "transp (≺⇩c)"
    by simp
next

  show "wfP (≺⇩c)"
    by auto
next

  show "⋀ι. ι ∈ G_Inf ⟹ prems_of ι ≠ []"
    by (auto simp: G_Inf_def)
next
  fix ι

  have "concl_of ι ≺⇩c main_prem_of ι"
    if ι_def: "ι = Infer [D, E] C" and
      infer: "resolution D E C"
    for E D C
    unfolding ι_def
    using infer
    using ground_resolution_smaller_conclusion
    by simp

  moreover have "concl_of ι ≺⇩c main_prem_of ι"
    if ι_def: "ι = Infer [D] C" and
      infer: "factoring D C"
    for D C
    unfolding ι_def
    using infer
    using ground_factoring_smaller_conclusion
    by simp

  ultimately show "ι ∈ G_Inf ⟹ concl_of ι ≺⇩c main_prem_of ι"
    unfolding G_Inf_def
    by fast
qed

end