# Theory Confluent_Quotient

theory Confluent_Quotient imports
Confluence
begin

text βΉFunctors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.βΊ

lemma Inter_finite_subset:
assumes "βA β π. finite A"
shows "ββ¬βπ. finite β¬ β§ (ββ¬) = (βπ)"
proof(cases "π = {}")
case False
then obtain A where A: "A β π" by auto
then have finA: "finite A" using assms by auto
hence fin: "finite (A - βπ)" by(rule finite_subset[rotated]) auto
let ?P = "Ξ»x A. A β π β§ x β A"
define f where "f x = Eps (?P x)" for x
let ?β¬ = "insert A (f ` (A - βπ))"
have "?P x (f x)" if "x β A - βπ" for x unfolding f_def by(rule someI_ex)(use that A in auto)
hence "(β?β¬) = (βπ)" "?β¬ β π" using A by auto
moreover have "finite ?β¬" using fin by simp
ultimately show ?thesis by blast
qed simp

locale wide_intersection_finite =
fixes E :: "'Fa β 'Fa β bool"
and mapFa :: "('a β 'a) β 'Fa β 'Fa"
and setFa :: "'Fa β 'a set"
assumes equiv: "equivp E"
and map_E: "E x y βΉ E (mapFa f x) (mapFa f y)"
and map_id: "mapFa id x = x"
and map_cong: "βaβsetFa x. f a = g a βΉ mapFa f x = mapFa g x"
and set_map: "setFa (mapFa f x) = f ` setFa x"
and finite: "finite (setFa x)"
begin

lemma binary_intersection:
assumes "E y z" and y: "setFa y β Y" and z: "setFa z β Z" and a: "a β Y" "a β Z"
shows "βx. E x y β§ setFa x β Y β§ setFa x β Z"
proof -
let ?f = "Ξ»b. if b β Z then b else a"
let ?u = "mapFa ?f y"
from βΉE y zβΊ have "E ?u (mapFa ?f z)" by(rule map_E)
also have "mapFa ?f z = mapFa id z" by(rule map_cong)(use z in auto)
also have "β¦ = z" by(rule map_id)
finally have "E ?u y" using βΉE y zβΊ equivp_symp[OF equiv] equivp_transp[OF equiv] by blast
moreover have "setFa ?u β Y" using a y by(subst set_map) auto
moreover have "setFa ?u β Z" using a by(subst set_map) auto
ultimately show ?thesis by blast
qed

lemma finite_intersection:
assumes E: "βyβA. E y z"
and fin: "finite A"
and sub: "βyβA. setFa y β Y y β§ a β Y y"
shows "βx. E x z β§ (βyβA. setFa x β Y y)"
using fin E sub
proof(induction)
case empty
then show ?case using equivp_reflp[OF equiv, of z] by(auto)
next
case (insert y A)
then obtain x where x: "E x z" "βyβA. setFa x β Y y β§ a β Y y" by auto
hence set_x: "setFa x β (βyβA. Y y)" "a β (βyβA. Y y)" by auto
from insert.prems have "E y z" and set_y: "setFa y β Y y" "a β Y y" by auto
from βΉE y zβΊ βΉE x zβΊ have "E x y" using equivp_symp[OF equiv] equivp_transp[OF equiv] by blast
from binary_intersection[OF this set_x(1) set_y(1) set_x(2) set_y(2)]
obtain x' where "E x' x" "setFa x' β β (Y ` A)" "setFa x' β Y y" by blast
then show ?case using βΉE x zβΊ equivp_transp[OF equiv] by blast
qed

lemma wide_intersection:
assumes inter_nonempty: "β Ss β  {}"
shows "(βAs β Ss. {(x, x'). E x x'} `` {x. setFa x β As}) β {(x, x'). E x x'} `` {x. setFa x β β Ss}" (is "?lhs β ?rhs")
proof
fix x
assume lhs: "x β ?lhs"
from inter_nonempty obtain a where a: "βAs β Ss. a β As" by auto
from lhs obtain y where y: "βAs. As β Ss βΉ E (y As) x β§ setFa (y As) β As"
by atomize_elim(rule choice, auto)
define Ts where "Ts = (Ξ»As. insert a (setFa (y As))) ` Ss"
have Ts_subset: "(βTs) β (βSs)" using a unfolding Ts_def by(auto dest: y)
have Ts_finite: "βBs β Ts. finite Bs" unfolding Ts_def by(auto dest: y intro: finite)
from Inter_finite_subset[OF this] obtain Us
where Us: "Us β Ts" and finite_Us: "finite Us" and Int_Us: "(βUs) β (βTs)" by force
let ?P = "Ξ»U As. As β Ss β§ U = insert a (setFa (y As))"
define Y where "Y U = Eps (?P U)" for U
have Y: "?P U (Y U)" if "U β Us" for U unfolding Y_def
by(rule someI_ex)(use that Us in βΉauto simp add: Ts_defβΊ)
let ?f = "Ξ»U. y (Y U)"
have *: "βzβ(?f ` Us). E z x" by(auto dest!: Y y)
have **: "βzβ(?f ` Us). setFa z β insert a (setFa z) β§ a β insert a (setFa z)" by auto
from finite_intersection[OF * _ **] finite_Us obtain u
where u: "E u x" and set_u: "βzβ(?f ` Us). setFa u β insert a (setFa z)" by auto
from set_u have "setFa u β (β Us)" by(auto dest: Y)
with Int_Us Ts_subset have "setFa u β (β Ss)" by auto
with u show "x β ?rhs" by auto
qed

end

text βΉSubdistributivity for quotients via confluenceβΊ

lemma rtranclp_transp_reflp: "R** = R" if "transp R" "reflp R"
apply(rule ext iffI)+
subgoal premises prems for x y using prems by(induction)(use that in βΉauto intro: reflpD transpDβΊ)
subgoal by(rule r_into_rtranclp)
done

lemma rtranclp_equivp: "R** = R" if "equivp R"
using that by(simp add: rtranclp_transp_reflp equivp_reflp_symp_transp)

locale confluent_quotient =
fixes Rb :: "'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 Rb"
and retract1_ab: "βx y. Rb (Ο_Fabb x) y βΉ βz. Eab x z β§ y = Ο_Fabb z β§ set_Fab z β set_Fab x"
and retract1_bc: "βx y. Rb (Ο_Fbcb x) y βΉ βz. Ebc x z β§ y = Ο_Fbcb z β§ set_Fbc z β set_Fbc x"
and generated_b: "Eb β€ equivclp Rb"
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: "Rb** (Ο_Fabb x) y βΉ βz. Eab x z β§ y = Ο_Fabb z β§ set_Fab z β set_Fab x"
by(induction rule: rtranclp_induct)(blast dest: retract1_ab intro: equivp_transp[OF equivp_ab] equivp_reflp[OF equivp_ab])+

lemma retract_bc: "Rb** (Ο_Fbcb x) y βΉ βz. Ebc x z β§ y = Ο_Fbcb z β§ set_Fbc z β set_Fbc x"
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"
from βΉEb y y'βΊ have "equivclp Rb y y'" using generated_b by blast
then obtain u where u: "Rb** y u" "Rb** y' u"
unfolding semiconfluentp_equivclp[OF confluent[THEN confluentp_imp_semiconfluentp]]
with xy y'z obtain xy' y'z'
where retract1: "Eab xy xy'" "Ο_Fabb xy' = u" "set_Fab xy' β set_Fab xy"
and retract2: "Ebc y'z y'z'" "Ο_Fbcb y'z' = u" "set_Fbc y'z' β set_Fbc y'z"
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)
moreover have "rel_Fbc B u (Ο_Fbcc y'z')" using y'z retract2 by(auto simp add: in_rel_Fbc)
moreover have "Ec (Ο_Fbcc y'z') z" using retract2 y'z equivp_symp[OF equivp_bc]
by(auto intro: Ο_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