Theory AC_Subterm_Criterion

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2016)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2016)
License: LGPL (see file COPYING.LESSER)
*)

section ‹AC Subterm Criterion›

theory AC_Subterm_Criterion
imports
  "Check-NT.Relative_DP_Framework"
  "Check-NT.AC_Rewriting"
  "../Orderings/Subterm_Multiset"
begin

lemma suptmulexeq_singleton_Var:
  assumes "{#Var x#} ⊵⇩# T"
  obtains "T = {#Var x#}" | "T = {#}"
proof -
  obtain X Y Z where x: "{#Var x#} = X + Z" and T: "T = Y + Z"
    and *: "∀y∈set_mset Y. ∃x∈set_mset X. x ⊳ y" using assms by (auto elim: ns_mul_ext_IdE)
  show ?thesis
  proof (cases "Z")
    case empty
    with x and T and * have "∀y∈set_mset T. Var x ⊳ y" by auto
    then have "T = {#}" by (cases T) auto
    then show ?thesis ..
  next
    case (add z Z')
    then have "Z = {#Var x#}" and "X = {#}" and [simp]: "z = Var x"
      using x and T by (auto split: if_splits)
    with * have "T = {#Var x#}" by (auto simp: T multiset_eq_iff)
    then show ?thesis ..
  qed
qed


subsection ‹Projections›

abbreviation "proj_mset f T ≡ ⋃# image_mset f T"

abbreviation subst_mset (infixl "⋅⇩m" 67)
where
  "M ⋅⇩m σ ≡ image_mset (λt. t ⋅ σ) M"

lemma proj_mset_cong:
  assumes "⋀x. x ∈# M ⟹ f x = g x"
  shows "proj_mset f M = proj_mset g M"
using image_mset_cong [of M f g, OF assms] by auto

context
  fixes proj :: "'f status"
    and F :: "'f sig"
begin

fun proj_term
where
  "proj_term (Var x) = {#Var x#}"
| "proj_term (Fun f ts) =
    (if (f, length ts) ∈ F then ⋃# mset (map (λi. proj_term (ts ! i)) (status proj (f, length ts)))
    else {#Fun f ts#})"

abbreviation suptproj_pred (infix "⊳⇧π" 55)
where
  "s ⊳⇧π t ≡ proj_term s ⊳⇩# proj_term t"

abbreviation suptprojeq_pred (infix "⊵⇧π" 55)
where
  "s ⊵⇧π t ≡ proj_term s ⊵⇩# proj_term t"

lemma proj_term_supteq:
  assumes "u ∈# proj_term t"
  shows "t ⊵ u"
using assms
apply (induct t)
apply (auto split: if_splits simp: in_multiset_in_set Fun_supteq dest: set_status_nth)
by (meson status_aux)

lemma proj_term_supt:
  assumes u: "u ∈# proj_term t"
  and neq: "proj_term t ≠ {# t #}"
  shows "t ⊳ u"
proof -
  from neq obtain f ts where t: "t = Fun f ts" by (cases t, auto)
  from neq have "proj_term t = ⋃#mset (map (λi. proj_term (ts ! i)) (status proj (f, length ts)))"
    unfolding t by auto
  from u[unfolded this] obtain i where "u ∈# proj_term (ts ! i)" and "i ∈ set (status proj (f,length ts))"
    by (auto simp: in_multiset_in_set dest: set_status_nth)
  from set_status_nth[OF refl this(2)] this(1) obtain ti where ti: "ti ∈ set ts" and "u ∈# proj_term ti" by auto
  from proj_term_supteq[OF this(2)] ti show ?thesis unfolding t by auto
qed

lemma proj_term_subst:
  "proj_mset proj_term (proj_term t ⋅⇩m σ) = proj_term (t ⋅ σ)"
proof (induct t)
  case (Fun f ts)
  then have "⋀i. i ∈# mset (status proj (f, length ts)) ⟹
    proj_mset (proj_term ∘ (λt. t ⋅ σ)) (proj_term (ts ! i)) = proj_term (map (λt. t ⋅ σ) ts ! i)"
    by (auto simp: in_multiset_in_set multiset.map_comp set_status_nth)
  then show ?case by (auto simp: mset_map multiset.map_comp intro: proj_mset_cong)
qed simp

lemma proj_term_idemp:
  "proj_mset proj_term (proj_term t) = proj_term t"
using proj_term_subst [of Var t] by simp

lemma proj_term_root:
  assumes "u ∈# proj_term t"
  obtains (Var) "root u = None"
  | (not_F) f and n where "root u = Some (f, n)" and "(f, n) ∉ F"
using assms
by (induct t arbitrary: u) (force split: if_splits simp: in_multiset_in_set status_aux)+

lemma suptmulexeq_subst:
  assumes "s ⊵⇧π t"
  shows "s ⋅ σ ⊵⇧π t ⋅ σ"
proof -
  obtain S T U where proj_s: "proj_term s = S + U" and "proj_term t = T + U"
    and *: "∀t' ∈ set_mset T. ∃s' ∈ set_mset S. s' ⊳ t'"
    using assms by (auto elim: ns_mul_ext_IdE)
  then have s: "proj_term (s ⋅ σ) = proj_mset proj_term (S ⋅⇩m σ) + proj_mset proj_term (U ⋅⇩m σ)"
    and t: "proj_term (t ⋅ σ) = proj_mset proj_term (T ⋅⇩m σ) + proj_mset proj_term (U ⋅⇩m σ)"
    by (auto simp: proj_term_subst [symmetric])
  { fix t' v assume "t' ∈# T" and v: "v ∈# proj_term (t' ⋅ σ)"
    with * obtain s' where "s' ∈ set_mset S" and "s' ⊳ t'" by force
    then have "s' ⋅ σ ⊳ t' ⋅ σ" by (auto dest: supt_subst)
    moreover have "t' ⋅ σ ⊵ v" by (rule proj_term_supteq [OF v])
    ultimately have "s' ⋅ σ ⊳ v" by (auto dest: supt_supteq_trans)
    moreover have "s' ⋅ σ ∈ set_mset (proj_term (s' ⋅ σ))"
    proof -
      have *: "s' ∈# proj_term s" using ‹s' ∈ set_mset S› by (auto simp: proj_s)
      show ?thesis
      apply (cases s', auto, insert ‹s' ⊳ t'›, blast)
      using * by (cases rule: proj_term_root) auto
    qed
    ultimately have "∃w ∈ set_mset S. ∃x ∈ set_mset (proj_term (w ⋅ σ)). x ⊳ v"
      using ‹s' ∈ set_mset S› by blast }
  then show ?thesis by (intro ns_mul_ext_IdI [OF s t]) auto
qed

lemma proj_mset_empty:
  "proj_mset f M = {#} ⟹ (∀x. x ∈# M ⟶ f x = {#})"
by (induct M) simp_all

lemma status_ne_imp_proj_term_ne:
  assumes "∀f ∈ F. status proj f ≠ []"
  shows "proj_term t ≠ {#}"
proof (induct t)
  case (Fun f ts)
  then have "(f, length ts) ∈ F ⟹ ?case"
    using assms [THEN bspec, of "(f, length ts)"]
    by (force simp: mset_map in_multiset_in_set dest: status_ne proj_mset_empty)
  then show ?case by simp
qed simp

lemma proj_mset_nth_map:
  "proj_mset (λi. proj_term (map g ss ! i))
     (mset (status proj (f, length ss))) =
    proj_mset (λi. proj_term (g (ss ! i)))
     (mset (status proj (f, length ss)))"
by (intro proj_mset_cong) (auto simp: in_multiset_in_set set_status_nth)

lemma proj_term_ns_mul_ext: "{# t #} ⊵⇩# proj_term t"
proof (cases "proj_term t = {# t #}")
  case False
  from proj_term_supt[OF _ this]
  show ?thesis using ns_mul_extI[OF refl refl, of "{#}" "{#}" _ _ "{#t#}"] by auto
qed auto

context
  fixes R :: "('f,'v)trs"
  assumes wf: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
  and rulesF: "⋀ l r. (l,r) ∈ R ⟹ root l ∈ Some ` F ⟹ l ⊵⇧π r"
begin
lemma rstep_proj_term: assumes st: "(s,t) ∈ rstep R"
  shows "(proj_term s, proj_term t) ∈ (ns_mul_ext ((rstep R)^*) {⊳})^*"
proof -
  let ?ns = "ns_mul_ext ((rstep R)^*) {⊳}"
  let ?sub = "{⊵⇩#}"
  let ?p = proj_term
  have sub: "?sub ⊆ ?ns" 
    by (rule ns_mul_ext_mono, auto)
  from st obtain C l r σ where s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and lr: "(l,r) ∈ R" by auto
  note lrF = rulesF[OF lr]
  show ?thesis unfolding s t
  proof (induct C)
    case Hole
    show ?case 
    proof (cases "root l ∈ Some ` F")
      case True
      from suptmulexeq_subst[OF rulesF[OF lr True], of σ] sub
      show ?thesis by auto
    next
      case False
      from wf[OF lr] obtain f ls where l: "l = Fun f ls" by (cases l, auto)
      from lr have "(l ⋅ σ, r ⋅ σ) ∈ rstep R" by auto
      hence "({# l ⋅ σ #}, {# r ⋅ σ #}) ∈ ?ns" by (intro ns_mul_ext_singleton, auto)
      with False have "(?p (l ⋅ σ), {# r ⋅ σ #}) ∈ ?ns" unfolding l by auto
      moreover have "{# r ⋅ σ #} ⊵⇩# ?p (r ⋅ σ)"
        by (rule proj_term_ns_mul_ext)
      hence "({# r ⋅ σ #}, ?p (r ⋅ σ)) ∈ ?ns" using sub by auto
      ultimately show ?thesis by auto
    qed
  next
    case (More f bef C aft)
    let ?n = "Suc (length bef + length aft)"
    let ?f = "(f,?n)"
    let ?C = "More f bef C aft"
    show ?case
    proof (cases "?f ∈ F")
      case False
      have "(?C ⟨l ⋅ σ⟩, ?C ⟨r ⋅ σ⟩) ∈ rstep R" by (intro rstepI[OF lr refl refl])
      with set_mp[OF sub ns_mul_ext_singleton] 
      show ?thesis using False by auto
    next
      case True
      def idx ≡ "status proj (f, Suc (length bef + length aft))"
      let ?i = "length bef"
      let ?g = "λ lr i. ?p ((bef @ C⟨lr ⋅ σ⟩ # aft) ! i)"
      let ?gen = "λ lr idx. ⋃#mset (map (?g lr) idx)"
      let ?l = "?gen l" let ?r = "?gen r"
      have id: "?thesis = ((?l idx, ?r idx) ∈ ?ns^*)"
        by (simp add: True idx_def[symmetric])
      show ?thesis unfolding id
      proof (induct idx)
        case (Cons i idx)
        have l: "?l (i # idx) = ?g l i + ?l idx" by (simp add: ac_simps)
        have r: "?r (i # idx) = ?g r i + ?r idx" by (simp add: ac_simps)
        have refl: "refl Id" unfolding refl_on_def by auto
        show ?case unfolding l r
          by (rule ns_ns_mul_ext_union_compat_rtrancl[OF _ _ Cons], insert More,
          cases "i = ?i"; cases "i - ?i", auto simp: nth_append intro: refl_rtrancl)
      qed simp
    qed
  qed
qed

lemma rsteps_proj_term: "(s,t) ∈ (rstep R)^* 
  ⟹ (proj_term s, proj_term t) ∈ (ns_mul_ext ((rstep R)^*) {⊳})^*"
  by (induct rule: rtrancl_induct, auto dest: rstep_proj_term)
end  

context
  assumes ne: "∀f∈F. status proj f ≠ []"
begin

lemma suptmulex_subst:
  assumes "s ⊳⇧π t"
  shows "s ⋅ σ ⊳⇧π t ⋅ σ"
proof -
  obtain S T U where S_ne: "S ≠ {#}"
    and proj_s: "proj_term s = S + U" and "proj_term t = T + U"
    and *: "∀t' ∈ set_mset T. ∃s' ∈ set_mset S. s' ⊳ t'"
    using assms by (auto elim: s_mul_ext_IdE)
  then have s: "proj_term (s ⋅ σ) = proj_mset proj_term (S ⋅⇩m σ) + proj_mset proj_term (U ⋅⇩m σ)"
    and t: "proj_term (t ⋅ σ) = proj_mset proj_term (T ⋅⇩m σ) + proj_mset proj_term (U ⋅⇩m σ)"
    by (auto simp: proj_term_subst [symmetric])
  have ne': "proj_mset proj_term (S ⋅⇩m σ) ≠ {#}"
    using S_ne
    by (auto dest!: proj_mset_empty simp: status_ne_imp_proj_term_ne [OF ne])
  { fix t' v assume "t' ∈# T" and v: "v ∈# proj_term (t' ⋅ σ)"
    with * obtain s' where "s' ∈ set_mset S" and "s' ⊳ t'" by force
    then have "s' ⋅ σ ⊳ t' ⋅ σ" by (auto dest: supt_subst)
    moreover have "t' ⋅ σ ⊵ v" by (rule proj_term_supteq [OF v])
    ultimately have "s' ⋅ σ ⊳ v" by (auto dest: supt_supteq_trans)
    moreover have "s' ⋅ σ ∈ set_mset (proj_term (s' ⋅ σ))"
    proof -
      have *: "s' ∈# proj_term s" using ‹s' ∈ set_mset S› by (auto simp: proj_s)
      show ?thesis
      apply (cases s', auto, insert ‹s' ⊳ t'›, blast)
      using * by (cases rule: proj_term_root) auto
    qed
    ultimately have "∃w ∈ set_mset S. ∃x ∈ set_mset (proj_term (w ⋅ σ)). x ⊳ v"
      using ‹s' ∈ set_mset S› by blast }
  then show ?thesis by (intro s_mul_ext_IdI [OF ne' s t]) auto
qed

theorem ac_subterm_proc: fixes P :: "('f,'v)trs"
  assumes fin: "finite_rel_dpp (P', Q', R, Rw, E)"
  and PQ: "⋀ l r. (l,r) ∈ P ∪ Q ⟹ l ⊵⇧π r"
  and RE: "⋀ l r. (l,r) ∈ R ∪ Rw ∪ E ⟹ root l ∈ Some ` F ⟹ l ⊵⇧π r"
  and P': "⋀ l r. (l,r) ∈ (P - P') ∪ (Q - Q') ⟹ l ⊳⇧π r"
  and E: "size_preserving_trs E" (* actually, size-non-increasing would suffice, but there is no definition for that *)
  and wf: "⋀ l r. (l,r) ∈ R ∪ Rw ∪ E ⟹ is_Fun l"
  shows "finite_rel_dpp (P, Q, R, Rw, E)"
proof (rule finite_rel_dpp_split_top[OF finite_rel_dpp_pairs_mono[OF fin]])  
  let ?S = "{(l,r). l ⊳⇧π r} :: ('f,'v)trs"
  def S ≡ ?S
  let ?S = "(relto {⊳} (rstep (R ∪ Rw ∪ E)))^+"
  let ?RE = "(rstep (R ∪ Rw ∪ E))^*"
  def relS ≡ "s_mul_ext ?RE ?S"
  def relNS ≡ "ns_mul_ext ?RE ?S"
  have subNS: "{⊵⇩#} ⊆ relNS" unfolding relNS_def
    by (rule ns_mul_ext_mono, auto)
  have subS: "{⊳⇩#} ⊆ relS" unfolding relS_def
    by (rule s_mul_ext_mono, auto)
  show "P - S ⊆ P'" "Q - S ⊆ P' ∪ Q'" using P' unfolding S_def by auto
  show "finite_rel_dpp (S ∩ (P ∪ Q), P ∪ Q - S, {}, R ∪ Rw, E)"
  proof
    fix s t σ
    assume "min_relchain (S ∩ (P ∪ Q), P ∪ Q - S, {}, R ∪ Rw, E) s t σ"
    hence chain: "min_relchain (S ∩ (P ∪ Q), P ∪ Q, {}, R ∪ Rw, E) s t σ" 
      unfolding min_relchain.simps by auto
    note chain = chain[unfolded min_relchain.simps, simplified]
    from chain have st: "⋀ i. (s i, t i) ∈ P ∪ Q" by auto
    let ?p = "proj_term"
    def ss ≡ "λ i. ?p (s (Suc i) ⋅ σ (Suc i))"
    def ts ≡ "λ i. ?p (t i ⋅ σ i)"
    {
      fix i
      from chain have steps: "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (rstep (R ∪ Rw ∪ E))⇧*" by auto
      have "(ts i, ss i) ∈ relNS^*" 
        unfolding ss_def ts_def relNS_def
        by (rule set_mp[OF rtrancl_mono[OF ns_mul_ext_mono] rsteps_proj_term[OF wf RE steps]], auto)
    } note ts = this
    have op: "order_pair ?S ?RE"
    proof (unfold_locales, goal_cases)
      case 4 show ?case by regexp
    next 
      case 5 show ?case by regexp
    qed (auto intro: trans_rtrancl refl_rtrancl)
    interpret order_pair relS relNS unfolding relS_def relNS_def
      using order_pair.mul_ext_order_pair[OF op] .
    {
      fix i
      from suptmulexeq_subst[OF PQ[OF st[of "Suc i"]]]
      have "ss i ⊵⇩# ts (Suc i)" unfolding ss_def ts_def .
      hence "(ss i, ts (Suc i)) ∈ relNS" using subNS by auto
      with ts[of i] have "(ts i, ts (Suc i)) ∈ relNS^*" by auto
      hence "(ts i, ts (Suc i)) ∈ relNS" unfolding rtrancl_NS .
    } note NS = this
    {
      fix i
      assume "(s (Suc i), t (Suc i)) ∈ S ∩ (P ∪ Q)"
      hence "s (Suc i) ⊳⇧π t (Suc i)" unfolding S_def by auto
      from suptmulex_subst[OF this]
      have "ss i ⊳⇩# ts (Suc i)" unfolding ss_def ts_def .
      hence "(ss i, ts (Suc i)) ∈ relS" using subS by auto
      with ts[of i] have "(ts i, ts (Suc i)) ∈ relNS^* O relS" by auto
      hence "(ts i, ts (Suc i)) ∈ relS" by (simp add: order_simps)
    } note S = this
    have "SN_on relS {ts 0}" unfolding relS_def
    proof (rule SN_s_mul_ext_strong[OF op], intro allI impI)
      fix ti
      assume "ti ∈# ts 0"
      from this[unfolded ts_def] have sub: "t 0 ⋅ σ 0 ⊵ ti" by (rule proj_term_supteq)
      let ?relac = "relstep (R ∪ Rw) E"
      have ctxt: "ctxt.closed ?relac" by (rule ctxt.closed_relto, auto)
      from chain have "SN_on ?relac {t 0 ⋅ σ 0}" by auto
      from ctxt_closed_SN_on_subt [OF ctxt this sub]
      have SN: "SN_on ?relac {ti}" .

      let ?T = "{t. SN_on ?relac {t}}"
      let ?rel = "?relac ∪ relto {⊳} (rstep E)"
      let ?RE = "rstep (R ∪ Rw ∪ E)"
      let ?R = "rstep (R ∪ Rw)"
      let ?E = "rstep E"
      interpret E_compatible ?relac "(rstep E)⇧*"
        by (standard, auto)
      interpret size_preserving_trs E by fact
      note SN_E = SN_suptrel[unfolded suptrel_def]  
      have "SN_on ?rel ?T"
        by (rule ctxt_closed_imp_SN_on_E_supt[OF ctxt SN_subset[OF SN_E]], regexp)
      with SN have "SN_on ?rel {ti}" unfolding SN_defs by blast
      hence "SN_on (?rel^+) {ti}" unfolding SN_on_trancl_SN_on_conv .
      hence "SN_on (relto ?R ({⊳} ∪ ?E)) {ti}" by (rule SN_on_mono) regexp
      hence SN: "SN_rel_on ?R ({⊳} ∪ ?E) {ti}" unfolding SN_rel_on_def .
      have "SN_on (relto {⊳} ?RE) {ti}" 
      proof (rule ccontr)
        assume "¬ ?thesis"
        hence "¬ SN_rel_on {⊳} ?RE {ti}" unfolding SN_rel_on_def by auto
        from this[unfolded SN_rel_on_ideriv] obtain f where
          f: "ideriv {⊳} ?RE f" and f0: "f 0 = ti" by auto
        from f have inf: "∃⇩∞i. f i ⊳ f (Suc i)" unfolding ideriv_def by auto
        show False
        proof (cases "INFM i. (f i, f (Suc i)) ∈ ?R")
          case False
          then obtain j where j: "⋀ i. i ≥ j ⟹ (f i, f (Suc i)) ∉ ?R" unfolding INFM_nat_le by blast
          def g ≡ "shift f j"
          have inf: "∃⇩∞i. g i ⊳ g (Suc i)" using inf unfolding g_def 
            using Infm_double_shift[of "λ x y. x ⊳ y" f j "shift f 1"]
            by auto
          {
            fix i
            from f have "(f (i + j), f (Suc (i + j))) ∈ {⊳} ∪ ?RE" unfolding ideriv_def by auto
            with j[of "i + j"] have "(g i, g (Suc i)) ∈ {⊳} ∪ ?E" unfolding rstep_union g_def by auto
          }
          hence "ideriv {⊳} ?E g" using inf by (auto simp: ideriv_def)
          hence nSN: "¬ SN_rel {⊳} ?E" unfolding SN_rel_ideriv by auto
          interpret size_preserving_trs E by fact
          from SN_suptrel[unfolded suptrel_def] nSN[unfolded SN_rel_on_def] 
          show False unfolding SN_trancl_SN_conv by blast
        next
          case True
          with f have "ideriv ?R ({⊳} ∪ ?E) f" unfolding ideriv_def rstep_union by auto
          hence "¬ SN_rel_on ?R ({⊳} ∪ ?E) {ti}" using f0 unfolding SN_rel_on_ideriv by auto
          with SN show False by blast
        qed
      qed
      thus "SN_on ?S {ti}" unfolding SN_on_trancl_SN_on_conv .
    qed
    from non_strict_ending[of ts, OF _ compat_NS_S this] NS
    obtain j where j: "⋀ i. i ≥ j ⟹ (ts i, ts (Suc i)) ∉ relS" by auto
    from chain[unfolded INFM_nat] obtain i where i: "i > j" and st: "(s i, t i) ∈ S ∩ (P ∪ Q)" by blast
    def k ≡ "i - 1"
    from i st have k: "k ≥ j" and st: "(s (Suc k), t (Suc k)) ∈ S ∩ (P ∪ Q)" unfolding k_def by auto
    from S[OF st] j[OF k] show False by auto
  qed
qed

corollary generalized_subterm_proc:
  fixes P :: "('f, 'v) trs"
  assumes fin: "finite_dpp (nfs, True, P', Pw', {},  R, Rw)"
  and P: "⋀ l r. (l,r) ∈ P ∪ Pw ⟹ l ⊵⇧π r"
  and R: "⋀ l r. (l,r) ∈ R ∪ Rw ⟹ root l ∈ Some ` F ⟹ l ⊵⇧π r"
  and P': "⋀ l r. (l,r) ∈ (P - P') ∪ (Pw - Pw') ⟹ l ⊳⇧π r"
  and wf: "⋀ l r. (l,r) ∈ R ∪ Rw ⟹ is_Fun l"
  shows "finite_dpp (nfs, True, P, Pw, {}, R, Rw)"
  unfolding finite_dpp_via_finite_rel_dpp
  by (rule ac_subterm_proc[OF fin[unfolded finite_dpp_via_finite_rel_dpp] P R P' _ wf], auto)  
end

end

end