Theory Lambda_Free_TKBO_Coefs
section ‹The Graceful Transfinite Knuth--Bendix Order with Subterm Coefficients for
Lambda-Free Higher-Order Terms›
theory Lambda_Free_TKBO_Coefs
imports Lambda_Free_KBO_Util Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal
abbrevs "=p" = "=⇩p"
and ">p" = ">⇩p"
and "≥p" = "≥⇩p"
and ">t" = ">⇩t"
and "≥t" = "≥⇩t"
and "!h" = "⇩h"
begin
text ‹
This theory defines the graceful transfinite Knuth--Bendix order (KBO) with
subterm coefficients for ‹λ›-free higher-order terms. The proof was
developed by copying that of the standard KBO and generalizing it along two
axes:\ subterm coefficients and ordinals. Both features complicate the
definitions and proofs substantially.
›
subsection ‹Setup›
locale tkbo_coefs = kbo_std_basis _ _ arity_sym arity_var wt_sym
for
arity_sym :: "'s ⇒ enat" and
arity_var :: "'v ⇒ enat" and
wt_sym :: "'s ⇒ hmultiset" +
fixes coef_sym :: "'s ⇒ nat ⇒ hmultiset"
assumes coef_sym_gt_0: "coef_sym f i > 0"
begin
abbreviation δ⇩h :: hmultiset where
"δ⇩h ≡ of_nat δ"
abbreviation ε⇩h :: hmultiset where
"ε⇩h ≡ of_nat ε"
abbreviation arity_sym⇩h :: "'s ⇒ hmultiset" where
"arity_sym⇩h f ≡ hmset_of_enat (arity_sym f)"
abbreviation arity_var⇩h :: "'v ⇒ hmultiset" where
"arity_var⇩h f ≡ hmset_of_enat (arity_var f)"
abbreviation arity_hd⇩h :: "('s, 'v) hd ⇒ hmultiset" where
"arity_hd⇩h f ≡ hmset_of_enat (arity_hd f)"
abbreviation arity⇩h :: "('s, 'v) tm ⇒ hmultiset" where
"arity⇩h s ≡ hmset_of_enat (arity s)"
lemma arity⇩h_conv: "arity⇩h s = arity_hd⇩h (head s) - of_nat (num_args s)"
unfolding arity_def by simp
lemma arity⇩h_App[simp]: "arity⇩h (App s t) = arity⇩h s - 1"
by (simp add: one_enat_def)
lemmas wary_App⇩h[intro] = wary_App[folded of_nat_lt_hmset_of_enat_iff]
lemmas wary_AppE⇩h = wary_AppE[folded of_nat_lt_hmset_of_enat_iff]
lemmas wary_num_args_le_arity_head⇩h =
wary_num_args_le_arity_head[folded of_nat_le_hmset_of_enat_iff]
lemmas wary_apps⇩h = wary_apps[folded of_nat_le_hmset_of_enat_iff]
lemmas wary_cases_apps⇩h[consumes 1, case_names apps] =
wary_cases_apps[folded of_nat_le_hmset_of_enat_iff]
lemmas ground_heads_arity⇩h = ground_heads_arity[folded hmset_of_enat_le]
lemmas some_ground_head_arity⇩h = some_ground_head_arity[folded hmset_of_enat_le]
lemmas ε⇩h_gt_0 = ε_gt_0[folded of_nat_less_hmset, unfolded of_nat_0]
lemmas δ⇩h_le_ε⇩h = δ_le_ε[folded of_nat_le_hmset]
lemmas arity_hd⇩h_lt_ω_if_δ⇩h_gt_0 = arity_hd_ne_infinity_if_δ_gt_0
[folded of_nat_less_hmset, unfolded of_nat_0, folded hmset_of_enat_lt_iff_ne_infinity]
lemma wt_sym_ge⇩h: "wt_sym f ≥ ε⇩h - δ⇩h * arity_sym⇩h f"
proof -
have "of_nat (the_enat (of_nat δ * arity_sym f)) = δ⇩h * arity_sym⇩h f"
by (cases "arity_sym f", simp add: of_nat_eq_enat,
metis arity_sym_ne_infinity_if_δ_gt_0 gr_zeroI mult_eq_0_iff of_nat_0 the_enat_0)
thus ?thesis
using wt_sym_ge[unfolded of_nat_minus_hmset] by metis
qed
lemmas unary_wt_sym_0_gt⇩h = unary_wt_sym_0_gt[folded hmset_of_enat_inject, unfolded hmset_of_enat_1]
lemmas unary_wt_sym_0_imp_δ⇩h_eq_ε⇩h = unary_wt_sym_0_imp_δ_eq_ε
[folded of_nat_inject_hmset, unfolded of_nat_0]
lemmas extf_ext_snoc_if_δ⇩h_eq_ε⇩h = extf_ext_snoc_if_δ_eq_ε[folded of_nat_inject_hmset]
lemmas extf_snoc_if_δ⇩h_eq_ε⇩h = ext_snoc.snoc[OF extf_ext_snoc_if_δ⇩h_eq_ε⇩h]
lemmas arity_sym⇩h_lt_ω_if_δ⇩h_gt_0 = arity_sym_ne_infinity_if_δ_gt_0
[folded of_nat_less_hmset hmset_of_enat_lt_iff_ne_infinity, unfolded of_nat_0]
lemmas arity_var⇩h_lt_ω_if_δ⇩h_gt_0 = arity_var_ne_infinity_if_δ_gt_0
[folded of_nat_less_hmset hmset_of_enat_lt_iff_ne_infinity, unfolded of_nat_0]
lemmas arity⇩h_lt_ω_if_δ⇩h_gt_0 = arity_ne_infinity_if_δ_gt_0
[folded of_nat_less_hmset hmset_of_enat_lt_iff_ne_infinity, unfolded of_nat_0]
lemmas warywary_subst_subst⇩h_conv = wary_subst_def[folded hmset_of_enat_le]
lemmas extf_singleton_nil_if_δ⇩h_eq_ε⇩h = extf_singleton_nil_if_δ_eq_ε[folded of_nat_inject_hmset]
lemma arity_sym⇩h_if_δ⇩h_gt_0_E:
assumes δ_gt_0: "δ⇩h > 0"
obtains n where "arity_sym⇩h f = of_nat n"
using arity_sym⇩h_lt_ω_if_δ⇩h_gt_0 assms lt_ω_imp_ex_of_nat by blast
lemma arity_var⇩h_if_δ⇩h_gt_0_E:
assumes δ_gt_0: "δ⇩h > 0"
obtains n where "arity_var⇩h f = of_nat n"
using arity_var⇩h_lt_ω_if_δ⇩h_gt_0 assms lt_ω_imp_ex_of_nat by blast
subsection ‹Weights and Subterm Coefficients›
abbreviation zhmset_of_tpoly :: "('a, hmultiset) tpoly ⇒ ('a, zhmultiset) tpoly" where
"zhmset_of_tpoly ≡ map_tpoly (λx. x) zhmset_of"
abbreviation eval_ztpoly :: "('a ⇒ zhmultiset) ⇒ ('a, hmultiset) tpoly ⇒ zhmultiset" where
"eval_ztpoly A p ≡ eval_tpoly A (zhmset_of_tpoly p)"
lemma eval_tpoly_eq_eval_ztpoly[simp]:
"zhmset_of (eval_tpoly A p) = eval_ztpoly (λv. zhmset_of (A v)) p"
by (induct p, simp_all add: zhmset_of_sum_list zhmset_of_prod_list o_def,
simp_all cong: map_cong)
definition min_ground_head :: "('s, 'v) hd ⇒ 's" where
"min_ground_head ζ =
(SOME f. f ∈ ground_heads ζ ∧
(∀g ∈ ground_heads ζ. wt_sym g + δ⇩h * arity_sym⇩h g ≥ wt_sym f + δ⇩h * arity_sym⇩h f))"