Theory Confluent_Quotient

theory Confluent_Quotient imports 
  Confluence
begin

section ‹Subdistributivity for quotients via confluence›

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 π_Faba :: "'Fab ⇒ 'Fa"
    and π_Fabb :: "'Fab ⇒ 'Fb"
    and π_Fbcb :: "'Fbc ⇒ 'Fb"
    and π_Fbcc :: "'Fbc ⇒ '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 π_Faba_respect: "rel_fun Eab Ea π_Faba π_Faba"
    and π_Fbcc_respect: "rel_fun Ebc Ec π_Fbcc π_Fbcc"
begin

lemma retract_ab: "R⇧*⇧* (π_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⇧*⇧* (π_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 ⊆ {(a, b). B a b}" "y' = π_Fbcb y'z" "z = π_Fbcc y'z"
    by(auto simp add: in_rel_Fab in_rel_Fbc)
  from ‹Eb y y'› have "equivclp R y y'" using generated by blast
  then obtain u where u: "R⇧*⇧* y u" "R⇧*⇧* 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: π_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