Theory KBO_as_WPO

subsection ‹A restricted equality between KBO and WPO›

text ‹The remaining difficulty to make KBO an instance of WPO is the
  different treatment of lexicographic comparisons, which is unrestricted in KBO,
  but there is a length-restriction in WPO. 
  Therefore we will only show that KBO is an instance of WPO if we compare terms with 
  bounded arity.›

text ‹This restriction does however not prohibit us from lifting properties of WPO to KBO.
  For instance, for several properties one can choose a large-enough bound restriction of WPO, 
  since there are only finitely many arities occurring in a property.›

theory KBO_as_WPO
  imports 
    WPO 
    KBO_Transformation
begin

definition bounded_arity :: "nat ⇒ ('f × nat)set ⇒ bool" where
  "bounded_arity b F = (∀ (f,n) ∈ F. n ≤ b)" 

lemma finite_funas_term[simp,intro]: "finite (funas_term t)" 
  by (induct t, auto)

context weight_fun begin

definition "weight_le s t ≡
  (vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t) ∧ weight s ≤ weight t)"

definition "weight_less s t ≡
  (vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t) ∧ weight s < weight t)"

lemma weight_le_less_iff: "weight_le s t ⟹ weight_less s t ⟷ weight s < weight t"
  by (auto simp: weight_le_def weight_less_def)

lemma weight_less_iff: "weight_less s t ⟹ weight_le s t ∧ weight s < weight t"
  by (auto simp: weight_le_def weight_less_def)


abbreviation "weight_NS ≡ {(t,s). weight_le s t}"

abbreviation "weight_S ≡ {(t,s). weight_less s t}"

lemma weight_le_mono_one:
  assumes S: "weight_le s t"
  shows "weight_le (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))" (is "weight_le ?s ?t")
proof -
  from S have w: "weight s ≤ weight t" and v: "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)" 
    by (auto simp: weight_le_def)
  have v': "vars_term_ms (SCF ?s) ⊆# vars_term_ms (SCF ?t)"
    using mset_replicate_mono[OF v] by simp
  have w': "weight ?s ≤ weight ?t" using sum_list_replicate_mono[OF w] by simp
  from v' w' show ?thesis by (auto simp: weight_le_def)
qed

lemma weight_le_ctxt: "weight_le s t ⟹ weight_le (C⟨s⟩) (C⟨t⟩)"
  by (induct C, auto intro: weight_le_mono_one)

lemma SCF_stable:
  assumes "vars_term_ms (SCF s) ⊆# vars_term_ms (SCF t)"
  shows "vars_term_ms (SCF (s ⋅ σ)) ⊆# vars_term_ms (SCF (t ⋅ σ))"
  unfolding scf_term_subst
  using vars_term_ms_subst_mono[OF assms].

lemma SN_weight_S: "SN weight_S"
proof-
  from wf_inv_image[OF wf_less]
  have wf: "wf {(s,t). weight s < weight t}" by (auto simp: inv_image_def)
  show ?thesis
    by (unfold SN_iff_wf, rule wf_subset[OF wf], auto simp: weight_less_def)
qed

lemma weight_less_imp_le: "weight_less s t ⟹ weight_le s t" by (simp add: weight_less_def weight_le_def)

lemma weight_le_Var_Var: "weight_le (Var x) (Var y) ⟷ x = y"
  by (auto simp: weight_le_def)
end

context kbo begin

lemma kbo_altdef:
    "kbo s t = (if weight_le t s
      then if weight_less t s
        then (True, True)
        else (case s of
          Var y ⇒ (False, (case t of Var x ⇒ x = y | Fun g ts ⇒ ts = [] ∧ least g))
        | Fun f ss ⇒ (case t of
            Var x ⇒ (True, True)
          | Fun g ts ⇒ if pr_strict (f, length ss) (g, length ts)
            then (True, True)
            else if pr_weak (f, length ss) (g, length ts)
            then lex_ext_unbounded kbo ss ts
            else (False, False)))
      else (False, False))"
  by (simp add: weight_le_less_iff weight_le_def)

end

context admissible_kbo begin

lemma weight_le_stable:
  assumes "weight_le s t"
  shows "weight_le (s ⋅ σ) (t ⋅ σ)"
  using assms weight_stable_le SCF_stable by (auto simp: weight_le_def)

lemma weight_less_stable:
  assumes "weight_less s t"
  shows "weight_less (s ⋅ σ) (t ⋅ σ)"
  using assms weight_stable_lt SCF_stable by (auto simp: weight_less_def)

lemma simple_arg_pos_weight: "simple_arg_pos weight_NS (f,n) i"
  unfolding simple_arg_pos_def
proof (intro allI impI, unfold snd_conv fst_conv)
  fix ts :: "('f,'a)term list" 
  assume i: "i < n" and len: "length ts = n" 
  from id_take_nth_drop[OF i[folded len]] i[folded len]
  obtain us vs where id: "Fun f ts = Fun f (us @ ts ! i # vs)" 
    and us: "us = take i ts" 
    and len: "length us = i" by auto
  have "length us < Suc (length us + length vs)" by auto
  from scf[OF this, of f] obtain j where [simp]: "scf (f, Suc (length us + length vs)) (length us) = Suc j"
    by (rule lessE)
  show "(Fun f ts, ts ! i) ∈ weight_NS" 
    unfolding weight_le_def id by (auto simp: o_def)
qed

lemma weight_lemmas:
  shows "refl weight_NS" and "trans weight_NS" and "trans weight_S"
    and "weight_NS O weight_S ⊆ weight_S" and "weight_S O weight_NS ⊆ weight_S"
  by (auto intro!: refl_onI transI simp: weight_le_def weight_less_def)

interpretation kbo': admissible_kbo w w0 pr_strict' pr_weak' least scf
  by (rule admissible_kbo')

context
  assumes least_global: "⋀ f g. least f ⟹ pr_weak g (f,0)"
    and least_trans: "⋀ f g. least f ⟹ pr_weak (f,0) g ⟹ least (fst g) ∧ snd g = 0" 
  fixes n :: nat
begin

lemma kbo_instance_of_wpo_with_SN_assms: "wpo_with_SN_assms 
  weight_S weight_NS (λf g. (pr_strict f g, pr_weak f g))
     (λ(f, n). n = 0 ∧ least f) full_status False (λf. False)" 
  apply (unfold_locales)
                      apply (auto simp: weight_lemmas SN_weight_S pr_SN pr_strict_irrefl
      weight_less_stable weight_le_stable weight_le_mono_one weight_less_imp_le
      simple_arg_pos_weight) 
         apply (force dest: least_global least_trans simp: pr_strict)+
  using SN_on_irrefl[OF SN_weight_S]
     apply (auto simp: pr_strict least irrefl_def dest:pr_weak_trans)
  done

interpretation wpo: wpo_with_SN_assms
  where S = weight_S and NS = weight_NS
    and prc = "λf g. (pr_strict f g, pr_weak f g)" and prl = "λ(f,n). n = 0 ∧ least f"
    and c = "λ_. Lex"
    and ssimple = False and large = "λf. False" and σσ = full_status
    and n = n 
  by (rule kbo_instance_of_wpo_with_SN_assms)

lemma kbo_as_wpo_with_assms: assumes "bounded_arity n (funas_term t)"
  shows "kbo s t = wpo.wpo s t"
proof -
  define m where "m = size s + size t" 
  from m_def assms show ?thesis
  proof (induct m arbitrary: s t rule: less_induct)
    case (less m s t)
    hence IH: "size si + size ti < size s + size t ⟹ bounded_arity n (funas_term ti) ⟹ kbo si ti = wpo.wpo si ti" for si ti :: "('f,'a)term" by auto
    note wpo_sI = arg_cong[OF wpo.wpo.simps, of fst, THEN iffD2]
    note wpo_nsI = arg_cong[OF wpo.wpo.simps, of snd, THEN iffD2]
    note bounded = less(3)
    show ?case
    proof (cases s)
      case s: (Var x)
      have "¬ weight_less t (Var x)"
        by (metis leD weight.simps(1) weight_le_less_iff weight_less_imp_le weight_w0)
      thus ?thesis
        by (cases t, auto simp add: s kbo_altdef wpo.wpo.simps)
    next
      case s: (Fun f ss)
      show ?thesis
      proof (cases t)
        case t: (Var y)
        { assume "weight_le t s"
          then have "∃s' ∈ set ss. weight_le t s'"
            apply (auto simp: s t weight_le_def)
            by (metis scf set_scf_list weight_w0)
          then obtain s' where s': "s' ∈ set ss" and "weight_le t s'" by auto
          from this(2) have "wpo.wpo_ns s' t"
          proof (induct s')
            case (Var x)
            then show ?case by (auto intro!:wpo_nsI simp: t weight_le_Var_Var)
          next
            case (Fun f' ss')
            from this(2) have "∃s'' ∈ set ss'. weight_le t s''"
              apply (auto simp: t weight_le_def)
              by (metis scf set_scf_list weight_w0)
            then obtain s'' where "s'' ∈ set ss'" and "weight_le t s''" by auto
            with Fun(1)[OF this] Fun(2)
            show ?case by (auto intro!: wpo_nsI simp: t in_set_conv_nth)
          qed
          with s' have "∃s' ∈ set ss. wpo.wpo_ns s' t" by auto
        }
        then 
        show ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t]
          by (auto simp add: s t weight_less_iff set_conv_nth, auto)
      next
        case t: (Fun g ts)
        {
          fix j
          assume "j < length ts" 
          hence "ts ! j ∈ set ts" by auto
          hence "funas_term (ts ! j) ⊆ funas_term t" unfolding t by auto
          with bounded have "bounded_arity n (funas_term (ts ! j))" unfolding bounded_arity_def by auto
        } note bounded_tj = this
        note IH_tj = IH[OF _ this]
        show ?thesis
        proof (cases "¬ weight_le t s ∨ weight_less t s")
          case True  
          thus ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t]
            unfolding s t by (auto simp: weight_less_iff)
        next
          case False
          let ?f = "(f,length ss)" 
          let ?g = "(g,length ts)" 
          from False have wle: "weight_le t s = True" "weight_less t s = False" 
            "(s, t) ∈ weight_NS ⟷ True" "(s, t) ∈ weight_S ⟷ False" by auto
          have lex: "(Lex = Lex ∧ Lex = Lex) = True" by simp
          have sig: "set (wpo.σ ?f) = {..<length ss}"
            "set (wpo.σ ?g) = {..<length ts}" by auto
          have map: "map ((!) ss) (wpo.σ ?f) = ss"
            "map ((!) ts) (wpo.σ ?g) = ts"
            by (auto simp: map_nth)
          have sizes: "i < length ss ⟹ size (ss ! i) < size s" for i unfolding s
            by (simp add: size_simp1)
          have sizet: "i < length ts ⟹ size (ts ! i) < size t" for i unfolding t
            by (simp add: size_simp1)
          have wpo: "wpo.wpo s t = 
             (if ∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t then (True, True)
              else if pr_weak ?f ?g ∧ (∀j∈{..<length ts}. wpo.wpo_s s (ts ! j))
              then if pr_strict ?f ?g then (True, True) else lex_ext wpo.wpo n ss ts
              else (False, False))" 
            unfolding wpo.wpo.simps[of s t]
            unfolding s t term.simps split Let_def lex if_True sig map
            unfolding s[symmetric] t[symmetric] wle if_True weight_less_iff if_False False snd_conv by auto
          have "kbo s t = (if pr_strict ?f ?g then (True, True)
               else if pr_weak ?f ?g then lex_ext_unbounded kbo ss ts
               else (False, False))" 
            unfolding kbo_altdef[of s t]
            unfolding s t term.simps split Let_def if_True 
            unfolding s[symmetric] t[symmetric] wle if_True weight_less_iff if_False by auto
          also have "lex_ext_unbounded kbo ss ts = lex_ext kbo n ss ts" 
            using bounded[unfolded t] unfolding bounded_arity_def lex_ext_def by auto
          also have "… = lex_ext wpo.wpo n ss ts" 
            by (rule lex_ext_cong[OF refl refl refl], rule IH_tj, auto dest!: sizes sizet)
          finally have kbo: "kbo s t =
              (if pr_strict ?f ?g then (True, True)
               else if pr_weak ?f ?g then lex_ext wpo.wpo n ss ts
               else (False, False))" .
          show ?thesis
          proof (cases "∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t")
            case True
            then obtain i where i: "i < length ss" and "wpo.wpo_ns (ss ! i) t" by auto
            then obtain b where "wpo.wpo (ss ! i) t = (b, True)" by (cases "wpo.wpo (ss ! i) t", auto)
            also have "wpo.wpo (ss ! i) t = kbo (ss ! i) t" using i by (intro IH[symmetric, OF _ bounded], auto dest: sizes)
            finally have "NS (ss ! i) t" by simp
            from kbo_supt_one[OF this]
            have "S (Fun f (take i ss @ ss ! i # drop (Suc i) ss)) t" .
            also have "(take i ss @ ss ! i # drop (Suc i) ss) = ss" using i by (metis id_take_nth_drop)
            also have "Fun f ss = s" unfolding s by simp
            finally have "S s t" .
            with S_imp_NS[OF this]
            have "kbo s t = (True,True)" by (cases "kbo s t", auto) 
            with True show ?thesis unfolding wpo by auto
          next
            case False
            hence False: "(∃i∈{..<length ss}. wpo.wpo_ns (ss ! i) t) = False" by simp
            {
              fix j
              assume NS: "NS s t" 
              assume j: "j < length ts" 
              (* here we make use of proven properties of KBO: subterm-property and transitivity,
                 perhaps there is a simple proof without already using these properties *)
              from kbo_supt_one[OF NS_refl, of g "take j ts" "ts ! j" "drop (Suc j) ts"]
              have S: "S t (ts ! j)" using id_take_nth_drop[OF j] unfolding t by auto
              from kbo_trans[of s t "ts ! j"] NS S have "S s (ts ! j)" by auto
              with S S_imp_NS[OF this]
              have "kbo s (ts ! j) = (True, True)" by (cases "kbo s (ts ! j)", auto)
              hence "wpo.wpo_s s (ts ! j)" 
                by (subst IH_tj[symmetric], insert sizet[OF j] j, auto)
            }
            thus ?thesis unfolding wpo kbo False if_False using lex_ext_stri_imp_nstri[of wpo.wpo n ss ts]
              by (cases "lex_ext wpo.wpo n ss ts", auto simp: pr_strict split: if_splits)
          qed
        qed
      qed
    qed
  qed
qed
end

text ‹This is the main theorem. It tells us that KBO can be seen as an instance of WPO, under mild preconditions:
  the parameter $n$ for the lexicographic extension has to be chosen high enough to cover the arities of all 
  terms that should be compared.›
lemma defines "prec ≡ ((λf g. (pr_strict' f g, pr_weak' f g)))" 
  and "prl ≡ (λ(f, n). n = 0 ∧ least f)" 
  shows 
    kbo_encoding_is_valid_wpo: "wpo_with_SN_assms weight_S weight_NS prec prl full_status False (λf. False)"
  and 
    kbo_as_wpo: "bounded_arity n (funas_term t) ⟹ kbo s t = wpo.wpo n weight_S weight_NS prec prl full_status (λ_. Lex) False (λf. False) s t" 
  unfolding prec_def prl_def
  subgoal by (intro admissible_kbo.kbo_instance_of_wpo_with_SN_assms[OF admissible_kbo'] 
        least_pr_weak' least_pr_weak'_trans)
  apply (subst kbo'_eq_kbo[symmetric])
  apply (subst admissible_kbo.kbo_as_wpo_with_assms[OF admissible_kbo' least_pr_weak' least_pr_weak'_trans, symmetric], (auto)[3])
  by auto

text ‹As a proof-of-concept we show that now properties of WPO can be used to prove these properties for KBO.
  Here, as example we consider closure under substitutions and strong normalization, 
  but the following idea can be applied for several more properties:
  if the property involves only terms where the arities are bounded, then just choose the parameter $n$ large enough.
  This even works for strong normalization, since in an infinite chain of KBO-decreases $t_1 > t_2 > t_3 > ...$ all terms have
  a weight of at most the weight of $t_1$, and this weight is also a bound on the arities.›

lemma KBO_stable_via_WPO: "S s t ⟹ S (s ⋅ (σ :: ('f,'a) subst)) (t ⋅ σ)"
proof -
  let ?terms = "{t, t ⋅ σ}" (* collect all rhss of comparisons *)
  let ?prec = "((λf g. (pr_strict' f g, pr_weak' f g)))" 
  let ?prl = "(λ(f, n). n = 0 ∧ least f)" 
  have "finite (⋃ (funas_term ` ?terms))" 
    by auto
  from finite_list[OF this] obtain F where F: "set F = ⋃ (funas_term ` ?terms)" by auto
  (* since there only finitely many symbols, we can take n as the maximal arity *)
  define n where "n = max_list (map snd F)" 

  (* now get a WPO for this choice of n *)
  interpret wpo: wpo_with_SN_assms
  where S = weight_S and NS = weight_NS
    and prc = ?prec and prl = ?prl
    and c = "λ_. Lex"
    and ssimple = False and large = "λf. False" and σσ = full_status
    and n = n 
    by (rule kbo_encoding_is_valid_wpo)

  {
    fix t
    assume "t ∈ ?terms" 
    hence "funas_term t ⊆ set F" unfolding F by auto
    hence "bounded_arity n (funas_term t)" unfolding bounded_arity_def 
      using max_list[of _ "map snd F", folded n_def] by fastforce
  }
  (* for all the terms we have that KBO = WPO *)
  note kbo_as_wpo = kbo_as_wpo[OF this]

  (* and finally transfer the existing property of WPO to KBO *)
  from wpo.WPO_S_subst[of s t σ]
  show "S s t ⟹ S (s ⋅ σ) (t ⋅ σ)"
    using kbo_as_wpo by auto
qed

lemma weight_is_arity_bound: "weight t ≤ b ⟹ bounded_arity b (funas_term t)" 
proof (induct t)
  case (Fun f ts)
  have "sum_list (map weight ts) ≤ weight (Fun f ts)" 
    using sum_list_scf_list[of ts "scf (f,length ts)", OF scf] by auto
  also have "… ≤ b" using Fun by auto
  finally have sum_b: "sum_list (map weight ts) ≤ b" .
  {
    fix t
    assume t: "t ∈ set ts" 
    from split_list[OF this] have "weight t ≤ sum_list (map weight ts)" by auto
    with sum_b have "bounded_arity b (funas_term t)" using t Fun by auto
  } note IH = this
  have "length ts = sum_list (map (λ _. 1) ts)" by (induct ts, auto)
  also have "… ≤ sum_list (map weight ts)"
    apply (rule sum_list_mono)
    subgoal for t using weight_gt_0[of t] by auto
    done
  also have "… ≤ b" by fact
  finally have len: "length ts ≤ b" by auto
  from IH len show ?case unfolding bounded_arity_def by auto
qed (auto simp: bounded_arity_def)
  
lemma KBO_SN_via_WPO: "SN {(s,t). S s t}"
proof 
  fix f :: "nat ⇒ ('f,'a)term" 
  assume "∀i. (f i, f (Suc i)) ∈ {(s, t). S s t}" 
  hence steps: "S (f i) (f (Suc i))" for i by auto
  define n where "n = weight (f 0)"

  have w_bound: "weight (f i) ≤ n" for i
  proof (induct i)
    case (Suc i)
    from steps[of i] have "weight (f (Suc i)) ≤ weight (f i)" 
      unfolding kbo.simps[of "f i"] by (auto split: if_splits)
    with Suc show ?case by simp
  qed (auto simp: n_def)

  let ?prec = "((λf g. (pr_strict' f g, pr_weak' f g)))" 
  let ?prl = "(λ(f, n). n = 0 ∧ least f)" 

  (* now get a WPO for this choice of n *)
  interpret wpo: wpo_with_SN_assms
  where S = weight_S and NS = weight_NS
    and prc = ?prec and prl = ?prl
    and c = "λ_. Lex"
    and ssimple = False and large = "λf. False" and σσ = full_status
    and n = n 
    by (rule kbo_encoding_is_valid_wpo)

  have "kbo (f i) (f (Suc i)) = wpo.wpo (f i) (f (Suc i))" for i
    by (rule kbo_as_wpo[OF weight_is_arity_bound[OF w_bound]])
  (* for all the terms in the infinite sequence f 0, f 1, ... 
     we have that KBO = WPO *)

  (* and finally derive contradiction to SN-property of WPO *)
  from steps[unfolded this] wpo.WPO_S_SN show False by auto
qed

end
  
end