theory Commutation_Ex imports "$AFP/Abstract-Rewriting/Abstract_Rewriting" begin text \@{theory Abstract_Rewriting} defines commutation as follows\ lemma "commute r s \ ((r\)\<^sup>* O s\<^sup>*) \ (s\<^sup>* O (r\)\<^sup>*)" by (rule commute_def) text \To use this definition the following introduction and destruction rules turn out to be useful\ lemma commuteI [intro]: "(\x y\<^sub>1 y\<^sub>2. (x, y\<^sub>1) \ r\<^sub>1\<^sup>* \ (x, y\<^sub>2) \ r\<^sub>2\<^sup>* \ \z. (y\<^sub>1, z) \ r\<^sub>2\<^sup>* \ (y\<^sub>2, z) \ r\<^sub>1\<^sup>*) \ 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) \ r\<^sub>1\<^sup>*" and "(x, z) \ r\<^sub>2\<^sup>*" shows "\u. (z, u) \ r\<^sub>1\<^sup>* \ (y, u) \ r\<^sub>2\<^sup>*" proof - from assms have "(y, z) \ (r\<^sub>1\)\<^sup>* O r\<^sub>2\<^sup>*" using rtrancl_converseI by fast with assms have "(y, z) \ r\<^sub>2\<^sup>* O (r\<^sub>1\)\<^sup>*" unfolding commute_def by auto then show ?thesis by (metis converseD relcomp.cases rtrancl_converse) qed text \We now define strong commutation\ definition strongly_commute :: "'a rel \ 'a rel \ bool" where "strongly_commute r\<^sub>1 r\<^sub>2 \ (\x y\<^sub>1 y\<^sub>2. (x, y\<^sub>1) \ r\<^sub>1 \ (x, y\<^sub>2) \ r\<^sub>2 \ (\z. (y\<^sub>1, z) \ r\<^sub>2\<^sup>= \ (y\<^sub>2, z) \ r\<^sub>1\<^sup>*))" text \Exercise: prove that strong commutation implies commutation\ lemma strongly_commute_imp_commute: assumes "strongly_commute r s" shows "commute r s" oops end