Theory Congruence

(*  Title:      HOL/Algebra/Congruence.thy
Author:     Clemens Ballarin, started 3 January 2008
with thanks to Paulo Emílio de Vilhena
*)

theory Congruence
imports
Main

begin

section ‹Objects›

subsection ‹Structure with Carrier Set.›

record 'a partial_object =
carrier :: "'a set"

lemma funcset_carrier:
" f  carrier X  carrier Y; x  carrier X   f x  carrier Y"
by (fact funcset_mem)

lemma funcset_carrier':
" f  carrier A  carrier A; x  carrier A   f x  carrier A"
by (fact funcset_mem)

subsection ‹Structure with Carrier and Equivalence Relation eq›

record 'a eq_object = "'a partial_object" +
eq :: "'a  'a  bool" (infixl ".=ı" 50)

definition
elem :: "_  'a  'a set  bool" (infixl ".∈ı" 50)
where "x .∈SA  (y  A. x .=Sy)"

definition
set_eq :: "_  'a set  'a set  bool" (infixl "{.=}ı" 50)
where "A {.=}SB  ((x  A. x .∈SB)  (x  B. x .∈SA))"

definition
eq_class_of :: "_  'a  'a set" ("class'_ofı")
where "class_ofSx = {y  carrier S. x .=Sy}"

definition
eq_classes :: "_  ('a set) set" ("classesı")
where "classesS= {class_ofSx | x. x  carrier S}"

definition
eq_closure_of :: "_  'a set  'a set" ("closure'_ofı")
where "closure_ofSA = {y  carrier S. y .∈SA}"

definition
eq_is_closed :: "_  'a set  bool" ("is'_closedı")
where "is_closedSA  A  carrier S  closure_ofSA = A"

abbreviation
not_eq :: "_  'a  'a  bool" (infixl ".≠ı" 50)
where "x .≠Sy  ¬(x .=Sy)"

abbreviation
not_elem :: "_  'a  'a set  bool" (infixl ".∉ı" 50)
where "x .∉SA  ¬(x .∈SA)"

abbreviation
set_not_eq :: "_  'a set  'a set  bool" (infixl "{.≠}ı" 50)
where "A {.≠}SB  ¬(A {.=}SB)"

locale equivalence =
fixes S (structure)
assumes refl [simp, intro]: "x  carrier S  x .= x"
and sym [sym]: " x .= y; x  carrier S; y  carrier S   y .= x"
and trans [trans]:
" x .= y; y .= z; x  carrier S; y  carrier S; z  carrier S   x .= z"

lemma equivalenceI:
fixes P :: "'a  'a  bool" and E :: "'a set"
assumes refl: "x.      x  E   P x x"
and    sym: "x y.    x  E; y  E   P x y  P y x"
and  trans: "x y z.  x  E; y  E; z  E   P x y  P y z  P x z"
shows "equivalence  carrier = E, eq = P "
unfolding equivalence_def using assms
by (metis eq_object.select_convs(1) partial_object.select_convs(1))

locale partition =
fixes A :: "'a set" and B :: "('a set) set"
assumes unique_class: "a. a  A  ∃!b  B. a  b"
and incl: "b. b  B  b  A"

lemma equivalence_subset:
assumes "equivalence L" "A  carrier L"
shows "equivalence (L carrier := A )"
proof -
interpret L: equivalence L
show ?thesis
by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
qed

(* Lemmas by Stephan Hohe *)

lemma elemI:
fixes R (structure)
assumes "a'  A" "a .= a'"
shows "a .∈ A"
unfolding elem_def using assms by auto

lemma (in equivalence) elem_exact:
assumes "a  carrier S" "a  A"
shows "a .∈ A"
unfolding elem_def using assms by auto

lemma elemE:
fixes S (structure)
assumes "a .∈ A"
and "a'. a'  A; a .= a'  P"
shows "P"
using assms unfolding elem_def by auto

lemma (in equivalence) elem_cong_l [trans]:
assumes "a  carrier S"  "a'  carrier S" "A  carrier S"
and "a' .= a" "a .∈ A"
shows "a' .∈ A"
using assms by (meson elem_def trans subsetCE)

lemma (in equivalence) elem_subsetD:
assumes "A  B" "a .∈ A"
shows "a .∈ B"
using assms by (fast intro: elemI elim: elemE dest: subsetD)

lemma (in equivalence) mem_imp_elem [simp, intro]:
assumes "x  carrier S"
shows "x  A  x .∈ A"
using assms unfolding elem_def by blast

lemma set_eqI:
fixes R (structure)
assumes "a. a  A  a .∈ B"
and   "b. b  B  b .∈ A"
shows "A {.=} B"
using assms unfolding set_eq_def by auto

lemma set_eqI2:
fixes R (structure)
assumes "a. a  A  b  B. a .= b"
and   "b. b  B  a  A. b .= a"
shows "A {.=} B"
using assms by (simp add: set_eqI elem_def)

lemma set_eqD1:
fixes R (structure)
assumes "A {.=} A'" and "a  A"
shows "a'A'. a .= a'"
using assms by (simp add: set_eq_def elem_def)

lemma set_eqD2:
fixes R (structure)
assumes "A {.=} A'" and "a'  A'"
shows "aA. a' .= a"
using assms by (simp add: set_eq_def elem_def)

lemma set_eqE:
fixes R (structure)
assumes "A {.=} B"
and " a  A. a .∈ B; b  B. b .∈ A   P"
shows "P"
using assms unfolding set_eq_def by blast

lemma set_eqE2:
fixes R (structure)
assumes "A {.=} B"
and " a  A. b  B. a .= b; b  B. a  A. b .= a   P"
shows "P"
using assms unfolding set_eq_def by (simp add: elem_def)

lemma set_eqE':
fixes R (structure)
assumes "A {.=} B" "a  A" "b  B"
and "a' b'.  a'  A; b'  B   b .= a'   a .= b'  P"
shows "P"
using assms by (meson set_eqE2)

lemma (in equivalence) eq_elem_cong_r [trans]:
assumes "A  carrier S" "A'  carrier S" "A {.=} A'"
shows " a  carrier S   a .∈ A  a .∈ A'"
using assms by (meson elemE elem_cong_l set_eqE subset_eq)

lemma (in equivalence) set_eq_sym [sym]:
assumes "A  carrier S" "B  carrier S"
shows "A {.=} B  B {.=} A"
using assms unfolding set_eq_def elem_def by auto

lemma (in equivalence) equal_set_eq_trans [trans]:
" A = B; B {.=} C   A {.=} C"
by simp

lemma (in equivalence) set_eq_equal_trans [trans]:
" A {.=} B; B = C   A {.=} C"
by simp

lemma (in equivalence) set_eq_trans_aux:
assumes "A  carrier S" "B  carrier S" "C  carrier S"
and "A {.=} B" "B {.=} C"
shows "a. a  A  a .∈ C"
using assms by (simp add: eq_elem_cong_r subset_iff)

corollary (in equivalence) set_eq_trans [trans]:
assumes "A  carrier S" "B  carrier S" "C  carrier S"
and "A {.=} B" " B {.=} C"
shows "A {.=} C"
proof (intro set_eqI)
show "a. a  A  a .∈ C" using set_eq_trans_aux assms by blast
next
show "b. b  C  b .∈ A" using set_eq_trans_aux set_eq_sym assms by blast
qed

lemma (in equivalence) is_closedI:
assumes closed: "x y. x .= y; x  A; y  carrier S  y  A"
and S: "A  carrier S"
shows "is_closed A"
unfolding eq_is_closed_def eq_closure_of_def elem_def
using S
by (blast dest: closed sym)

lemma (in equivalence) closure_of_eq:
assumes "A  carrier S" "x  closure_of A"
shows " x'  carrier S; x .= x'   x'  closure_of A"
using assms elem_cong_l sym unfolding eq_closure_of_def by blast

lemma (in equivalence) is_closed_eq [dest]:
assumes "is_closed A" "x  A"
shows " x .= x'; x'  carrier S   x'  A"
using assms closure_of_eq [where A = A] unfolding eq_is_closed_def by simp

corollary (in equivalence) is_closed_eq_rev [dest]:
assumes "is_closed A" "x'  A"
shows " x .= x'; x  carrier S   x  A"
using sym is_closed_eq assms by (meson contra_subsetD eq_is_closed_def)

lemma closure_of_closed [simp, intro]:
fixes S (structure)
shows
unfolding eq_closure_of_def by auto

lemma closure_of_memI:
fixes S (structure)
assumes "a .∈ A" "a  carrier S"
shows "a  closure_of A"

lemma closure_ofI2:
fixes S (structure)
assumes "a .= a'" and "a'  A" and "a  carrier S"
shows "a  closure_of A"
by (meson assms closure_of_memI elem_def)

lemma closure_of_memE:
fixes S (structure)
assumes "a  closure_of A"
and "a  carrier S; a .∈ A  P"
shows "P"
using eq_closure_of_def assms by fastforce

lemma closure_ofE2:
fixes S (structure)
assumes "a  closure_of A"
and "a'. a  carrier S; a'  A; a .= a'  P"
shows "P"
using assms by (meson closure_of_memE elemE)

lemma (in partition) equivalence_from_partition: contributor ‹Paulo Emílio de Vilhena›
"equivalence  carrier = A, eq = (λx y. y  (THE b. b  B  x  b))"
unfolding partition_def equivalence_def
proof (auto)
let ?f = "λx. THE b. b  B  x  b"
show "x. x  A  x  ?f x"
using unique_class by (metis (mono_tags, lifting) theI')
show "x y.  x  A; y  A   y  ?f x  x  ?f y"
using unique_class by (metis (mono_tags, lifting) the_equality)
show "x y z.  x  A; y  A; z  A   y  ?f x  z  ?f y  z  ?f x"
using unique_class by (metis (mono_tags, lifting) the_equality)
qed

lemma (in partition) partition_coverture: "B = A" contributor ‹Paulo Emílio de Vilhena›
by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)

lemma (in partition) disjoint_union: contributor ‹Paulo Emílio de Vilhena›
assumes "b1  B" "b2  B"
and "b1  b2  {}"
shows "b1 = b2"
proof (rule ccontr)
assume "b1  b2"
obtain a where "a  A" "a  b1" "a  b2"
using assms(2-3) incl by blast
thus False using unique_class b1  b2 assms(1) assms(2) by blast
qed

lemma partitionI: contributor ‹Paulo Emílio de Vilhena›
fixes A :: "'a set" and B :: "('a set) set"
assumes "B = A"
and "b1 b2.  b1  B; b2  B   b1  b2  {}  b1 = b2"
shows "partition A B"
proof
show "a. a  A  ∃!b. b  B  a  b"
proof (rule ccontr)
fix a assume "a  A" "∄!b. b  B  a  b"
then obtain b1 b2 where "b1  B" "a  b1"
and "b2  B" "a  b2" "b1  b2" using assms(1) by blast
thus False using assms(2) by blast
qed
next
show "b. b  B  b  A" using assms(1) by blast
qed

lemma (in partition) remove_elem: contributor ‹Paulo Emílio de Vilhena›
assumes "b  B"
shows "partition (A - b) (B - {b})"
proof
show "a. a  A - b  ∃!b'. b'  B - {b}  a  b'"
using unique_class by fastforce
next
show "b'. b'  B - {b}  b'  A - b"
using assms unique_class incl partition_axioms partition_coverture by fastforce
qed

lemma disjoint_sum: contributor ‹Paulo Emílio de Vilhena›
" finite B; finite A; partition A B  (bB. ab. f a) = (aA. f a)"
proof (induct arbitrary: A set: finite)
case empty thus ?case using partition.unique_class by fastforce
next
case (insert b B')
have "(b(insert b B'). ab. f a) = (ab. f a) + (bB'. ab. f a)"
also have "... = (ab. f a) + (a(A - b). f a)"
using partition.remove_elem[of A "insert b B'" b] insert.hyps insert.prems
by (metis Diff_insert_absorb finite_Diff insert_iff)
finally show "(b(insert b B'). ab. f a) = (aA. f a)"
using partition.remove_elem[of A "insert b B'" b] insert.prems
by (metis add.commute insert_iff partition.incl sum.subset_diff)
qed

lemma (in partition) disjoint_sum: contributor ‹Paulo Emílio de Vilhena›
assumes "finite A"
shows "(bB. ab. f a) = (aA. f a)"
proof -
have "finite B"
by (simp add: assms finite_UnionD partition_coverture)
thus ?thesis using disjoint_sum assms partition_axioms by blast
qed

lemma (in equivalence) set_eq_insert_aux: contributor ‹Paulo Emílio de Vilhena›
assumes "A  carrier S"
and "x  carrier S" "x'  carrier S" "x .= x'"
and "y  insert x A"
shows "y .∈ insert x' A"
by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)

corollary (in equivalence) set_eq_insert: contributor ‹Paulo Emílio de Vilhena›
assumes "A  carrier S"
and "x  carrier S" "x'  carrier S" "x .= x'"
shows "insert x A {.=} insert x' A"
by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)

lemma (in equivalence) set_eq_pairI: contributor ‹Paulo Emílio de Vilhena›
assumes xx': "x .= x'"
and carr: "x  carrier S" "x'  carrier S" "y  carrier S"
shows "{x, y} {.=} {x', y}"
using assms set_eq_insert by simp

lemma (in equivalence) closure_inclusion:
assumes "A  B"
shows
unfolding eq_closure_of_def using assms elem_subsetD by auto

lemma (in equivalence) classes_small:
assumes "is_closed B"
and "A  B"
shows "closure_of A  B"
by (metis assms closure_inclusion eq_is_closed_def)

lemma (in equivalence) classes_eq:
assumes "A  carrier S"
shows "A {.=} closure_of A"
using assms by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)

lemma (in equivalence) complete_classes:
assumes "is_closed A"
shows "A = closure_of A"
using assms by (simp add: eq_is_closed_def)

lemma (in equivalence) closure_idem_weak:

lemma (in equivalence) closure_idem_strong:
assumes "A  carrier S"
shows
using assms closure_of_eq complete_classes is_closedI by auto

lemma (in equivalence) classes_consistent:
assumes "A  carrier S"
shows "is_closed (closure_of A)"
using closure_idem_strong by (simp add: assms eq_is_closed_def)

lemma (in equivalence) classes_coverture:

proof
show
unfolding eq_classes_def eq_class_of_def by blast
next
show  unfolding eq_classes_def eq_class_of_def
proof
fix x assume "x  carrier S"
hence "x  {y  carrier S. x .= y}" using refl by simp
thus "x  {{y  carrier S. x .= y} |x. x  carrier S}" by blast
qed
qed

lemma (in equivalence) disjoint_union:
assumes "class1  classes" "class2  classes"
and "class1  class2  {}"
shows "class1 = class2"
proof -
obtain x y where x: "x  carrier S" "class1 = class_of x"
and y: "y  carrier S" "class2 = class_of y"
using assms(1-2) unfolding eq_classes_def by blast
obtain z   where z: "z  carrier S" "z  class1  class2"
using assms classes_coverture by fastforce
hence "x .= z  y .= z" using x y unfolding eq_class_of_def by blast
hence "x .= y" using x y z trans sym by meson
hence
unfolding eq_class_of_def using local.sym trans x y by blast
thus ?thesis using x y by simp
qed

lemma (in equivalence) partition_from_equivalence:

proof (intro partitionI)
show  using classes_coverture by simp
next
show "class1 class2.  class1  classes; class2  classes
class1  class2  {}  class1 = class2"
using disjoint_union by simp
qed

lemma (in equivalence) disjoint_sum:
assumes "finite (carrier S)"
shows "(cclasses. xc. f x) = (x(carrier S). f x)"
proof -
have
unfolding eq_classes_def using assms by auto
thus ?thesis using disjoint_sum assms partition_from_equivalence by blast
qed

end