Theory Lambda_Free_KBOs

(*  Title:       Knuth-Bendix Orders for Lambda-Free Higher-Order Terms
    Author:      Heiko Becker <heikobecker92@gmail.com>, 2016
    Author:      Jasmin Blanchette <jasmin.blanchette at inria.fr>, 2016
    Author:      Uwe Waldmann <waldmann at mpi-inf.mpg.de>, 2016
    Author:      Daniel Wand <dwand at mpi-inf.mpg.de>, 2016
    Maintainer:  Jasmin Blanchette <jasmin.blanchette at inria.fr>
*)

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

theory Lambda_Free_KBOs
imports Lambda_Free_KBO_App Lambda_Free_KBO_Basic Lambda_Free_TKBO_Coefs Lambda_Encoding_KBO
begin

locale simple_kbo_instances
begin

definition arity_sym :: "nat ⇒ enat" where
  "arity_sym n = ∞"

definition arity_var :: "nat ⇒ enat" where
  "arity_var n = ∞"

definition ground_head_var :: "nat ⇒ nat set" where
  "ground_head_var x = UNIV"

definition gt_sym :: "nat ⇒ nat ⇒ bool" where
  "gt_sym g f ⟷ g > f"

definition ε :: nat where
  "ε = 1"

definition δ :: nat where
  "δ = 0"

definition wt_sym :: "nat ⇒ nat" where
  "wt_sym n = 1"

definition wt_sym⇩h :: "nat ⇒ hmultiset" where
  "wt_sym⇩h n = 1"

definition coef_sym⇩h :: "nat ⇒ nat ⇒ hmultiset" where
  "coef_sym⇩h n i = 1"

sublocale kbo_app: kbo_app gt_sym wt_sym ε len_lexext
  by unfold_locales (auto simp: gt_sym_def ε_def wt_sym_def intro: wf_less[folded wfP_def])

sublocale kbo_basic: kbo_basic gt_sym wt_sym ε "λf. len_lexext" ground_head_var
  by unfold_locales (auto simp: ground_head_var_def gt_sym_def ε_def wt_sym_def)

sublocale kbo_std: kbo_std ground_head_var gt_sym ε δ "λf. len_lexext" arity_sym arity_var wt_sym
  by unfold_locales
    (auto simp: arity_sym_def arity_var_def ground_head_var_def ε_def δ_def wt_sym_def)

sublocale tkbo_coefs: tkbo_coefs ground_head_var gt_sym ε δ "λf. len_lexext" arity_sym arity_var
    wt_sym⇩h coef_sym⇩h
  by unfold_locales (auto simp: ε_def δ_def wt_sym⇩h_def coef_sym⇩h_def)

end

end