# Theory KBO_Transformation

section ‹The Knuth--Bendix Order as an instance of WPO›

text ‹Making the Knuth--Bendix an instance of WPO is more complicated than in the
case of RPO and LPO, because of syntactic and semantic differences.
We face the two main challenges in two different theories and sub-sections.›

subsection ‹Aligning least elements›

text ‹In all of RPO, LPO and WPO there is the concept of a minimal term, e.g.,
a constant term $c$ where $c$ is least in precedence among \emph{all function symbols}.
By contrast, in KBO a constant $c$ is minimal if it has minimal weight and has
least precende \emph{among all constants of minimal weight}.›

text ‹In this theory we prove that for any KBO one can modify the precedence in a way
that least constants $c$ also have least precendence among \emph{all function symbols},
without changing the defined order. Hence, afterwards it will be simpler to relate such
a KBO to WPO.›

theory KBO_Transformation
imports WPO Knuth_Bendix_Order.KBO
begin

begin

lemma weight_w0_unary:
assumes *: "weight t = w0" "t = Fun f ts" "ts = t1 # ts'"
shows "ts' = []" "w (f,1) = 0"
proof -
have "w0 + sum_list (map weight ts') ≤ weight t1 + sum_list (map weight ts')"
also have "… = sum_list (map weight ts)" unfolding * by simp
also have "… ≤ sum_list (map weight (scf_list (scf (f, length ts)) ts))"
by (rule sum_list_scf_list, insert scf, auto)
finally have "w (f,length ts) + w0 + sum_list (map weight ts') ≤ weight t" unfolding * by simp
with *(1) have sum: "sum_list (map weight ts') = 0" and wf: "w (f,length ts) = 0" by auto
with weight_gt_0 show ts': "ts' = []" by (cases ts', auto)
with wf show "w (f,1) = 0" using * by auto
qed

definition lConsts :: "('f × nat)set" where "lConsts = { (f,0) | f. least f}"
definition pr_strict' where "pr_strict' f g = (f ∉ lConsts ∧ (pr_strict f g ∨ g ∈ lConsts))"
definition pr_weak' where "pr_weak' f g = ((f ∉ lConsts ∧ pr_weak f g) ∨ g ∈ lConsts)"

apply (unfold_locales)
subgoal by (rule w0)
subgoal by (rule w0)
subgoal for f g n using adm[of f g n] unfolding pr_weak'_def by (auto simp: lConsts_def)
subgoal for f using least[of f] unfolding pr_weak'_def lConsts_def by auto
subgoal by (rule scf)
subgoal for f using pr_weak_refl[of f] unfolding pr_weak'_def by auto
subgoal for f g h using pr_weak_trans[of f g h] unfolding pr_weak'_def by auto
subgoal for f g using pr_strict[of f g] unfolding pr_strict'_def pr_weak'_def by auto
proof -
show "SN {(x, y). pr_strict' x y}" (is "SN ?R")
proof
fix f
assume "∀ i. (f i, f (Suc i)) ∈ ?R"
hence steps: "⋀ i. (f i, f (Suc i)) ∈ ?R" by blast
have "f i ∉ lConsts" for i using steps[of i] unfolding pr_strict'_def by auto
hence "pr_strict (f i) (f (Suc i))" for i using steps[of i] unfolding pr_strict'_def by auto
with pr_SN show False by auto
qed
qed

lemma least_pr_weak': "least f ⟹ pr_weak' g (f,0)" unfolding lConsts_def pr_weak'_def by auto

lemma least_pr_weak'_trans: "least f ⟹ pr_weak' (f,0) g ⟹ least (fst g) ∧ snd g = 0"
unfolding lConsts_def pr_weak'_def by auto

context
begin
interpretation kbo': admissible_kbo w w0 pr_strict' pr_weak' least scf

lemma kbo'_eq_kbo: "kbo'.kbo s t = kbo s t"
proof (induct s t rule: kbo.induct)
case (1 s t)
note simps = kbo.simps[of s t] kbo'.kbo.simps[of s t]
show ?case unfolding simps
apply (intro if_cong refl, intro term.case_cong refl)
proof -
fix f ss g ts
assume *: "vars_term_ms (SCF t) ⊆# vars_term_ms (SCF s) ∧ weight t ≤ weight s"
"¬ weight t < weight s"
and s: "s = Fun f ss"
and t: "t = Fun g ts"
let ?g = "(g,length ts)"
let ?f = "(f,length ss)"
have IH: "(if pr_strict ?f ?g then (True, True)
else if pr_weak ?f ?g then lex_ext_unbounded kbo ss ts else (False, False))
= (if pr_strict ?f ?g then (True, True)
else if pr_weak ?f ?g then lex_ext_unbounded kbo'.kbo ss ts else (False, False))"
by (intro if_cong refl lex_ext_unbounded_cong, insert 1[OF * s t], auto)
let ?P = "pr_strict' ?f ?g = pr_strict ?f ?g ∧ (¬ pr_strict ?f ?g ⟶ pr_weak' ?f ?g = pr_weak ?f ?g)"
show "(if pr_strict' ?f ?g then (True, True)
else if pr_weak' ?f ?g then lex_ext_unbounded kbo'.kbo ss ts else (False, False)) =
(if pr_strict ?f ?g then (True, True)
else if pr_weak ?f ?g then lex_ext_unbounded kbo ss ts else (False, False))"
proof (cases ?P)
case True
thus ?thesis unfolding IH by auto
next
case notP: False
hence fgC: "?f ∈ lConsts ∨ ?g ∈ lConsts" unfolding pr_strict'_def pr_weak'_def by auto
hence weight: "weight s = w0" "weight t = w0" using * unfolding lConsts_def least s t by auto
show ?thesis
proof (cases "ss = [] ∧ ts = []")
case empty: True
with weight have "w ?f = w0" "w ?g = w0" unfolding s t by auto
with empty have ?P unfolding pr_strict'_def pr_weak'_def using pr_weak_trans[of _ "(g,0)" "(f,0)"]
pr_weak_trans[of _ "(f,0)" "(g,0)"]
by (auto simp: lConsts_def pr_strict least)
with notP show ?thesis by blast
next
case False
{
fix f and t :: "('f,'a)term"  and t1 ts' ts and g
assume *: "weight t = w0" "t = Fun f ts" "ts = t1 # ts'"
from weight_w0_unary[OF this]
have ts': "ts' = []" and w: "w (f,1) = 0" .
have "pr_weak (f, Suc (length ts')) g" by (cases g, auto)
} note unary = this
from fgC have "ss = [] ∨ ts = []" unfolding lConsts_def least by auto
thus ?thesis
proof
assume ss: "ss = []"
with False obtain t1 ts' where ts: "ts = t1 # ts'" by (cases ts, auto)
show ?thesis unfolding ss ts using unary[OF weight(2) t ts]
by (simp add: lex_ext_unbounded.simps pr_strict'_def lConsts_def pr_strict)
next
assume ts: "ts = []"
with False obtain s1 ss' where ss: "ss = s1 # ss'" by (cases ss, auto)
show ?thesis unfolding ss ts using unary[OF weight(1) s ss]
by (simp add: lex_ext_unbounded.simps pr_strict'_def pr_weak'_def lConsts_def pr_strict)
qed
qed
qed
qed
qed
end
end
end