Theory Ground_Superposition

theory Ground_Superposition
  imports
    Ground_Critical_Pairs
    First_Order_Clause.Selection_Function
    First_Order_Clause.Ground_Order
    First_Order_Clause.Ground_Clause
begin

section ‹Superposition Calculus›


locale ground_superposition_calculus = 
  ground_order_with_equality where lesst = lesst +
  selection_function select +
  ground_critical_pair_theorem "TYPE('f)"
for
  lesst :: "'f gterm  'f gterm  bool" and
  select :: "'f gatom clause  'f gatom clause"
begin

subsection ‹Ground Rules›

inductive superposition ::
  "'f gatom clause  'f gatom clause  'f gatom clause  bool"
where
  superpositionI: "
    E = add_mset LE E' 
    D = add_mset LD D' 
    D c E 
    𝒫  {Pos, Neg} 
    LE = 𝒫 (Upair κtG u) 
    LD = t  t' 
    u t κtG 
    t' t t 
    (𝒫 = Pos  select E = {#}  is_strictly_maximal LE E) 
    (𝒫 = Neg  (select E = {#}  is_maximal LE E  is_maximal LE (select E))) 
    select D = {#} 
    is_strictly_maximal LD D 
    C = add_mset (𝒫 (Upair κt'G u)) (E' + D') 
    superposition D E C"

inductive eq_resolution :: "'f gatom clause  'f gatom 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 :: "'f gatom clause  'f gatom clause  bool" where
  eq_factoringI: "
    D = add_mset L1 (add_mset L2 D') 
    L1 = t  t' 
    L2 = t  t'' 
    select D = {#} 
    is_maximal L1 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' :: 
  "'f gatom clause  'f gatom clause  'f gatom clause  bool"
where
  superposition'I: "
    P1 = add_mset L1 P1' 
    P2 = add_mset L2 P2' 
    P2 c P1 
    𝒫  {Pos, Neg} 
    L1 = 𝒫 (Upair stG s') 
    L2 = t  t' 
    s' t stG 
    t' t t 
    (𝒫 = Pos  select P1 = {#}  is_strictly_maximal L1 P1) 
    (𝒫 = Neg  (select P1 = {#}  is_maximal L1 P1  is_maximal L1 (select P1))) 
    select P2 = {#} 
    is_strictly_maximal L2 P2 
    C = add_mset (𝒫 (Upair st'G s')) (P1' + P2') 
    superposition' P2 P1 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 L1 P1' L2 P2' 𝒫 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 L1 P1' L2 P2' 𝒫 s t s' t')
    thus ?thesis
      using superposition'I
      by (metis literals_distinct(2))
  qed
qed

inductive pos_superposition ::
  "'f gatom clause  'f gatom clause  'f gatom clause  bool"
where
 pos_superpositionI: "
    P1 = add_mset L1 P1' 
    P2 = add_mset L2 P2' 
    P2 c P1 
    L1 = stG  s' 
    L2 = t  t' 
    s' t stG 
    t' t t 
    select P1 = {#} 
    is_strictly_maximal L1 P1 
    select P2 = {#} 
    is_strictly_maximal L2 P2 
    C = add_mset (st'G  s') (P1' + P2') 
    pos_superposition P2 P1 C"

lemma superposition_if_pos_superposition:
  assumes step: "pos_superposition P2 P1 C"
  shows "superposition P2 P1 C"
  using step
proof (cases P2 P1 C rule: pos_superposition.cases)
  case (pos_superpositionI L1 P1' L2 P2' s t s' t')
  thus ?thesis
    using superpositionI
    by (metis insert_iff)
qed

inductive neg_superposition ::
  "'f gatom clause  'f gatom clause  'f gatom clause  bool"
where
 neg_superpositionI: 
   "P1 = add_mset L1 P1' 
    P2 = add_mset L2 P2' 
    P2 c P1 
    L1 = stG !≈ s' 
    L2 = t  t' 
    s' t stG 
    t' t t 
    select P1 = {#}  is_maximal L1 P1  is_maximal L1 (select P1) 
    select P2 = {#} 
    is_strictly_maximal L2 P2 
    C = add_mset (Neg (Upair st'G s')) (P1' + P2') 
    neg_superposition P2 P1 C"

lemma superposition_if_neg_superposition:
  assumes "neg_superposition P2 P1 C"
  shows "superposition P2 P1 C"
  using assms
proof (cases P2 P1 C rule: neg_superposition.cases)
  case (neg_superpositionI L1 P1' L2 P2' s t s' t')
  then show ?thesis
    using superpositionI
    by (metis insert_iff)
qed

lemma superposition_iff_pos_or_neg:
  "superposition P2 P1 C 
    pos_superposition P2 P1 C  neg_superposition P2 P1 C"
proof (rule iffI)
  assume "superposition P2 P1 C"
  thus "pos_superposition P2 P1 C  neg_superposition P2 P1 C"
  proof (cases P2 P1 C rule: superposition.cases)
    case (superpositionI L1 P1' L2 P2' 𝒫 s t s' t')
    then show ?thesis
      using pos_superpositionI[of P1 L1 P1' P2 L2 P2' s t s' t']
      using neg_superpositionI[of P1 L1 P1' P2 L2 P2' s t s' t']
      by metis
  qed
next
  assume "pos_superposition P2 P1 C  neg_superposition P2 P1 C"
  thus "superposition P2 P1 C"
    using 
      superposition_if_neg_superposition
      superposition_if_pos_superposition
    by metis
qed


subsection ‹Ground Layer›

definition G_Inf :: "'f gatom clause inference set" where
  "G_Inf =
    {Infer [P2, P1] C | P2 P1 C. superposition P2 P1 C} 
    {Infer [P] C | P C. eq_resolution P C} 
    {Infer [P] C | P C. 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 N1 N2  ((I :: 'f gterm rel). refl I  trans I  sym I 
    compatible_with_gctxt I  upair ` I ⊫s N1  upair ` I ⊫s N2)"

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 L1 P1' L2 P2' 𝒫 s t s' t')

  have "P1' + add_mset (𝒫 (Upair st'G s')) P2' c P1' + {#𝒫 (Upair stG s')#}"
    unfolding lessc_def
  proof (intro one_step_implies_multp ballI)
    fix K assume "K ∈# add_mset (𝒫 (Upair st'G s')) P2'"

    moreover have "𝒫 (Upair st'G s') l 𝒫 (Upair stG s')"
    proof -
      have  "st'G t stG"
        using t' t t 
        by simp

      hence "multp (≺t) {#st'G, s'#} {#stG, s'#}"
        by (simp add: add_mset_commute multp_cancel_add_mset)

      have ?thesis if "𝒫 = Pos"
        unfolding that lessl_def
        using multp (≺t) {#st'G, s'#} {#stG, s'#} 
        by simp

      moreover have ?thesis if "𝒫 = Neg"
        unfolding that lessl_def
        using multp (≺t) {#st'G, s'#} {#stG, s'#} multp_double_doubleI
        by force

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

    moreover have "K ∈# P2'. K l 𝒫 (Upair stG s')"
    proof -
      have "is_strictly_maximal L2 P1"
        using superpositionI
        by argo

      hence "K ∈# P2'. ¬ Pos (Upair t t') l K  Pos (Upair t t')  K"
        unfolding 
          is_strictly_maximal_def
          P1 = add_mset L2 P2' L2 = t  t'
        by simp

      hence "K ∈# P2'. K l Pos (Upair t t')"
        by auto

      have thesis_if_Neg: "Pos (Upair t t') l 𝒫 (Upair stG s')"
        if "𝒫 = Neg"
      proof -
        have "t t stG"
          using term.order.less_eq_subterm_property .

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

          moreover hence "t' t stG"
            using superpositionI(8) 
            by order

          ultimately show ?thesis
            by (auto intro: one_step_implies_multp[of _ _ _ "{#}", simplified])
        next
          assume "t = stG"
          thus ?thesis
            using t' t t
            by simp
        qed
        thus "Pos (Upair t t') l 𝒫 (Upair stG s')"
          using 𝒫 = Neg
          by (simp add: lessl_def)
      qed

      have thesis_if_Pos: "Pos (Upair t t') l 𝒫 (Upair stG s')"
        if "𝒫 = Pos" and "is_maximal L1 P2"
      proof (cases "s")
        case Hole
        show ?thesis
        proof (cases "t' t s'")
          case True

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

          thus ?thesis
            unfolding Hole 𝒫 = Pos
            by (auto simp: lessl_def)
        next
          case False
          hence "s' t t'"
            by order

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

          hence "𝒫 (Upair stG s') l Pos (Upair t t')"
            using 𝒫 = Pos
            by (simp add: lessl_def)

          moreover have "K ∈# P1'. K l 𝒫 (Upair stG s')"
            using that
            unfolding superpositionI is_maximal_def
            by auto

          ultimately have "K ∈# P1'. K l Pos (Upair t t')"
            by auto
            
          hence "P2 c P1"
            using 
              𝒫 (Upair stG 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 lessc_def
            by blast

          hence False
            using P1 c P2 by order

          thus ?thesis ..
        qed
      next
        case (More f ts1 ctxt ts2)
        hence "t t stG"
          using term.order.subterm_property[of s t]
          by simp

        moreover hence "t' t stG"
          using t' t t 
          by order

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

        hence "Pos (Upair t t') l 𝒫 (Upair stG s')"
          using 𝒫 = Pos
          by (simp add: lessl_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 ∈# P2'"
        have "K l t  t'"
          using K∈#P2'. K l t  t' K ∈# P2' 
          by metis

        also have "t  t' l 𝒫 (Upair stG s')"
        proof (rule thesis_if_Pos[OF 𝒫 = Pos])

          have "is_strictly_maximal L1 P2"
            using 𝒫 = Pos superpositionI 
            by simp

          thus "is_maximal L1 P2"
            by blast
        qed

        finally show "K l 𝒫 (Upair stG s')" .
      next
        fix K assume "𝒫 = Neg" "K ∈# P2'"

        have "K l t  t'"
          using K∈#P2'. K l t  t' K ∈# P2' 
          by metis

        also have "t  t' l 𝒫 (Upair stG s')"
          using thesis_if_Neg[OF 𝒫 = Neg] .

        finally show "K l 𝒫 (Upair stG s')" .
      qed
    qed

    ultimately show "j ∈# {#𝒫 (Upair stG s')#}. K l j"
      by auto
  qed simp

  moreover have "C = add_mset (𝒫 (Upair st'G s')) (P1' + P2')"
    unfolding superpositionI ..

  moreover have "P2 = P1' + {#𝒫 (Upair stG 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 lessc_def
    by (metis add.left_neutral add_mset_add_single 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 L1 L2 P' t t' t'')
  have "is_maximal L1 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: lessl_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 lessc_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: lessl_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 :: "'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

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 [P2, P1] C" and
      infer: "superposition P2 P1 C"
    for P2 P1 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 "DN. 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