src/HOL/Equiv_Relations.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 66364 fa3247e6ee4b
child 67399 eab6ce8368fa
permissions -rw-r--r--
tuned;
wenzelm@63653
     1
(*  Title:      HOL/Equiv_Relations.thy
wenzelm@63653
     2
    Author:     Lawrence C Paulson, 1996 Cambridge University Computer Laboratory
paulson@15300
     3
*)
paulson@15300
     4
wenzelm@60758
     5
section \<open>Equivalence Relations in Higher-Order Set Theory\<close>
paulson@15300
     6
paulson@15300
     7
theory Equiv_Relations
blanchet@66364
     8
  imports Groups_Big
paulson@15300
     9
begin
paulson@15300
    10
wenzelm@60758
    11
subsection \<open>Equivalence relations -- set version\<close>
paulson@15300
    12
wenzelm@63653
    13
definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
wenzelm@63653
    14
  where "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
paulson@15300
    15
wenzelm@63653
    16
lemma equivI: "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
haftmann@40815
    17
  by (simp add: equiv_def)
haftmann@40815
    18
haftmann@40815
    19
lemma equivE:
haftmann@40815
    20
  assumes "equiv A r"
haftmann@40815
    21
  obtains "refl_on A r" and "sym r" and "trans r"
haftmann@40815
    22
  using assms by (simp add: equiv_def)
haftmann@40815
    23
wenzelm@60758
    24
text \<open>
wenzelm@63653
    25
  Suppes, Theorem 70: \<open>r\<close> is an equiv relation iff \<open>r\<inverse> O r = r\<close>.
paulson@15300
    26
wenzelm@63653
    27
  First half: \<open>equiv A r \<Longrightarrow> r\<inverse> O r = r\<close>.
wenzelm@60758
    28
\<close>
paulson@15300
    29
wenzelm@63653
    30
lemma sym_trans_comp_subset: "sym r \<Longrightarrow> trans r \<Longrightarrow> r\<inverse> O r \<subseteq> r"
wenzelm@63653
    31
  unfolding trans_def sym_def converse_unfold by blast
paulson@15300
    32
wenzelm@63653
    33
lemma refl_on_comp_subset: "refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
wenzelm@63653
    34
  unfolding refl_on_def by blast
paulson@15300
    35
wenzelm@63653
    36
lemma equiv_comp_eq: "equiv A r \<Longrightarrow> r\<inverse> O r = r"
paulson@15300
    37
  apply (unfold equiv_def)
paulson@15300
    38
  apply clarify
paulson@15300
    39
  apply (rule equalityI)
nipkow@30198
    40
   apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
paulson@15300
    41
  done
paulson@15300
    42
wenzelm@60758
    43
text \<open>Second half.\<close>
paulson@15300
    44
wenzelm@63653
    45
lemma comp_equivI: "r\<inverse> O r = r \<Longrightarrow> Domain r = A \<Longrightarrow> equiv A r"
nipkow@30198
    46
  apply (unfold equiv_def refl_on_def sym_def trans_def)
paulson@15300
    47
  apply (erule equalityE)
wenzelm@63653
    48
  apply (subgoal_tac "\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r")
paulson@15300
    49
   apply fast
paulson@15300
    50
  apply fast
paulson@15300
    51
  done
paulson@15300
    52
paulson@15300
    53
wenzelm@60758
    54
subsection \<open>Equivalence classes\<close>
paulson@15300
    55
wenzelm@63653
    56
lemma equiv_class_subset: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} \<subseteq> r``{b}"
wenzelm@61799
    57
  \<comment> \<open>lemma for the next result\<close>
wenzelm@63653
    58
  unfolding equiv_def trans_def sym_def by blast
paulson@15300
    59
wenzelm@63653
    60
theorem equiv_class_eq: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} = r``{b}"
paulson@15300
    61
  apply (assumption | rule equalityI equiv_class_subset)+
paulson@15300
    62
  apply (unfold equiv_def sym_def)
paulson@15300
    63
  apply blast
paulson@15300
    64
  done
paulson@15300
    65
wenzelm@63653
    66
lemma equiv_class_self: "equiv A r \<Longrightarrow> a \<in> A \<Longrightarrow> a \<in> r``{a}"
wenzelm@63653
    67
  unfolding equiv_def refl_on_def by blast
paulson@15300
    68
wenzelm@63653
    69
lemma subset_equiv_class: "equiv A r \<Longrightarrow> r``{b} \<subseteq> r``{a} \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r"
wenzelm@61799
    70
  \<comment> \<open>lemma for the next result\<close>
wenzelm@63653
    71
  unfolding equiv_def refl_on_def by blast
paulson@15300
    72
wenzelm@63653
    73
lemma eq_equiv_class: "r``{a} = r``{b} \<Longrightarrow> equiv A r \<Longrightarrow> b \<in> A \<Longrightarrow> (a, b) \<in> r"
nipkow@17589
    74
  by (iprover intro: equalityD2 subset_equiv_class)
paulson@15300
    75
wenzelm@63653
    76
lemma equiv_class_nondisjoint: "equiv A r \<Longrightarrow> x \<in> (r``{a} \<inter> r``{b}) \<Longrightarrow> (a, b) \<in> r"
wenzelm@63653
    77
  unfolding equiv_def trans_def sym_def by blast
paulson@15300
    78
wenzelm@63653
    79
lemma equiv_type: "equiv A r \<Longrightarrow> r \<subseteq> A \<times> A"
wenzelm@63653
    80
  unfolding equiv_def refl_on_def by blast
paulson@15300
    81
wenzelm@63653
    82
lemma equiv_class_eq_iff: "equiv A r \<Longrightarrow> (x, y) \<in> r \<longleftrightarrow> r``{x} = r``{y} \<and> x \<in> A \<and> y \<in> A"
paulson@15300
    83
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
paulson@15300
    84
wenzelm@63653
    85
lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r"
paulson@15300
    86
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
paulson@15300
    87
paulson@15300
    88
wenzelm@60758
    89
subsection \<open>Quotients\<close>
paulson@15300
    90
wenzelm@63653
    91
definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90)
wenzelm@63653
    92
  where "A//r = (\<Union>x \<in> A. {r``{x}})"  \<comment> \<open>set of equiv classes\<close>
paulson@15300
    93
paulson@15300
    94
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
wenzelm@63653
    95
  unfolding quotient_def by blast
paulson@15300
    96
wenzelm@63653
    97
lemma quotientE: "X \<in> A//r \<Longrightarrow> (\<And>x. X = r``{x} \<Longrightarrow> x \<in> A \<Longrightarrow> P) \<Longrightarrow> P"
wenzelm@63653
    98
  unfolding quotient_def by blast
paulson@15300
    99
wenzelm@63653
   100
lemma Union_quotient: "equiv A r \<Longrightarrow> \<Union>(A//r) = A"
wenzelm@63653
   101
  unfolding equiv_def refl_on_def quotient_def by blast
paulson@15300
   102
wenzelm@63653
   103
lemma quotient_disj: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> X = Y \<or> X \<inter> Y = {}"
paulson@15300
   104
  apply (unfold quotient_def)
paulson@15300
   105
  apply clarify
paulson@15300
   106
  apply (rule equiv_class_eq)
paulson@15300
   107
   apply assumption
paulson@15300
   108
  apply (unfold equiv_def trans_def sym_def)
paulson@15300
   109
  apply blast
paulson@15300
   110
  done
paulson@15300
   111
paulson@15300
   112
lemma quotient_eqI:
wenzelm@63653
   113
  "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> X = Y"
paulson@15300
   114
  apply (clarify elim!: quotientE)
wenzelm@63653
   115
  apply (rule equiv_class_eq)
wenzelm@63653
   116
   apply assumption
wenzelm@63653
   117
  apply (unfold equiv_def sym_def trans_def)
wenzelm@63653
   118
  apply blast
paulson@15300
   119
  done
paulson@15300
   120
paulson@15300
   121
lemma quotient_eq_iff:
wenzelm@63653
   122
  "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> X = Y \<longleftrightarrow> (x, y) \<in> r"
wenzelm@63653
   123
  apply (rule iffI)
wenzelm@63653
   124
   prefer 2
wenzelm@63653
   125
   apply (blast del: equalityI intro: quotient_eqI)
paulson@15300
   126
  apply (clarify elim!: quotientE)
wenzelm@63653
   127
  apply (unfold equiv_def sym_def trans_def)
wenzelm@63653
   128
  apply blast
paulson@15300
   129
  done
paulson@15300
   130
wenzelm@63653
   131
lemma eq_equiv_class_iff2: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> {x}//r = {y}//r \<longleftrightarrow> (x, y) \<in> r"
wenzelm@63653
   132
  by (simp add: quotient_def eq_equiv_class_iff)
paulson@15300
   133
paulson@15300
   134
lemma quotient_empty [simp]: "{}//r = {}"
wenzelm@63653
   135
  by (simp add: quotient_def)
paulson@15300
   136
wenzelm@63653
   137
lemma quotient_is_empty [iff]: "A//r = {} \<longleftrightarrow> A = {}"
wenzelm@63653
   138
  by (simp add: quotient_def)
paulson@15300
   139
wenzelm@63653
   140
lemma quotient_is_empty2 [iff]: "{} = A//r \<longleftrightarrow> A = {}"
wenzelm@63653
   141
  by (simp add: quotient_def)
paulson@15300
   142
nipkow@15302
   143
lemma singleton_quotient: "{x}//r = {r `` {x}}"
wenzelm@63653
   144
  by (simp add: quotient_def)
nipkow@15302
   145
wenzelm@63653
   146
lemma quotient_diff1: "inj_on (\<lambda>a. {a}//r) A \<Longrightarrow> a \<in> A \<Longrightarrow> (A - {a})//r = A//r - {a}//r"
wenzelm@63653
   147
  unfolding quotient_def inj_on_def by blast
wenzelm@63653
   148
nipkow@15302
   149
wenzelm@60758
   150
subsection \<open>Refinement of one equivalence relation WRT another\<close>
lp15@59528
   151
wenzelm@63653
   152
lemma refines_equiv_class_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> R``(S``{a}) = S``{a}"
lp15@59528
   153
  by (auto simp: equiv_class_eq_iff)
lp15@59528
   154
wenzelm@63653
   155
lemma refines_equiv_class_eq2: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> S``(R``{a}) = S``{a}"
lp15@59528
   156
  by (auto simp: equiv_class_eq_iff)
lp15@59528
   157
wenzelm@63653
   158
lemma refines_equiv_image_eq: "R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> (\<lambda>X. S``X) ` (A//R) = A//S"
lp15@59528
   159
   by (auto simp: quotient_def image_UN refines_equiv_class_eq2)
lp15@59528
   160
lp15@59528
   161
lemma finite_refines_finite:
wenzelm@63653
   162
  "finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> finite (A//S)"
wenzelm@63653
   163
  by (erule finite_surj [where f = "\<lambda>X. S``X"]) (simp add: refines_equiv_image_eq)
lp15@59528
   164
lp15@59528
   165
lemma finite_refines_card_le:
wenzelm@63653
   166
  "finite (A//R) \<Longrightarrow> R \<subseteq> S \<Longrightarrow> equiv A R \<Longrightarrow> equiv A S \<Longrightarrow> card (A//S) \<le> card (A//R)"
wenzelm@63653
   167
  by (subst refines_equiv_image_eq [of R S A, symmetric])
wenzelm@63653
   168
    (auto simp: card_image_le [where f = "\<lambda>X. S``X"])
lp15@59528
   169
blanchet@55022
   170
wenzelm@60758
   171
subsection \<open>Defining unary operations upon equivalence classes\<close>
paulson@15300
   172
wenzelm@63653
   173
text \<open>A congruence-preserving function.\<close>
haftmann@40816
   174
wenzelm@63653
   175
definition congruent :: "('a \<times> 'a) set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
wenzelm@63653
   176
  where "congruent r f \<longleftrightarrow> (\<forall>(y, z) \<in> r. f y = f z)"
haftmann@40816
   177
wenzelm@63653
   178
lemma congruentI: "(\<And>y z. (y, z) \<in> r \<Longrightarrow> f y = f z) \<Longrightarrow> congruent r f"
haftmann@40817
   179
  by (auto simp add: congruent_def)
haftmann@40816
   180
wenzelm@63653
   181
lemma congruentD: "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
haftmann@40817
   182
  by (auto simp add: congruent_def)
paulson@15300
   183
wenzelm@63653
   184
abbreviation RESPECTS :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  (infixr "respects" 80)
wenzelm@63653
   185
  where "f respects r \<equiv> congruent r f"
paulson@15300
   186
paulson@15300
   187
wenzelm@63653
   188
lemma UN_constant_eq: "a \<in> A \<Longrightarrow> \<forall>y \<in> A. f y = c \<Longrightarrow> (\<Union>y \<in> A. f y) = c"
wenzelm@61799
   189
  \<comment> \<open>lemma required to prove \<open>UN_equiv_class\<close>\<close>
paulson@15300
   190
  by auto
paulson@15300
   191
wenzelm@63653
   192
lemma UN_equiv_class: "equiv A r \<Longrightarrow> f respects r \<Longrightarrow> a \<in> A \<Longrightarrow> (\<Union>x \<in> r``{a}. f x) = f a"
wenzelm@61799
   193
  \<comment> \<open>Conversion rule\<close>
wenzelm@63653
   194
  apply (rule equiv_class_self [THEN UN_constant_eq])
wenzelm@63653
   195
    apply assumption
wenzelm@63653
   196
   apply assumption
paulson@15300
   197
  apply (unfold equiv_def congruent_def sym_def)
paulson@15300
   198
  apply (blast del: equalityI)
paulson@15300
   199
  done
paulson@15300
   200
paulson@15300
   201
lemma UN_equiv_class_type:
wenzelm@63653
   202
  "equiv A r \<Longrightarrow> f respects r \<Longrightarrow> X \<in> A//r \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> (\<Union>x \<in> X. f x) \<in> B"
paulson@15300
   203
  apply (unfold quotient_def)
paulson@15300
   204
  apply clarify
paulson@15300
   205
  apply (subst UN_equiv_class)
paulson@15300
   206
     apply auto
paulson@15300
   207
  done
paulson@15300
   208
wenzelm@60758
   209
text \<open>
paulson@15300
   210
  Sufficient conditions for injectiveness.  Could weaken premises!
wenzelm@63653
   211
  major premise could be an inclusion; \<open>bcong\<close> could be
wenzelm@63653
   212
  \<open>\<And>y. y \<in> A \<Longrightarrow> f y \<in> B\<close>.
wenzelm@60758
   213
\<close>
paulson@15300
   214
paulson@15300
   215
lemma UN_equiv_class_inject:
wenzelm@63653
   216
  "equiv A r \<Longrightarrow> f respects r \<Longrightarrow>
wenzelm@63653
   217
    (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) \<Longrightarrow> X \<in> A//r ==> Y \<in> A//r
wenzelm@63653
   218
    \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<Longrightarrow> (x, y) \<in> r)
wenzelm@63653
   219
    \<Longrightarrow> X = Y"
paulson@15300
   220
  apply (unfold quotient_def)
paulson@15300
   221
  apply clarify
paulson@15300
   222
  apply (rule equiv_class_eq)
paulson@15300
   223
   apply assumption
paulson@15300
   224
  apply (subgoal_tac "f x = f xa")
paulson@15300
   225
   apply blast
paulson@15300
   226
  apply (erule box_equals)
paulson@15300
   227
   apply (assumption | rule UN_equiv_class)+
paulson@15300
   228
  done
paulson@15300
   229
paulson@15300
   230
wenzelm@60758
   231
subsection \<open>Defining binary operations upon equivalence classes\<close>
paulson@15300
   232
wenzelm@63653
   233
text \<open>A congruence-preserving function of two arguments.\<close>
haftmann@40817
   234
wenzelm@63653
   235
definition congruent2 :: "('a \<times> 'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> bool"
wenzelm@63653
   236
  where "congruent2 r1 r2 f \<longleftrightarrow> (\<forall>(y1, z1) \<in> r1. \<forall>(y2, z2) \<in> r2. f y1 y2 = f z1 z2)"
haftmann@40817
   237
haftmann@40817
   238
lemma congruent2I':
haftmann@40817
   239
  assumes "\<And>y1 z1 y2 z2. (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
haftmann@40817
   240
  shows "congruent2 r1 r2 f"
haftmann@40817
   241
  using assms by (auto simp add: congruent2_def)
haftmann@40817
   242
wenzelm@63653
   243
lemma congruent2D: "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
wenzelm@63092
   244
  by (auto simp add: congruent2_def)
paulson@15300
   245
wenzelm@63653
   246
text \<open>Abbreviation for the common case where the relations are identical.\<close>
wenzelm@63653
   247
abbreviation RESPECTS2:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  (infixr "respects2" 80)
wenzelm@63653
   248
  where "f respects2 r \<equiv> congruent2 r r f"
nipkow@19979
   249
paulson@15300
   250
paulson@15300
   251
lemma congruent2_implies_congruent:
wenzelm@63653
   252
  "equiv A r1 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a \<in> A \<Longrightarrow> congruent r2 (f a)"
wenzelm@63653
   253
  unfolding congruent_def congruent2_def equiv_def refl_on_def by blast
paulson@15300
   254
paulson@15300
   255
lemma congruent2_implies_congruent_UN:
wenzelm@63653
   256
  "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a \<in> A2 \<Longrightarrow>
paulson@15300
   257
    congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)"
paulson@15300
   258
  apply (unfold congruent_def)
paulson@15300
   259
  apply clarify
paulson@15300
   260
  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
paulson@15300
   261
  apply (simp add: UN_equiv_class congruent2_implies_congruent)
nipkow@30198
   262
  apply (unfold congruent2_def equiv_def refl_on_def)
paulson@15300
   263
  apply (blast del: equalityI)
paulson@15300
   264
  done
paulson@15300
   265
paulson@15300
   266
lemma UN_equiv_class2:
wenzelm@63653
   267
  "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f \<Longrightarrow> a1 \<in> A1 \<Longrightarrow> a2 \<in> A2 \<Longrightarrow>
wenzelm@63653
   268
    (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2"
wenzelm@63653
   269
  by (simp add: UN_equiv_class congruent2_implies_congruent congruent2_implies_congruent_UN)
paulson@15300
   270
paulson@15300
   271
lemma UN_equiv_class_type2:
wenzelm@63653
   272
  "equiv A1 r1 \<Longrightarrow> equiv A2 r2 \<Longrightarrow> congruent2 r1 r2 f
wenzelm@63653
   273
    \<Longrightarrow> X1 \<in> A1//r1 \<Longrightarrow> X2 \<in> A2//r2
wenzelm@63653
   274
    \<Longrightarrow> (\<And>x1 x2. x1 \<in> A1 \<Longrightarrow> x2 \<in> A2 \<Longrightarrow> f x1 x2 \<in> B)
wenzelm@63653
   275
    \<Longrightarrow> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
paulson@15300
   276
  apply (unfold quotient_def)
paulson@15300
   277
  apply clarify
paulson@15300
   278
  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
wenzelm@63653
   279
      congruent2_implies_congruent quotientI)
paulson@15300
   280
  done
paulson@15300
   281
paulson@15300
   282
lemma UN_UN_split_split_eq:
paulson@15300
   283
  "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
paulson@15300
   284
    (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
wenzelm@61799
   285
  \<comment> \<open>Allows a natural expression of binary operators,\<close>
wenzelm@61799
   286
  \<comment> \<open>without explicit calls to \<open>split\<close>\<close>
paulson@15300
   287
  by auto
paulson@15300
   288
paulson@15300
   289
lemma congruent2I:
wenzelm@63653
   290
  "equiv A1 r1 \<Longrightarrow> equiv A2 r2
wenzelm@63653
   291
    \<Longrightarrow> (\<And>y z w. w \<in> A2 \<Longrightarrow> (y,z) \<in> r1 \<Longrightarrow> f y w = f z w)
wenzelm@63653
   292
    \<Longrightarrow> (\<And>y z w. w \<in> A1 \<Longrightarrow> (y,z) \<in> r2 \<Longrightarrow> f w y = f w z)
wenzelm@63653
   293
    \<Longrightarrow> congruent2 r1 r2 f"
wenzelm@61799
   294
  \<comment> \<open>Suggested by John Harrison -- the two subproofs may be\<close>
wenzelm@63653
   295
  \<comment> \<open>\<^emph>\<open>much\<close> simpler than the direct proof.\<close>
nipkow@30198
   296
  apply (unfold congruent2_def equiv_def refl_on_def)
paulson@15300
   297
  apply clarify
paulson@15300
   298
  apply (blast intro: trans)
paulson@15300
   299
  done
paulson@15300
   300
paulson@15300
   301
lemma congruent2_commuteI:
paulson@15300
   302
  assumes equivA: "equiv A r"
wenzelm@63653
   303
    and commute: "\<And>y z. y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> f y z = f z y"
wenzelm@63653
   304
    and congt: "\<And>y z w. w \<in> A \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> f w y = f w z"
paulson@15300
   305
  shows "f respects2 r"
paulson@15300
   306
  apply (rule congruent2I [OF equivA equivA])
paulson@15300
   307
   apply (rule commute [THEN trans])
paulson@15300
   308
     apply (rule_tac [3] commute [THEN trans, symmetric])
paulson@15300
   309
       apply (rule_tac [5] sym)
haftmann@25482
   310
       apply (rule congt | assumption |
paulson@15300
   311
         erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
paulson@15300
   312
  done
paulson@15300
   313
haftmann@24728
   314
wenzelm@60758
   315
subsection \<open>Quotients and finiteness\<close>
haftmann@24728
   316
wenzelm@60758
   317
text \<open>Suggested by Florian Kammüller\<close>
haftmann@24728
   318
wenzelm@63653
   319
lemma finite_quotient: "finite A \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> finite (A//r)"
wenzelm@61799
   320
  \<comment> \<open>recall @{thm equiv_type}\<close>
haftmann@24728
   321
  apply (rule finite_subset)
haftmann@24728
   322
   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
haftmann@24728
   323
  apply (unfold quotient_def)
haftmann@24728
   324
  apply blast
haftmann@24728
   325
  done
haftmann@24728
   326
wenzelm@63653
   327
lemma finite_equiv_class: "finite A \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> X \<in> A//r \<Longrightarrow> finite X"
haftmann@24728
   328
  apply (unfold quotient_def)
haftmann@24728
   329
  apply (rule finite_subset)
haftmann@24728
   330
   prefer 2 apply assumption
haftmann@24728
   331
  apply blast
haftmann@24728
   332
  done
haftmann@24728
   333
wenzelm@63653
   334
lemma equiv_imp_dvd_card: "finite A \<Longrightarrow> equiv A r \<Longrightarrow> \<forall>X \<in> A//r. k dvd card X \<Longrightarrow> k dvd card A"
berghofe@26791
   335
  apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]])
haftmann@24728
   336
   apply assumption
haftmann@24728
   337
  apply (rule dvd_partition)
wenzelm@63653
   338
    prefer 3 apply (blast dest: quotient_disj)
wenzelm@63653
   339
   apply (simp_all add: Union_quotient equiv_type)
haftmann@24728
   340
  done
haftmann@24728
   341
wenzelm@63653
   342
lemma card_quotient_disjoint: "finite A \<Longrightarrow> inj_on (\<lambda>x. {x} // r) A \<Longrightarrow> card (A//r) = card A"
wenzelm@63653
   343
  apply (simp add:quotient_def)
wenzelm@63653
   344
  apply (subst card_UN_disjoint)
wenzelm@63653
   345
     apply assumption
wenzelm@63653
   346
    apply simp
wenzelm@63653
   347
   apply (fastforce simp add:inj_on_def)
haftmann@24728
   348
  apply simp
wenzelm@63653
   349
  done
haftmann@24728
   350
haftmann@40812
   351
wenzelm@60758
   352
subsection \<open>Projection\<close>
blanchet@55022
   353
wenzelm@63653
   354
definition proj :: "('b \<times> 'a) set \<Rightarrow> 'b \<Rightarrow> 'a set"
wenzelm@63653
   355
  where "proj r x = r `` {x}"
blanchet@55022
   356
wenzelm@63653
   357
lemma proj_preserves: "x \<in> A \<Longrightarrow> proj r x \<in> A//r"
wenzelm@63653
   358
  unfolding proj_def by (rule quotientI)
blanchet@55022
   359
blanchet@55022
   360
lemma proj_in_iff:
wenzelm@63653
   361
  assumes "equiv A r"
wenzelm@63653
   362
  shows "proj r x \<in> A//r \<longleftrightarrow> x \<in> A"
wenzelm@63653
   363
    (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@63653
   364
proof
wenzelm@63653
   365
  assume ?rhs
wenzelm@63653
   366
  then show ?lhs by (simp add: proj_preserves)
wenzelm@63653
   367
next
wenzelm@63653
   368
  assume ?lhs
wenzelm@63653
   369
  then show ?rhs
wenzelm@63653
   370
    unfolding proj_def quotient_def
wenzelm@63653
   371
  proof clarsimp
wenzelm@63653
   372
    fix y
wenzelm@63653
   373
    assume y: "y \<in> A" and "r `` {x} = r `` {y}"
wenzelm@63653
   374
    moreover have "y \<in> r `` {y}"
wenzelm@63653
   375
      using assms y unfolding equiv_def refl_on_def by blast
wenzelm@63653
   376
    ultimately have "(x, y) \<in> r" by blast
wenzelm@63653
   377
    then show "x \<in> A"
wenzelm@63653
   378
      using assms unfolding equiv_def refl_on_def by blast
wenzelm@63653
   379
  qed
blanchet@55022
   380
qed
blanchet@55022
   381
wenzelm@63653
   382
lemma proj_iff: "equiv A r \<Longrightarrow> {x, y} \<subseteq> A \<Longrightarrow> proj r x = proj r y \<longleftrightarrow> (x, y) \<in> r"
wenzelm@63653
   383
  by (simp add: proj_def eq_equiv_class_iff)
blanchet@55022
   384
blanchet@55022
   385
(*
blanchet@55022
   386
lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
blanchet@55022
   387
unfolding proj_def equiv_def refl_on_def by blast
blanchet@55022
   388
*)
blanchet@55022
   389
wenzelm@63653
   390
lemma proj_image: "proj r ` A = A//r"
wenzelm@63653
   391
  unfolding proj_def[abs_def] quotient_def by blast
blanchet@55022
   392
wenzelm@63653
   393
lemma in_quotient_imp_non_empty: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<noteq> {}"
wenzelm@63653
   394
  unfolding quotient_def using equiv_class_self by fast
blanchet@55022
   395
wenzelm@63653
   396
lemma in_quotient_imp_in_rel: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> {x, y} \<subseteq> X \<Longrightarrow> (x, y) \<in> r"
wenzelm@63653
   397
  using quotient_eq_iff[THEN iffD1] by fastforce
blanchet@55022
   398
wenzelm@63653
   399
lemma in_quotient_imp_closed: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> x \<in> X \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> X"
wenzelm@63653
   400
  unfolding quotient_def equiv_def trans_def by blast
blanchet@55022
   401
wenzelm@63653
   402
lemma in_quotient_imp_subset: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> X \<subseteq> A"
wenzelm@63653
   403
  using in_quotient_imp_in_rel equiv_type by fastforce
blanchet@55022
   404
blanchet@55022
   405
wenzelm@60758
   406
subsection \<open>Equivalence relations -- predicate version\<close>
haftmann@40812
   407
wenzelm@63653
   408
text \<open>Partial equivalences.\<close>
haftmann@40812
   409
wenzelm@63653
   410
definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
wenzelm@63653
   411
  where "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)"
wenzelm@61799
   412
    \<comment> \<open>John-Harrison-style characterization\<close>
haftmann@40812
   413
wenzelm@63653
   414
lemma part_equivpI: "\<exists>x. R x x \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R"
haftmann@45969
   415
  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)
haftmann@40812
   416
haftmann@40812
   417
lemma part_equivpE:
haftmann@40812
   418
  assumes "part_equivp R"
haftmann@40812
   419
  obtains x where "R x x" and "symp R" and "transp R"
haftmann@40812
   420
proof -
haftmann@40812
   421
  from assms have 1: "\<exists>x. R x x"
haftmann@40812
   422
    and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y"
wenzelm@63653
   423
    unfolding part_equivp_def by blast+
haftmann@40812
   424
  from 1 obtain x where "R x x" ..
haftmann@40812
   425
  moreover have "symp R"
haftmann@40812
   426
  proof (rule sympI)
haftmann@40812
   427
    fix x y
haftmann@40812
   428
    assume "R x y"
haftmann@40812
   429
    with 2 [of x y] show "R y x" by auto
haftmann@40812
   430
  qed
haftmann@40812
   431
  moreover have "transp R"
haftmann@40812
   432
  proof (rule transpI)
haftmann@40812
   433
    fix x y z
haftmann@40812
   434
    assume "R x y" and "R y z"
haftmann@40812
   435
    with 2 [of x y] 2 [of y z] show "R x z" by auto
haftmann@40812
   436
  qed
haftmann@40812
   437
  ultimately show thesis by (rule that)
haftmann@40812
   438
qed
haftmann@40812
   439
wenzelm@63653
   440
lemma part_equivp_refl_symp_transp: "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R"
haftmann@40812
   441
  by (auto intro: part_equivpI elim: part_equivpE)
haftmann@40812
   442
wenzelm@63653
   443
lemma part_equivp_symp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
haftmann@40812
   444
  by (erule part_equivpE, erule sympE)
haftmann@40812
   445
wenzelm@63653
   446
lemma part_equivp_transp: "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
haftmann@40812
   447
  by (erule part_equivpE, erule transpE)
haftmann@40812
   448
wenzelm@63653
   449
lemma part_equivp_typedef: "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}"
kaliszyk@44204
   450
  by (auto elim: part_equivpE)
haftmann@40812
   451
haftmann@40812
   452
wenzelm@63653
   453
text \<open>Total equivalences.\<close>
haftmann@40812
   454
wenzelm@63653
   455
definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
wenzelm@63653
   456
  where "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" \<comment> \<open>John-Harrison-style characterization\<close>
haftmann@40812
   457
wenzelm@63653
   458
lemma equivpI: "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R"
haftmann@45969
   459
  by (auto elim: reflpE sympE transpE simp add: equivp_def)
haftmann@40812
   460
haftmann@40812
   461
lemma equivpE:
haftmann@40812
   462
  assumes "equivp R"
haftmann@40812
   463
  obtains "reflp R" and "symp R" and "transp R"
haftmann@40812
   464
  using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)
haftmann@40812
   465
wenzelm@63653
   466
lemma equivp_implies_part_equivp: "equivp R \<Longrightarrow> part_equivp R"
haftmann@40812
   467
  by (auto intro: part_equivpI elim: equivpE reflpE)
haftmann@40812
   468
wenzelm@63653
   469
lemma equivp_equiv: "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
haftmann@46752
   470
  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])
haftmann@40812
   471
wenzelm@63653
   472
lemma equivp_reflp_symp_transp: "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
haftmann@40812
   473
  by (auto intro: equivpI elim: equivpE)
haftmann@40812
   474
wenzelm@63653
   475
lemma identity_equivp: "equivp (op =)"
haftmann@40812
   476
  by (auto intro: equivpI reflpI sympI transpI)
haftmann@40812
   477
wenzelm@63653
   478
lemma equivp_reflp: "equivp R \<Longrightarrow> R x x"
haftmann@40812
   479
  by (erule equivpE, erule reflpE)
haftmann@40812
   480
wenzelm@63653
   481
lemma equivp_symp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x"
haftmann@40812
   482
  by (erule equivpE, erule sympE)
haftmann@40812
   483
wenzelm@63653
   484
lemma equivp_transp: "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
haftmann@40812
   485
  by (erule equivpE, erule transpE)
haftmann@40812
   486
blanchet@55024
   487
hide_const (open) proj
blanchet@55024
   488
paulson@15300
   489
end