Theory LPO

section ‹The Lexicographic Path Order as an instance of WPO›

text ‹We first directly define the strict- and non-strict lexicographic path orders (LPO)
  w.r.t.\ some precedence, and then show that it is an instance of WPO.
  For this instance we use the trivial reduction pair in WPO ($\emptyset$, UNIV) and
  the status is the full one, i.e., taking parameters [0,..,n-1] for each n-ary symbol.›

theory LPO
  imports
    WPO
begin

context
  fixes "pr" :: "('f × nat ⇒ 'f × nat ⇒ bool × bool)"
    and prl :: "'f × nat ⇒ bool"
    and n :: nat
begin
fun lpo :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool" 
  where
    "lpo (Var x) (Var y) = (False, x = y)" |
    "lpo (Var x) (Fun g ts) = (False, ts = [] ∧ prl (g,0))" |
    "lpo (Fun f ss) (Var y) = (let con = (∃ s ∈ set ss. snd (lpo s (Var y))) in (con,con))" |
    "lpo (Fun f ss) (Fun g ts) = (
      if (∃ s ∈ set ss. snd (lpo 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 (lpo (Fun f ss) t))
           then if prs
              then (True,True) 
              else lex_ext lpo n ss ts
           else (False,False)))"

end


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

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

abbreviation "lpo_pr ≡ lpo prc prl n" 
abbreviation "lpo_s ≡ λ s t. fst (lpo_pr s t)"
abbreviation "lpo_ns ≡ λ s t. snd (lpo_pr s t)"

lemma lpo_eq_wpo: "lpo_pr s t = wpo s t"
proof - 
  note simps = wpo.simps
  show ?thesis 
  proof (induct s t rule: lpo.induct[of _ prc prl 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. lpo_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
    have lex: "(Lex = Lex ∧ Lex = Lex) = True" by simp
    show ?case
      unfolding lpo.simps simps[of "Fun f ss" "Fun g ts"] term.simps id id' if_False if_True lex
        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] refl])
      assume "¬ (∃si∈set ss. lpo_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. lpo_s (Fun f ss) t)"
        unfolding set_conv_nth by auto
      assume "prns ∧ (∀t∈set ts. lpo_s (Fun f ss) t)" "¬ prs" 
      note IH = IH(2-)[OF this]
      show "lex_ext wpo n ss ts = lex_ext lpo_pr n ss ts" 
        using IH by (intro lex_ext_cong, auto)
    qed
  qed
qed

abbreviation "LPO_S ≡ {(s,t). lpo_s s t}"
abbreviation "LPO_NS ≡ {(s,t). lpo_ns s t}"

theorem LPO_SN_order_pair: "SN_order_pair LPO_S LPO_NS"
  unfolding lpo_eq_wpo by (rule WPO_SN_order_pair)

theorem LPO_S_subst: "(s,t) ∈ LPO_S ⟹ (s ⋅ σ, t ⋅ σ) ∈ LPO_S" for σ :: "('f,'a)subst" 
  using WPO_S_subst unfolding lpo_eq_wpo .

theorem LPO_NS_subst: "(s,t) ∈ LPO_NS ⟹ (s ⋅ σ, t ⋅ σ) ∈ LPO_NS" for σ :: "('f,'a)subst"
  using WPO_NS_subst unfolding lpo_eq_wpo .

theorem LPO_NS_ctxt: "(s,t) ∈ LPO_NS ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ LPO_NS" 
  using WPO_NS_ctxt unfolding lpo_eq_wpo .

theorem LPO_S_ctxt: "(s,t) ∈ LPO_S ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ LPO_S" 
  using WPO_S_ctxt unfolding lpo_eq_wpo by auto

theorem LPO_S_subset_LPO_NS: "LPO_S ⊆ LPO_NS" 
  using WPO_S_subset_WPO_NS unfolding lpo_eq_wpo .

theorem supt_subset_LPO_S: "{⊳} ⊆ LPO_S" 
  using supt_subset_WPO_S unfolding lpo_eq_wpo by auto

theorem supteq_subset_LPO_NS: "{⊵} ⊆ LPO_NS" 
  using supteq_subset_WPO_NS unfolding lpo_eq_wpo by auto

end

end