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