Quelle Equiv_Relations.thy Sprache: Isabelle

(*  Title:      HOL/Equiv_Relations.thy
    Author:     Lawrence C Paulson, 1996 Cambridge University Computer Laboratory
*)

section \<open>Equivalence Relations in Higher-Order Set Theory\<close>

theory Equiv_Relations
  imports BNF_Least_Fixpoint
begin

subsection \<open>Equivalence relations -- set version\<close>

definition equiv :: "'a set \ ('a \ 'a) set \ bool"
  where "equiv A r \ r \ A \ A \ refl_on A r \ sym r \ trans r"

lemma equivI: "r \ A \ A \ refl_on A r \ sym r \ trans r \ equiv A r"
  by (simp add: equiv_def)

lemma equivE:
  assumes "equiv A r"
  obtains "r \ A \ A" and "refl_on A r" and "sym r" and "trans r"
  using assms by (simp add: equiv_def)

text \<open>
  Suppes, Theorem 70: \<open>r\<close> is an equiv relation iff \<open>r\<inverse> O r = r\<close>.

  First half: \<open>equiv A r \<Longrightarrow> r\<inverse> O r = r\<close>.
\<close>

lemma sym_trans_comp_subset:
  assumes "r \ A \ A" and "sym_on A r" and "trans_on A r"
  shows "r\ O r \ r"
proof (rule subsetI)
  fix p
  assume "p \ r\ O r"
  then obtain x y z where "p = (x, z)" and "(y, x) \ r" and "(y, z) \ r"
    by auto
  hence "x \ A" and "y \ A" and "z \ A"
    using \<open>r \<subseteq> A \<times> A\<close> by auto
  have "(x, y) \ r"
    using \<open>(y, x) \<in> r\<close> \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>sym_on A r\<close> by (simp add: sym_on_def)
  hence "(x, z) \ r"
    using \<open>trans_on A r\<close>[THEN trans_onD, OF \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>z \<in> A\<close>] \<open>(y, z) \<in> r\<close> by blast
  thus "p \ r"
    unfolding \<open>p = (x, z)\<close> .
qed

lemma refl_on_comp_subset: "r \ A \ A \ refl_on A r \ r \ r\ O r"
  unfolding refl_on_def by blast

lemma equiv_comp_eq: "equiv A r \ r\ O r = r"
proof (rule subset_antisym)
  show "equiv A r \ r\ O r \ r"
    by (rule sym_trans_comp_subset[of r A]) (auto elim: equivE intro: sym_on_subset trans_on_subset)
next
  show "equiv A r \ r \ r\ O r"
    by (rule refl_on_comp_subset[of r A]) (auto elim: equivE)
qed

text \<open>Second half.\<close>

lemma comp_equivI:
  assumes "r\ O r = r" "Domain r = A"
  shows "equiv A r"
proof (rule equivI)
  show "r \ A \ A"
    using assms by auto

  have *: "\x y. (x, y) \ r \ (y, x) \ r"
    using assms by blast

  thus "refl_on A r" "sym r" "trans r"
    unfolding refl_on_def sym_def trans_def
    using assms by auto
qed

subsection \<open>Equivalence classes\<close>

lemma equiv_class_subset: "equiv A r \ (a, b) \ r \ r``{a} \ r``{b}"
  \<comment> \<open>lemma for the next result\<close>
  unfolding equiv_def trans_def sym_def by blast

theorem equiv_class_eq:
  assumes "equiv A r" and "(a, b) \ r"
  shows "r``{a} = r``{b}"
proof (intro subset_antisym equiv_class_subset[OF \<open>equiv A r\<close>])
  show "(a, b) \ r"
    using \<open>(a, b) \<in> r\<close> .
next
  have "sym r"
    using \<open>equiv A r\<close> by (auto elim: equivE)
  thus "(b, a) \ r"
    using \<open>(a, b) \<in> r\<close>
    by (auto dest: symD)
qed

lemma equiv_class_self: "equiv A r \ a \ A \ a \ r``{a}"
  unfolding equiv_def refl_on_def by blast

lemma subset_equiv_class: "equiv A r \ r``{b} \ r``{a} \ b \ A \ (a, b) \ r"
  \<comment> \<open>lemma for the next result\<close>
  unfolding equiv_def refl_on_def by blast

lemma eq_equiv_class: "r``{a} = r``{b} \ equiv A r \ b \ A \ (a, b) \ r"
  by (iprover intro: equalityD2 subset_equiv_class)

lemma equiv_class_nondisjoint: "equiv A r \ x \ (r``{a} \ r``{b}) \ (a, b) \ r"
  unfolding equiv_def trans_def sym_def by blast

lemma equiv_type: "equiv A r \ r \ A \ A"
  unfolding equiv_def refl_on_def by blast

lemma equiv_class_eq_iff: "equiv A r \ (x, y) \ r \ r``{x} = r``{y} \ x \ A \ y \ A"
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

lemma eq_equiv_class_iff: "equiv A r \ x \ A \ y \ A \ r``{x} = r``{y} \ (x, y) \ r"
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

lemma disjnt_equiv_class: "equiv A r \ disjnt (r``{a}) (r``{b}) \ (a, b) \ r"
  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)

subsection \<open>Quotients\<close>

definition quotient :: "'a set \ ('a \ 'a) set \ 'a set set" (infixl \'/'/\ 90)
  where "A//r = (\x \ A. {r``{x}})" \ \set of equiv classes\

lemma quotientI: "x \ A \ r``{x} \ A//r"
  unfolding quotient_def by blast

lemma quotientE: "X \ A//r \ (\x. X = r``{x} \ x \ A \ P) \ P"
  unfolding quotient_def by blast

lemma Union_quotient: "equiv A r \ \(A//r) = A"
  unfolding equiv_def refl_on_def quotient_def by blast

lemma quotient_disj_strong:
  assumes "r \ A \ A" and "sym_on A r" and "trans_on A r" and "X \ A//r" and "Y \ A//r"
  shows "X = Y \ X \ Y = {}"
proof -
  obtain x where "x \ A" and "X = {x'. (x, x') \ r}"
    using \<open>X \<in> A//r\<close> unfolding quotient_def UN_iff by blast

  moreover obtain y where "y \ A" and "Y = {y'. (y, y') \ r}"
    using \<open>Y \<in> A//r\<close> unfolding quotient_def UN_iff by blast

  have f8: "\a aa. (aa, a) \ r \ (a, aa) \ r"
    using \<open>r \<subseteq> A \<times> A\<close>[unfolded subset_eq] \<open>sym_on A r\<close>[THEN sym_onD] by blast
  have f9: "\a aa ab. (aa, ab) \ r \ (aa, a) \ r \ (a, ab) \ r"
    using \<open>r \<subseteq> A \<times> A\<close>[unfolded subset_eq] \<open>trans_on A r\<close>[THEN trans_onD] by blast
  then have "\a aa. aa \ Y \ (y, a) \ r \ (a, aa) \ r"
    using \<open>Y = {y'. (y, y') \<in> r}\<close> by simp
  then show ?thesis
    using f9 f8 \<open>X = {x'. (x, x') \<in> r}\<close> \<open>Y = {y'. (y, y') \<in> r}\<close>
      Collect_cong disjoint_iff_not_equal mem_Collect_eq by blast
qed

lemma quotient_disj: "equiv A r \ X \ A//r \ Y \ A//r \ X = Y \ X \ Y = {}"
  by (rule quotient_disj_strong[of r A X Y])
    (auto elim: equivE intro: sym_on_subset trans_on_subset)

lemma quotient_eqI:
  assumes "equiv A r" "X \ A//r" "Y \ A//r" and xy: "x \ X" "y \ Y" "(x, y) \ r"
  shows "X = Y"
proof -
  obtain a b where "a \ A" and a: "X = r `` {a}" and "b \ A" and b: "Y = r `` {b}"
    using assms by (auto elim!: quotientE)
  moreover have "sym r" and "trans r"
    using \<open>equiv A r\<close>
    by (auto elim: equivE)
  ultimately have "(a,b) \ r"
      using xy unfolding sym_def trans_def by blast
  then show ?thesis
    unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>])
qed

lemma quotient_eq_iff:
  assumes "equiv A r" "X \ A//r" "Y \ A//r" and xy: "x \ X" "y \ Y"
  shows "X = Y \ (x, y) \ r"
proof
  assume L: "X = Y"
  with assms show "(x, y) \ r"
    unfolding equiv_def sym_def trans_def by (blast elim!: quotientE)
next
  assume \<section>: "(x, y) \<in> r" show "X = Y"
    by (rule quotient_eqI) (use \<section> assms in \<open>blast+\<close>)
qed

lemma eq_equiv_class_iff2: "equiv A r \ x \ A \ y \ A \ {x}//r = {y}//r \ (x, y) \ r"
  by (simp add: quotient_def eq_equiv_class_iff)

lemma quotient_empty [simp]: "{}//r = {}"
  by (simp add: quotient_def)

lemma quotient_is_empty [iff]: "A//r = {} \ A = {}"
  by (simp add: quotient_def)

lemma quotient_is_empty2 [iff]: "{} = A//r \ A = {}"
  by (simp add: quotient_def)

lemma singleton_quotient: "{x}//r = {r `` {x}}"
  by (simp add: quotient_def)

lemma quotient_diff1: "inj_on (\a. {a}//r) A \ a \ A \ (A - {a})//r = A//r - {a}//r"
  unfolding quotient_def inj_on_def by blast

subsection \<open>Refinement of one equivalence relation WRT another\<close>

lemma refines_equiv_class_eq: "R \ S \ equiv A R \ equiv A S \ R``(S``{a}) = S``{a}"
  by (auto simp: equiv_class_eq_iff)

lemma refines_equiv_class_eq2: "R \ S \ equiv A R \ equiv A S \ S``(R``{a}) = S``{a}"
  by (auto simp: equiv_class_eq_iff)

lemma refines_equiv_image_eq: "R \ S \ equiv A R \ equiv A S \ (\X. S``X) ` (A//R) = A//S"
   by (auto simp: quotient_def image_UN refines_equiv_class_eq2)

lemma finite_refines_finite:
  "finite (A//R) \ R \ S \ equiv A R \ equiv A S \ finite (A//S)"
  by (erule finite_surj [where f = "\X. S``X"]) (simp add: refines_equiv_image_eq)

lemma finite_refines_card_le:
  "finite (A//R) \ R \ S \ equiv A R \ equiv A S \ card (A//S) \ card (A//R)"
  by (subst refines_equiv_image_eq [of R S A, symmetric])
    (auto simp: card_image_le [where f = "\X. S``X"])

subsection \<open>Defining unary operations upon equivalence classes\<close>

text \<open>A congruence-preserving function.\<close>

definition congruent :: "('a \ 'a) set \ ('a \ 'b) \ bool"
  where "congruent r f \ (\(y, z) \ r. f y = f z)"

lemma congruentI: "(\y z. (y, z) \ r \ f y = f z) \ congruent r f"
  by (auto simp add: congruent_def)

lemma congruentD: "congruent r f \ (y, z) \ r \ f y = f z"
  by (auto simp add: congruent_def)

abbreviation RESPECTS :: "('a \ 'b) \ ('a \ 'a) set \ bool" (infixr \respects\ 80)
  where "f respects r \ congruent r f"

lemma UN_constant_eq: "a \ A \ \y \ A. f y = c \ (\y \ A. f y) = c"
  \<comment> \<open>lemma required to prove \<open>UN_equiv_class\<close>\<close>
  by auto

lemma UN_equiv_class:
  assumes "equiv A r" "f respects r" "a \ A"
  shows "(\x \ r``{a}. f x) = f a"
  \<comment> \<open>Conversion rule\<close>
proof -
  have \<section>: "\<forall>x\<in>r `` {a}. f x = f a"
    using assms unfolding equiv_def congruent_def sym_def by blast
  show ?thesis
    by (iprover intro: assms UN_constant_eq [OF equiv_class_self \<section>])
qed

lemma UN_equiv_class_type:
  assumes r: "equiv A r" "f respects r" and X: "X \ A//r" and AB: "\x. x \ A \ f x \ B"
  shows "(\x \ X. f x) \ B"
  using assms unfolding quotient_def
  by (auto simp: UN_equiv_class [OF r])

text \<open>
  Sufficient conditions for injectiveness.  Could weaken premises!
  major premise could be an inclusion; \<open>bcong\<close> could be
  \<open>\<And>y. y \<in> A \<Longrightarrow> f y \<in> B\<close>.
\<close>

lemma UN_equiv_class_inject:
  assumes "equiv A r" "f respects r"
    and eq: "(\x \ X. f x) = (\y \ Y. f y)"
    and X: "X \ A//r" and Y: "Y \ A//r"
    and fr: "\x y. x \ A \ y \ A \ f x = f y \ (x, y) \ r"
  shows "X = Y"
proof -
  obtain a b where "a \ A" and a: "X = r `` {a}" and "b \ A" and b: "Y = r `` {b}"
    using assms by (auto elim!: quotientE)
  then have "\ (f ` r `` {a}) = f a" "\ (f ` r `` {b}) = f b"
    by (iprover intro: UN_equiv_class [OF \<open>equiv A r\<close>] assms)+
  then have "f a = f b"
    using eq unfolding a b by (iprover intro: trans sym)
  then have "(a,b) \ r"
    using fr \<open>a \<in> A\<close> \<open>b \<in> A\<close> by blast
  then show ?thesis
    unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>])
qed

subsection \<open>Defining binary operations upon equivalence classes\<close>

text \<open>A congruence-preserving function of two arguments.\<close>

definition congruent2 :: "('a \ 'a) set \ ('b \ 'b) set \ ('a \ 'b \ 'c) \ bool"
  where "congruent2 r1 r2 f \ (\(y1, z1) \ r1. \(y2, z2) \ r2. f y1 y2 = f z1 z2)"

lemma congruent2I':
  assumes "\y1 z1 y2 z2. (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"
  shows "congruent2 r1 r2 f"
  using assms by (auto simp add: congruent2_def)

lemma congruent2D: "congruent2 r1 r2 f \ (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"
  by (auto simp add: congruent2_def)

text \<open>Abbreviation for the common case where the relations are identical.\<close>
abbreviation RESPECTS2:: "('a \ 'a \ 'b) \ ('a \ 'a) set \ bool" (infixr \respects2\ 80)
  where "f respects2 r \ congruent2 r r f"

lemma congruent2_implies_congruent:
  "equiv A r1 \ congruent2 r1 r2 f \ a \ A \ congruent r2 (f a)"
  unfolding congruent_def congruent2_def equiv_def refl_on_def by blast

lemma congruent2_implies_congruent_UN:
  assumes "equiv A1 r1" "equiv A2 r2" "congruent2 r1 r2 f" "a \ A2"
  shows "congruent r1 (\x1. \x2 \ r2``{a}. f x1 x2)"
  unfolding congruent_def
proof clarify
  fix c d
  assume cd: "(c,d) \ r1"
  then have "c \ A1" "d \ A1"
    using \<open>equiv A1 r1\<close> by (auto elim!: equiv_type [THEN subsetD, THEN SigmaE2])
  moreover have "f c a = f d a"
    using assms cd unfolding congruent2_def equiv_def refl_on_def by blast
  ultimately show "\ (f c ` r2 `` {a}) = \ (f d ` r2 `` {a})"
    using assms by (simp add: UN_equiv_class congruent2_implies_congruent)
qed

lemma UN_equiv_class2:
  "equiv A1 r1 \ equiv A2 r2 \ congruent2 r1 r2 f \ a1 \ A1 \ a2 \ A2 \
    (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2"
  by (simp add: UN_equiv_class congruent2_implies_congruent congruent2_implies_congruent_UN)

lemma UN_equiv_class_type2:
  "equiv A1 r1 \ equiv A2 r2 \ congruent2 r1 r2 f
    \<Longrightarrow> X1 \<in> A1//r1 \<Longrightarrow> X2 \<in> A2//r2
    \<Longrightarrow> (\<And>x1 x2. x1 \<in> A1 \<Longrightarrow> x2 \<in> A2 \<Longrightarrow> f x1 x2 \<in> B)
    \<Longrightarrow> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
  unfolding quotient_def
  by (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
                   congruent2_implies_congruent quotientI)

lemma UN_UN_split_split_eq:
  "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) =
    (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
  \<comment> \<open>Allows a natural expression of binary operators,\<close>
  \<comment> \<open>without explicit calls to \<open>split\<close>\<close>
  by auto

lemma congruent2I:
  "equiv A1 r1 \ equiv A2 r2
    \<Longrightarrow> (\<And>y z w. w \<in> A2 \<Longrightarrow> (y,z) \<in> r1 \<Longrightarrow> f y w = f z w)
    \<Longrightarrow> (\<And>y z w. w \<in> A1 \<Longrightarrow> (y,z) \<in> r2 \<Longrightarrow> f w y = f w z)
    \<Longrightarrow> congruent2 r1 r2 f"
  \<comment> \<open>Suggested by John Harrison -- the two subproofs may be\<close>
  \<comment> \<open>\<^emph>\<open>much\<close> simpler than the direct proof.\<close>
  unfolding congruent2_def equiv_def refl_on_def
  by (blast intro: trans)

lemma congruent2_commuteI:
  assumes equivA: "equiv A r"
    and commute: "\y z. y \ A \ z \ A \ f y z = f z y"
    and congt: "\y z w. w \ A \ (y,z) \ r \ f w y = f w z"
  shows "f respects2 r"
proof (rule congruent2I [OF equivA equivA])
  note eqv = equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2]
  show "\y z w. \w \ A; (y, z) \ r\ \ f y w = f z w"
    by (iprover intro: commute [THEN trans] sym congt elim: eqv)
  show "\y z w. \w \ A; (y, z) \ r\ \ f w y = f w z"
    by (iprover intro: congt elim: eqv)
qed

subsection \<open>Quotients and finiteness\<close>

text \<open>Suggested by Florian Kammüller\<close>

lemma finite_quotient:
  assumes "finite A" "r \ A \ A"
  shows "finite (A//r)"
    \<comment> \<open>recall @{thm equiv_type}\<close>
proof -
  have "A//r \ Pow A"
    using assms unfolding quotient_def by blast
  moreover have "finite (Pow A)"
    using assms by simp
  ultimately show ?thesis
    by (iprover intro: finite_subset)
qed

lemma finite_equiv_class: "finite A \ r \ A \ A \ X \ A//r \ finite X"
  unfolding quotient_def
  by (erule rev_finite_subset) blast

lemma equiv_imp_dvd_card:
  assumes "finite A" "equiv A r" "\X. X \ A//r \ k dvd card X"
  shows "k dvd card A"
proof (rule Union_quotient [THEN subst])
  show "k dvd card (\ (A // r))"
    apply (rule dvd_partition)
    using assms
    by (auto simp: Union_quotient dest: quotient_disj)
qed (use assms in blast)

subsection \<open>Kernel of a Function\<close>

definition kernel :: "('a \ 'b) \ ('a * 'a) set" where
"kernel f = {(x,y). f x = f y}"

lemma equiv_kernel: "equiv UNIV (kernel f)"
unfolding kernel_def equiv_def refl_on_def sym_def trans_def by auto

lemma respects_kernel: "f respects (kernel f)"
by (simp add: congruent_def kernel_def)

lemma inj_on_vimage_image: "inj_on (\b. f -` {b}) (f ` A)"
using inj_on_def by fastforce

lemma kernel_Image: "kernel f `` A = f -` (f ` A)"
unfolding kernel_def by (auto simp add: rev_image_eqI)

lemma quotient_kernel_eq_image: "A // kernel f = (\b. f -` {b}) ` f ` A"
by(auto simp: quotient_def kernel_Image)

lemma bij_betw_image_quotient_kernel: "bij_betw (\b. f -` {b}) (f ` A) (A // kernel f)"
by (simp add: bij_betw_def inj_on_vimage_image quotient_kernel_eq_image)

subsection \<open>Projection\<close>

definition proj :: "('b \ 'a) set \ 'b \ 'a set"
  where "proj r x = r `` {x}"

lemma proj_preserves: "x \ A \ proj r x \ A//r"
  unfolding proj_def by (rule quotientI)

lemma proj_in_iff:
  assumes "equiv A r"
  shows "proj r x \ A//r \ x \ A"
    (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by (simp add: proj_preserves)
next
  assume ?lhs
  then show ?rhs
    unfolding proj_def quotient_def
  proof safe
    fix y
    assume y: "y \ A" and "r `` {x} = r `` {y}"
    moreover have "y \ r `` {y}"
      using assms y unfolding equiv_def refl_on_def by blast
    ultimately have "(x, y) \ r" by blast
    then show "x \ A"
      using assms unfolding equiv_def refl_on_def by blast
  qed
qed

lemma proj_iff: "equiv A r \ {x, y} \ A \ proj r x = proj r y \ (x, y) \ r"
  by (simp add: proj_def eq_equiv_class_iff)

(*
lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
unfolding proj_def equiv_def refl_on_def by blast
*)

lemma proj_image: "proj r ` A = A//r"
  unfolding proj_def[abs_def] quotient_def by blast

lemma in_quotient_imp_non_empty: "equiv A r \ X \ A//r \ X \ {}"
  unfolding quotient_def using equiv_class_self by fast

lemma in_quotient_imp_in_rel: "equiv A r \ X \ A//r \ {x, y} \ X \ (x, y) \ r"
  using quotient_eq_iff[THEN iffD1] by fastforce

lemma in_quotient_imp_closed: "equiv A r \ X \ A//r \ x \ X \ (x, y) \ r \ y \ X"
  unfolding quotient_def equiv_def trans_def by blast

lemma in_quotient_imp_subset: "equiv A r \ X \ A//r \ X \ A"
  using in_quotient_imp_in_rel equiv_type by fastforce

subsection \<open>Equivalence relations -- predicate version\<close>

text \<open>Partial equivalences.\<close>

definition part_equivp :: "('a \ 'a \ bool) \ bool"
  where "part_equivp R \ (\x. R x x) \ (\x y. R x y \ R x x \ R y y \ R x = R y)"
    \<comment> \<open>John-Harrison-style characterization\<close>

lemma part_equivpI: "\x. R x x \ symp R \ transp R \ part_equivp R"
  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)

lemma part_equivpE:
  assumes "part_equivp R"
  obtains x where "R x x" and "symp R" and "transp R"
proof -
  from assms have 1: "\x. R x x"
    and 2: "\x y. R x y \ R x x \ R y y \ R x = R y"
    unfolding part_equivp_def by blast+
  from 1 obtain x where "R x x" ..
  moreover have "symp R"
  proof (rule sympI)
    fix x y
    assume "R x y"
    with 2 [of x y] show "R y x" by auto
  qed
  moreover have "transp R"
  proof (rule transpI)
    fix x y z
    assume "R x y" and "R y z"
    with 2 [of x y] 2 [of y z] show "R x z" by auto
  qed
  ultimately show thesis by (rule that)
qed

lemma part_equivp_refl_symp_transp: "part_equivp R \ (\x. R x x) \ symp R \ transp R"
  by (auto intro: part_equivpI elim: part_equivpE)

lemma part_equivp_symp: "part_equivp R \ R x y \ R y x"
  by (erule part_equivpE, erule sympE)

lemma part_equivp_transp: "part_equivp R \ R x y \ R y z \ R x z"
  by (erule part_equivpE, erule transpE)

lemma part_equivp_typedef: "part_equivp R \ \d. d \ {c. \x. R x x \ c = Collect (R x)}"
  by (auto elim: part_equivpE)

text \<open>Total equivalences.\<close>

definition equivp :: "('a \ 'a \ bool) \ bool"
  where "equivp R \ (\x y. R x y = (R x = R y))" \ \John-Harrison-style characterization\

lemma equivpI: "reflp R \ symp R \ transp R \ equivp R"
  by (auto elim: reflpE sympE transpE simp add: equivp_def)

lemma equivpE:
  assumes "equivp R"
  obtains "reflp R" and "symp R" and "transp R"
  using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)

lemma equivp_implies_part_equivp: "equivp R \ part_equivp R"
  by (auto intro: part_equivpI elim: equivpE reflpE)

lemma equivp_equiv: "equiv UNIV A \ equivp (\x y. (x, y) \ A)"
  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])

lemma equivp_reflp_symp_transp: "equivp R \ reflp R \ symp R \ transp R"
  by (auto intro: equivpI elim: equivpE)

lemma identity_equivp: "equivp (=)"
  by (auto intro: equivpI reflpI sympI transpI)

lemma equivp_reflp: "equivp R \ R x x"
  by (erule equivpE, erule reflpE)

lemma equivp_symp: "equivp R \ R x y \ R y x"
  by (erule equivpE, erule sympE)

lemma equivp_transp: "equivp R \ R x y \ R y z \ R x z"
  by (erule equivpE, erule transpE)

lemma equivp_rtranclp: "symp r \ equivp r\<^sup>*\<^sup>*"
  by(intro equivpI reflpI sympI transpI)(auto dest: sympD[OF symp_rtranclp])

lemmas equivp_rtranclp_symclp [simp] = equivp_rtranclp[OF symp_on_symclp]

lemma equivp_vimage2p: "equivp R \ equivp (vimage2p f f R)"
  by(auto simp add: equivp_def vimage2p_def dest: fun_cong)

lemma equivp_imp_transp: "equivp R \ transp R"
  by(simp add: equivp_reflp_symp_transp)

subsection \<open>Equivalence closure\<close>

definition equivclp :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" where
  "equivclp r = (symclp r)\<^sup>*\<^sup>*"

lemma transp_equivclp [simp]: "transp (equivclp r)"
  by(simp add: equivclp_def)

lemma reflp_equivclp [simp]: "reflp (equivclp r)"
  by(simp add: equivclp_def)

lemma symp_equivclp [simp]: "symp (equivclp r)"
  by(simp add: equivclp_def)

lemma equivp_evquivclp [simp]: "equivp (equivclp r)"
  by(simp add: equivpI)

lemma tranclp_equivclp [simp]: "(equivclp r)\<^sup>+\<^sup>+ = equivclp r"
  by(simp add: equivclp_def)

lemma rtranclp_equivclp [simp]: "(equivclp r)\<^sup>*\<^sup>* = equivclp r"
  by(simp add: equivclp_def)

lemma symclp_equivclp [simp]: "symclp (equivclp r) = equivclp r"
  by(simp add: equivclp_def symp_symclp_eq)

lemma equivclp_symclp [simp]: "equivclp (symclp r) = equivclp r"
  by(simp add: equivclp_def)

lemma equivclp_conversep [simp]: "equivclp (conversep r) = equivclp r"
  by(simp add: equivclp_def)

lemma equivclp_sym [sym]: "equivclp r x y \ equivclp r y x"
  by(rule sympD[OF symp_equivclp])

lemma equivclp_OO_equivclp_le_equivclp: "equivclp r OO equivclp r \ equivclp r"
  by(rule transp_relcompp_less_eq transp_equivclp)+

lemma rtranlcp_le_equivclp: "r\<^sup>*\<^sup>* \ equivclp r"
  unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree)

lemma rtranclp_conversep_le_equivclp: "r\\\<^sup>*\<^sup>* \ equivclp r"
  unfolding equivclp_def by(rule rtranclp_mono)(simp add: symclp_pointfree)

lemma symclp_rtranclp_le_equivclp: "symclp r\<^sup>*\<^sup>* \ equivclp r"
  unfolding symclp_pointfree
  by(rule le_supI)(simp_all add: rtranclp_conversep[symmetric] rtranlcp_le_equivclp rtranclp_conversep_le_equivclp)

lemma r_OO_conversep_into_equivclp:
  "r\<^sup>*\<^sup>* OO r\\\<^sup>*\<^sup>* \ equivclp r"
  by(blast intro: order_trans[OF _ equivclp_OO_equivclp_le_equivclp] relcompp_mono rtranlcp_le_equivclp rtranclp_conversep_le_equivclp del: predicate2I)

lemma equivclp_induct [consumes 1, case_names base step, induct pred: equivclp]:
  assumes a: "equivclp r a b"
    and cases: "P a" "\y z. equivclp r a y \ r y z \ r z y \ P y \ P z"
  shows "P b"
  using a unfolding equivclp_def
  by(induction rule: rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE)

lemma converse_equivclp_induct [consumes 1, case_names base step]:
  assumes major: "equivclp r a b"
    and cases: "P b" "\y z. r y z \ r z y \ equivclp r z b \ P z \ P y"
  shows "P a"
  using major unfolding equivclp_def
  by(induction rule: converse_rtranclp_induct; fold equivclp_def; blast intro: cases elim: symclpE)

lemma equivclp_refl [simp]: "equivclp r x x"
  by(rule reflpD[OF reflp_equivclp])

lemma r_into_equivclp [intro]: "r x y \ equivclp r x y"
  unfolding equivclp_def by(blast intro: symclpI)

lemma converse_r_into_equivclp [intro]: "r y x \ equivclp r x y"
  unfolding equivclp_def by(blast intro: symclpI)

lemma rtranclp_into_equivclp: "r\<^sup>*\<^sup>* x y \ equivclp r x y"
  using rtranlcp_le_equivclp[of r] by blast

lemma converse_rtranclp_into_equivclp: "r\<^sup>*\<^sup>* y x \ equivclp r x y"
  by(blast intro: equivclp_sym rtranclp_into_equivclp)

lemma equivclp_into_equivclp: "\ equivclp r a b; r b c \ r c b \ \ equivclp r a c"
  unfolding equivclp_def by(erule rtranclp.rtrancl_into_rtrancl)(auto intro: symclpI)

lemma equivclp_trans [trans]: "\ equivclp r a b; equivclp r b c \ \ equivclp r a c"
  using equivclp_OO_equivclp_le_equivclp[of r] by blast

hide_const (open) proj

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.