Quelle Confluent_Quotient.thy Sprache: Isabelle

theory Confluent_Quotient imports
  Confluence
begin

text \<open>Functors with finite setters preserve wide intersection for any equivalence relation that respects the mapper.\<close>

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 ?\<B> = "insert A (f ` (A - \<Inter>\<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 \<open>E y z\<close> 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 \<open>E y z\<close> 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 \<open>E y z\<close> \<open>E x z\<close> 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 \<open>E x z\<close> 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 \<open>auto simp add: Ts_def\<close>)
  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 \<open>Subdistributivity for quotients via confluence\<close>

lemma rtranclp_transp_reflp: "R\<^sup>*\<^sup>* = R" if "transp R" "reflp R"
  apply(rule ext iffI)+
  subgoal premises prems for x y using prems by(induction)(use that in \<open>auto intro: reflpD transpD\<close>)
  subgoal by(rule r_into_rtranclp)
  done

lemma rtranclp_equivp: "R\<^sup>*\<^sup>* = 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 \<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 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 \<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: "Rb\<^sup>*\<^sup>* (\_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\<^sup>*\<^sup>* (\_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 \<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 Rb y y'" using generated_b by blast
  then obtain u where u: "Rb\<^sup>*\<^sup>* y u" "Rb\<^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" "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: \<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

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.