Theory Ground_Term_Order

theory Ground_Term_Order
  imports
    Ground_Context
    Context_Compatible_Order
    Term_Order_Notation
    Transitive_Closure_Extra
begin

locale context_compatible_ground_order = context_compatible_order where Fun = GFun

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

interpretation term_order_notation.

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

end

locale ground_term_order =
  wellfounded_strict_order less⇩t +
  total_strict_order less⇩t +
  context_compatible_ground_order less⇩t +
  subterm_property less⇩t
  for less⇩t :: "'f gterm ⇒ 'f gterm ⇒ bool"
begin

interpretation term_order_notation.


end

end