Theory Lambda_Free_KBO_App

(*  Title:       The Applicative Knuth-Bendix Order for Lambda-Free Higher-Order Terms
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

section ‹The Applicative Knuth--Bendix Order for Lambda-Free Higher-Order Terms›

theory Lambda_Free_KBO_App
imports Lambda_Free_KBO_Util
abbrevs ">t" = ">⇩t"
  and "≥t" = "≥⇩t"
begin

text ‹
This theory defines the applicative Knuth--Bendix order, a variant of KBO for ‹λ›-free
higher-order terms. It corresponds to the order obtained by applying the standard first-order KBO on
the applicative encoding of higher-order terms and assigning the lowest precedence to the
application symbol.
›

locale kbo_app = gt_sym "(>⇩s)"
    for gt_sym :: "'s ⇒ 's ⇒ bool" (infix ‹>⇩s› 50) +
  fixes
    wt_sym :: "'s ⇒ nat" and
    ε :: nat and
    ext :: "(('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
    ext_ext_irrefl_before_trans: "ext_irrefl_before_trans ext" and
    ext_ext_compat_list: "ext_compat_list ext" and
    ext_ext_hd_or_tl: "ext_hd_or_tl ext"
begin

lemma ext_mono[mono]: "gt ≤ gt' ⟹ ext gt ≤ ext gt'"
  by (simp add: ext.mono ext_ext_compat_list[unfolded ext_compat_list_def, THEN conjunct1])

fun wt :: "('s, 'v) tm ⇒ nat" where
  "wt (Hd (Var x)) = ε"
| "wt (Hd (Sym f)) = wt_sym f"
| "wt (App s t) = wt s + wt t"

inductive gt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>⇩t› 50) where
  gt_wt: "vars_mset t ⊇# vars_mset s ⟹ wt t > wt s ⟹ t >⇩t s"
| gt_sym_sym: "wt_sym g = wt_sym f ⟹ g >⇩s f ⟹ Hd (Sym g) >⇩t Hd (Sym f)"
| gt_sym_app: "vars s = {} ⟹ wt t = wt s ⟹ t = Hd (Sym g) ⟹ is_App s ⟹ t >⇩t s"
| gt_app_app: "vars_mset t ⊇# vars_mset s ⟹ wt t = wt s ⟹ t = App t1 t2 ⟹ s = App s1 s2 ⟹
    ext (>⇩t) [t1, t2] [s1, s2] ⟹ t >⇩t s"

abbreviation ge :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹≥⇩t› 50) where
  "t ≥⇩t s ≡ t >⇩t s ∨ t = s"

end

end