Theory Lambda_Free_KBO_Util
section ‹Utilities for Knuth--Bendix Orders for Lambda-Free Higher-Order Terms›
theory Lambda_Free_KBO_Util
imports Lambda_Free_RPOs.Lambda_Free_Term Lambda_Free_RPOs.Extension_Orders Polynomials.Polynomials
begin
locale kbo_basic_basis = gt_sym "(>⇩s)"
for gt_sym :: "'s ⇒ 's ⇒ bool" (infix ">⇩s" 50) +
fixes
wt_sym :: "'s ⇒ nat" and
ε :: nat and
ground_heads_var :: "'v ⇒ 's set" and
extf :: "'s ⇒ (('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm list ⇒ ('s, 'v) tm list ⇒
bool"
assumes
ε_gt_0: "ε > 0" and
wt_sym_ge_ε: "wt_sym f ≥ ε" and
ground_heads_var_nonempty: "ground_heads_var x ≠ {}" and
extf_ext_irrefl_before_trans: "ext_irrefl_before_trans (extf f)" and
extf_ext_compat_list_strong: "ext_compat_list_strong (extf f)" and
extf_ext_hd_or_tl: "ext_hd_or_tl (extf f)"
begin
lemma wt_sym_gt_0: "wt_sym f > 0"
by (rule less_le_trans[OF ε_gt_0 wt_sym_ge_ε])
end
locale kbo_std_basis = ground_heads "(>⇩s)" arity_sym arity_var
for
gt_sym :: "'s ⇒ 's ⇒ bool" (infix ">⇩s" 50) and
arity_sym :: "'s ⇒ enat" and
arity_var :: "'v ⇒ enat" +
fixes
wt_sym :: "'s ⇒ 'n::{ord,semiring_1}" and
ε :: nat and
δ :: nat and
extf :: "'s ⇒ (('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm list ⇒ ('s, 'v) tm list ⇒
bool"
assumes
ε_gt_0: "ε > 0" and
δ_le_ε: "δ ≤ ε" and
arity_hd_ne_infinity_if_δ_gt_0: "δ > 0 ⟹ arity_hd ζ ≠ ∞" and
wt_sym_ge: "wt_sym f ≥ of_nat (ε - the_enat (of_nat δ * arity_sym f))" and
unary_wt_sym_0_gt: "arity_sym f = 1 ⟹ wt_sym f = 0 ⟹ f >⇩s g ∨ g = f" and
unary_wt_sym_0_imp_δ_eq_ε: "arity_sym f = 1 ⟹ wt_sym f = 0 ⟹ δ = ε" and
extf_ext_irrefl_before_trans: "ext_irrefl_before_trans (extf f)" and
extf_ext_compat_list_strong: "ext_compat_list_strong (extf f)" and
extf_ext_hd_or_tl: "ext_hd_or_tl (extf f)" and
extf_ext_snoc_if_δ_eq_ε: "δ = ε ⟹ ext_snoc (extf f)"
begin
lemma arity_sym_ne_infinity_if_δ_gt_0: "δ > 0 ⟹ arity_sym f ≠ ∞"
by (metis arity_hd.simps(2) arity_hd_ne_infinity_if_δ_gt_0)
lemma arity_var_ne_infinity_if_δ_gt_0: "δ > 0 ⟹ arity_var x ≠ ∞"
by (metis arity_hd.simps(1) arity_hd_ne_infinity_if_δ_gt_0)
lemma arity_ne_infinity_if_δ_gt_0: "δ > 0 ⟹ arity s ≠ ∞"
unfolding arity_def
by (induct s rule: tm_induct_apps)
(metis arity_hd_ne_infinity_if_δ_gt_0 enat.distinct(2) enat.exhaust idiff_enat_enat)
lemma extf_ext_irrefl: "ext_irrefl (extf f)"
by (rule ext_irrefl_before_trans.axioms(1)[OF extf_ext_irrefl_before_trans])
lemma extf_ext: "ext (extf f)"
by (rule ext_irrefl.axioms(1)[OF extf_ext_irrefl])
lemma
extf_ext_compat_cons: "ext_compat_cons (extf f)" and
extf_ext_compat_snoc: "ext_compat_snoc (extf f)" and
extf_ext_singleton: "ext_singleton (extf f)"
by (rule ext_compat_list_strong.axioms[OF extf_ext_compat_list_strong])+
lemma extf_ext_compat_list: "ext_compat_list (extf f)"
using extf_ext_compat_list_strong
by (simp add: ext_compat_list_axioms_def ext_compat_list_def ext_compat_list_strong.compat_list
ext_compat_list_strong_def ext_singleton.axioms(1))
lemma extf_ext_wf_bounded: "ext_wf_bounded (extf f)"
unfolding ext_wf_bounded_def using extf_ext_irrefl_before_trans extf_ext_hd_or_tl by simp
lemmas extf_mono_strong = ext.mono_strong[OF extf_ext]
lemmas extf_mono = ext.mono[OF extf_ext, mono]
lemmas extf_map = ext.map[OF extf_ext]
lemmas extf_irrefl = ext_irrefl.irrefl[OF extf_ext_irrefl]
lemmas extf_trans_from_irrefl =
ext_irrefl_before_trans.trans_from_irrefl[OF extf_ext_irrefl_before_trans]
lemmas extf_compat_cons = ext_compat_cons.compat_cons[OF extf_ext_compat_cons]
lemmas extf_compat_append_left = ext_compat_cons.compat_append_left[OF extf_ext_compat_cons]
lemmas extf_compat_append_right = ext_compat_snoc.compat_append_right[OF extf_ext_compat_snoc]
lemmas extf_compat_list = ext_compat_list.compat_list[OF extf_ext_compat_list]
lemmas extf_singleton = ext_singleton.singleton[OF extf_ext_singleton]
lemmas extf_wf_bounded = ext_wf_bounded.wf_bounded[OF extf_ext_wf_bounded]
lemmas extf_snoc_if_δ_eq_ε = ext_snoc.snoc[OF extf_ext_snoc_if_δ_eq_ε]
lemma extf_singleton_nil_if_δ_eq_ε: "δ = ε ⟹ extf f gt [s] []"
by (rule extf_snoc_if_δ_eq_ε[of _ _ "[]", simplified])
end
sublocale kbo_basic_basis < kbo_std_basis _ _ "λ_. ∞" "λ_. ∞" _ _ 0
unfolding kbo_std_basis_def kbo_std_basis_axioms_def
by (auto simp: wt_sym_gt_0 ε_gt_0 wt_sym_ge_ε less_not_refl2 ground_heads_var_nonempty
gt_sym_axioms ground_heads_def ground_heads_axioms_def extf_ext_irrefl_before_trans
extf_ext_compat_list_strong extf_ext_hd_or_tl)
end