Theory Ordered_Resolution

theory Ordered_Resolution
  imports
    First_Order_Clause.Nonground_Order
    First_Order_Clause.Nonground_Selection_Function
    First_Order_Clause.Nonground_Typing
    First_Order_Clause.Typed_Tiebreakers
    Saturation_Framework.Lifting_to_Non_Ground_Calculi
  
    Ground_Ordered_Resolution
begin

locale ordered_resolution_calculus =
  witnessed_nonground_typing where
  welltyped = welltyped and term_to_ground = "term_to_ground :: 't ⇒ 't⇩G" and
  id_subst = "id_subst :: 'subst" +

  nonground_order where less⇩t = less⇩t +

  nonground_selection_function where
  select = select and atom_subst = "(⋅t)" and atom_vars = term.vars and
  atom_from_ground = term.from_ground and atom_to_ground = term.to_ground +
  tiebreakers tiebreakers
for
  select :: "'t select" and
  less⇩t :: "'t ⇒ 't ⇒ bool" and
  tiebreakers :: "('t⇩G, 't) tiebreakers" and
  welltyped :: "('v :: infinite, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool"
begin

inductive factoring :: "('t, 'v, 'ty) typed_clause ⇒ ('t, 'v, 'ty) typed_clause ⇒ bool" where
  factoringI: 
  "D = add_mset l⇩1 (add_mset l⇩2 D') ⟹
   l⇩1 = Pos t⇩1 ⟹
   l⇩2 = Pos t⇩2 ⟹
   C = (add_mset l⇩1 D') ⋅ μ ⟹
   factoring (𝒱, D) (𝒱, C)"
if
  "select D = {#}"
  "is_maximal (l⇩1 ⋅l μ) (D ⋅ μ)"
  "type_preserving_on (clause.vars D) 𝒱 μ" 
  "term.is_imgu μ {{t⇩1, t⇩2}}"

inductive resolution ::
  "('t, 'v, 'ty) typed_clause ⇒
   ('t, 'v, 'ty) typed_clause ⇒
   ('t, 'v, 'ty) typed_clause ⇒ bool" where
  resolutionI: 
  "E = add_mset l⇩1 E' ⟹
   D = add_mset l⇩2 D' ⟹
   l⇩1 = Neg t⇩1 ⟹
   l⇩2 = Pos t⇩2 ⟹
   C = (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ ⟹
   resolution (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C)"
if
  "infinite_variables_per_type 𝒱⇩1"
  "infinite_variables_per_type 𝒱⇩2"
  "term.is_renaming ρ⇩1"
  "term.is_renaming ρ⇩2"
  "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}"
  "type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 μ" 
  "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩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 ⊙ μ)"
  "∀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"

abbreviation factoring_inferences where
 "factoring_inferences ≡ { Infer [D] C | D C. factoring D C }"

abbreviation resolution_inferences where
 "resolution_inferences ≡ { Infer [D, E] C | D E C. resolution D E C }"

definition inferences :: "('t, 'v, 'ty) typed_clause inference set" where
 "inferences ≡ resolution_inferences ∪ factoring_inferences"

abbreviation bottom⇩F :: "('t, 'v, 'ty) typed_clause set" ("⊥⇩F") where
  "bottom⇩F ≡ {(𝒱, {#}) | 𝒱. infinite_variables_per_type 𝒱 }"

end

end