(* Title: Equivalence_Relations.thy
Author: Clara L\"oh
*)
section \Equivalence Relations\
theory Equivalence_Relations
imports Complex_Main
begin
text \Equivalence relations are relations on a given set
that are reflexive, symmetric, and transitive\
definition is_relation_on :: "'a set => ('a \ 'a) set => bool" where
"is_relation_on X r = (r \ X \ X)"
definition is_reflexive :: "'a set => ('a \ 'a) set => bool" where
"is_reflexive X r = (\ x \ X. (x,x) \ r)"
definition is_symmetric :: "'a set => ('a \ 'a) set => bool" where
"is_symmetric X r = (\ x \ X. \ y \ X.
(x,y) \ r --> (y,x) \ r)"
definition is_transitive :: "'a set => ('a \ 'a) set => bool" where
"is_transitive X r = (\ x \ X. \ y \ X. \ z \ X.
((x,y) \ r \ (y,z) \ r) --> (x,z) \ r)"
definition is_equivalence_relation :: "'a set => ('a \ 'a) set => bool" where
"is_equivalence_relation X r = (is_relation_on X r
\ is_reflexive X r
\ is_symmetric X r
\ is_transitive X r)"
text \The diagonal (i.e., the identity relation) is an
equivalence relation:\
lemma diagonal_is_equivalence_relation:
fixes X
shows "is_equivalence_relation X {(x,y). x \ X \ y\ X \ x = y}"
proof -
define diag_X where "diag_X = {(x,y). x \ X \ y \ X \ x = y}"
have diag_X_is_relation_on_X: "is_relation_on X diag_X"
proof -
have "\ xy \ diag_X. xy \ X \ X"
proof (intro ballI)
fix xy :: "'a \ 'a" assume xy_in_diag_X: "xy \ diag_X"
define x :: 'a where "x = fst xy"
define y :: 'a where "y = snd xy"
have "xy = (x,y)"
using x_def y_def by (simp add: prod_eqI)
then show "xy \ X \ X"
using diag_X_def xy_in_diag_X by simp
qed
then show ?thesis
using subsetI [of diag_X] by (simp add: is_relation_on_def)
qed
(*
unfolding is_relation_on_def
proof (intro subsetI ballI)
fix xy :: "'a \ 'a" assume xy_in_diag_X: "xy \ diag_X"
define x :: 'a where "x = fst xy"
define y :: 'a where "y = snd xy"
have "xy = (x,y)"
using x_def y_def by (simp add: prod_eqI)
then show "xy \ X \ X"
using diag_X_def xy_in_diag_X by simp
qed
*)
have diag_X_is_reflexive: "is_reflexive X diag_X"
proof -
have "\ x \ X. (x,x) \ diag_X"
proof (intro ballI)
fix x :: 'a assume x_in_X: "x \ X"
show "(x,x) \ diag_X"
by (simp add: diag_X_def x_in_X)
qed
then show ?thesis
by (simp add: is_reflexive_def)
qed
(*
unfolding is_reflexive_def
proof (intro ballI)
fix x :: 'a assume x_in_X: "x \ X"
show "(x,x) \ diag_X"
by (simp add: diag_X_def x_in_X)
qed
*)
have diag_X_is_symmetric: "is_symmetric X diag_X"
proof -
have "\ x \ X. \ y \ X.
(x,y) \ diag_X --> (y,x) \ diag_X"
proof (intro ballI impI)
fix x :: 'a assume x_in_X: "x \ X"
fix y :: 'a assume y_in_X: "y \ X"
assume xy_in_diag_X: "(x,y) \ diag_X"
from xy_in_diag_X diag_X_def
have "x = y"
by simp
then have "y = x"
by simp
then show "(y,x) \ diag_X"
by (simp add: diag_X_def x_in_X y_in_X)
qed
then show ?thesis
by (simp add: is_symmetric_def)
qed
have diag_X_is_transitive: "is_transitive X diag_X"
proof -
have "\ x \ X. \ y \ X. \ z \ X.
((x,y) \ diag_X \ (y,z) \ diag_X) --> (x,z) \ diag_X"
proof (intro ballI impI)
fix x :: 'a assume x_in_X: "x \ X"
fix y :: 'a assume y_in_X: "y \ X"
fix z :: 'a assume z_in_X: "z \ X"
assume xy_yz_in_diag_X: "(x,y) \ diag_X \ (y,z) \ diag_X"
from xy_yz_in_diag_X diag_X_def
have x_eq_y: "x = y"
by simp
from xy_yz_in_diag_X diag_X_def
have y_eq_z: "y = z"
by simp
then have x_eq_z: "x = z"
using x_eq_y y_eq_z by simp
then show "(x,z) \ diag_X"
using x_eq_z by (simp add: diag_X_def x_in_X z_in_X)
qed
then show ?thesis
by (simp only: is_transitive_def)
qed
from diag_X_is_relation_on_X
diag_X_is_reflexive
diag_X_is_symmetric
diag_X_is_transitive
show ?thesis by (simp add: is_equivalence_relation_def diag_X_def)
qed
text \As a slightly more concrete example, we show that the relation
of having a rational difference on the real numbers is an equivalence
relation.\
text \The set of all real numbers\
definition allreals :: "real set" where
"allreals = UNIV"
definition rational_diff :: "(real \ real) set" where
"rational_diff = {(x,y) . x \ allreals \ y \ allreals \ x-y \ Rats}"
lemma rational_diffs_in_reals_is_equivalence_relation:
shows "is_equivalence_relation allreals rational_diff"
proof -
have ratdiff_is_relation_on_R: "is_relation_on allreals rational_diff"
unfolding is_relation_on_def
proof (intro subsetI ballI)
fix xy :: "real \ real" assume "xy \ rational_diff"
then show "xy \ allreals \ allreals"
using rational_diff_def allreals_def by simp
qed
have ratdiff_is_reflexive: "is_reflexive allreals rational_diff"
unfolding is_reflexive_def
proof (intro ballI)
fix x :: real
show "(x,x) \ rational_diff"
by (simp add: rational_diff_def allreals_def)
qed
have ratdiff_is_symmetric: "is_symmetric allreals rational_diff"
unfolding is_symmetric_def
proof (intro ballI impI)
fix x :: real
fix y :: real
assume xy_in_ratdiff: "(x,y) \ rational_diff"
have "x-y \ Rats"
using xy_in_ratdiff rational_diff_def by auto
then have "-(x-y) \ Rats"
by (simp only: Rats_minus_iff)
(*alternatively: using Rats_minus_iff[of "x-y"] by simp *)
then have "y-x \ Rats"
by (simp add: arith)
then show "(y,x) \ rational_diff"
by (simp add: rational_diff_def allreals_def)
qed
have ratdiff_is_transitive: "is_transitive allreals rational_diff"
unfolding is_transitive_def
proof (intro ballI impI)
fix x :: real
fix y :: real
fix z :: real
assume xy_yz_ratdiff: "(x,y) \ rational_diff \ (y,z) \ rational_diff"
have xy_diff: "x-y \ Rats"
using xy_yz_ratdiff rational_diff_def by auto
have "(y,z) \ rational_diff"
using xy_yz_ratdiff by auto
then have yz_diff: "y-z \ Rats"
using rational_diff_def by auto
have "(x-y) + (y-z) \ Rats"
using xy_diff yz_diff by (simp only: Rats_add)
then have "x-z \ Rats"
using xy_diff yz_diff by (simp add: arith)
then show "(x,z) \ rational_diff"
by (simp add: rational_diff_def allreals_def)
qed
from ratdiff_is_relation_on_R
ratdiff_is_reflexive
ratdiff_is_symmetric
ratdiff_is_transitive
show ?thesis by (simp add: is_equivalence_relation_def)
qed
text \Moreover, we show that the relation of having even difference
on the integers is an equivalence relation.\
definition even_diff :: "(int \ int) set" where
"even_diff = {(x,y) . x \ Ints \ y \ Ints
\ (\ a \ Ints. x - y = 2 * a)}"
lemma even_diffs_in_integers_is_equivalence_relation:
shows "is_equivalence_relation Ints even_diff"
proof -
have evendiff_is_relation_on_Z: "is_relation_on Ints even_diff"
unfolding is_relation_on_def
proof (intro subsetI ballI)
fix xy :: "int \ int" assume "xy \ even_diff"
then show "xy \ Ints \ Ints"
using even_diff_def by (simp add: Ints_def)
qed
have evendiff_is_reflexive: "is_reflexive Ints even_diff"
unfolding is_reflexive_def
proof (intro ballI)
fix x :: int
have "x-x = 2 * 0"
by simp
then have "\ a \ Ints. x - x = 2 * a"
by (simp add: bexI)
then show "(x,x) \ even_diff"
by (simp add: Ints_def even_diff_def)
qed
have evendiff_is_symmetric: "is_symmetric Ints even_diff"
unfolding is_symmetric_def
proof (intro ballI impI)
fix x :: int
fix y :: int
assume xy_in_evendiff: "(x,y) \ even_diff"
from xy_in_evendiff obtain a :: int
where "x-y = 2*a" by (auto simp add: even_diff_def)
then have "y-x = 2 * (-a)"
by simp
then have "\ a \ Ints. y - x = 2 * a"
by (simp add: Ints_def)
then show "(y,x) \ even_diff"
by (simp add: Ints_def even_diff_def)
qed
have evendiff_is_transitive: "is_transitive Ints even_diff"
unfolding is_transitive_def
proof (intro ballI impI)
fix x :: int
fix y :: int
fix z :: int
assume xy_yz_in_evendiff: "(x,y) \ even_diff \ (y,z) \ even_diff"
from xy_yz_in_evendiff obtain a :: int
where "x-y = 2*a" by (auto simp add: even_diff_def)
moreover from xy_yz_in_evendiff obtain b :: int
where "y-z = 2*b" by (auto simp add: even_diff_def)
moreover define c :: int
where "c = a + b"
ultimately have xz_diff: "x-z = 2 * c"
by arith
have "c \ Ints"
proof -
have "a \ Ints" by (simp add: Ints_def)
moreover have "b \ Ints" by (simp add: Ints_def)
ultimately show "c \ Ints"
using c_def Ints_add by simp
qed
then have "\ c \ Ints. x-z = 2 * c"
using xz_diff by simp
then show "(x,z) \ even_diff"
by (simp add: Ints_def even_diff_def)
qed
from evendiff_is_relation_on_Z
evendiff_is_reflexive
evendiff_is_symmetric
evendiff_is_transitive
show ?thesis by (simp add: is_equivalence_relation_def)
qed
end