# Theory RPO

```section ‹The Recursive Path Order as an instance of WPO›

text ‹This theory defines the recursive path order (RPO) that given two terms provides two Booleans,
whether the terms can be strictly or non-strictly oriented. It is proven that RPO is an instance of WPO, and hence,
carries over all the nice properties of WPO immediately.›
theory RPO
imports
WPO
begin

context
fixes "pr" :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
and prl :: "'f × nat ⇒ bool"
and c :: "'f × nat ⇒ order_tag"
and n :: nat
begin

fun rpo  :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
"rpo (Var x) (Var y) = (False, x = y)" |
"rpo (Var x) (Fun g ts) = (False, ts = [] ∧ prl (g,0))" |
"rpo (Fun f ss) (Var y) = (let con = (∃ s ∈ set ss. snd (rpo s (Var y))) in (con,con))" |
"rpo (Fun f ss) (Fun g ts) = (
if (∃ s ∈ set ss. snd (rpo s (Fun g ts)))
then (True,True)
else (let (prs,prns) = pr (f,length ss) (g,length ts) in
if prns ∧ (∀ t ∈ set ts. fst (rpo (Fun f ss) t))
then if prs
then (True,True)
else if c (f,length ss) = Lex ∧ c (g,length ts) = Lex
then lex_ext rpo n ss ts
else if c (f,length ss) = Mul ∧ c (g,length ts) = Mul
then mul_ext rpo ss ts
else (length ss ≠ 0 ∧ length ts = 0, length ts = 0)
else (False,False)))"
end

locale rpo_with_assms = precedence prc prl
for prc :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
and prl :: "'f × nat ⇒ bool"
and c :: "'f × nat ⇒ order_tag"
and n :: nat
begin

sublocale wpo_with_SN_assms n "{}" UNIV prc prl full_status c False "λ _. False"
by (unfold_locales, auto simp: refl_on_def trans_def simple_arg_pos_def irrefl_def)

abbreviation "rpo_pr ≡ rpo prc prl c n"
abbreviation "rpo_s ≡ λ s t. fst (rpo_pr s t)"
abbreviation "rpo_ns ≡ λ s t. snd (rpo_pr s t)"

lemma rpo_eq_wpo: "rpo_pr s t = wpo s t"
proof -
note simps = wpo.simps
show ?thesis
proof (induct s t rule: rpo.induct[of _ prc prl c n])
case (1 x y)
then show ?case by (simp add: simps)
next
case (2 x g ts)
then show ?case by (auto simp: simps)
next
case (3 f ss y)
then show ?case by (auto simp: simps[of "Fun f ss" "Var y"] Let_def set_conv_nth)
next
case IH: (4 f ss g ts)
have id: "⋀ s. (s ∈ {}) = False" "⋀ s. (s ∈ UNIV) = True"
and "(∃i∈{0..<length ss}. wpo_ns (ss ! i) t) = (∃si∈set ss. wpo_ns si t)"
by (auto, force simp: set_conv_nth)
have id': "map ((!) ss) (σ (f, length ss)) = ss" for f ss by (intro nth_equalityI, auto)
have ex: "(∃i∈set (σ (f, length ss)). wpo_ns (ss ! i) (Fun g ts)) = (∃ si ∈ set ss. rpo_ns si (Fun g ts))"
using IH(1) unfolding set_conv_nth by auto
obtain prs prns where prc: "prc (f, length ss) (g, length ts) = (prs, prns)" by force
show ?case
unfolding rpo.simps simps[of "Fun f ss" "Fun g ts"] term.simps id id' if_False if_True
Let_def ex prc split
proof (rule sym, rule if_cong[OF refl refl], rule if_cong[OF conj_cong[OF refl] if_cong[OF refl refl if_cong[OF refl _ if_cong]] refl])
assume "¬ (∃si∈set ss. rpo_ns si (Fun g ts))"
note IH = IH(2-)[OF this prc[symmetric] refl]
from IH(1) show "(∀j∈set (σ (g, length ts)). wpo_s (Fun f ss) (ts ! j)) = (∀t∈set ts. rpo_s (Fun f ss) t)"
unfolding set_conv_nth by auto
assume "prns ∧ (∀t∈set ts. rpo_s (Fun f ss) t)" "¬ prs"
note IH = IH(2-)[OF this]
{
assume "c (f, length ss) = Lex ∧ c (g, length ts) = Lex"
from IH(1)[OF this]
show "lex_ext wpo n ss ts = lex_ext rpo_pr n ss ts"
by (intro lex_ext_cong, auto)
}
{
assume "¬ (c (f, length ss) = Lex ∧ c (g, length ts) = Lex)" "c (f, length ss) = Mul ∧ c (g, length ts) = Mul"
from IH(2)[OF this]
show "mul_ext wpo ss ts = mul_ext rpo_pr ss ts"
by (intro mul_ext_cong, auto)
}
qed auto
qed
qed

abbreviation "RPO_S ≡ {(s,t). rpo_s s t}"
abbreviation "RPO_NS ≡ {(s,t). rpo_ns s t}"

theorem RPO_SN_order_pair: "SN_order_pair RPO_S RPO_NS"
unfolding rpo_eq_wpo by (rule wpo_SN_order_pair)

theorem RPO_S_subst: "(s,t) ∈ RPO_S ⟹ (s ⋅ σ, t ⋅ σ) ∈ RPO_S" for σ :: "('f,'a)subst"
using WPO_S_subst unfolding rpo_eq_wpo .

theorem RPO_NS_subst: "(s,t) ∈ RPO_NS ⟹ (s ⋅ σ, t ⋅ σ) ∈ RPO_NS" for σ :: "('f,'a)subst"
using WPO_NS_subst unfolding rpo_eq_wpo .

theorem RPO_NS_ctxt: "(s,t) ∈ RPO_NS ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ RPO_NS"
using WPO_NS_ctxt unfolding rpo_eq_wpo .

theorem RPO_S_ctxt: "(s,t) ∈ RPO_S ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ RPO_S"
using WPO_S_ctxt unfolding rpo_eq_wpo by auto

theorem RPO_S_subset_RPO_NS: "RPO_S ⊆ RPO_NS"
using WPO_S_subset_WPO_NS unfolding rpo_eq_wpo .

theorem supt_subset_RPO_S: "{⊳} ⊆ RPO_S"
using supt_subset_WPO_S unfolding rpo_eq_wpo by auto

theorem supteq_subset_RPO_NS: "{⊵} ⊆ RPO_NS"
using supteq_subset_WPO_NS unfolding rpo_eq_wpo by auto

end
end
```