Theory Ground_Superposition

theory Ground_Superposition
  imports
    Ground_Term_Context
    First_Order_Clause.Ground_Order_With_Equality
    First_Order_Clause.Selection_Function

    First_Order_Clause.Ground_Term_Rewrite_System
    First_Order_Clause.Uprod_Literal_Functor
begin

section ‹Superposition Calculus›

locale ground_superposition_calculus =
  ground_term_context where apply_context = apply_context +
  context_compatible_ground_order where less⇩t = less⇩t and apply_context = apply_context +
  selection_function select 
for
  apply_context :: "'c ⇒ 't ⇒ 't" and
  less⇩t :: "'t ⇒ 't ⇒ bool" and
  select :: "'t clause ⇒ 't clause"
begin

subsection ‹Ground Rules›

inductive superposition :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
  superpositionI:
   "E = add_mset L⇩E E' ⟹
    D = add_mset L⇩D D' ⟹
    D ≺⇩c E ⟹
    𝒫 ∈ {Pos, Neg} ⟹
    L⇩E = 𝒫 (Upair κ⟨t⟩ u) ⟹
    L⇩D = t ≈ t' ⟹
    u ≺⇩t κ⟨t⟩ ⟹
    t' ≺⇩t t ⟹
    (𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal L⇩E E) ∨
    (𝒫 = Neg ∧ (select E = {#} ∧ is_maximal L⇩E E ∨ is_maximal L⇩E (select E))) ⟹
    select D = {#} ⟹
    is_strictly_maximal L⇩D D ⟹
    C = add_mset (𝒫 (Upair κ⟨t'⟩ u)) (E' + D') ⟹
    superposition D E C"

inductive eq_resolution :: "'t clause ⇒ 't clause ⇒ bool" where
  eq_resolutionI:
   "D = add_mset L D' ⟹
    L = t !≈ t ⟹
    select D = {#} ∧ is_maximal L D ∨ is_maximal L (select D) ⟹
    C = D' ⟹
    eq_resolution D C"

inductive eq_factoring :: "'t clause ⇒ 't clause ⇒ bool" where
  eq_factoringI:
   "D = add_mset L⇩1 (add_mset L⇩2 D') ⟹
    L⇩1 = t ≈ t' ⟹
    L⇩2 = t ≈ t'' ⟹
    select D = {#} ⟹
    is_maximal L⇩1 D ⟹
    t' ≺⇩t t ⟹
    C = add_mset (t' !≈ t'') (add_mset (t ≈ t'') D') ⟹
    eq_factoring D C"

abbreviation eq_resolution_inferences where
  "eq_resolution_inferences ≡ {Infer [D] C | D C. eq_resolution D C}"

abbreviation eq_factoring_inferences where
  "eq_factoring_inferences ≡ {Infer [D] C | D C. eq_factoring D C}"

abbreviation superposition_inferences where
  "superposition_inferences ≡ {Infer [D, E] C | D E C. superposition D E C}"

subsubsection ‹Alternative Specification of the Superposition Rule›

inductive superposition' :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
  superposition'I: 
   "P⇩1 = add_mset L⇩1 P⇩1' ⟹
    P⇩2 = add_mset L⇩2 P⇩2' ⟹
    P⇩2 ≺⇩c P⇩1 ⟹
    𝒫 ∈ {Pos, Neg} ⟹
    L⇩1 = 𝒫 (Upair s⟨t⟩ s') ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩ ⟹
    t' ≺⇩t t ⟹
    (𝒫 = Pos ⟶ select P⇩1 = {#} ∧ is_strictly_maximal L⇩1 P⇩1) ⟹
    (𝒫 = Neg ⟶ (select P⇩1 = {#} ∧ is_maximal L⇩1 P⇩1 ∨ is_maximal L⇩1 (select P⇩1))) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal L⇩2 P⇩2 ⟹
    C = add_mset (𝒫 (Upair s⟨t'⟩ s')) (P⇩1' + P⇩2') ⟹
    superposition' P⇩2 P⇩1 C"

lemma "superposition' = superposition"
proof (intro ext iffI)
  fix P1 P2 C
  assume "superposition' P2 P1 C"
  thus "superposition P2 P1 C"
  proof (cases P2 P1 C rule: superposition'.cases)
    case (superposition'I L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
    thus ?thesis
      using superpositionI
      by force
  qed
next
  fix P1 P2 C
  assume "superposition P1 P2 C"
  thus "superposition' P1 P2 C"
  proof (cases P1 P2 C rule: superposition.cases)
    case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
    thus ?thesis
      using superposition'I
      by auto
  qed
qed

inductive pos_superposition :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
 pos_superpositionI: 
   "P⇩1 = add_mset L⇩1 P⇩1' ⟹
    P⇩2 = add_mset L⇩2 P⇩2' ⟹
    P⇩2 ≺⇩c P⇩1 ⟹
    L⇩1 = s⟨t⟩ ≈ s' ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩ ⟹
    t' ≺⇩t t ⟹
    select P⇩1 = {#} ⟹
    is_strictly_maximal L⇩1 P⇩1 ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal L⇩2 P⇩2 ⟹
    C = add_mset (s⟨t'⟩ ≈ s') (P⇩1' + P⇩2') ⟹
    pos_superposition P⇩2 P⇩1 C"

lemma superposition_if_pos_superposition:
  assumes step: "pos_superposition P⇩2 P⇩1 C"
  shows "superposition P⇩2 P⇩1 C"
  using step
proof (cases P⇩2 P⇩1 C rule: pos_superposition.cases)
  case (pos_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
  thus ?thesis
    using superpositionI
    by blast
qed

inductive neg_superposition :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
 neg_superpositionI:
   "P⇩1 = add_mset L⇩1 P⇩1' ⟹
    P⇩2 = add_mset L⇩2 P⇩2' ⟹
    P⇩2 ≺⇩c P⇩1 ⟹
    L⇩1 = s⟨t⟩ !≈ s' ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩ ⟹
    t' ≺⇩t t ⟹
    select P⇩1 = {#} ∧ is_maximal L⇩1 P⇩1 ∨ is_maximal L⇩1 (select P⇩1) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal L⇩2 P⇩2 ⟹
    C = add_mset (Neg (Upair s⟨t'⟩ s')) (P⇩1' + P⇩2') ⟹
    neg_superposition P⇩2 P⇩1 C"

lemma superposition_if_neg_superposition:
  assumes "neg_superposition P⇩2 P⇩1 C"
  shows "superposition P⇩2 P⇩1 C"
  using assms
proof (cases P⇩2 P⇩1 C rule: neg_superposition.cases)
  case (neg_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
  then show ?thesis
    using superpositionI
    by blast
qed

lemma superposition_iff_pos_or_neg:
  "superposition P⇩2 P⇩1 C ⟷
    pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
proof (rule iffI)
  assume "superposition P⇩2 P⇩1 C"
  thus "pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
  proof (cases P⇩2 P⇩1 C rule: superposition.cases)
    case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
    then show ?thesis
      using pos_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
      using neg_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
      by blast
  qed
next
  assume "pos_superposition P⇩2 P⇩1 C ∨ neg_superposition P⇩2 P⇩1 C"
  thus "superposition P⇩2 P⇩1 C"
    using
      superposition_if_neg_superposition
      superposition_if_pos_superposition
    by metis
qed


subsection ‹Ground Layer›

sublocale ground_term_rewrite_system
  by unfold_locales

definition G_Inf :: "'t clause inference set" where
  "G_Inf =
    {Infer [P⇩2, P⇩1] C | P⇩2 P⇩1 C. superposition P⇩2 P⇩1 C} ∪
    {Infer [P] C | P C. eq_resolution P C} ∪
    {Infer [P] C | P C. eq_factoring P 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 :: 't rel). refl I ⟶ trans I ⟶ sym I ⟶
    compatible_with_context I ⟶ upair ` I ⊫s N⇩1 ⟶ upair ` I ⊫s N⇩2)"

lemma superposition_smaller_conclusion:
  assumes
    step: "superposition P1 P2 C"
  shows "C ≺⇩c P2"
  using step
proof (cases P1 P2 C rule: superposition.cases)
  case (superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')

  have "P⇩1' + add_mset (𝒫 (Upair s⟨t'⟩ s')) P⇩2' ≺⇩c P⇩1' + {#𝒫 (Upair s⟨t⟩ s')#}"
    unfolding less⇩c_def
  proof (intro one_step_implies_multp ballI)
    fix K assume "K ∈# add_mset (𝒫 (Upair s⟨t'⟩ s')) P⇩2'"

    moreover have "𝒫 (Upair s⟨t'⟩ s') ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
    proof -
      have  "s⟨t'⟩ ≺⇩t s⟨t⟩"
        using ‹t' ≺⇩t t›
        by simp

      hence "multp (≺⇩t) {#s⟨t'⟩, s'#} {#s⟨t⟩, s'#}"
        by (simp add: add_mset_commute multp_cancel_add_mset)

      have ?thesis if "𝒫 = Pos"
        unfolding that less⇩l_def
        using ‹multp (≺⇩t) {#s⟨t'⟩, s'#} {#s⟨t⟩, s'#}›
        by simp

      moreover have ?thesis if "𝒫 = Neg"
        unfolding that less⇩l_def
        using ‹multp (≺⇩t) {#s⟨t'⟩, s'#} {#s⟨t⟩, s'#}› multp_double_doubleI
        by force

      ultimately show ?thesis
        using ‹𝒫 ∈ {Pos, Neg}›
        by auto
    qed

    moreover have "∀K ∈# P⇩2'. K ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
    proof -
      have "is_strictly_maximal L⇩2 P1"
        using superpositionI
        by argo

      hence "∀K ∈# P⇩2'. ¬ Pos (Upair t t') ≺⇩l K ∧ Pos (Upair t t') ≠ K"
        unfolding
          is_strictly_maximal_def
          ‹P1 = add_mset L⇩2 P⇩2'› ‹L⇩2 = t ≈ t'›
        by simp

      hence "∀K ∈# P⇩2'. K ≺⇩l Pos (Upair t t')"
        by auto

      have thesis_if_Neg: "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
        if "𝒫 = Neg"
      proof -
        have "t ≼⇩t s⟨t⟩"
          using term.order.less_eq_subterm_property .

        hence "multp (≺⇩t) {#t, t'#} {#s⟨t⟩, s', s⟨t⟩, s'#}"
          unfolding reflclp_iff
        proof (elim disjE)
          assume "t ≺⇩t s⟨t⟩"

          moreover hence "t' ≺⇩t s⟨t⟩"
            using superpositionI(8)
            by order

          ultimately show ?thesis
            by (auto intro: one_step_implies_multp[of _ _ _ "{#}", simplified])
        next
          assume "t = s⟨t⟩"
          thus ?thesis
            using ‹t' ≺⇩t t›
            by simp
        qed
        thus "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
          using ‹𝒫 = Neg›
          by (simp add: less⇩l_def)
      qed

      have thesis_if_Pos: "Pos (Upair t t') ≼⇩l 𝒫 (Upair s⟨t⟩ s')"
        if "𝒫 = Pos" and "is_maximal L⇩1 P2"
      proof (cases "s = □")
        case Hole: True

        show ?thesis 
        proof (cases "t' ≼⇩t s'")
          case True

          hence "(multp (≺⇩t))⇧=⇧= {#t, t'#} {#s⟨t⟩, s'#}"
            unfolding Hole
            by (simp add: multp_cancel_add_mset)

          thus ?thesis
            unfolding Hole ‹𝒫 = Pos›
            by (auto simp: less⇩l_def)
        next
          case False
          hence "s' ≺⇩t t'"
            by order

          hence "multp (≺⇩t) {#s⟨t⟩, s'#} {#t, t'#}"
            by (simp add: Hole multp_cancel_add_mset)

          hence "𝒫 (Upair s⟨t⟩ s') ≺⇩l Pos (Upair t t')"
            using ‹𝒫 = Pos›
            by (simp add: less⇩l_def)

          moreover have "∀K ∈# P⇩1'. K ≼⇩l 𝒫 (Upair s⟨t⟩ s')"
            using that
            unfolding superpositionI is_maximal_def
            by auto

          ultimately have "∀K ∈# P⇩1'. K ≼⇩l Pos (Upair t t')"
            by auto

          hence "P2 ≺⇩c P1"
            using
              ‹𝒫 (Upair s⟨t⟩ s') ≺⇩l Pos (Upair t t')›
              one_step_implies_multp[of P1 P2 "(≺⇩l)" "{#}", simplified]
              literal.order.multp_if_maximal_less_that_maximal
              superpositionI
              that
            unfolding less⇩c_def
            by blast

          hence False
            using ‹P1 ≺⇩c P2› by order

          thus ?thesis ..
        qed
      next
        case False

        hence "t ≺⇩t s⟨t⟩"
          using term.order.subterm_property[of s t]
          by simp

        moreover hence "t' ≺⇩t s⟨t⟩"
          using ‹t' ≺⇩t t›
          by order

        ultimately have "multp (≺⇩t) {#t, t'#} {#s⟨t⟩, s'#}"
          using one_step_implies_multp[of "{#s⟨t⟩, s'#}" "{#t, t'#}" "(≺⇩t)" "{#}"]
          by simp

        hence "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
          using ‹𝒫 = Pos›
          by (simp add: less⇩l_def)

        thus ?thesis
          by order
      qed

      have "𝒫 = Pos ∨ 𝒫 = Neg"
        using ‹𝒫 ∈ {Pos, Neg}›
        by simp

      thus ?thesis
      proof (elim disjE; intro ballI)
        fix K assume "𝒫 = Pos" "K ∈# P⇩2'"
        have "K ≺⇩l t ≈ t'"
          using ‹∀K∈#P⇩2'. K ≺⇩l t ≈ t'› ‹K ∈# P⇩2'›
          by metis

        also have "t ≈ t' ≼⇩l 𝒫 (Upair s⟨t⟩ s')"
        proof (rule thesis_if_Pos[OF ‹𝒫 = Pos›])

          have "is_strictly_maximal L⇩1 P2"
            using ‹𝒫 = Pos› superpositionI
            by simp

          thus "is_maximal L⇩1 P2"
            by blast
        qed

        finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩ s')" .
      next
        fix K assume "𝒫 = Neg" "K ∈# P⇩2'"

        have "K ≺⇩l t ≈ t'"
          using ‹∀K∈#P⇩2'. K ≺⇩l t ≈ t'› ‹K ∈# P⇩2'›
          by metis

        also have "t ≈ t' ≺⇩l 𝒫 (Upair s⟨t⟩ s')"
          using thesis_if_Neg[OF ‹𝒫 = Neg›] .

        finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩ s')" .
      qed
    qed

    ultimately show "∃j ∈# {#𝒫 (Upair s⟨t⟩ s')#}. K ≺⇩l j"
      by auto
  qed simp

  moreover have "C = add_mset (𝒫 (Upair s⟨t'⟩ s')) (P⇩1' + P⇩2')"
    unfolding superpositionI ..

  moreover have "P2 = P⇩1' + {#𝒫 (Upair s⟨t⟩ s')#}"
    unfolding superpositionI 
    by simp

  ultimately show ?thesis
    by simp
qed

lemma ground_eq_resolution_smaller_conclusion:
  assumes step: "eq_resolution P C"
  shows "C ≺⇩c P"
  using step
proof (cases P C rule: eq_resolution.cases)
  case (eq_resolutionI L t)
  then show ?thesis
    unfolding less⇩c_def
    by (metis add.left_neutral add_single_right_eq_add_mset empty_not_add_mset multi_member_split
        one_step_implies_multp union_commute)
qed

lemma ground_eq_factoring_smaller_conclusion:
  assumes step: "eq_factoring P C"
  shows "C ≺⇩c P"
  using step
proof (cases P C rule: eq_factoring.cases)
  case (eq_factoringI L⇩1 L⇩2 P' t t' t'')
  have "is_maximal L⇩1 P"
    using eq_factoringI
    by simp

  hence "∀K ∈# add_mset (Pos (Upair t t'')) P'. ¬ Pos (Upair t t') ≺⇩l K"
    unfolding eq_factoringI is_maximal_def
    by auto

  hence "¬ Pos (Upair t t') ≺⇩l Pos (Upair t t'')"
    by simp

  hence "Pos (Upair t t'') ≼⇩l Pos (Upair t t')"
    by order

  hence "t'' ≼⇩t t'"
    unfolding reflclp_iff
    by (auto simp: less⇩l_def multp_cancel_add_mset)

  have "C = add_mset (Neg (Upair t' t'')) (add_mset (Pos (Upair t t'')) P')"
    using eq_factoringI
    by argo

  moreover have "add_mset (Neg (Upair t' t'')) (add_mset (Pos (Upair t t'')) P') ≺⇩c P"
    unfolding eq_factoringI less⇩c_def
  proof (intro one_step_implies_multp[of "{#_#}" "{#_#}", simplified])
    have "t'' ≺⇩t t"
      using ‹t' ≺⇩t t› ‹t'' ≼⇩t t'›
      by order

    hence "multp (≺⇩t) {#t', t'', t', t''#} {#t, t'#}"
      using one_step_implies_multp[of _ _ _ "{#}", simplified]
      by (metis ‹t' ≺⇩t t› diff_empty id_remove_1_mset_iff_notin insert_iff
          set_mset_add_mset_insert)

    thus "Neg (Upair t' t'') ≺⇩l Pos (Upair t t')"
      by (simp add: less⇩l_def)
  qed

  ultimately show ?thesis
    by argo
qed

sublocale 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 rel"
    assume "refl I" and "trans I" and "sym I" and "compatible_with_context I" and
      "(λ(x, y). Upair x y) ` I ⊫s N1"

    hence "∀C ∈ N2. (λ(x, y). Upair x y) ` I ⊫s {C}"
      using ball_G_entails
      by (simp add: G_entails_def)

    then show "(λ(x, y). Upair x y) ` 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


subsection ‹Redundancy Criterion›

sublocale 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 [P⇩2, P⇩1] C" and
      infer: "superposition P⇩2 P⇩1 C"
    for P⇩2 P⇩1 C
    unfolding ι_def
    using infer
    using superposition_smaller_conclusion
    by simp

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

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

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

lemma redundant_infer_singleton:
  assumes "∃D∈N. G_entails (insert D (set (side_prems_of ι))) {concl_of ι} ∧ D ≺⇩c main_prem_of ι"
  shows "redundant_infer N ι"
proof-
  obtain D where D:
    "D ∈ N"
    "G_entails (insert D (set (side_prems_of ι))) {concl_of ι}"
    "D ≺⇩c main_prem_of ι"
    using assms
    by blast

  show ?thesis
    unfolding redundant_infer_def
    by (rule exI[of _ "{D}"]) (auto simp: D)
qed

end

end