Theory Lambda_Free_RPOs

(*  Title:       Recursive Path Orders for Lambda-Free Higher-Order Terms
    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 ‹Recursive Path Orders for Lambda-Free Higher-Order Terms›

theory Lambda_Free_RPOs
imports Lambda_Free_RPO_App Lambda_Free_RPO_Optim Lambda_Encoding
begin

locale simple_rpo_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"

sublocale app: rpo_app gt_sym len_lexext
  by unfold_locales (auto simp: gt_sym_def intro: wf_less[folded wfP_def])

sublocale std: rpo ground_head_var gt_sym "λf. len_lexext" arity_sym arity_var
  by unfold_locales (auto simp: arity_var_def arity_sym_def ground_head_var_def)

sublocale optim: rpo_optim ground_head_var gt_sym "λf. len_lexext" arity_sym arity_var
  by unfold_locales

end

end