Theory Precedence
subsection ‹Precedence›
text
‹A precedence consists of two compatible relations (strict and non-strict) on symbols such that
the strict relation is strongly normalizing. In the formalization we model this via a
function "prc" (precedence-compare) which returns two Booleans, indicating whether the one symbol is
strictly or weakly bigger than the other symbol. Moreover, there also is a function "prl"
(precedence-least) which gives quick access to whether a symbol is least in precedence, i.e.,
without comparing it to all other symbols explicitly.›
theory Precedence
imports
"Abstract-Rewriting.Abstract_Rewriting"
begin
locale irrefl_precedence =
fixes prc :: "'f ⇒ 'f ⇒ bool × bool"
and prl :: "'f ⇒ bool"
assumes prc_refl: "prc f f = (False, True)"
and prc_stri_imp_nstri: "fst (prc f g) ⟹ snd (prc f g)"
and prl: "prl g ⟹ snd (prc f g) = True"
and prl3: "prl f ⟹ snd (prc f g) ⟹ prl g"
and prc_compat: "prc f g = (s1, ns1) ⟹ prc g h = (s2, ns2) ⟹ prc f h = (s, ns) ⟹
(ns1 ∧ ns2 ⟶ ns) ∧ (ns1 ∧ s2 ⟶ s) ∧ (s1 ∧ ns2 ⟶ s)"
begin
lemma prl2:
assumes g: "prl g" shows "fst (prc g f) = False"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain b where gf: "prc g f = (True, b)" by (cases "prc g f", auto)
obtain b1 b2 where gg: "prc g g = (b1, b2)" by force
obtain b' where fg: "prc f g = (b', True)" using prl[OF g, of f] by (cases "prc f g", auto)
from prc_compat[OF gf fg gg] gg have gg: "fst (prc g g)" by auto
with prc_refl[of g] show False by auto
qed
abbreviation "pr ≡ (prc, prl)"
end
locale precedence = irrefl_precedence +
constrains prc :: "'f ⇒ 'f ⇒ bool × bool"
and prl :: "'f ⇒ bool"
assumes prc_SN: "SN {(f, g). fst (prc f g)}"
end