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 ∈ A. finite A"
  shows "∃B⊆A. finite B ∧ (∩B) = (∩A)"
proof(cases "A = {}")
  case False
  then obtain A where A: "A ∈ A" by auto
  then have finA: "finite A" using assms by auto
  hence fin: "finite (A - ∩A)" by(rule finite_subset[rotated]) auto
  let ?P = "λx A. A ∈ A ∧ x ∉ A"
  define f where "f x = Eps (?P x)" for x
  let ?B = "insert A (f ` (A - ∩A))"
  have "?P x (f x)" if "x ∈ A - ∩A" for x unfolding f_def by(rule someI_ex)(use that A in auto)
  hence "(∩?B) = (∩A)" "?B ⊆ A" using A by auto
  moreover have "finite ?B" 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"
    by(auto simp add: in_rel_Fab in_rel_Fbc)
  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]]
    by(auto simp add: rtranclp_conversep)
  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