src/HOL/Algebra/Congruence.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68443 43055b016688
child 69895 6b03a8cf092d
permissions -rw-r--r--
More on Algebra by Paulo and Martin
     1 (*  Title:      HOL/Algebra/Congruence.thy
     2     Author:     Clemens Ballarin, started 3 January 2008
     3     with thanks to Paulo Emílio de Vilhena
     4 *)
     5 
     6 theory Congruence
     7   imports
     8     Main
     9     "HOL-Library.FuncSet"
    10 begin
    11 
    12 section \<open>Objects\<close>
    13 
    14 subsection \<open>Structure with Carrier Set.\<close>
    15 
    16 record 'a partial_object =
    17   carrier :: "'a set"
    18 
    19 lemma funcset_carrier:
    20   "\<lbrakk> f \<in> carrier X \<rightarrow> carrier Y; x \<in> carrier X \<rbrakk> \<Longrightarrow> f x \<in> carrier Y"
    21   by (fact funcset_mem)
    22 
    23 lemma funcset_carrier':
    24   "\<lbrakk> f \<in> carrier A \<rightarrow> carrier A; x \<in> carrier A \<rbrakk> \<Longrightarrow> f x \<in> carrier A"
    25   by (fact funcset_mem)
    26 
    27 
    28 subsection \<open>Structure with Carrier and Equivalence Relation \<open>eq\<close>\<close>
    29 
    30 record 'a eq_object = "'a partial_object" +
    31   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
    32 
    33 definition
    34   elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
    35   where "x .\<in>\<^bsub>S\<^esub> A \<longleftrightarrow> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
    36 
    37 definition
    38   set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
    39   where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
    40 
    41 definition
    42   eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index>")
    43   where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
    44 
    45 definition
    46   eq_classes :: "_ \<Rightarrow> ('a set) set" ("classes\<index>")
    47   where "classes\<^bsub>S\<^esub> = {class_of\<^bsub>S\<^esub> x | x. x \<in> carrier S}"
    48 
    49 definition
    50   eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index>")
    51   where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
    52 
    53 definition
    54   eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index>")
    55   where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
    56 
    57 abbreviation
    58   not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
    59   where "x .\<noteq>\<^bsub>S\<^esub> y \<equiv> \<not>(x .=\<^bsub>S\<^esub> y)"
    60 
    61 abbreviation
    62   not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50)
    63   where "x .\<notin>\<^bsub>S\<^esub> A \<equiv> \<not>(x .\<in>\<^bsub>S\<^esub> A)"
    64 
    65 abbreviation
    66   set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50)
    67   where "A {.\<noteq>}\<^bsub>S\<^esub> B \<equiv> \<not>(A {.=}\<^bsub>S\<^esub> B)"
    68 
    69 locale equivalence =
    70   fixes S (structure)
    71   assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x"
    72     and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x"
    73     and trans [trans]:
    74       "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z"
    75 
    76 lemma equivalenceI:
    77   fixes P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and E :: "'a set"
    78   assumes refl: "\<And>x.     \<lbrakk> x \<in> E \<rbrakk> \<Longrightarrow> P x x"
    79     and    sym: "\<And>x y.   \<lbrakk> x \<in> E; y \<in> E \<rbrakk> \<Longrightarrow> P x y \<Longrightarrow> P y x"
    80     and  trans: "\<And>x y z. \<lbrakk> x \<in> E; y \<in> E; z \<in> E \<rbrakk> \<Longrightarrow> P x y \<Longrightarrow> P y z \<Longrightarrow> P x z"
    81   shows "equivalence \<lparr> carrier = E, eq = P \<rparr>"
    82   unfolding equivalence_def using assms
    83   by (metis eq_object.select_convs(1) partial_object.select_convs(1))
    84 
    85 locale partition =
    86   fixes A :: "'a set" and B :: "('a set) set"
    87   assumes unique_class: "\<And>a. a \<in> A \<Longrightarrow> \<exists>!b \<in> B. a \<in> b"
    88     and incl: "\<And>b. b \<in> B \<Longrightarrow> b \<subseteq> A"
    89 
    90 lemma equivalence_subset:
    91   assumes "equivalence L" "A \<subseteq> carrier L"
    92   shows "equivalence (L\<lparr> carrier := A \<rparr>)"
    93 proof -
    94   interpret L: equivalence L
    95     by (simp add: assms)
    96   show ?thesis
    97     by (unfold_locales, simp_all add: L.sym assms rev_subsetD, meson L.trans assms(2) contra_subsetD)
    98 qed
    99 
   100 
   101 (* Lemmas by Stephan Hohe *)
   102 
   103 lemma elemI:
   104   fixes R (structure)
   105   assumes "a' \<in> A" "a .= a'"
   106   shows "a .\<in> A"
   107   unfolding elem_def using assms by auto
   108 
   109 lemma (in equivalence) elem_exact:
   110   assumes "a \<in> carrier S" "a \<in> A"
   111   shows "a .\<in> A"
   112   unfolding elem_def using assms by auto
   113 
   114 lemma elemE:
   115   fixes S (structure)
   116   assumes "a .\<in> A"
   117     and "\<And>a'. \<lbrakk>a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
   118   shows "P"
   119   using assms unfolding elem_def by auto
   120 
   121 lemma (in equivalence) elem_cong_l [trans]:
   122   assumes "a \<in> carrier S"  "a' \<in> carrier S" "A \<subseteq> carrier S"
   123     and "a' .= a" "a .\<in> A"
   124   shows "a' .\<in> A"
   125   using assms by (meson elem_def trans subsetCE)
   126 
   127 lemma (in equivalence) elem_subsetD:
   128   assumes "A \<subseteq> B" "a .\<in> A"
   129   shows "a .\<in> B"
   130   using assms by (fast intro: elemI elim: elemE dest: subsetD)
   131 
   132 lemma (in equivalence) mem_imp_elem [simp, intro]:
   133   assumes "x \<in> carrier S"
   134   shows "x \<in> A \<Longrightarrow> x .\<in> A"
   135   using assms unfolding elem_def by blast
   136 
   137 lemma set_eqI:
   138   fixes R (structure)
   139   assumes "\<And>a. a \<in> A \<Longrightarrow> a .\<in> B"
   140     and   "\<And>b. b \<in> B \<Longrightarrow> b .\<in> A"
   141   shows "A {.=} B"
   142   using assms unfolding set_eq_def by auto
   143 
   144 lemma set_eqI2:
   145   fixes R (structure)
   146   assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b \<in> B. a .= b"
   147     and   "\<And>b. b \<in> B \<Longrightarrow> \<exists>a \<in> A. b .= a"
   148   shows "A {.=} B"
   149   using assms by (simp add: set_eqI elem_def)  
   150 
   151 lemma set_eqD1:
   152   fixes R (structure)
   153   assumes "A {.=} A'" and "a \<in> A"
   154   shows "\<exists>a'\<in>A'. a .= a'"
   155   using assms by (simp add: set_eq_def elem_def)
   156 
   157 lemma set_eqD2:
   158   fixes R (structure)
   159   assumes "A {.=} A'" and "a' \<in> A'"
   160   shows "\<exists>a\<in>A. a' .= a"
   161   using assms by (simp add: set_eq_def elem_def)
   162 
   163 lemma set_eqE:
   164   fixes R (structure)
   165   assumes "A {.=} B"
   166     and "\<lbrakk> \<forall>a \<in> A. a .\<in> B; \<forall>b \<in> B. b .\<in> A \<rbrakk> \<Longrightarrow> P"
   167   shows "P"
   168   using assms unfolding set_eq_def by blast
   169 
   170 lemma set_eqE2:
   171   fixes R (structure)
   172   assumes "A {.=} B"
   173     and "\<lbrakk> \<forall>a \<in> A. \<exists>b \<in> B. a .= b; \<forall>b \<in> B. \<exists>a \<in> A. b .= a \<rbrakk> \<Longrightarrow> P"
   174   shows "P"
   175   using assms unfolding set_eq_def by (simp add: elem_def) 
   176 
   177 lemma set_eqE':
   178   fixes R (structure)
   179   assumes "A {.=} B" "a \<in> A" "b \<in> B"
   180     and "\<And>a' b'. \<lbrakk> a' \<in> A; b' \<in> B \<rbrakk> \<Longrightarrow> b .= a' \<Longrightarrow>  a .= b' \<Longrightarrow> P"
   181   shows "P"
   182   using assms by (meson set_eqE2)
   183 
   184 lemma (in equivalence) eq_elem_cong_r [trans]:
   185   assumes "A \<subseteq> carrier S" "A' \<subseteq> carrier S" "A {.=} A'"
   186   shows "\<lbrakk> a \<in> carrier S \<rbrakk> \<Longrightarrow> a .\<in> A \<Longrightarrow> a .\<in> A'"
   187   using assms by (meson elemE elem_cong_l set_eqE subset_eq)
   188 
   189 lemma (in equivalence) set_eq_sym [sym]:
   190   assumes "A \<subseteq> carrier S" "B \<subseteq> carrier S"
   191   shows "A {.=} B \<Longrightarrow> B {.=} A"
   192   using assms unfolding set_eq_def elem_def by auto
   193 
   194 lemma (in equivalence) equal_set_eq_trans [trans]:
   195   "\<lbrakk> A = B; B {.=} C \<rbrakk> \<Longrightarrow> A {.=} C"
   196   by simp
   197 
   198 lemma (in equivalence) set_eq_equal_trans [trans]:
   199   "\<lbrakk> A {.=} B; B = C \<rbrakk> \<Longrightarrow> A {.=} C"
   200   by simp
   201 
   202 lemma (in equivalence) set_eq_trans_aux:
   203   assumes "A \<subseteq> carrier S" "B \<subseteq> carrier S" "C \<subseteq> carrier S"
   204     and "A {.=} B" "B {.=} C"
   205   shows "\<And>a. a \<in> A \<Longrightarrow> a .\<in> C"
   206   using assms by (simp add: eq_elem_cong_r subset_iff) 
   207 
   208 corollary (in equivalence) set_eq_trans [trans]:
   209   assumes "A \<subseteq> carrier S" "B \<subseteq> carrier S" "C \<subseteq> carrier S"
   210     and "A {.=} B" " B {.=} C"
   211   shows "A {.=} C"
   212 proof (intro set_eqI)
   213   show "\<And>a. a \<in> A \<Longrightarrow> a .\<in> C" using set_eq_trans_aux assms by blast 
   214 next
   215   show "\<And>b. b \<in> C \<Longrightarrow> b .\<in> A" using set_eq_trans_aux set_eq_sym assms by blast
   216 qed
   217 
   218 lemma (in equivalence) is_closedI:
   219   assumes closed: "\<And>x y. \<lbrakk>x .= y; x \<in> A; y \<in> carrier S\<rbrakk> \<Longrightarrow> y \<in> A"
   220     and S: "A \<subseteq> carrier S"
   221   shows "is_closed A"
   222   unfolding eq_is_closed_def eq_closure_of_def elem_def
   223   using S
   224   by (blast dest: closed sym)
   225 
   226 lemma (in equivalence) closure_of_eq:
   227   assumes "A \<subseteq> carrier S" "x \<in> closure_of A"
   228   shows "\<lbrakk> x' \<in> carrier S; x .= x' \<rbrakk> \<Longrightarrow> x' \<in> closure_of A"
   229   using assms elem_cong_l sym unfolding eq_closure_of_def by blast 
   230 
   231 lemma (in equivalence) is_closed_eq [dest]:
   232   assumes "is_closed A" "x \<in> A"
   233   shows "\<lbrakk> x .= x'; x' \<in> carrier S \<rbrakk> \<Longrightarrow> x' \<in> A"
   234   using assms closure_of_eq [where A = A] unfolding eq_is_closed_def by simp
   235 
   236 corollary (in equivalence) is_closed_eq_rev [dest]:
   237   assumes "is_closed A" "x' \<in> A"
   238   shows "\<lbrakk> x .= x'; x \<in> carrier S \<rbrakk> \<Longrightarrow> x \<in> A"
   239   using sym is_closed_eq assms by (meson contra_subsetD eq_is_closed_def)
   240 
   241 lemma closure_of_closed [simp, intro]:
   242   fixes S (structure)
   243   shows "closure_of A \<subseteq> carrier S"
   244   unfolding eq_closure_of_def by auto
   245 
   246 lemma closure_of_memI:
   247   fixes S (structure)
   248   assumes "a .\<in> A" "a \<in> carrier S"
   249   shows "a \<in> closure_of A"
   250   by (simp add: assms eq_closure_of_def)
   251 
   252 lemma closure_ofI2:
   253   fixes S (structure)
   254   assumes "a .= a'" and "a' \<in> A" and "a \<in> carrier S"
   255   shows "a \<in> closure_of A"
   256   by (meson assms closure_of_memI elem_def)
   257 
   258 lemma closure_of_memE:
   259   fixes S (structure)
   260   assumes "a \<in> closure_of A"
   261     and "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
   262   shows "P"
   263   using eq_closure_of_def assms by fastforce
   264 
   265 lemma closure_ofE2:
   266   fixes S (structure)
   267   assumes "a \<in> closure_of A"
   268     and "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
   269   shows "P"
   270   using assms by (meson closure_of_memE elemE)
   271 
   272 
   273 (* Lemmas by Paulo Emílio de Vilhena *)
   274 
   275 lemma (in partition) equivalence_from_partition:
   276   "equivalence \<lparr> carrier = A, eq = (\<lambda>x y. y \<in> (THE b. b \<in> B \<and> x \<in> b))\<rparr>"
   277     unfolding partition_def equivalence_def
   278 proof (auto)
   279   let ?f = "\<lambda>x. THE b. b \<in> B \<and> x \<in> b"
   280   show "\<And>x. x \<in> A \<Longrightarrow> x \<in> ?f x"
   281     using unique_class by (metis (mono_tags, lifting) theI')
   282   show "\<And>x y. \<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<in> ?f x \<Longrightarrow> x \<in> ?f y"
   283     using unique_class by (metis (mono_tags, lifting) the_equality)
   284   show "\<And>x y z. \<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> y \<in> ?f x \<Longrightarrow> z \<in> ?f y \<Longrightarrow> z \<in> ?f x"
   285     using unique_class by (metis (mono_tags, lifting) the_equality)
   286 qed
   287 
   288 lemma (in partition) partition_coverture: "\<Union>B = A"
   289   by (meson Sup_le_iff UnionI unique_class incl subsetI subset_antisym)
   290 
   291 lemma (in partition) disjoint_union:
   292   assumes "b1 \<in> B" "b2 \<in> B"
   293     and "b1 \<inter> b2 \<noteq> {}"
   294   shows "b1 = b2"
   295 proof (rule ccontr)
   296   assume "b1 \<noteq> b2"
   297   obtain a where "a \<in> A" "a \<in> b1" "a \<in> b2"
   298     using assms(2-3) incl by blast
   299   thus False using unique_class \<open>b1 \<noteq> b2\<close> assms(1) assms(2) by blast
   300 qed
   301 
   302 lemma partitionI:
   303   fixes A :: "'a set" and B :: "('a set) set"
   304   assumes "\<Union>B = A"
   305     and "\<And>b1 b2. \<lbrakk> b1 \<in> B; b2 \<in> B \<rbrakk> \<Longrightarrow> b1 \<inter> b2 \<noteq> {} \<Longrightarrow> b1 = b2"
   306   shows "partition A B"
   307 proof
   308   show "\<And>a. a \<in> A \<Longrightarrow> \<exists>!b. b \<in> B \<and> a \<in> b"
   309   proof (rule ccontr)
   310     fix a assume "a \<in> A" "\<nexists>!b. b \<in> B \<and> a \<in> b"
   311     then obtain b1 b2 where "b1 \<in> B" "a \<in> b1"
   312                         and "b2 \<in> B" "a \<in> b2" "b1 \<noteq> b2" using assms(1) by blast
   313     thus False using assms(2) by blast
   314   qed
   315 next
   316   show "\<And>b. b \<in> B \<Longrightarrow> b \<subseteq> A" using assms(1) by blast
   317 qed
   318 
   319 lemma (in partition) remove_elem:
   320   assumes "b \<in> B"
   321   shows "partition (A - b) (B - {b})"
   322 proof
   323   show "\<And>a. a \<in> A - b \<Longrightarrow> \<exists>!b'. b' \<in> B - {b} \<and> a \<in> b'"
   324     using unique_class by fastforce
   325 next
   326   show "\<And>b'. b' \<in> B - {b} \<Longrightarrow> b' \<subseteq> A - b"
   327     using assms unique_class incl partition_axioms partition_coverture by fastforce
   328 qed
   329 
   330 lemma disjoint_sum:
   331   "\<lbrakk> finite B; finite A; partition A B\<rbrakk> \<Longrightarrow> (\<Sum>b\<in>B. \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
   332 proof (induct arbitrary: A set: finite)
   333   case empty thus ?case using partition.unique_class by fastforce
   334 next
   335   case (insert b B')
   336   have "(\<Sum>b\<in>(insert b B'). \<Sum>a\<in>b. f a) = (\<Sum>a\<in>b. f a) + (\<Sum>b\<in>B'. \<Sum>a\<in>b. f a)"
   337     by (simp add: insert.hyps(1) insert.hyps(2))
   338   also have "... = (\<Sum>a\<in>b. f a) + (\<Sum>a\<in>(A - b). f a)"
   339     using partition.remove_elem[of A "insert b B'" b] insert.hyps insert.prems
   340     by (metis Diff_insert_absorb finite_Diff insert_iff)
   341   finally show "(\<Sum>b\<in>(insert b B'). \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
   342     using partition.remove_elem[of A "insert b B'" b] insert.prems
   343     by (metis add.commute insert_iff partition.incl sum.subset_diff)
   344 qed
   345 
   346 lemma (in partition) disjoint_sum:
   347   assumes "finite A"
   348   shows "(\<Sum>b\<in>B. \<Sum>a\<in>b. f a) = (\<Sum>a\<in>A. f a)"
   349 proof -
   350   have "finite B"
   351     by (simp add: assms finite_UnionD partition_coverture)
   352   thus ?thesis using disjoint_sum assms partition_axioms by blast
   353 qed
   354 
   355 lemma (in equivalence) set_eq_insert_aux:
   356   assumes "A \<subseteq> carrier S"
   357     and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
   358     and "y \<in> insert x A"
   359   shows "y .\<in> insert x' A"
   360   by (metis assms(1) assms(4) assms(5) contra_subsetD elemI elem_exact insert_iff)
   361 
   362 corollary (in equivalence) set_eq_insert:
   363   assumes "A \<subseteq> carrier S"
   364     and "x \<in> carrier S" "x' \<in> carrier S" "x .= x'"
   365   shows "insert x A {.=} insert x' A"
   366   by (meson set_eqI assms set_eq_insert_aux sym equivalence_axioms)
   367 
   368 lemma (in equivalence) set_eq_pairI:
   369   assumes xx': "x .= x'"
   370     and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
   371   shows "{x, y} {.=} {x', y}"
   372   using assms set_eq_insert by simp
   373 
   374 lemma (in equivalence) closure_inclusion:
   375   assumes "A \<subseteq> B"
   376   shows "closure_of A \<subseteq> closure_of B"
   377   unfolding eq_closure_of_def using assms elem_subsetD by auto
   378 
   379 lemma (in equivalence) classes_small:
   380   assumes "is_closed B"
   381     and "A \<subseteq> B"
   382   shows "closure_of A \<subseteq> B"
   383   by (metis assms closure_inclusion eq_is_closed_def)
   384 
   385 lemma (in equivalence) classes_eq:
   386   assumes "A \<subseteq> carrier S"
   387   shows "A {.=} closure_of A"
   388   using assms by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE)
   389 
   390 lemma (in equivalence) complete_classes:
   391   assumes "is_closed A"
   392   shows "A = closure_of A"
   393   using assms by (simp add: eq_is_closed_def)
   394 
   395 lemma (in equivalence) closure_idem_weak:
   396   "closure_of (closure_of A) {.=} closure_of A"
   397   by (simp add: classes_eq set_eq_sym)
   398 
   399 lemma (in equivalence) closure_idem_strong:
   400   assumes "A \<subseteq> carrier S"
   401   shows "closure_of (closure_of A) = closure_of A"
   402   using assms closure_of_eq complete_classes is_closedI by auto
   403 
   404 lemma (in equivalence) classes_consistent:
   405   assumes "A \<subseteq> carrier S"
   406   shows "is_closed (closure_of A)"
   407   using closure_idem_strong by (simp add: assms eq_is_closed_def)
   408 
   409 lemma (in equivalence) classes_coverture:
   410   "\<Union>classes = carrier S"
   411 proof
   412   show "\<Union>classes \<subseteq> carrier S"
   413     unfolding eq_classes_def eq_class_of_def by blast
   414 next
   415   show "carrier S \<subseteq> \<Union>classes" unfolding eq_classes_def eq_class_of_def
   416   proof
   417     fix x assume "x \<in> carrier S"
   418     hence "x \<in> {y \<in> carrier S. x .= y}" using refl by simp
   419     thus "x \<in> \<Union>{{y \<in> carrier S. x .= y} |x. x \<in> carrier S}" by blast
   420   qed
   421 qed
   422 
   423 lemma (in equivalence) disjoint_union:
   424   assumes "class1 \<in> classes" "class2 \<in> classes"
   425     and "class1 \<inter> class2 \<noteq> {}"
   426     shows "class1 = class2"
   427 proof -
   428   obtain x y where x: "x \<in> carrier S" "class1 = class_of x"
   429                and y: "y \<in> carrier S" "class2 = class_of y"
   430     using assms(1-2) unfolding eq_classes_def by blast
   431   obtain z   where z: "z \<in> carrier S" "z \<in> class1 \<inter> class2"
   432     using assms classes_coverture by fastforce
   433   hence "x .= z \<and> y .= z" using x y unfolding eq_class_of_def by blast
   434   hence "x .= y" using x y z trans sym by meson
   435   hence "class_of x = class_of y"
   436     unfolding eq_class_of_def using local.sym trans x y by blast
   437   thus ?thesis using x y by simp
   438 qed
   439 
   440 lemma (in equivalence) partition_from_equivalence:
   441   "partition (carrier S) classes"
   442 proof (intro partitionI)
   443   show "\<Union>classes = carrier S" using classes_coverture by simp
   444 next
   445   show "\<And>class1 class2. \<lbrakk> class1 \<in> classes; class2 \<in> classes \<rbrakk> \<Longrightarrow>
   446                           class1 \<inter> class2 \<noteq> {} \<Longrightarrow> class1 = class2"
   447     using disjoint_union by simp
   448 qed
   449 
   450 lemma (in equivalence) disjoint_sum:
   451   assumes "finite (carrier S)"
   452   shows "(\<Sum>c\<in>classes. \<Sum>x\<in>c. f x) = (\<Sum>x\<in>(carrier S). f x)"
   453 proof -
   454   have "finite classes"
   455     unfolding eq_classes_def using assms by auto
   456   thus ?thesis using disjoint_sum assms partition_from_equivalence by blast
   457 qed
   458   
   459 end