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

  fixes "pr" :: "('f × nat  'f × nat  bool × bool)"
    and prl :: "'f × nat  bool"
    and n :: nat
fun lpo :: "('f, 'v) term  ('f, 'v) term  bool × bool" 
    "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)))"


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

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)

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)
    case (2 x g ts)
    then show ?case by (auto simp: simps)
    case (3 f ss y)
    then show ?case by (auto simp: simps[of "Fun f ss" "Var y"] Let_def set_conv_nth)
    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) = (siset 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: "(iset (σ (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 "¬ (siset ss. lpo_ns si (Fun g ts))" 
      note IH = IH(2-)[OF this prc[symmetric] refl]
      from IH(1) show "(jset (σ (g, length ts)). wpo_s (Fun f ss) (ts ! j)) = (tset ts. lpo_s (Fun f ss) t)"
        unfolding set_conv_nth by auto
      assume "prns  (tset 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)

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