Quelle  Congruence.thy

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

theory Congruence
  imports
    Main
    "HOL-Library.FuncSet"
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 .∈🪙S🪙 A ⟷ (∃y ∈ A. x .=🪙S🪙 y)"

definition
  set_eq :: "_ ==> 'a set ==> 'a set ==> bool" (infixl ‹{.=}🍋› 50)
  where "A {.=}🪙S🪙 B ⟷ ((∀x ∈ A. x .∈🪙S🪙 B) ∧ (∀x ∈ B. x .∈🪙S🪙 A))"

definition
  eq_class_of :: "_ ==> 'a ==> 'a set" (‹class'_of🍋›)
  where "class_of🪙S🪙 x = {y ∈ carrier S. x .=🪙S🪙 y}"

definition
  eq_classes :: "_ ==> ('a set) set" (‹classes🍋›)
  where "classes🪙S🪙 = {class_of🪙S🪙 x | x. x ∈ carrier S}"

definition
  eq_closure_of :: "_ ==> 'a set ==> 'a set" (‹closure'_of🍋›)
  where "closure_of🪙S🪙 A = {y ∈ carrier S. y .∈🪙S🪙 A}"

definition
  eq_is_closed :: "_ ==> 'a set ==> bool" (‹is'_closed🍋›)
  where "is_closed🪙S🪙 A ⟷ A ⊆ carrier S ∧ closure_of🪙S🪙 A = A"

abbreviation
  not_eq :: "_ ==> 'a ==> 'a ==> bool" (infixl ‹.≠🍋› 50)
  where "x .≠🪙S🪙 y ≡ ¬(x .=🪙S🪙 y)"

abbreviation
  not_elem :: "_ ==> 'a ==> 'a set ==> bool" (infixl ‹.∉🍋› 50)
  where "x .∉🪙S🪙 A ≡ ¬(x .∈🪙S🪙 A)"

abbreviation
  set_not_eq :: "_ ==> 'a set ==> 'a set ==> bool" (infixl ‹{.≠}🍋› 50)
  where "A {.≠}🪙S🪙 B ≡ ¬(A {.=}🪙S🪙 B)"

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
    by (simp add: assms)
  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 "∃a∈A. 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 "closure_of A ⊆ carrier S"
  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"
  by (simp add: assms eq_closure_of_def)

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] ==> (∑b∈B. ∑a∈b. f a) = (∑a∈A. 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'). ∑a∈b. f a) = (∑a∈b. f a) + (∑b∈B'. ∑a∈b. f a)"
    by (simp add: insert.hyps(1) insert.hyps(2))
  also have "... = (∑a∈b. 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'). ∑a∈b. f a) = (∑a∈A. 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 "(∑b∈B. ∑a∈b. f a) = (∑a∈A. 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 "closure_of A ⊆ closure_of B"
  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:
  "closure_of (closure_of A) {.=} closure_of A"
  by (simp add: classes_eq set_eq_sym)

lemma (in equivalence) closure_idem_strong:
  assumes "A ⊆ carrier S"
  shows "closure_of (closure_of A) = closure_of A"
  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:
  "∪classes = carrier S"
proof
  show "∪classes ⊆ carrier S"
    unfolding eq_classes_def eq_class_of_def by blast
next
  show "carrier S ⊆ ∪classes" 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 "class_of x = class_of y"
    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:
  "partition (carrier S) classes"
proof (intro partitionI)
  show "∪classes = carrier S" 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 "(∑c∈classes. ∑x∈c. f x) = (∑x∈(carrier S). f x)"
proof -
  have "finite classes"
    unfolding eq_classes_def using assms by auto
  thus ?thesis using disjoint_sum assms partition_from_equivalence by blast
qed
  
end