Theory Untyped_Superposition

theory Untyped_Superposition
  imports 
    First_Order_Clause.Nonground_Order_With_Equality
    First_Order_Clause.Nonground_Selection_Function
    First_Order_Clause.Tiebreakers
    First_Order_Clause.Infinite_Variables

    Ground_Term_Context
begin

locale untyped_superposition_calculus =
  nonground_term_with_context where
  term_vars = "term_vars :: 't ⇒ 'v set" and
  term_to_ground = "term_to_ground :: 't ⇒ 't⇩G" +

  context_compatible_nonground_order where less⇩t = less⇩t +

  nonground_selection_function where
  select = select and atom_subst = "(⋅a)" and atom_vars = atom.vars and
  atom_is_ground = atom.is_ground and atom_to_ground = atom.to_ground and
  atom_from_ground = atom.from_ground +

  "term": exists_imgu where vars = term_vars and subst = "(⋅t)" and is_ground = term_is_ground +

  infinite_variables where
  variables = "UNIV :: 'v set" and exists_nonground = term.exists_nonground +

  ground_term_context' +

  tiebreakers tiebreakers +

  (* TODO: *)
  subst_eq where vars = term_vars and subst = "(⋅t)" and is_ground = term_is_ground +
  vars_grounded_iff_is_grounding where 
  vars = term_vars and subst = "(⋅t)" and is_ground = term_is_ground and base_vars = term_vars and 
  base_subst = "(⋅t)" and base_is_ground = term_is_ground +
  subst_updates_compat where vars = term_vars and subst = "(⋅t)" and is_ground = term_is_ground
  for
    select :: "'t atom select" and
    less⇩t :: "'t ⇒ 't ⇒ bool" and
    tiebreakers :: "('t⇩G atom, 't atom) tiebreakers" 
begin

interpretation term_order_notation .

inductive eq_resolution :: "'t clause ⇒ 't clause ⇒ bool" where
  eq_resolutionI:
  "D = add_mset l D' ⟹
   l = t !≈ t' ⟹
   C = D' ⋅ μ ⟹
   eq_resolution D C"
if 
  "term.is_imgu μ {{t, t'}}"
  "select D = {#} ⟹ is_maximal (l ⋅l μ) (D ⋅ μ)"
  "select D ≠ {#} ⟹ is_maximal (l ⋅l μ) (select D ⋅ μ)"

inductive eq_factoring :: "'t clause ⇒ 't clause ⇒ bool" where
  eq_factoringI:
  "D = add_mset l⇩1 (add_mset l⇩2 D') ⟹
   l⇩1 = t⇩1 ≈ t⇩1' ⟹
   l⇩2 = t⇩2 ≈ t⇩2' ⟹
   C = add_mset (t⇩1 ≈ t⇩2') (add_mset (t⇩1' !≈ t⇩2') D') ⋅ μ ⟹
   eq_factoring D C"
if
  "select D = {#}"
  "is_maximal (l⇩1 ⋅l μ) (D ⋅ μ)"
  "¬ (t⇩1 ⋅t μ ≼⇩t t⇩1' ⋅t μ)"
  "term.is_imgu μ {{t⇩1, t⇩2}}"

inductive superposition :: "'t clause ⇒ 't clause ⇒ 't clause ⇒ bool" where
  superpositionI:
  "E = add_mset l⇩1 E' ⟹
   D = add_mset l⇩2 D' ⟹
   l⇩1 = 𝒫 (Upair c⇩1⟨t⇩1⟩ t⇩1') ⟹
   l⇩2 = 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 D E C"
if
  "𝒫 ∈ {Pos, Neg}"
  "term.is_renaming ρ⇩1"
  "term.is_renaming ρ⇩2"
  "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}"
  "¬ term.is_Var t⇩1"
  "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}}"
  "¬ (E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ)"
  "¬ (c⇩1⟨t⇩1⟩ ⋅t ρ⇩1 ⊙ μ ≼⇩t t⇩1' ⋅t ρ⇩1 ⊙ μ)"
  "¬ (t⇩2 ⋅t ρ⇩2 ⊙ μ ≼⇩t t⇩2' ⋅t ρ⇩2 ⊙ μ)"
  "𝒫 = 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 ⊙ μ)"
  "select D = {#}"
  "is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ)"

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

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

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

definition inferences :: "'t clause inference set" where
  "inferences ≡ superposition_inferences ∪ eq_resolution_inferences ∪ eq_factoring_inferences"

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

end

end