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