theory Confluent_Quotient imports
Confluence
begin
section \<open>Subdistributivity for quotients via confluence\<close>
locale confluent_quotient =
fixes R :: "'Fb \ 'Fb \ bool"
and Ea :: "'Fa \ 'Fa \ bool"
and Eb :: "'Fb \ 'Fb \ bool"
and Ec :: "'Fc \ 'Fc \ bool"
and Eab :: "'Fab \ 'Fab \ bool"
and Ebc :: "'Fbc \ 'Fbc \ 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 \ 'b \ bool) \ 'Fa \ 'Fb \ bool"
and rel_Fbc :: "('b \ 'c \ bool) \ 'Fb \ 'Fc \ bool"
and rel_Fac :: "('a \ 'c \ bool) \ 'Fa \ 'Fc \ bool"
and set_Fab :: "'Fab \ ('a \ 'b) set"
and set_Fbc :: "'Fbc \ ('b \ 'c) set"
assumes confluent: "confluentp R"
and retract1_ab: "\x y. R (\_Fabb x) y \ \z. Eab x z \ y = \_Fabb z"
and retract1_bc: "\x y. R (\_Fbcb x) y \ \z. Ebc x z \ y = \_Fbcb z"
and generated: "Eb \ equivclp R"
and set_ab: "\x y. Eab x y \ set_Fab x = set_Fab y"
and set_bc: "\x y. Ebc x y \ 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: "\A x y. rel_Fab A x y \ (\z. z \ {x. set_Fab x \ {(x, y). A x y}} \ \_Faba z = x \ \_Fabb z = y)"
and in_rel_Fbc: "\B x y. rel_Fbc B x y \ (\z. z \ {x. set_Fbc x \ {(x, y). B x y}} \ \_Fbcb z = x \ \_Fbcc z = y)"
and rel_compp: "\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>* (\_Fabb x) y \ \z. Eab x z \ y = \_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>* (\_Fbcb x) y \ \z. Ebc x z \ y = \_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 \ 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 \ {(a, b). A a b}" "x = \_Faba xy" "y = \_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'" "\_Fabb xy' = u"
and retract2: "Ebc y'z y'z'" "\_Fbcb y'z' = u"
by(auto dest!: retract_ab retract_bc)
from retract1(1) xy have "Ea x (\_Faba xy')" by(auto dest: \_Faba_respect[THEN rel_funD])
moreover have "rel_Fab A (\_Faba xy') u" using xy retract1
by(auto simp add: in_rel_Fab dest: set_ab)
moreover have "rel_Fbc B u (\_Fbcc y'z')" using y'z retract2
by(auto simp add: in_rel_Fbc dest: set_bc)
moreover have "Ec (\_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
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
