Theory HOL-Library.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"
    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