Theory Reduction_Order

theory Reduction_Order
imports Trs
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2014, 2016)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Reduction_Order
imports 
  QTRS.Trs
begin

locale reduction_order =
  fixes less :: "('a, 'b) term ⇒ ('a, 'b) term ⇒ bool" (infix "≻" 50)
  assumes SN_less: "SN {(x, y). x ≻ y}"
    and ctxt: "s ≻ t ⟹ C⟨s⟩ ≻ C⟨t⟩"
    and subst: "s ≻ t ⟹ s ⋅ σ ≻ t ⋅ σ"
    and trans: "s ≻ t ⟹ t ≻ u ⟹ s ≻ u"
begin

abbreviation less_set ("{≻}")
where
  "{≻} ≡ {(x, y). x ≻ y}"

lemma subst_closed_less: "subst.closed {≻}"
using subst by auto

lemma ctxt_closed_less: "ctxt.closed {≻}"
using ctxt by auto

lemma trans_less: "trans {≻}" by (auto simp: trans_def dest: trans)

lemma trancl_less_set [simp]: "{≻}+ = {≻}"
by (auto elim: trancl.induct dest: trans)

lemma rtancl_less_set [simp]: "{≻}* = {≻}="
by (unfold rtrancl_trancl_reflcl) simp

lemma irrefl: "¬ s ≻ s"
  using SN_less by (auto simp: SN_defs)

lemma less_neq:
  "s ≻ t ⟹ s ≠ t"
  "s ≻ t ⟹ t ≠ s"
  by (auto simp: irrefl)

abbreviation lesseq (infix "≽" 50) where
  "s ≽ t ≡ (op ≻)== s t"

lemma compatible_rstep_imp_less:
  assumes "R ⊆ {≻}"
    and "(s, t) ∈ rstep R"
  shows "s ≻ t"
  using assms (2, 1) by (induct) (auto intro: subst ctxt)

lemma compatible_rstep_trancl_imp_less:
  assumes "R ⊆ {≻}"
    and "(s, t) ∈ (rstep R)+"
  shows "s ≻ t"
  using assms(2) and compatible_rstep_imp_less [OF assms(1)]
    by (induct) (auto dest: trans)

end

locale gtotal_reduction_order = reduction_order +
  assumes gtotal: "ground s ⟹ ground t ⟹ s = t ∨ s ≻ t ∨ t ≻ s"

definition "fground F t ⟷ funas_term t ⊆ F ∧ ground t"
definition "FGROUND F r = Restr r {t. fground F t}"

-- ‹reduction orders that are total on ‹E›-euqivalent ground terms›
locale egtotal_reduction_order = reduction_order +
  fixes E
  assumes egtotal: "(s, t) ∈ (rstep E)* ⟹ ground s ⟹ ground t ⟹ s = t ∨ s ≻ t ∨ t ≻ s"

end