Theory TRS.More_Abstract_Rewriting

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2017)
Author:  Julian Nagele <julian.nagele@uibk.ac.at> (2017)
License: LGPL (see file COPYING.LESSER)
*)
theory More_Abstract_Rewriting
  imports
    "Abstract-Rewriting.Abstract_Rewriting"
    "Decreasing-Diagrams-II.Decreasing_Diagrams_II"
begin

section ‹Results that belong to @‹theory Abstract_Rewriting››

lemma rtrancl_eq_CR:
  assumes "r* = s*"
  shows "CR r ⟷ CR s"
  using assms by (auto simp: CR_defs join_def rtrancl_converse)

lemma diamond_I':
  assumes "⋀ s t u. (s, t) ∈ r ⟹ (s, u) ∈ r ⟹ ∃ v. (t, v) ∈ r ∧ (u, v) ∈ r"
  shows "◇ r"
  apply (intro diamond_I subrelI)
  apply (auto dest: relcompE)
  subgoal for t s u
    using assms[of s u t] by auto
  done

subsection ‹Commutation›

text ‹Short notation for diamond commutation of two relations.›
definition "comm r s ⟷
  (∀x y z. (x, y) ∈ r ∧ (x, z) ∈ s ⟶ (∃u. (y, u) ∈ s ∧ (z, u) ∈ r))"

lemma commI [intro?]:
  assumes "⋀x y z. ⟦(x, y) ∈ r; (x, z) ∈ s⟧ ⟹ (∃u. (y, u) ∈ s ∧ (z, u) ∈ r)"
  shows "comm r s"
  using assms by (auto simp: comm_def)

lemma commE:
  assumes "comm r s" and "(x, y) ∈ r" and "(x, z) ∈ s"
  obtains u where "(y, u) ∈ s" and "(z, u) ∈ r"
  using assms by (force simp: comm_def)

lemma comm_swap:
  "comm r s ⟷ comm s r"
  by (auto elim: commE intro!: commI)

lemma comm_rtrancl:
  assumes "comm r s"
  shows "comm (r*) s"
proof
  fix x y z
  assume "(x, y) ∈ r*" and "(x, z) ∈ s"
  then show "∃u. (y, u) ∈ s ∧ (z, u) ∈ r*" (is "∃u. ?P u y z")
  proof (induct)
    case base
    moreover have "(z, z) ∈ r*" by blast
    ultimately show ?case by blast
  next
    case (step a b)
    then obtain u where "(a, u) ∈ s" and "(z, u) ∈ r*" by blast
    moreover with ‹(a, b) ∈ r› and ‹comm r s› obtain v
      where "(b, v) ∈ s" and "(u, v) ∈ r*" by (blast elim: commE)
    ultimately have "(b, v) ∈ s" and "(z, v) ∈ r*" by auto
    then show ?case by blast
  qed
qed

definition locally_commute :: "'a rel ⇒ 'a rel  ⇒ bool"
where
  "locally_commute r1 r2 ⟷
    (∀x y1 y2. (x, y1) ∈ r1 ∧ (x, y2) ∈ r2 ⟶ (∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*))"

lemma locally_commute_E11:
  "locally_commute r1 r2 ⟹ (x, y) ∈ r1 ⟹ (x, z) ∈ r2 ⟹
    ∃u. (z, u) ∈ r1* ∧ (y, u) ∈ r2*"
unfolding locally_commute_def by blast

lemma locally_commuteI [intro]:
  "⟦⋀x y1 y2. (x, y1) ∈ r1 ⟹ (x, y2) ∈ r2 ⟹ ∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*⟧ ⟹ locally_commute r1 r2"
unfolding locally_commute_def by auto

definition strongly_commute :: "'a rel ⇒ 'a rel  ⇒ bool"
where
  "strongly_commute r1 r2 ⟷
    (∀x y1 y2. (x, y1) ∈ r1 ∧ (x, y2) ∈ r2 ⟶ (∃z. (y1, z) ∈ r2= ∧ (y2, z) ∈ r1*))"

lemma strongly_commute_E11:
  "strongly_commute r1 r2 ⟹ (x, y) ∈ r1 ⟹ (x, z) ∈ r2 ⟹
    ∃u. (z, u) ∈ r1* ∧ (y, u) ∈ r2="
unfolding strongly_commute_def by blast

lemma strongly_commuteI [intro]:
  "⟦⋀x y1 y2. (x, y1) ∈ r1 ⟹ (x, y2) ∈ r2 ⟹ ∃z. (y1, z) ∈ r2= ∧ (y2, z) ∈ r1*⟧ ⟹ strongly_commute r1 r2"
unfolding strongly_commute_def by auto

lemma commuteI [intro]:
  "⟦⋀x y1 y2. (x, y1) ∈ r1* ⟹ (x, y2) ∈ r2* ⟹ ∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*⟧ ⟹ commute r1 r2"
unfolding commute_def by auto (metis converse_converse relcomp.simps rtrancl_converseD)

lemma commuteE:
  assumes "commute r1 r2"
    and "(x, y) ∈ r1*"
    and "(x, z) ∈ r2*"
  shows "∃u. (z, u) ∈ r1* ∧ (y, u) ∈ r2*"
proof -
  from assms have "(y, z) ∈ (r1¯)* O r2*" using rtrancl_converseI by fast
  with assms have "(y, z) ∈  r2* O (r1¯)*" unfolding commute_def  by auto
  then show ?thesis by (metis converseD relcomp.cases rtrancl_converse)
qed

definition semi_commute  :: "'a rel ⇒ 'a rel  ⇒ bool"
where
  "semi_commute r1 r2 ⟷
    (∀x y1 y2. (x, y1) ∈ r1 ∧ (x, y2) ∈ r2* ⟶ (∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*))"

lemma semi_commute_iff_commute:
  "semi_commute r1 r2 ⟷ commute r1 r2"
proof
  assume "commute r1 r2"
  then show "semi_commute r1 r2"
  unfolding semi_commute_def by (auto dest: commuteE)
next
  assume *:"semi_commute r1 r2"
  show "commute r1 r2"
  proof
    fix x y1 y2
    assume "(x, y1) ∈ r1*" and 2:"(x, y2) ∈ r2*"
    then obtain n where "(x, y1) ∈ r1^^n" by auto
    then show "∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*"
    proof (induct n arbitrary: y1)
      case 0 then show ?case using 2 by auto
    next
      case (Suc n)
      then obtain yn where "(x, yn) ∈ r1 ^^ n" and 1:"(yn, y1) ∈ r1" by auto
      with Suc obtain z where "(yn, z) ∈ r2* ∧ (y2, z) ∈ r1*" by auto
      with 1 2 * show ?case unfolding semi_commute_def using rtrancl_trans by metis
    qed
  qed
qed

lemma strongly_commute_E1n:
  assumes "strongly_commute r1 r2"
  shows "(x, y) ∈ r2= ⟹ (x, z) ∈ r1 ^^ n ⟹ ∃u. (y, u) ∈ r1* ∧ (z, u) ∈ r2="
proof (induct n arbitrary: x y z)
  case (Suc m)
  from Suc(3) obtain w where xw: "(x, w) ∈ r1^^m" and wz: "(w, z) ∈ r1" by auto
  from Suc(1) [OF Suc(2) xw] obtain u where yu: "(y, u) ∈ r1*" and wu: "(w, u) ∈ r2=" by auto
  then have "w = u ∨ (w, u) ∈ r2" by auto
  then show ?case
  proof
    assume "w = u"
    with yu wz have "(y, z) ∈ r1*" by auto
    then show ?thesis by blast
  next
    assume "(w, u) ∈ r2"
    from strongly_commute_E11 [OF assms wz this] yu show ?thesis using rtrancl_trans by metis
  qed
qed auto

lemma strongly_commute_imp_commute:
  assumes "strongly_commute r1 r2"
  shows "commute r1 r2"
proof -
  have "semi_commute r1 r2" unfolding semi_commute_def
  proof (intro allI impI)
    fix x y1 y2
    assume *:"(x, y1) ∈ r1 ∧ (x, y2) ∈ r2*"
    then obtain n where "(x, y2) ∈ r2 ^^ n" and "(x, y1) ∈ r1" by auto
    then show "∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*"
    proof (induct n arbitrary: y2)
      case (Suc n)
      then obtain y where "(x, y) ∈ r2 ^^ n" and "(y, y2) ∈ r2" by auto
      from Suc(1)[OF this(1) Suc(3)] obtain z where yz:"(y1, z) ∈ r2*" "(y, z) ∈ r1* " by auto
      from ‹(y, y2) ∈ r2› have "(y, y2) ∈ r2=" by auto
      from strongly_commute_E1n[OF assms this] yz obtain u where "(y2, u) ∈ r1* ∧ (z, u) ∈ r2="
        by blast
      moreover with yz have "(y1, u) ∈ r2*" by auto
      ultimately show ?case by auto
    qed auto
  qed
  with semi_commute_iff_commute show ?thesis ..
qed

lemma comm_imp_commute:
  assumes "comm r s"
  shows "commute r s"
by (metis assms commE comm_rtrancl comm_swap commuteI)

lemma commute_between_imp_commute:
  assumes "commute s1 s2" and "r1 ⊆ s1" and "s1 ⊆ r1*" and "r2 ⊆ s2" and "s2 ⊆ r2*"
  shows "commute r1 r2"
proof
  fix x y1 y2
  assume "(x, y1) ∈ r1*" and "(x, y2) ∈ r2*"
  then have "(x, y1) ∈ s1*" and "(x, y2) ∈ s2*"
    using assms rtrancl_subset by blast+
  then obtain v where "(y1, v) ∈ s2*" and "(y2, v) ∈ s1*"
    using assms(1) by (auto dest : commuteE)
  then show "∃z. (y1, z) ∈ r2* ∧ (y2, z) ∈ r1*"
    using assms rtrancl_subset by blast
qed

lemma comm_between_imp_commute:
  assumes "comm s1 s2" and "r1 ⊆ s1" and "s1 ⊆ r1*" and "r2 ⊆ s2" and "s2 ⊆ r2*"
  shows "commute r1 r2"
using commute_between_imp_commute comm_imp_commute assms by blast

lemma CR_between_imp_CR:
  assumes "CR s" and "r ⊆ s" and "s ⊆ r*" shows "CR r"
using commute_between_imp_commute CR_iff_self_commute assms by blast

lemma Newman_commute:
  assumes sn: "SN (R ∪ S)" and lc: "locally_commute R S"
  shows "commute R S"
proof -
  let ?R = "λs. {(s,t) |t. (s,t) ∈ R}"
  let ?S = "λs. {(s,t) |t. (s,t) ∈ S}"
  let ?r = "((R ∪ S)¯)+"
  have R: "(⋃i. ?R i) = R" and S: "(⋃i. ?S i) = S" by auto
  show ?thesis
  proof (intro dd_commute[of "?r" ?R ?S, unfolded R S], goal_cases)
    case (3 a b s t u)
    have [simp]: "a = s" "b = s" using 3 by auto
    have "(s, t) ∈ R" "(s, u) ∈ S" and c: "(t, s) ∈ ?r" "(u, s) ∈ ?r" using 3 by auto
    then obtain v where v: "(t, v) ∈ S*" "(u, v) ∈ R*" using lc
      by (auto simp: peak_iff rtrancl_converse dest: locally_commute_E11)
    have "(t, v) ∈ conversion'' ?R ?S (under ?r s)" using v(1) c(1)
    proof (induct rule: converse_rtrancl_induct)
      case (step y z)
      have "(z, s) ∈ ((R ∪ S)¯)+" using step(1,4)
        by (intro trancl_into_trancl2[of z y]) auto
      moreover have "(y, z) ∈ conversion'' ?R ?S (under ?r s)"
        using step(1,4) by (auto simp: under_def)
      ultimately show ?case using step by auto
    qed auto
    moreover have "(v, u) ∈ conversion'' ?R ?S (under ?r s)" using v(2) c(2)
    proof (induct rule: converse_rtrancl_induct)
      case (step y z)
      have "(z, s) ∈ ((R ∪ S)¯)+" using step(1,4)
        by (intro trancl_into_trancl2[of z y]) auto
      moreover have "(z, y) ∈ conversion'' ?R ?S (under ?r s)"
        using step(1,4) by (auto simp: under_def)
      ultimately show ?case using step by auto
    qed auto
    ultimately show ?case
      by (intro relcompI[OF _ relcompI[OF _ relcompI[OF _ relcompI]], of t v _ v _ v _ v _ u]) auto
  qed (insert sn, auto intro: wf_trancl simp: SN_iff_wf)
qed

end