subsection ‹A restricted equality between KBO and WPO› text ‹The remaining difficulty to make KBO an instance of WPO is the different treatment of lexicographic comparisons, which is unrestricted in KBO, but there is a length-restriction in WPO. Therefore we will only show that KBO is an instance of WPO if we compare terms with bounded arity.› text ‹This restriction does however not prohibit us from lifting properties of WPO to KBO. For instance, for several properties one can choose a large-enough bound restriction of WPO, since there are only finitely many arities occurring in a property.› theory KBO_as_WPO imports WPO KBO_Transformation begin definition bounded_arity :: "nat ⇒ ('f × nat)set ⇒ bool" where "bounded_arity b F = (∀ (f,n) ∈ F. n ≤ b)" lemma finite_funas_term[simp,intro]: "finite (funas_term t)" by (induct t, auto) context weight_fun begin definition "weight_le s t ≡ (vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t) ∧ weight s ≤ weight t)" definition "weight_less s t ≡ (vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t) ∧ weight s < weight t)" lemma weight_le_less_iff: "weight_le s t ⟹ weight_less s t ⟷ weight s < weight t" by (auto simp: weight_le_def weight_less_def) lemma weight_less_iff: "weight_less s t ⟹ weight_le s t ∧ weight s < weight t" by (auto simp: weight_le_def weight_less_def) abbreviation "weight_NS ≡ {(t,s). weight_le s t}" abbreviation "weight_S ≡ {(t,s). weight_less s t}" lemma weight_le_mono_one: assumes S: "weight_le s t" shows "weight_le (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))" (is "weight_le ?s ?t") proof - from S have w: "weight s ≤ weight t" and v: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)" by (auto simp: weight_le_def) have v': "vars_term_ms (SCF ?s) ⊆# vars_term_ms (SCF ?t)" using mset_replicate_mono[OF v] by simp have w': "weight ?s ≤ weight ?t" using sum_list_replicate_mono[OF w] by simp from v' w' show ?thesis by (auto simp: weight_le_def) qed lemma weight_le_ctxt: "weight_le s t ⟹ weight_le (C⟨s⟩) (C⟨t⟩)" by (induct C, auto intro: weight_le_mono_one) lemma SCF_stable: assumes "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)" shows "vars_term_ms (SCF (s ⋅ σ)) ⊆# vars_term_ms (SCF (t ⋅ σ))" unfolding scf_term_subst using vars_term_ms_subst_mono[OF assms]. lemma SN_weight_S: "SN weight_S" proof- from wf_inv_image[OF wf_less] have wf: "wf {(s,t). weight s < weight t}" by (auto simp: inv_image_def) show ?thesis by (unfold SN_iff_wf, rule wf_subset[OF wf], auto simp: weight_less_def) qed lemma weight_less_imp_le: "weight_less s t ⟹ weight_le s t" by (simp add: weight_less_def weight_le_def) lemma weight_le_Var_Var: "weight_le (Var x) (Var y) ⟷ x = y" by (auto simp: weight_le_def) end context kbo begin lemma kbo_altdef: "kbo s t = (if weight_le t s then if weight_less t s then (True, True) else (case s of Var y ⇒ (False, (case t of Var x ⇒ x = y | Fun g ts ⇒ ts = [] ∧ least g)) | Fun f ss ⇒ (case t of Var x ⇒ (True, True) | Fun g ts ⇒ if pr_strict (f, length ss) (g, length ts) then (True, True) else if pr_weak (f, length ss) (g, length ts) then lex_ext_unbounded kbo ss ts else (False, False))) else (False, False))" by (simp add: weight_le_less_iff weight_le_def) end context admissible_kbo begin lemma weight_le_stable: assumes "weight_le s t" shows "weight_le (s ⋅ σ) (t ⋅ σ)" using assms weight_stable_le SCF_stable by (auto simp: weight_le_def) lemma weight_less_stable: assumes "weight_less s t" shows "weight_less (s ⋅ σ) (t ⋅ σ)" using assms weight_stable_lt SCF_stable by (auto simp: weight_less_def) lemma simple_arg_pos_weight: "simple_arg_pos weight_NS (f,n) i" unfolding simple_arg_pos_def proof (intro allI impI, unfold snd_conv fst_conv) fix ts :: "('f,'a)term list" assume i: "i < n" and len: "length ts = n" from id_take_nth_drop[OF i[folded len]] i[folded len] obtain us vs where id: "Fun f ts = Fun f (us @ ts ! i # vs)" and us: "us = take i ts" and len: "length us = i" by auto have "length us < Suc (length us + length vs)" by auto from scf[OF this, of f] obtain j where [simp]: "scf (f, Suc (length us + length vs)) (length us) = Suc j" by (rule lessE) show "(Fun f ts, ts ! i) ∈ weight_NS" unfolding weight_le_def id by (auto simp: o_def) qed lemma weight_lemmas: shows "refl weight_NS" and "trans weight_NS" and "trans weight_S" and "weight_NS O weight_S ⊆ weight_S" and "weight_S O weight_NS ⊆ weight_S" by (auto intro!: refl_onI transI simp: weight_le_def weight_less_def) interpretation kbo': admissible_kbo w w0 pr_strict' pr_weak' least scf by (rule admissible_kbo') context assumes least_global: "⋀ f g. least f ⟹ pr_weak g (f,0)" and least_trans: "⋀ f g. least f ⟹ pr_weak (f,0) g ⟹ least (fst g) ∧ snd g = 0" fixes n :: nat begin lemma kbo_instance_of_wpo_with_assms: "wpo_with_assms weight_S weight_NS (λf g. (pr_strict f g, pr_weak f g)) (λ(f, n). n = 0 ∧ least f) full_status False (λf. False)" apply (unfold_locales) apply (auto simp: weight_lemmas SN_weight_S pr_SN pr_strict_irrefl weight_less_stable weight_le_stable weight_le_mono_one weight_less_imp_le simple_arg_pos_weight) apply (force dest: least_global least_trans simp: pr_strict)+ using SN_on_irrefl[OF SN_weight_S] apply (auto simp: pr_strict least irrefl_def dest:pr_weak_trans) done interpretation wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = "λf g. (pr_strict f g, pr_weak f g)" and prl = "λ(f,n). n = 0 ∧ least f" and c = "λ_. Lex" and ssimple = False and large = "λf. False" and σσ = full_status and n = n by (rule kbo_instance_of_wpo_with_assms) lemma kbo_as_wpo_with_assms: assumes "bounded_arity n (funas_term t)" shows "kbo s t = wpo.wpo s t" proof - define m where "m = size s + size t" from m_def assms show ?thesis proof (induct m arbitrary: s t rule: less_induct) case (less m s t) hence IH: "size si + size ti < size s + size t ⟹ bounded_arity n (funas_term ti) ⟹ kbo si ti = wpo.wpo si ti" for si ti :: "('f,'a)term" by auto note wpo_sI = arg_cong[OF wpo.wpo.simps, of fst, THEN iffD2] note wpo_nsI = arg_cong[OF wpo.wpo.simps, of snd, THEN iffD2] note bounded = less(3) show ?case proof (cases s) case s: (Var x) have "¬ weight_less t (Var x)" by (metis leD weight.simps(1) weight_le_less_iff weight_less_imp_le weight_w0) thus ?thesis by (cases t, auto simp add: s kbo_altdef wpo.wpo.simps) next case s: (Fun f ss) show ?thesis proof (cases t) case t: (Var y) { assume "weight_le t s" then have "∃s' ∈ set ss. weight_le t s'" apply (auto simp: s t weight_le_def) by (metis scf set_scf_list weight_w0) then obtain s' where s': "s' ∈ set ss" and "weight_le t s'" by auto from this(2) have "wpo.wpo_ns s' t" proof (induct s') case (Var x) then show ?case by (auto intro!:wpo_nsI simp: t weight_le_Var_Var) next case (Fun f' ss') from this(2) have "∃s'' ∈ set ss'. weight_le t s''" apply (auto simp: t weight_le_def) by (metis scf set_scf_list weight_w0) then obtain s'' where "s'' ∈ set ss'" and "weight_le t s''" by auto with Fun(1)[OF this] Fun(2) show ?case by (auto intro!: wpo_nsI simp: t in_set_conv_nth) qed with s' have "∃s' ∈ set ss. wpo.wpo_ns s' t" by auto } then show ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t] by (auto simp add: s t weight_less_iff set_conv_nth, auto) next case t: (Fun g ts) { fix j assume "j < length ts" hence "ts ! j ∈ set ts" by auto hence "funas_term (ts ! j) ⊆ funas_term t" unfolding t by auto with bounded have "bounded_arity n (funas_term (ts ! j))" unfolding bounded_arity_def by auto } note bounded_tj = this note IH_tj = IH[OF _ this] show ?thesis proof (cases "¬ weight_le t s ∨ weight_less t s") case True thus ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t] unfolding s t by (auto simp: weight_less_iff) next case False let ?f = "(f,length ss)" let ?g = "(g,length ts)" from False have wle: "weight_le t s = True" "weight_less t s = False" "(s, t) ∈ weight_NS ⟷ True" "(s, t) ∈ weight_S ⟷ False" by auto have lex: "(Lex = Lex ∧ Lex = Lex) = True" by simp have sig: "set (wpo.σ ?f) = {..<length ss}" "set (wpo.σ ?g) = {..<length ts}" by auto have map: "map ((!) ss) (wpo.σ ?f) = ss" "map ((!) ts) (wpo.σ ?g) = ts" by (auto simp: map_nth) have sizes: "i < length ss ⟹ size (ss ! i) < size s" for i unfolding s by (simp add: size_simp1) have sizet: "i < length ts ⟹ size (ts ! i) < size t" for i unfolding t by (simp add: size_simp1) have wpo: "wpo.wpo s t = (if ∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t then (True, True) else if pr_weak ?f ?g ∧ (∀j∈{..<length ts}. wpo.wpo_s s (ts ! j)) then if pr_strict ?f ?g then (True, True) else lex_ext wpo.wpo n ss ts else (False, False))" unfolding wpo.wpo.simps[of s t] unfolding s t term.simps split Let_def lex if_True sig map unfolding s[symmetric] t[symmetric] wle if_True weight_less_iff if_False False snd_conv by auto have "kbo s t = (if pr_strict ?f ?g then (True, True) else if pr_weak ?f ?g then lex_ext_unbounded kbo ss ts else (False, False))" unfolding kbo_altdef[of s t] unfolding s t term.simps split Let_def if_True unfolding s[symmetric] t[symmetric] wle if_True weight_less_iff if_False by auto also have "lex_ext_unbounded kbo ss ts = lex_ext kbo n ss ts" using bounded[unfolded t] unfolding bounded_arity_def lex_ext_def by auto also have "… = lex_ext wpo.wpo n ss ts" by (rule lex_ext_cong[OF refl refl refl], rule IH_tj, auto dest!: sizes sizet) finally have kbo: "kbo s t = (if pr_strict ?f ?g then (True, True) else if pr_weak ?f ?g then lex_ext wpo.wpo n ss ts else (False, False))" . show ?thesis proof (cases "∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t") case True then obtain i where i: "i < length ss" and "wpo.wpo_ns (ss ! i) t" by auto then obtain b where "wpo.wpo (ss ! i) t = (b, True)" by (cases "wpo.wpo (ss ! i) t", auto) also have "wpo.wpo (ss ! i) t = kbo (ss ! i) t" using i by (intro IH[symmetric, OF _ bounded], auto dest: sizes) finally have "NS (ss ! i) t" by simp from kbo_supt_one[OF this] have "S (Fun f (take i ss @ ss ! i # drop (Suc i) ss)) t" . also have "(take i ss @ ss ! i # drop (Suc i) ss) = ss" using i by (metis id_take_nth_drop) also have "Fun f ss = s" unfolding s by simp finally have "S s t" . with S_imp_NS[OF this] have "kbo s t = (True,True)" by (cases "kbo s t", auto) with True show ?thesis unfolding wpo by auto next case False hence False: "(∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t) = False" by simp { fix j assume NS: "NS s t" assume j: "j < length ts" (* here we make use of proven properties of KBO: subterm-property and transitivity, perhaps there is a simple proof without already using these properties *) from kbo_supt_one[OF NS_refl, of g "take j ts" "ts ! j" "drop (Suc j) ts"] have S: "S t (ts ! j)" using id_take_nth_drop[OF j] unfolding t by auto from kbo_trans[of s t "ts ! j"] NS S have "S s (ts ! j)" by auto with S S_imp_NS[OF this] have "kbo s (ts ! j) = (True, True)" by (cases "kbo s (ts ! j)", auto) hence "wpo.wpo_s s (ts ! j)" by (subst IH_tj[symmetric], insert sizet[OF j] j, auto) } thus ?thesis unfolding wpo kbo False if_False using lex_ext_stri_imp_nstri[of wpo.wpo n ss ts] by (cases "lex_ext wpo.wpo n ss ts", auto simp: pr_strict split: if_splits) qed qed qed qed qed qed end text ‹This is the main theorem. It tells us that KBO can be seen as an instance of WPO, under mild preconditions: the parameter $n$ for the lexicographic extension has to be chosen high enough to cover the arities of all terms that should be compared.› lemma defines "prec ≡ ((λf g. (pr_strict' f g, pr_weak' f g)))" and "prl ≡ (λ(f, n). n = 0 ∧ least f)" shows kbo_encoding_is_valid_wpo: "wpo_with_assms weight_S weight_NS prec prl full_status False (λf. False)" and kbo_as_wpo: "bounded_arity n (funas_term t) ⟹ kbo s t = wpo.wpo n weight_S weight_NS prec prl full_status (λ_. Lex) False (λf. False) s t" unfolding prec_def prl_def subgoal by (intro admissible_kbo.kbo_instance_of_wpo_with_assms[OF admissible_kbo'] least_pr_weak' least_pr_weak'_trans) apply (subst kbo'_eq_kbo[symmetric]) apply (subst admissible_kbo.kbo_as_wpo_with_assms[OF admissible_kbo' least_pr_weak' least_pr_weak'_trans, symmetric], (auto)[3]) by auto text ‹As a proof-of-concept we show that now properties of WPO can be used to prove these properties for KBO. Here, as example we consider closure under substitutions and strong normalization, but the following idea can be applied for several more properties: if the property involves only terms where the arities are bounded, then just choose the parameter $n$ large enough. This even works for strong normalization, since in an infinite chain of KBO-decreases $t_1 > t_2 > t_3 > ...$ all terms have a weight of at most the weight of $t_1$, and this weight is also a bound on the arities.› lemma KBO_stable_via_WPO: "S s t ⟹ S (s ⋅ (σ :: ('f,'a) subst)) (t ⋅ σ)" proof - let ?terms = "{t, t ⋅ σ}" (* collect all rhss of comparisons *) let ?prec = "((λf g. (pr_strict' f g, pr_weak' f g)))" let ?prl = "(λ(f, n). n = 0 ∧ least f)" have "finite (⋃ (funas_term ` ?terms))" by auto from finite_list[OF this] obtain F where F: "set F = ⋃ (funas_term ` ?terms)" by auto (* since there only finitely many symbols, we can take n as the maximal arity *) define n where "n = max_list (map snd F)" (* now get a WPO for this choice of n *) interpret wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = ?prec and prl = ?prl and c = "λ_. Lex" and ssimple = False and large = "λf. False" and σσ = full_status and n = n by (rule kbo_encoding_is_valid_wpo) { fix t assume "t ∈ ?terms" hence "funas_term t ⊆ set F" unfolding F by auto hence "bounded_arity n (funas_term t)" unfolding bounded_arity_def using max_list[of _ "map snd F", folded n_def] by fastforce } (* for all the terms we have that KBO = WPO *) note kbo_as_wpo = kbo_as_wpo[OF this] (* and finally transfer the existing property of WPO to KBO *) from wpo.WPO_S_subst[of s t σ] show "S s t ⟹ S (s ⋅ σ) (t ⋅ σ)" using kbo_as_wpo by auto qed lemma weight_is_arity_bound: "weight t ≤ b ⟹ bounded_arity b (funas_term t)" proof (induct t) case (Fun f ts) have "sum_list (map weight ts) ≤ weight (Fun f ts)" using sum_list_scf_list[of ts "scf (f,length ts)", OF scf] by auto also have "… ≤ b" using Fun by auto finally have sum_b: "sum_list (map weight ts) ≤ b" . { fix t assume t: "t ∈ set ts" from split_list[OF this] have "weight t ≤ sum_list (map weight ts)" by auto with sum_b have "bounded_arity b (funas_term t)" using t Fun by auto } note IH = this have "length ts = sum_list (map (λ _. 1) ts)" by (induct ts, auto) also have "… ≤ sum_list (map weight ts)" apply (rule sum_list_mono) subgoal for t using weight_gt_0[of t] by auto done also have "… ≤ b" by fact finally have len: "length ts ≤ b" by auto from IH len show ?case unfolding bounded_arity_def by auto qed (auto simp: bounded_arity_def) lemma KBO_SN_via_WPO: "SN {(s,t). S s t}" proof fix f :: "nat ⇒ ('f,'a)term" assume "∀i. (f i, f (Suc i)) ∈ {(s, t). S s t}" hence steps: "S (f i) (f (Suc i))" for i by auto define n where "n = weight (f 0)" have w_bound: "weight (f i) ≤ n" for i proof (induct i) case (Suc i) from steps[of i] have "weight (f (Suc i)) ≤ weight (f i)" unfolding kbo.simps[of "f i"] by (auto split: if_splits) with Suc show ?case by simp qed (auto simp: n_def) let ?prec = "((λf g. (pr_strict' f g, pr_weak' f g)))" let ?prl = "(λ(f, n). n = 0 ∧ least f)" (* now get a WPO for this choice of n *) interpret wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = ?prec and prl = ?prl and c = "λ_. Lex" and ssimple = False and large = "λf. False" and σσ = full_status and n = n by (rule kbo_encoding_is_valid_wpo) have "kbo (f i) (f (Suc i)) = wpo.wpo (f i) (f (Suc i))" for i by (rule kbo_as_wpo[OF weight_is_arity_bound[OF w_bound]]) (* for all the terms in the infinite sequence f 0, f 1, ... we have that KBO = WPO *) (* and finally derive contradiction to SN-property of WPO *) from steps[unfolded this] wpo.WPO_S_SN show False by auto qed end end