Theory Ground_Superposition

theory Ground_Superposition
  imports
    (* Theories from the Isabelle distribution *)
    Main

    (* Theories from the AFP *)
    "Saturation_Framework.Calculus"
    "Saturation_Framework_Extensions.Clausal_Calculus"
    "Abstract-Rewriting.Abstract_Rewriting"

    (* Theories from this formalization *)
    "Abstract_Rewriting_Extra"
    "Ground_Critical_Pairs"
    "Multiset_Extra"
    "Term_Rewrite_System"
    "Transitive_Closure_Extra"
    "Uprod_Extra"
    "HOL_Extra"
    Relation_Extra
    Clausal_Calculus_Extra
    Selection_Function
    Ground_Ordering
    Ground_Type_System
begin


hide_type Inference_System.inference
hide_const
  Inference_System.Infer
  Inference_System.prems_of
  Inference_System.concl_of
  Inference_System.main_prem_of

no_notation subst_compose (infixl "∘⇩s" 75)
no_notation subst_apply_term (infixl "⋅" 67)

section ‹Superposition Calculus›

locale ground_superposition_calculus = ground_ordering less_trm + select select
  for
    less_trm :: "'f gterm ⇒ 'f gterm ⇒ bool" (infix "≺⇩t" 50) and
    select :: "'f gatom clause ⇒ 'f gatom clause" +
  assumes
    ground_critical_pair_theorem: "⋀(R :: 'f gterm rel). ground_critical_pair_theorem R"
begin

subsection ‹Ground Rules›

inductive ground_superposition ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
  ground_superpositionI: "
    E = add_mset L⇩E E' ⟹
    D = add_mset L⇩D D' ⟹
    D ≺⇩c E ⟹
    𝒫 ∈ {Pos, Neg} ⟹
    L⇩E = 𝒫 (Upair κ⟨t⟩⇩G u) ⟹
    L⇩D = t ≈ t' ⟹
    u ≺⇩t κ⟨t⟩⇩G ⟹
    t' ≺⇩t t ⟹
    (𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal_lit L⇩E E) ∨
    (𝒫 = Neg ∧ (select E = {#} ∧ is_maximal_lit L⇩E E ∨ is_maximal_lit L⇩E (select E))) ⟹
    select D = {#} ⟹
    is_strictly_maximal_lit L⇩D D ⟹
    C = add_mset (𝒫 (Upair κ⟨t'⟩⇩G u)) (E' + D') ⟹
    ground_superposition D E C"

inductive ground_eq_resolution ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ bool" where
  ground_eq_resolutionI: "
    D = add_mset L D' ⟹
    L = Neg (Upair t t) ⟹
    select D = {#} ∧ is_maximal_lit L D ∨ is_maximal_lit L (select D) ⟹
    C = D' ⟹
    ground_eq_resolution D C"

inductive ground_eq_factoring ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ bool" where
  ground_eq_factoringI: "
    D = add_mset L⇩1 (add_mset L⇩2 D') ⟹
    L⇩1 = t ≈ t' ⟹
    L⇩2 = t ≈ t'' ⟹
    select D = {#} ⟹
    is_maximal_lit L⇩1 D ⟹
    t' ≺⇩t t ⟹
    C = add_mset (Neg (Upair t' t'')) (add_mset (t ≈ t'') D') ⟹
    ground_eq_factoring D C"


subsubsection ‹Alternative Specification of the Superposition Rule›

inductive ground_superposition' ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
  ground_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⟩⇩G s') ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩⇩G ⟹
    t' ≺⇩t t ⟹
    (𝒫 = Pos ⟶ select P⇩1 = {#} ∧ is_strictly_maximal_lit L⇩1 P⇩1) ⟹
    (𝒫 = Neg ⟶ (select P⇩1 = {#} ∧ is_maximal_lit L⇩1 P⇩1 ∨ is_maximal_lit L⇩1 (select P⇩1))) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal_lit L⇩2 P⇩2 ⟹
    C = add_mset (𝒫 (Upair s⟨t'⟩⇩G s')) (P⇩1' + P⇩2') ⟹
    ground_superposition' P⇩2 P⇩1 C"

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

inductive ground_pos_superposition ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
  ground_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⟩⇩G ≈ s' ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩⇩G ⟹
    t' ≺⇩t t ⟹
    select P⇩1 = {#} ⟹
    is_strictly_maximal_lit L⇩1 P⇩1 ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal_lit L⇩2 P⇩2 ⟹
    C = add_mset (s⟨t'⟩⇩G ≈ s') (P⇩1' + P⇩2') ⟹
    ground_pos_superposition P⇩2 P⇩1 C"

lemma ground_superposition_if_ground_pos_superposition:
  assumes step: "ground_pos_superposition P⇩2 P⇩1 C"
  shows "ground_superposition P⇩2 P⇩1 C"
  using step
proof (cases P⇩2 P⇩1 C rule: ground_pos_superposition.cases)
  case (ground_pos_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
  thus ?thesis
    using ground_superpositionI
    by (metis insert_iff)
qed

inductive ground_neg_superposition ::
  "'f gatom clause ⇒ 'f gatom clause ⇒ 'f gatom clause ⇒ bool"
where
  ground_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 = Neg (Upair s⟨t⟩⇩G s') ⟹
    L⇩2 = t ≈ t' ⟹
    s' ≺⇩t s⟨t⟩⇩G ⟹
    t' ≺⇩t t ⟹
    select P⇩1 = {#} ∧ is_maximal_lit L⇩1 P⇩1 ∨ is_maximal_lit L⇩1 (select P⇩1) ⟹
    select P⇩2 = {#} ⟹
    is_strictly_maximal_lit L⇩2 P⇩2 ⟹
    C = add_mset (Neg (Upair s⟨t'⟩⇩G s')) (P⇩1' + P⇩2') ⟹
    ground_neg_superposition P⇩2 P⇩1 C"

lemma ground_superposition_if_ground_neg_superposition:
  assumes "ground_neg_superposition P⇩2 P⇩1 C"
  shows "ground_superposition P⇩2 P⇩1 C"
  using assms
proof (cases P⇩2 P⇩1 C rule: ground_neg_superposition.cases)
  case (ground_neg_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' s t s' t')
  then show ?thesis
    using ground_superpositionI
    by (metis insert_iff)
qed

lemma ground_superposition_iff_pos_or_neg:
  "ground_superposition P⇩2 P⇩1 C ⟷
    ground_pos_superposition P⇩2 P⇩1 C ∨ ground_neg_superposition P⇩2 P⇩1 C"
proof (rule iffI)
  assume "ground_superposition P⇩2 P⇩1 C"
  thus "ground_pos_superposition P⇩2 P⇩1 C ∨ ground_neg_superposition P⇩2 P⇩1 C"
  proof (cases P⇩2 P⇩1 C rule: ground_superposition.cases)
    case (ground_superpositionI L⇩1 P⇩1' L⇩2 P⇩2' 𝒫 s t s' t')
    then show ?thesis
      using ground_pos_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
      using ground_neg_superpositionI[of P⇩1 L⇩1 P⇩1' P⇩2 L⇩2 P⇩2' s t s' t']
      by metis
  qed
next
  assume "ground_pos_superposition P⇩2 P⇩1 C ∨ ground_neg_superposition P⇩2 P⇩1 C"
  thus "ground_superposition P⇩2 P⇩1 C"
    using ground_superposition_if_ground_neg_superposition
      ground_superposition_if_ground_pos_superposition
    by metis
qed


subsection ‹Ground Layer›

definition G_Inf :: "'f gatom clause inference set" where
  "G_Inf =
    {Infer [P⇩2, P⇩1] C | P⇩2 P⇩1 C. ground_superposition P⇩2 P⇩1 C} ∪
    {Infer [P] C | P C. ground_eq_resolution P C} ∪
    {Infer [P] C | P C. ground_eq_factoring P C}"

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

definition G_entails :: "'f gatom clause set ⇒ 'f gatom clause set ⇒ bool" where
  "G_entails N⇩1 N⇩2 ⟷ (∀(I :: 'f gterm rel). refl I ⟶ trans I ⟶ sym I ⟶
    compatible_with_gctxt I ⟶ upair ` I ⊫s N⇩1 ⟶ upair ` I ⊫s N⇩2)"

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

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

    moreover have "𝒫 (Upair s⟨t'⟩⇩G s') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
    proof -
      have  "s⟨t'⟩⇩G ≺⇩t s⟨t⟩⇩G"
        using ‹t' ≺⇩t t› less_trm_compatible_with_gctxt by simp
      hence "multp (≺⇩t) {#s⟨t'⟩⇩G, s'#} {#s⟨t⟩⇩G, s'#}"
        using transp_less_trm
        by (simp add: add_mset_commute multp_cancel_add_mset)

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

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

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

    moreover have "∀K ∈# P⇩2'. K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
    proof -
      have "is_strictly_maximal_lit L⇩2 P1"
        using ground_superpositionI by argo
      hence "∀K ∈# P⇩2'. ¬ Pos (Upair t t') ≺⇩l K ∧ Pos (Upair t t') ≠ K"
        unfolding literal_order.is_greatest_in_mset_iff
        unfolding ‹P1 = add_mset L⇩2 P⇩2'› ‹L⇩2 = t ≈ t'›
        by auto
      hence "∀K ∈# P⇩2'. K ≺⇩l Pos (Upair t t')"
        using literal_order.totalp_on_less[THEN totalpD] by metis

      have thesis_if_Neg: "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
        if "𝒫 = Neg"
      proof -
        have "t ≼⇩t s⟨t⟩⇩G"
          using lesseq_trm_if_subtermeq .
        hence " multp (≺⇩t) {#t, t'#} {#s⟨t⟩⇩G, s', s⟨t⟩⇩G, s'#}"
          unfolding reflclp_iff
        proof (elim disjE)
          assume "t ≺⇩t s⟨t⟩⇩G"
          moreover hence "t' ≺⇩t s⟨t⟩⇩G"
            by (meson ‹t' ≺⇩t t› transpD transp_less_trm)
          ultimately show ?thesis
            by (auto intro: one_step_implies_multp[of _ _ _ "{#}", simplified])
        next
          assume "t = s⟨t⟩⇩G"
          thus ?thesis
            using ‹t' ≺⇩t t›
            by (smt (verit, ccfv_SIG) add.commute add_mset_add_single add_mset_commute bex_empty
                one_step_implies_multp set_mset_add_mset_insert set_mset_empty singletonD
                union_single_eq_member)
        qed
        thus "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
          using ‹𝒫 = Neg›
          by (simp add: less_lit_def)
      qed

      have thesis_if_Pos: "Pos (Upair t t') ≼⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
        if "𝒫 = Pos" and "is_maximal_lit L⇩1 P2"
      proof (cases "s")
        case GHole
        show ?thesis
        proof (cases "t' ≼⇩t s'")
          case True
          hence "(multp (≺⇩t))⇧=⇧= {#t, t'#} {#s⟨t⟩⇩G, s'#}"
            unfolding GHole
            using transp_less_trm
            by (simp add: multp_cancel_add_mset)
          thus ?thesis
            unfolding GHole ‹𝒫 = Pos›
            by (auto simp: less_lit_def)
        next
          case False
          hence "s' ≺⇩t t'"
            by order
          hence "multp (≺⇩t) {#s⟨t⟩⇩G, s'#} {#t, t'#}"
            using transp_less_trm
            by (simp add: GHole multp_cancel_add_mset)
          hence "𝒫 (Upair s⟨t⟩⇩G s') ≺⇩l Pos (Upair t t')"
            using ‹𝒫 = Pos›
            by (simp add: less_lit_def)
          moreover have "∀K ∈# P⇩1'. K ≼⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
            using that
            unfolding ground_superpositionI
            unfolding literal_order.is_maximal_in_mset_iff
            by auto
          ultimately have "∀K ∈# P⇩1'. K ≼⇩l Pos (Upair t t')"
            using literal_order.transp_on_less
            by (metis (no_types, lifting) reflclp_iff transpD)
          hence "P2 ≺⇩c P1"
            using ‹𝒫 (Upair s⟨t⟩⇩G s') ≺⇩l Pos (Upair t t')›
              one_step_implies_multp[of P1 P2 "(≺⇩l)" "{#}", simplified]
            unfolding ground_superpositionI less_cls_def
            by (metis ‹∀K∈#P⇩1'. K ≼⇩l (𝒫 (Upair s⟨t⟩⇩G s'))› empty_not_add_mset insert_iff reflclp_iff
                set_mset_add_mset_insert transpD literal_order.transp_on_less)
          hence False
            using ‹P1 ≺⇩c P2› by order
          thus ?thesis ..
        qed
      next
        case (GMore f ts1 ctxt ts2)
        hence "t ≺⇩t s⟨t⟩⇩G"
          using less_trm_if_subterm[of s t] by simp
        moreover hence "t' ≺⇩t s⟨t⟩⇩G"
          using ‹t' ≺⇩t t› by order
        ultimately have "multp (≺⇩t) {#t, t'#} {#s⟨t⟩⇩G, s'#}"
          using one_step_implies_multp[of "{#s⟨t⟩⇩G, s'#}" "{#t, t'#}" "(≺⇩t)" "{#}"] by simp
        hence "Pos (Upair t t') ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')"
          using ‹𝒫 = Pos›
          by (simp add: less_lit_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⟩⇩G s')"
        proof (rule thesis_if_Pos[OF ‹𝒫 = Pos›])
          have "is_strictly_maximal_lit L⇩1 P2"
            using ‹𝒫 = Pos› ground_superpositionI literal.simps(4)
            by (metis literal.simps(4))
          thus "is_maximal_lit L⇩1 P2"
            using literal_order.is_maximal_in_mset_if_is_greatest_in_mset by metis
        qed
        finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G 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⟩⇩G s')"
          using thesis_if_Neg[OF ‹𝒫 = Neg›] .
        finally show "K ≺⇩l 𝒫 (Upair s⟨t⟩⇩G s')" .
      qed
    qed

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

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

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

  ultimately show ?thesis
    by simp
qed

lemma ground_eq_resolution_smaller_conclusion:
  assumes step: "ground_eq_resolution P C"
  shows "C ≺⇩c P"
  using step
proof (cases P C rule: ground_eq_resolution.cases)
  case (ground_eq_resolutionI L t)
  then show ?thesis
    using clause_order.totalp_on_less unfolding less_cls_def
    by (metis add.right_neutral add_mset_add_single empty_iff empty_not_add_mset
        one_step_implies_multp set_mset_empty)
qed

lemma ground_eq_factoring_smaller_conclusion:
  assumes step: "ground_eq_factoring P C"
  shows "C ≺⇩c P"
  using step
proof (cases P C rule: ground_eq_factoring.cases)
  case (ground_eq_factoringI L⇩1 L⇩2 P' t t' t'')
  have "is_maximal_lit L⇩1 P"
    using ground_eq_factoringI by simp
  hence "∀K ∈# add_mset (Pos (Upair t t'')) P'. ¬ Pos (Upair t t') ≺⇩l K"
    unfolding ground_eq_factoringI
    by (simp add: literal_order.is_maximal_in_mset_iff literal_order.neq_iff)
  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
    using transp_less_trm
    by (auto simp: less_lit_def multp_cancel_add_mset)

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

  moreover have "add_mset (Neg (Upair t' t'')) (add_mset (Pos (Upair t t'')) P') ≺⇩c P"
    unfolding ground_eq_factoringI less_cls_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_lit_def)
  qed

  ultimately show ?thesis
    by argo
qed

end

sublocale ground_superposition_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 :: "'f gterm rel"
    assume "refl I" and "trans I" and "sym I" and "compatible_with_gctxt 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

end