Theory Lambda_Free_RPO_App

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

theory Lambda_Free_RPO_App
imports Lambda_Free_Term Extension_Orders
abbrevs ">t" = ">⇩t"
  and "≥t" = "≥⇩t"
begin

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

locale rpo_app = gt_sym "(>⇩s)"
    for gt_sym :: "'s ⇒ 's ⇒ bool" (infix ‹>⇩s› 50) +
  fixes ext :: "(('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool) ⇒ ('s, 'v) tm list ⇒ ('s, 'v) tm list ⇒ bool"
  assumes
    ext_ext_trans_before_irrefl: "ext_trans_before_irrefl ext" and
    ext_ext_compat_list: "ext_compat_list 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])

inductive gt :: "('s, 'v) tm ⇒ ('s, 'v) tm ⇒ bool" (infix ‹>⇩t› 50) where
  gt_sub: "is_App t ⟹ (fun t >⇩t s ∨ fun t = s) ∨ (arg t >⇩t s ∨ arg t = s) ⟹ t >⇩t s"
| gt_sym_sym: "g >⇩s f ⟹ Hd (Sym g) >⇩t Hd (Sym f)"
| gt_sym_app: "Hd (Sym g) >⇩t s1 ⟹ Hd (Sym g) >⇩t s2 ⟹ Hd (Sym g) >⇩t App s1 s2"
| gt_app_app: "ext (>⇩t) [t1, t2] [s1, s2] ⟹ App t1 t2 >⇩t s1 ⟹ App t1 t2 >⇩t s2 ⟹
    App t1 t2 >⇩t App s1 s2"

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

end

end