Theory Superposition_Alternative_Rules

theory Superposition_Alternative_Rules
  imports Superposition
begin

context superposition_calculus
begin

subsubsection ‹Alternative Specification of the Superposition Rule›

inductive superposition' ::
  "('t, 'v, 'ty) typed_clause ⇒ 
   ('t, 'v, 'ty) typed_clause ⇒ 
   ('t, 'v, 'ty) typed_clause ⇒ bool" where
  superposition'I:
   "(term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩1) ⟹
    (term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩2) ⟹
    term.is_renaming ρ⇩1 ⟹
    term.is_renaming ρ⇩2 ⟹
    clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
    E = add_mset l⇩1 E' ⟹
    D = add_mset l⇩2 D' ⟹
    𝒫 ∈ {Pos, Neg} ⟹
    l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1') ⟹
    l⇩2 = t⇩2 ≈ t⇩2' ⟹
    ¬ term.is_Var t⇩1 ⟹
    type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ ⟹
    term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}} ⟹
    ∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
    ∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
    type_preserving_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
    type_preserving_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
    (clause.weakly_welltyped 𝒱⇩3 C ⟹ literal.weakly_welltyped 𝒱⇩2 l⇩2) ⟹
    ¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
    (𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
     𝒫 = Neg ∧ (select E = {#} ∧ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
                  is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ))) ⟹
    select D = {#} ⟹
    is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
    ¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
    ¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
    C = add_mset (𝒫 (Upair (c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ (t⇩1' ⋅t ρ⇩1))) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
    superposition' (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C)"

lemma superposition_eq_superposition': "superposition = superposition'"
proof (intro ext iffI)
  fix D E C
  assume "superposition D E C"
  then show "superposition' D E C"

  proof (cases D E C rule: superposition.cases)
    case (superpositionI 𝒫 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D t⇩1 𝒱⇩3 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 C E' D')

    show ?thesis
    proof (unfold superpositionI(1-3), rule superposition'I; (rule superpositionI)?)

      show "𝒫 = Pos ∧ select E = {#} ∧ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
       𝒫 = Neg ∧ (select E = {#} ∧ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ∨
                   is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (select E ⋅ ρ⇩1 ⊙ μ))"
        using superpositionI
        by fastforce
    qed
  qed
next
  fix D E C
  assume "superposition' D E C"
  then show "superposition D E C"
  proof (cases D E C rule: superposition'.cases)
    case (superposition'I 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' 𝒫 c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)

    show ?thesis
    proof (unfold superposition'I(1-3), rule superpositionI; (rule superposition'I)?)

      show
        "𝒫 = Pos ⟹ select E = {#}"
        "𝒫 = Pos ⟹ is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
        "𝒫 = Neg ⟹ select E = {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
        "𝒫 = Neg ⟹ select E ≠ {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (select E ⋅ ρ⇩1 ⊙ μ)"
        using superposition'I(23) is_maximal_not_empty
        by auto
    qed
  qed
qed

inductive pos_superposition ::
  "('t, 'v, 'ty) typed_clause ⇒ ('t, 'v, 'ty) typed_clause ⇒ ('t, 'v, 'ty) typed_clause ⇒ bool"
where
  pos_superpositionI:
   "(term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩1) ⟹
    (term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩2) ⟹
    term.is_renaming ρ⇩1 ⟹
    term.is_renaming ρ⇩2 ⟹
    clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
    E = add_mset l⇩1 E' ⟹
    D = add_mset l⇩2 D' ⟹
    l⇩1 = c⇩1⟨t⇩1⟩ ≈ t⇩1' ⟹
    l⇩2 = t⇩2 ≈ t⇩2' ⟹
    ¬ term.is_Var t⇩1 ⟹
    type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ ⟹
    term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}} ⟹
    ∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
    ∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
    type_preserving_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
    type_preserving_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
    (clause.weakly_welltyped 𝒱⇩3 C ⟹ literal.weakly_welltyped 𝒱⇩2 l⇩2) ⟹
    ¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
    select E = {#} ⟹
    is_strictly_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ) ⟹
    select D = {#} ⟹
    is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
    ¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
    ¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
    C = add_mset ((c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ ≈ (t⇩1' ⋅t ρ⇩1)) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
    pos_superposition (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C)"

lemma superposition_if_pos_superposition:
  assumes "pos_superposition D E C"
  shows "superposition D E C"
  using assms
proof (cases rule: pos_superposition.cases)
  case (pos_superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)

  then show ?thesis
    using superpositionI[of Pos 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D t⇩1 𝒱⇩3 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 C E' D']
    by blast
qed

inductive neg_superposition ::
  "('t, 'v, 'ty) typed_clause ⇒ ('t, 'v, 'ty) typed_clause ⇒ ('t, 'v, 'ty) typed_clause ⇒ bool"
where
  neg_superpositionI:
   "(term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩1) ⟹
    (term.exists_nonground ⟹ infinite_variables_per_type 𝒱⇩2) ⟹
    term.is_renaming ρ⇩1 ⟹
    term.is_renaming ρ⇩2 ⟹
    clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ⟹
    E = add_mset l⇩1 E' ⟹
    D = add_mset l⇩2 D' ⟹
    l⇩1 = c⇩1⟨t⇩1⟩ !≈ t⇩1' ⟹
    l⇩2 = t⇩2 ≈ t⇩2' ⟹
    ¬ term.is_Var t⇩1 ⟹
    type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ ⟹
    term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}} ⟹
    ∀x ∈ clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x) ⟹
    ∀x ∈ clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x) ⟹
    type_preserving_on (clause.vars E) 𝒱⇩1 ρ⇩1 ⟹
    type_preserving_on (clause.vars D) 𝒱⇩2 ρ⇩2 ⟹
    (clause.weakly_welltyped 𝒱⇩3 C ⟹ literal.weakly_welltyped 𝒱⇩2 l⇩2) ⟹
    ¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ) ⟹
    (select E = {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)) ⟹
    (select E ≠ {#} ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) ((select E) ⋅ ρ⇩1 ⊙ μ)) ⟹
    select D = {#} ⟹
    is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ) ⟹
    ¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ) ⟹
    ¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ) ⟹
    C = add_mset ((c⇩1 ⋅t⇩c ρ⇩1)⟨t⇩2' ⋅t ρ⇩2⟩ !≈ (t⇩1' ⋅t ρ⇩1)) (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
    neg_superposition (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C)"

lemma superposition_if_neg_superposition:
  assumes "neg_superposition E D C"
  shows "superposition E D C"
  using assms
proof (cases E D C rule: neg_superposition.cases)
  case (neg_superpositionI 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C)
 
  then show ?thesis
    using
      superpositionI[of Neg 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D t⇩1 𝒱⇩3 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 C E' D']
      literals_distinct(2)
    by blast
qed

lemma superposition_iff_pos_or_neg:
  "superposition D E C ⟷ pos_superposition D E C ∨ neg_superposition D E C"
proof (rule iffI)
  assume "superposition D E C"
  thus "pos_superposition D E C ∨ neg_superposition D E C"
  proof (cases D E C rule: superposition.cases)
    case (superpositionI 𝒫 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D t⇩1 𝒱⇩3 μ t⇩2 c⇩1 t⇩1' t⇩2' l⇩1 l⇩2 C E' D')

    show ?thesis
    proof(cases "𝒫 = Pos")
      case True

      then show ?thesis
        using
          superpositionI
          pos_superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C]
        unfolding superpositionI(1-3)
        by argo
    next
      case False

      then show ?thesis
        using
          superpositionI
          neg_superpositionI[of 𝒱⇩1 𝒱⇩2 ρ⇩1 ρ⇩2 E D l⇩1 E' l⇩2 D' c⇩1 t⇩1 t⇩1' t⇩2 t⇩2' 𝒱⇩3 μ C]
        using superpositionI(4)
        unfolding superpositionI(1-3)
        by blast
    qed
  qed
next
  assume "pos_superposition D E C ∨ neg_superposition D E C"

  thus "superposition D E C"
    using superposition_if_neg_superposition superposition_if_pos_superposition
    by fast
qed

end

end