theory Commutation
  imports
    "$AFP/Abstract-Rewriting/Abstract_Rewriting"
begin

text \<open>@{theory Abstract_Rewriting} defines commutation as follows\<close>

lemma "commute r s \<longleftrightarrow> ((r\<inverse>)\<^sup>* O s\<^sup>*) \<subseteq> (s\<^sup>* O (r\<inverse>)\<^sup>*)"
  by (rule commute_def)

text \<open>To use this definition the following introduction rule turns out to be useful\<close>

lemma commuteI [intro]:
  "(\<And>x y\<^sub>1 y\<^sub>2. (x, y\<^sub>1) \<in> r\<^sub>1\<^sup>* \<Longrightarrow> (x, y\<^sub>2) \<in> r\<^sub>2\<^sup>* \<Longrightarrow> \<exists>z. (y\<^sub>1, z) \<in> r\<^sub>2\<^sup>* \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*) \<Longrightarrow> commute r\<^sub>1 r\<^sub>2"
unfolding commute_def by auto (metis converse_converse relcomp.simps rtrancl_converseD)

text \<open>We now define strong commutation\<close>

definition strongly_commute :: "'a rel \<Rightarrow> 'a rel  \<Rightarrow> bool"
where
  "strongly_commute r\<^sub>1 r\<^sub>2 \<longleftrightarrow>
    (\<forall>x y\<^sub>1 y\<^sub>2. (x, y\<^sub>1) \<in> r\<^sub>1 \<and> (x, y\<^sub>2) \<in> r\<^sub>2 \<longrightarrow> (\<exists>z. (y\<^sub>1, z) \<in> r\<^sub>2\<^sup>= \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*))"

text \<open>Exercise: prove that strong commutation implies commutation\<close>

lemma strongly_commute_imp_commute:
  assumes "strongly_commute r s"
  shows "commute r s"
  oops

text \<open>Here's a possible Solution\<close>

definition semi_commute :: "'a rel \<Rightarrow> 'a rel  \<Rightarrow> bool"
where
  "semi_commute r\<^sub>1 r\<^sub>2 \<longleftrightarrow>
    (\<forall>x y\<^sub>1 y\<^sub>2. (x, y\<^sub>1) \<in> r\<^sub>1 \<and> (x, y\<^sub>2) \<in> r\<^sub>2\<^sup>* \<longrightarrow> (\<exists>z. (y\<^sub>1, z) \<in> r\<^sub>2\<^sup>* \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*))"

lemma semi_commute_imp_commute:
  "semi_commute r\<^sub>1 r\<^sub>2 \<Longrightarrow> commute r\<^sub>1 r\<^sub>2"
proof
  fix x y\<^sub>1 y\<^sub>2
  assume *:"semi_commute r\<^sub>1 r\<^sub>2" and "(x, y\<^sub>1) \<in> r\<^sub>1\<^sup>*" and 2:"(x, y\<^sub>2) \<in> r\<^sub>2\<^sup>*"
  then obtain n where "(x, y\<^sub>1) \<in> r\<^sub>1 ^^ n" by auto
  then show "\<exists>z. (y\<^sub>1, z) \<in> r\<^sub>2\<^sup>* \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*"
  proof (induct n arbitrary: y\<^sub>1)
    case 0 then show ?case using 2 by auto
  next
    case (Suc n)
    then obtain y\<^sub>n where "(x, y\<^sub>n) \<in> r\<^sub>1 ^^ n" and 1:"(y\<^sub>n, y\<^sub>1) \<in> r\<^sub>1" by auto
    then obtain z where "(y\<^sub>n, z) \<in> r\<^sub>2\<^sup>* \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*" using Suc by auto
    then show ?case using rtrancl_trans 1 2 * unfolding semi_commute_def by metis
  qed
qed

lemma strongly_commute_D1n:
  assumes "strongly_commute r\<^sub>1 r\<^sub>2"
  shows "(x, y) \<in> r\<^sub>2 \<Longrightarrow> (x, z) \<in> r\<^sub>1 ^^ n \<Longrightarrow> \<exists>u. (y, u) \<in> r\<^sub>1\<^sup>* \<and> (z, u) \<in> r\<^sub>2\<^sup>="
proof (induct n arbitrary: x y z)
  case (Suc m)
  from Suc(3) obtain w where xw: "(x, w) \<in> r\<^sub>1 ^^ m" and wz: "(w, z) \<in> r\<^sub>1" by auto
  with Suc obtain u where yu: "(y, u) \<in> r\<^sub>1\<^sup>*" and wu: "(w, u) \<in> r\<^sub>2\<^sup>=" by blast
  then have "w = u \<or> (w, u) \<in> r\<^sub>2" by auto
  then show ?case
  proof (rule disjE)
    assume "w = u"
    then have "(y, z) \<in> r\<^sub>1\<^sup>*" using yu wz by auto
    then show ?thesis by blast
  next
    assume "(w, u) \<in> r\<^sub>2"
    then obtain t where "\<exists>ua. (u, t) \<in> r\<^sub>1\<^sup>* \<and> (z, t) \<in> r\<^sub>2\<^sup>="
      using assms wz unfolding strongly_commute_def by blast
    then show ?thesis using rtrancl_trans yu by metis
  qed
qed auto

lemma strongly_commute_imp_commute:
  assumes "strongly_commute r\<^sub>1 r\<^sub>2"
  shows "commute r\<^sub>1 r\<^sub>2"
proof (rule semi_commute_imp_commute)
  show "semi_commute r\<^sub>1 r\<^sub>2" unfolding semi_commute_def
  proof (intro allI impI)
    fix x y\<^sub>1 y\<^sub>2
    assume "(x, y\<^sub>1) \<in> r\<^sub>1 \<and> (x, y\<^sub>2) \<in> r\<^sub>2\<^sup>*"
    then obtain n where "(x, y\<^sub>2) \<in> r\<^sub>2 ^^ n" and "(x, y\<^sub>1) \<in> r\<^sub>1" by auto
    then show "\<exists>z. (y\<^sub>1, z) \<in> r\<^sub>2\<^sup>* \<and> (y\<^sub>2, z) \<in> r\<^sub>1\<^sup>*"
    proof (induct n arbitrary: y\<^sub>2)
      case (Suc n)
      then obtain y where "(x, y) \<in> r\<^sub>2 ^^ n" and "(y, y\<^sub>2) \<in> r\<^sub>2" by auto
      with Suc obtain z where y\<^sub>1z:"(y\<^sub>1, z) \<in> r\<^sub>2\<^sup>*" and "(y, z) \<in> r\<^sub>1\<^sup>* " by auto
      then obtain u where u: "(y\<^sub>2, u) \<in> r\<^sub>1\<^sup>* \<and> (z, u) \<in> r\<^sub>2\<^sup>="
        using assms \<open>(y, y\<^sub>2) \<in> r\<^sub>2\<close> by (auto dest: strongly_commute_D1n)
      moreover have "(y\<^sub>1, u) \<in> r\<^sub>2\<^sup>*" using y\<^sub>1z u by auto
      ultimately show ?case by auto
    qed auto
  qed
qed

end