Theory First_Order_Clause.Ground_Term_Order

theory Ground_Term_Order
  imports
    Generic_Context
    Context_Compatible_Order
    Term_Order_Notation
    Transitive_Closure_Extra
begin

locale subterm_property =
  strict_order where less = less⇩t +
  "context"
  for less⇩t :: "'t ⇒ 't ⇒ bool" +
  assumes
    subterm_property [simp]: "⋀t c. c ≠ □ ⟹ less⇩t t c⟨t⟩"
begin

interpretation term_order_notation .

lemma less_eq_subterm_property: "t ≼⇩t c⟨t⟩"
  using subterm_property
  by (metis apply_hole reflclp_iff)

end

locale context_compatible_ground_term_order =
  wellfounded_strict_order where less = less⇩t +
  total_strict_order where less = less⇩t +
  context_compatible_order where less = less⇩t +
  subterm_property
begin

interpretation term_order_notation .

end

locale ground_term_order =
  wellfounded_strict_order where less = less⇩t +
  total_strict_order where less = less⇩t
for less⇩t :: "'t ⇒ 't ⇒ bool"
begin

interpretation term_order_notation .

end

end