Theory Precedence

section ‹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 precedence =
  fixes prc :: "'f ⇒ 'f ⇒ bool × bool"
    and prl :: "'f ⇒ bool"
  assumes prc_refl: "prc f f = (False, True)"
    and prc_SN: "SN {(f, g). fst (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)"
    and prc_stri_imp_nstri: "fst (prc f g) ⟹ snd (prc f g)"
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 SN_on_irrefl[OF prc_SN] show False by blast
qed

abbreviation "pr ≡ (prc, prl)"

end

end