theory KBO_More imports KBO QTRS.Term_Order "../Termination_and_Complexity/Simple_Termination" begin text ‹Incrementality of KBO w.r.t. precedence.› locale two_kbos = kbo1: kbo w w0 scf least1 S1 W1 + kbo2: kbo w w0 scf least2 S2 W2 for w w0 scf and least1 :: "'f ⇒ bool" and S1 W1 least2 S2 W2 begin lemma kbo_prec_mono: assumes least_imp: "⋀f::'f. least1 f ⟹ least2 f" and S_imp: "⋀fn gm. S1 fn gm ⟹ S2 fn gm" and W_imp: "⋀fn gm. W1 fn gm ⟹ W2 fn gm" shows "(kbo1.S s t ⟶ kbo2.S s t) ∧ (kbo1.NS s t ⟶ kbo2.NS s t)" (is "(?S s t ⟶ ?S' s t) ∧ (?N s t ⟶ ?N' s t)") proof (induct rule: kbo1.kbo.induct) case (1 s t) note simps = kbo1.kbo.simps kbo2.kbo.simps note [simp del] = simps note lex_mono = lex_ext_unbounded_mono[of _ _ "kbo1.kbo" "kbo2.kbo"] note lex_mono1 = lex_mono[THEN conjunct1, rule_format] note lex_mono2 = lex_mono[THEN conjunct2, rule_format] show ?case unfolding simps[of s t] using 1 by (auto split: term.splits simp: least_imp S_imp W_imp intro!: lex_mono1 lex_mono2) qed end context admissible_kbo begin section ‹use KBO as ce-compatible reduction pair / triple› abbreviation kbo_S where "kbo_S ≡ {(s,t). S s t}" abbreviation kbo_NS where "kbo_NS ≡ {(s,t). NS s t}" lemma kbo_NS_supteq: "s ⊵ t ⟹ (s,t) ∈ kbo_NS" using NS_supteq by blast lemma kbo_ce_compat: "ce_trs cn ⊆ kbo_S ∩ kbo_NS" proof - obtain c n where cn: "cn = (c,n)" by force { fix s t assume "(s,t) ∈ ce_trs cn" hence "s ⊳ t" unfolding cn ce_trs.simps by auto from S_supt[OF this] have "(s,t) ∈ kbo_S" by simp with S_imp_NS[of s t] have "(s,t) ∈ kbo_S ∩ kbo_NS" by auto } thus ?thesis by auto qed lemma S_ce_compat: "ce_trs cn ⊆ kbo_S" using kbo_ce_compat by blast lemma NS_ce_compat: "ce_trs cn ⊆ kbo_NS" using kbo_ce_compat by blast lemma kbo_redpair: "mono_ce_af_redtriple_order kbo_S kbo_NS kbo_NS full_af" proof (unfold_locales) show "SN kbo_S" using kbo_strongly_normalizing unfolding SN_defs by blast show "subst.closed kbo_S" using S_subst by auto show "subst.closed kbo_NS" using NS_subst by auto show "ctxt.closed kbo_NS" by (rule, insert NS_ctxt, blast) show "kbo_S O kbo_NS ⊆ kbo_S" using S_NS_compat by auto show "kbo_NS O kbo_S ⊆ kbo_S" using NS_S_compat by auto show "trans kbo_S" using S_trans unfolding trans_def by auto show "trans kbo_NS" using NS_trans unfolding trans_def by auto show "refl kbo_NS" using NS_refl unfolding refl_on_def by auto show "af_compatible full_af kbo_NS" by (rule full_af) show "∃ n. ∀ m ≥ n. ∀ c. ce_trs (c,m) ⊆ kbo_NS" using NS_ce_compat by blast show "∃ n. ∀ m ≥ n. ∀ c . ce_trs (c,m) ⊆ kbo_S" using S_ce_compat by blast show "kbo_S ⊆ kbo_NS" using S_imp_NS by blast qed lemma kbo_S_mono: "ctxt.closed kbo_S" by (rule, insert S_ctxt, blast) section ‹Strong Normalization via Kruskal› lemma pr_strict_reflclp_imp_pr_weak: assumes "pr_strict⇧=⇧= x y" shows "pr_weak x y" using assms by (auto simp: pr_strict) lemma pr_strict_trans: "pr_strict fn gm ⟹ pr_strict gm hk ⟹ pr_strict fn hk" using pr_weak_trans unfolding pr_strict by blast lemma transp_on_pr_strict: "transp_on pr_strict UNIV" using pr_strict_trans unfolding transp_on_def by blast lemma irreflp_on_pr_strict: "irreflp_on pr_strict UNIV" using pr_strict_irrefl unfolding irreflp_on_def by blast lemma po_on_pr_strict: "po_on pr_strict¯¯ UNIV" proof show "irreflp_on pr_strict¯¯ UNIV" by (simp) (rule irreflp_on_pr_strict) next show "transp_on pr_strict¯¯ UNIV" by (simp) (rule transp_on_pr_strict) qed lemma wfp_on_pr_strict: "wfp_on pr_strict¯¯ (UNIV::('f × nat) set)" using pr_SN unfolding wfp_on_SN_conv by auto definition "scfs fn = map (scf fn) [0 ..< snd fn]" lemma weight_list_conv: "sum_list (map (λ(t⇩i, i). weight t⇩i * scf (f, n) i) (zip ts [0 ..< n])) = sum_list (map (λ(t⇩i, c⇩i). weight t⇩i * c⇩i) (zip ts (scfs (f, n))))" by (auto simp: scfs_def zip_map2 o_def intro: arg_cong) lemma S_subterm_one: assumes "t ∈ set ts" shows "S (Fun f ts) t" proof - from ‹t ∈ set ts› have "Fun f ts ⊳ t" by auto with S_supt show ?thesis by blast qed text ‹Lemmas for \emph{simple weights} (i.e., without subterm coefficient functions).› context assumes scf_1: "i < n ⟹ scf (f, n) i = 1" begin lemma weight_simp' [simp]: "weight (Fun f ts) = w (f, length ts) + (∑t←ts. weight t)" proof - def n ≡ "length ts" have *: "zip (map weight ts) (map (scf (f, n)) [0..<n]) = map (λt. (weight t, 1)) ts" (is "?xs = ?ys") proof (rule nth_equalityI) show length_eq: "length ?xs = length ?ys" by (simp add: n_def) show "∀i<length ?xs. ?xs ! i = ?ys ! i" proof (intro allI impI) fix i assume "i < length ?xs" then have *: "i < length (map weight ts)" "i < length (map (scf (f, n)) [0..<n])" and "i < n" by auto then have len': "i < length [0..<n]" by (simp add: nth_def) from ‹i < n› have ith: "[0..<n] ! i = i" by simp have map_ith: "map (scf (f, n)) [0..<n] ! i = 1" using scf_1 [OF ‹i < n›] by (simp add: ith nth_map [OF len']) show "?xs ! i = ?ys ! i" unfolding nth_zip [OF *] map_ith using ‹i < n› unfolding n_def by simp qed qed have "(∑(ti, i)←zip ts [0..<n]. weight ti * scf (f, n) i) = (∑tii←zip ts [0..<n]. weight (fst tii) * scf (f, n) (snd tii))" unfolding split_def .. also have "… = (∑wic←zip (map weight ts) (map (scf (f, n)) [0..<n]). fst wic * snd wic)" by (simp add: zip_map_map split_def o_def) also have "… = (∑wic←map (λt. (weight t, 1)) ts. fst wic * snd wic)" unfolding * .. also have "… = (∑wic←map (λt. (weight t, 1::nat)) ts. fst wic * 1)" by (induct ts) auto also have "… = (∑t←ts. weight t)" by (induct ts) auto finally show ?thesis unfolding weight.simps by (simp add: n_def) qed lemma subseq_weight: assumes "subseq ss ts" shows "(∑s←ss. weight s) ≤ (∑t←ts. weight t)" using assms by (induct) simp+ lemma concat_map_singleton: assumes "⋀x. x ∈ set xs ⟹ f x = [g x]" shows "concat (map f xs) = map g xs" using assms by (induct xs) simp_all lemma wqo_on_map': fixes P and Q and h defines "P' ≡ λx y. P x y ∧ Q (h x) (h y)" assumes "wqo_on P⇧=⇧= A" and "wqo_on Q B" and subset: "h ` A ⊆ B" shows "wqo_on P'⇧=⇧= A" proof let ?Q = "λx y. Q (h x) (h y)" from ‹wqo_on P⇧=⇧= A› have "transp_on P⇧=⇧= A" by (rule wqo_on_imp_transp_on) then show "transp_on P'⇧=⇧= A" using ‹wqo_on Q B› and subset unfolding wqo_on_def transp_on_def P'_def by blast from ‹wqo_on P⇧=⇧= A› have "almost_full_on P⇧=⇧= A" by (rule wqo_on_imp_almost_full_on) from ‹wqo_on Q B› have "almost_full_on Q B" by (rule wqo_on_imp_almost_full_on) show "almost_full_on P'⇧=⇧= A" proof fix f assume *: "∀i::nat. f i ∈ A" from almost_full_on_imp_homogeneous_subseq [OF ‹almost_full_on P⇧=⇧= A› this] obtain g :: "nat ⇒ nat" where g: "⋀i j. i < j ⟹ g i < g j" and **: "∀i. f (g i) ∈ A ∧ P⇧=⇧= (f (g i)) (f (g (Suc i)))" using * by auto from chain_transp_on_less [OF ** ‹transp_on P⇧=⇧= A›] have **: "⋀i j. i < j ⟹ P⇧=⇧= (f (g i)) (f (g j))" . let ?g = "λi. h (f (g i))" from * and subset have B: "⋀i. ?g i ∈ B" by auto with ‹almost_full_on Q B› [unfolded almost_full_on_def good_def, THEN bspec, of ?g] obtain i j :: nat where "i < j" and "Q (?g i) (?g j)" by blast with ** [OF ‹i < j›] have "P'⇧=⇧= (f (g i)) (f (g j))" by (auto simp: P'_def) with g [OF ‹i < j›] show "good P'⇧=⇧= f" by (auto simp: good_def) qed qed lemma scf_list_id [simp]: "scf_list (scf (f, length ss)) ss = ss" proof - let ?scf = "scf (f, length ss)" have [simp]: "⋀i x. i < length ss ⟹ replicate (?scf i) x = [x]" using scf_1 [of _ "length ss" f] by simp have "concat (map (λ(x, i). replicate (?scf i) x) (zip ss [0 ..< length ss])) = map fst (zip ss [0 ..< length ss])" by (rule concat_map_singleton) (auto simp: in_set_zip) also have "… = ss" by (auto) finally show ?thesis by (simp add: scf_list_def) qed lemma SCF_id [simp]: "SCF = (λx. x)" proof fix t :: "('f, 'v) term" show "SCF t = t" by (induct t) (auto simp: map_idI) qed lemma subseq_vars_term_ms: assumes "subseq ts ss" shows "vars_term_ms (SCF (Fun g ts)) ⊆# vars_term_ms (SCF (Fun f ss))" using assms proof (induct) case (list_emb_Cons xs ys y) obtain m1 m2 where id: "⋃#image_mset vars_term_ms (mset xs) = m1" "⋃#image_mset vars_term_ms (mset ys) = m2" by auto from list_emb_Cons have IH: "m1 ⊆# m2" by (auto simp: id) also have "… ⊆# vars_term_ms y + m2" by (rule mset_subset_eq_add_right) finally show ?case by (simp add: id) qed auto text ‹ Without subterm coefficient functions, @{term S} is a simplification-order. › lemma simplification_order: assumes "wqo_on pr_strict¯¯⇧=⇧= UNIV" shows "simplification_order {(x :: ('f, 'v) term, y). S x y}" (is "simplification_order ?kbo") proof (unfold simplification_order_def) let ?P = "λx y. pr_strict x y ∧ w x ≥ w y" have "range w ⊆ UNIV" by auto from wqo_on_map' [OF assms wqo_on_UNIV_nat this] have "wqo_on ?P¯¯⇧=⇧= UNIV" by (auto simp: conversep_iff [abs_def]) moreover have "emb UNIV ?P ⊆ ?kbo" proof (rule emb_subsetI) show "⋀s t u. (s, t) ∈ ?kbo ⟹ (t, u) ∈ ?kbo ⟹ (s, u) ∈ ?kbo" and "⋀C s t. (s, t) ∈ ?kbo ⟹ (C⟨s⟩, C⟨t⟩) ∈ ?kbo" and "⋀σ s t. (s, t) ∈ ?kbo ⟹ (s ⋅ σ, t ⋅ σ) ∈ ?kbo" by (auto simp del: kbo.simps dest: S_trans S_ctxt S_subst) next fix t f and ts :: "('f, 'v) term list" assume "t ∈ set ts" from S_subterm_one [OF this] show "(Fun f ts, t) ∈ ?kbo" by simp next fix f g and ss ts :: "('f, 'v) term list" presume strict: "pr_strict (f, length ss) (g, length ts)" and w: "w (f, length ss) ≥ w (g, length ts)" and "subseq ts ss" have "vars_term_ms (SCF (Fun g ts)) ⊆# vars_term_ms (SCF (Fun f ss))" by (rule subseq_vars_term_ms) fact moreover have "weight (Fun f ss) ≥ weight (Fun g ts)" using subseq_weight [OF ‹subseq ts ss›] and w unfolding weight_simp' by simp ultimately show "(Fun f ss, Fun g ts) ∈ ?kbo" using strict by (simp add: kbo.simps) qed simp_all moreover have "rewrite_order ?kbo" by (auto simp del: kbo.simps simp: rewrite_order_def rewrite_relation_def irrefl_def S_irrefl trans_def dest: S_ctxt S_subst S_trans) ultimately show "rewrite_order ?kbo ∧ (∃Q. wqo_on Q¯¯⇧=⇧= UNIV ∧ emb UNIV Q ⊆ ?kbo)" by blast qed text ‹ Alternative termination proof for the case that @{term "pr_strict¯¯⇧=⇧="} is a well-quasi-order. › lemma assumes "wqo_on pr_strict¯¯⇧=⇧= UNIV" shows "SN {(x :: ('f, 'v) term, y). S x y}" by (rule simplification_order_imp_SN [OF simplification_order [OF assms]]) declare weight_simp' [simp del] end end end