Theory Generic_Usable_Rules

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2012-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2011-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Generic_Usable_Rules
imports
  QTRS.Term_Order
  QTRS.Q_Restricted_Rewriting
  QTRS.Trs_Impl
begin

type_synonym ('f,'v)usable_rules_checker = "bool ⇒ bool ⇒ bool ⇒ 'f af ⇒ ('f,'v)terms ⇒ ('f,'v)rules ⇒ ('f,'v)rules option ⇒ ('f,'v)trs ⇒ ('f,'v)rules option"

(* one might generalize this to have an alternation between af_redpair and ce_af_redpair, as soon as IsaFoR contains
   some non-ce-compatible orders *)
definition usable_rules_checker :: "('f,'v)usable_rules_checker ⇒ bool"
  where "usable_rules_checker checker ≡ ∀ nfs m Q R π U_opt sts U S NS. checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt sts = Some U ⟶ ce_af_redpair S NS π ⟶ set U ⊆ NS ⟶ (∃ f. 
           (∀ s t u σ τ. (s,t) ∈ sts ⟶ s ⋅ σ ∈ NF_terms Q ⟶ NF_subst nfs (s,t) σ Q ⟶ (t ⋅ σ, u ⋅ τ) ∈ (qrstep nfs Q (set R))^* ⟶ (m ⟶ SN_on (qrstep nfs Q (set R)) {t ⋅ σ}) ⟶ (t ⋅ f σ, u ⋅ f τ) ∈ NS^*))"


end