theory Commutation_Ex
  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 and destruction rules turn 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)

lemma commuteD [dest]:
  assumes "commute r\<^sub>1 r\<^sub>2"
    and "(x, y) \<in> r\<^sub>1\<^sup>*"
    and "(x, z) \<in> r\<^sub>2\<^sup>*"
  shows "\<exists>u. (z, u) \<in> r\<^sub>1\<^sup>* \<and> (y, u) \<in> r\<^sub>2\<^sup>*"
proof -
  from assms have "(y, z) \<in> (r\<^sub>1\<inverse>)\<^sup>* O r\<^sub>2\<^sup>*" using rtrancl_converseI by fast
  with assms have "(y, z) \<in>  r\<^sub>2\<^sup>* O (r\<^sub>1\<inverse>)\<^sup>*" unfolding commute_def  by auto
  then show ?thesis by (metis converseD relcomp.cases rtrancl_converse)
qed

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

end