diff -r a3f7f00b4fd8 -r fce780f9c9c6 src/HOL/Library/Confluent_Quotient.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Confluent_Quotient.thy	Sun Jan 19 07:50:35 2020 +0100
@@ -0,0 +1,74 @@
+theory Confluent_Quotient imports 
+  Confluence
+begin
+
+section \<open>Subdistributivity for quotients via confluence\<close>
+
+locale confluent_quotient =
+  fixes R :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool"
+    and Ea :: "'Fa \<Rightarrow> 'Fa \<Rightarrow> bool"
+    and Eb :: "'Fb \<Rightarrow> 'Fb \<Rightarrow> bool"
+    and Ec :: "'Fc \<Rightarrow> 'Fc \<Rightarrow> bool"
+    and Eab :: "'Fab \<Rightarrow> 'Fab \<Rightarrow> bool"
+    and Ebc :: "'Fbc \<Rightarrow> 'Fbc \<Rightarrow> bool"
+    and \<pi>_Faba :: "'Fab \<Rightarrow> 'Fa"
+    and \<pi>_Fabb :: "'Fab \<Rightarrow> 'Fb"
+    and \<pi>_Fbcb :: "'Fbc \<Rightarrow> 'Fb"
+    and \<pi>_Fbcc :: "'Fbc \<Rightarrow> 'Fc"
+    and rel_Fab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fb \<Rightarrow> bool"
+    and rel_Fbc :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fb \<Rightarrow> 'Fc \<Rightarrow> bool"
+    and rel_Fac :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'Fa \<Rightarrow> 'Fc \<Rightarrow> bool"
+    and set_Fab :: "'Fab \<Rightarrow> ('a \<times> 'b) set"
+    and set_Fbc :: "'Fbc \<Rightarrow> ('b \<times> 'c) set"
+  assumes confluent: "confluentp R"
+    and retract1_ab: "\<And>x y. R (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z"
+    and retract1_bc: "\<And>x y. R (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z"
+    and generated: "Eb \<le> equivclp R"
+    and set_ab: "\<And>x y. Eab x y \<Longrightarrow> set_Fab x = set_Fab y"
+    and set_bc: "\<And>x y. Ebc x y \<Longrightarrow> set_Fbc x = set_Fbc y"
+    and transp_a: "transp Ea"
+    and transp_c: "transp Ec"
+    and equivp_ab: "equivp Eab"
+    and equivp_bc: "equivp Ebc"
+    and in_rel_Fab: "\<And>A x y. rel_Fab A x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fab x \<subseteq> {(x, y). A x y}} \<and> \<pi>_Faba z = x \<and> \<pi>_Fabb z = y)"
+    and in_rel_Fbc: "\<And>B x y. rel_Fbc B x y \<longleftrightarrow> (\<exists>z. z \<in> {x. set_Fbc x \<subseteq> {(x, y). B x y}} \<and> \<pi>_Fbcb z = x \<and> \<pi>_Fbcc z = y)"
+    and rel_compp: "\<And>A B. rel_Fac (A OO B) = rel_Fab A OO rel_Fbc B"
+    and \<pi>_Faba_respect: "rel_fun Eab Ea \<pi>_Faba \<pi>_Faba"
+    and \<pi>_Fbcc_respect: "rel_fun Ebc Ec \<pi>_Fbcc \<pi>_Fbcc"
+begin
+
+lemma retract_ab: "R\<^sup>*\<^sup>* (\<pi>_Fabb x) y \<Longrightarrow> \<exists>z. Eab x z \<and> y = \<pi>_Fabb z"
+  by(induction rule: rtranclp_induct)(blast dest: retract1_ab intro: equivp_transp[OF equivp_ab] equivp_reflp[OF equivp_ab])+
+
+lemma retract_bc: "R\<^sup>*\<^sup>* (\<pi>_Fbcb x) y \<Longrightarrow> \<exists>z. Ebc x z \<and> y = \<pi>_Fbcb z"
+  by(induction rule: rtranclp_induct)(blast dest: retract1_bc intro: equivp_transp[OF equivp_bc] equivp_reflp[OF equivp_bc])+
+
+lemma subdistributivity: "rel_Fab A OO Eb OO rel_Fbc B \<le> Ea OO rel_Fac (A OO B) OO Ec"
+proof(rule predicate2I; elim relcomppE)
+  fix x y y' z
+  assume "rel_Fab A x y" and "Eb y y'" and "rel_Fbc B y' z"
+  then obtain xy y'z
+    where xy: "set_Fab xy \<subseteq> {(a, b). A a b}" "x = \<pi>_Faba xy" "y = \<pi>_Fabb xy"
+      and y'z: "set_Fbc y'z \<subseteq> {(a, b). B a b}" "y' = \<pi>_Fbcb y'z" "z = \<pi>_Fbcc y'z"
+    by(auto simp add: in_rel_Fab in_rel_Fbc)
+  from \<open>Eb y y'\<close> have "equivclp R y y'" using generated by blast
+  then obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
+    unfolding semiconfluentp_equivclp[OF confluent[THEN confluentp_imp_semiconfluentp]]
+    by(auto simp add: rtranclp_conversep)
+  with xy y'z obtain xy' y'z'
+    where retract1: "Eab xy xy'" "\<pi>_Fabb xy' = u"
+      and retract2: "Ebc y'z y'z'" "\<pi>_Fbcb y'z' = u"
+    by(auto dest!: retract_ab retract_bc)
+  from retract1(1) xy have "Ea x (\<pi>_Faba xy')" by(auto dest: \<pi>_Faba_respect[THEN rel_funD])
+  moreover have "rel_Fab A (\<pi>_Faba xy') u" using xy retract1
+    by(auto simp add: in_rel_Fab dest: set_ab)
+  moreover have "rel_Fbc B u (\<pi>_Fbcc y'z')" using y'z retract2
+    by(auto simp add: in_rel_Fbc dest: set_bc)
+  moreover have "Ec (\<pi>_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc]
+    by(auto dest: \<pi>_Fbcc_respect[THEN rel_funD])
+  ultimately show "(Ea OO rel_Fac (A OO B) OO Ec) x z" unfolding rel_compp by blast
+qed
+
+end
+
+end
\ No newline at end of file