SSL 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.13 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders