Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Confluent_Quotient.thy Sprache: Isabelle

Original von: Isabelle^©

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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.