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 context admissible_kbo 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')" by (rule add_right_mono, rule weight_w0) 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)" lemma admissible_kbo': "admissible_kbo w w0 pr_strict' pr_weak' least scf" 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 by (rule admissible_kbo') 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" . from adm[OF w] ts' 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