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