Theory Reduction_Order_Impl

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2016)
License: LGPL (see file COPYING.LESSER)
*)
theory Reduction_Order_Impl
  imports
    Reduction_Order
    "Certification_Monads.Check_Monad"
begin

text ‹Ground-total reduction orders with respect to a given signature.›
record ('f, 'v) redord =
  valid :: "shows check"
  less :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool"
  min_const :: "'f"

hide_const (open) valid less min_const
  
locale reduction_order_impl =
  fixes ro :: "'a ⇒ ('f × nat) list ⇒ ('f::show, 'v::show) redord"
  assumes valid: "isOK (redord.valid (ro r F)) ⟹
     (redord.min_const (ro r F), 0) ∈ set F ∧
     reduction_order (redord.less (ro r F)) ∧
     (∀s t. fground (set F) s ∧ fground (set F) t ⟶
       s = t ∨ redord.less (ro r F) s t ∨ redord.less (ro r F) t s) ∧
     (∃less.
       gtotal_reduction_order less ∧
       (∀s t. redord.less (ro r F) s t ⟶ less s t) ∧
       (∀t. ground t ⟶ less⇧=⇧= t (Fun (redord.min_const (ro r F)) [])))"

end