src/HOL/Equiv_Relations.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30198 922f944f03b2
child 35216 7641e8d831d2
permissions -rw-r--r--
simplified method setup;
     1 (*  Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Copyright   1996  University of Cambridge
     3 *)
     4 
     5 header {* Equivalence Relations in Higher-Order Set Theory *}
     6 
     7 theory Equiv_Relations
     8 imports Finite_Set Relation Plain
     9 begin
    10 
    11 subsection {* Equivalence relations *}
    12 
    13 locale equiv =
    14   fixes A and r
    15   assumes refl_on: "refl_on A r"
    16     and sym: "sym r"
    17     and trans: "trans r"
    18 
    19 text {*
    20   Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
    21   r = r"}.
    22 
    23   First half: @{text "equiv A r ==> r\<inverse> O r = r"}.
    24 *}
    25 
    26 lemma sym_trans_comp_subset:
    27     "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
    28   by (unfold trans_def sym_def converse_def) blast
    29 
    30 lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
    31   by (unfold refl_on_def) blast
    32 
    33 lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"
    34   apply (unfold equiv_def)
    35   apply clarify
    36   apply (rule equalityI)
    37    apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+
    38   done
    39 
    40 text {* Second half. *}
    41 
    42 lemma comp_equivI:
    43     "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
    44   apply (unfold equiv_def refl_on_def sym_def trans_def)
    45   apply (erule equalityE)
    46   apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")
    47    apply fast
    48   apply fast
    49   done
    50 
    51 
    52 subsection {* Equivalence classes *}
    53 
    54 lemma equiv_class_subset:
    55   "equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}"
    56   -- {* lemma for the next result *}
    57   by (unfold equiv_def trans_def sym_def) blast
    58 
    59 theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
    60   apply (assumption | rule equalityI equiv_class_subset)+
    61   apply (unfold equiv_def sym_def)
    62   apply blast
    63   done
    64 
    65 lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}"
    66   by (unfold equiv_def refl_on_def) blast
    67 
    68 lemma subset_equiv_class:
    69     "equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
    70   -- {* lemma for the next result *}
    71   by (unfold equiv_def refl_on_def) blast
    72 
    73 lemma eq_equiv_class:
    74     "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
    75   by (iprover intro: equalityD2 subset_equiv_class)
    76 
    77 lemma equiv_class_nondisjoint:
    78     "equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"
    79   by (unfold equiv_def trans_def sym_def) blast
    80 
    81 lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
    82   by (unfold equiv_def refl_on_def) blast
    83 
    84 theorem equiv_class_eq_iff:
    85   "equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
    86   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
    87 
    88 theorem eq_equiv_class_iff:
    89   "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
    90   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
    91 
    92 
    93 subsection {* Quotients *}
    94 
    95 definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
    96   [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
    97 
    98 lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
    99   by (unfold quotient_def) blast
   100 
   101 lemma quotientE:
   102   "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
   103   by (unfold quotient_def) blast
   104 
   105 lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
   106   by (unfold equiv_def refl_on_def quotient_def) blast
   107 
   108 lemma quotient_disj:
   109   "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"
   110   apply (unfold quotient_def)
   111   apply clarify
   112   apply (rule equiv_class_eq)
   113    apply assumption
   114   apply (unfold equiv_def trans_def sym_def)
   115   apply blast
   116   done
   117 
   118 lemma quotient_eqI:
   119   "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r|] ==> X = Y" 
   120   apply (clarify elim!: quotientE)
   121   apply (rule equiv_class_eq, assumption)
   122   apply (unfold equiv_def sym_def trans_def, blast)
   123   done
   124 
   125 lemma quotient_eq_iff:
   126   "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> r)" 
   127   apply (rule iffI)  
   128    prefer 2 apply (blast del: equalityI intro: quotient_eqI) 
   129   apply (clarify elim!: quotientE)
   130   apply (unfold equiv_def sym_def trans_def, blast)
   131   done
   132 
   133 lemma eq_equiv_class_iff2:
   134   "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
   135 by(simp add:quotient_def eq_equiv_class_iff)
   136 
   137 
   138 lemma quotient_empty [simp]: "{}//r = {}"
   139 by(simp add: quotient_def)
   140 
   141 lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"
   142 by(simp add: quotient_def)
   143 
   144 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"
   145 by(simp add: quotient_def)
   146 
   147 
   148 lemma singleton_quotient: "{x}//r = {r `` {x}}"
   149 by(simp add:quotient_def)
   150 
   151 lemma quotient_diff1:
   152   "\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r"
   153 apply(simp add:quotient_def inj_on_def)
   154 apply blast
   155 done
   156 
   157 subsection {* Defining unary operations upon equivalence classes *}
   158 
   159 text{*A congruence-preserving function*}
   160 locale congruent =
   161   fixes r and f
   162   assumes congruent: "(y,z) \<in> r ==> f y = f z"
   163 
   164 abbreviation
   165   RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
   166     (infixr "respects" 80) where
   167   "f respects r == congruent r f"
   168 
   169 
   170 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
   171   -- {* lemma required to prove @{text UN_equiv_class} *}
   172   by auto
   173 
   174 lemma UN_equiv_class:
   175   "equiv A r ==> f respects r ==> a \<in> A
   176     ==> (\<Union>x \<in> r``{a}. f x) = f a"
   177   -- {* Conversion rule *}
   178   apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
   179   apply (unfold equiv_def congruent_def sym_def)
   180   apply (blast del: equalityI)
   181   done
   182 
   183 lemma UN_equiv_class_type:
   184   "equiv A r ==> f respects r ==> X \<in> A//r ==>
   185     (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
   186   apply (unfold quotient_def)
   187   apply clarify
   188   apply (subst UN_equiv_class)
   189      apply auto
   190   done
   191 
   192 text {*
   193   Sufficient conditions for injectiveness.  Could weaken premises!
   194   major premise could be an inclusion; bcong could be @{text "!!y. y \<in>
   195   A ==> f y \<in> B"}.
   196 *}
   197 
   198 lemma UN_equiv_class_inject:
   199   "equiv A r ==> f respects r ==>
   200     (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
   201     ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
   202     ==> X = Y"
   203   apply (unfold quotient_def)
   204   apply clarify
   205   apply (rule equiv_class_eq)
   206    apply assumption
   207   apply (subgoal_tac "f x = f xa")
   208    apply blast
   209   apply (erule box_equals)
   210    apply (assumption | rule UN_equiv_class)+
   211   done
   212 
   213 
   214 subsection {* Defining binary operations upon equivalence classes *}
   215 
   216 text{*A congruence-preserving function of two arguments*}
   217 locale congruent2 =
   218   fixes r1 and r2 and f
   219   assumes congruent2:
   220     "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
   221 
   222 text{*Abbreviation for the common case where the relations are identical*}
   223 abbreviation
   224   RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
   225     (infixr "respects2" 80) where
   226   "f respects2 r == congruent2 r r f"
   227 
   228 
   229 lemma congruent2_implies_congruent:
   230     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
   231   by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast
   232 
   233 lemma congruent2_implies_congruent_UN:
   234   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
   235     congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)"
   236   apply (unfold congruent_def)
   237   apply clarify
   238   apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
   239   apply (simp add: UN_equiv_class congruent2_implies_congruent)
   240   apply (unfold congruent2_def equiv_def refl_on_def)
   241   apply (blast del: equalityI)
   242   done
   243 
   244 lemma UN_equiv_class2:
   245   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2
   246     ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2"
   247   by (simp add: UN_equiv_class congruent2_implies_congruent
   248     congruent2_implies_congruent_UN)
   249 
   250 lemma UN_equiv_class_type2:
   251   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f
   252     ==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2
   253     ==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B)
   254     ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
   255   apply (unfold quotient_def)
   256   apply clarify
   257   apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
   258     congruent2_implies_congruent quotientI)
   259   done
   260 
   261 lemma UN_UN_split_split_eq:
   262   "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
   263     (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
   264   -- {* Allows a natural expression of binary operators, *}
   265   -- {* without explicit calls to @{text split} *}
   266   by auto
   267 
   268 lemma congruent2I:
   269   "equiv A1 r1 ==> equiv A2 r2
   270     ==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
   271     ==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z)
   272     ==> congruent2 r1 r2 f"
   273   -- {* Suggested by John Harrison -- the two subproofs may be *}
   274   -- {* \emph{much} simpler than the direct proof. *}
   275   apply (unfold congruent2_def equiv_def refl_on_def)
   276   apply clarify
   277   apply (blast intro: trans)
   278   done
   279 
   280 lemma congruent2_commuteI:
   281   assumes equivA: "equiv A r"
   282     and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
   283     and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"
   284   shows "f respects2 r"
   285   apply (rule congruent2I [OF equivA equivA])
   286    apply (rule commute [THEN trans])
   287      apply (rule_tac [3] commute [THEN trans, symmetric])
   288        apply (rule_tac [5] sym)
   289        apply (rule congt | assumption |
   290          erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
   291   done
   292 
   293 
   294 subsection {* Quotients and finiteness *}
   295 
   296 text {*Suggested by Florian Kammüller*}
   297 
   298 lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
   299   -- {* recall @{thm equiv_type} *}
   300   apply (rule finite_subset)
   301    apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
   302   apply (unfold quotient_def)
   303   apply blast
   304   done
   305 
   306 lemma finite_equiv_class:
   307   "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
   308   apply (unfold quotient_def)
   309   apply (rule finite_subset)
   310    prefer 2 apply assumption
   311   apply blast
   312   done
   313 
   314 lemma equiv_imp_dvd_card:
   315   "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
   316     ==> k dvd card A"
   317   apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]])
   318    apply assumption
   319   apply (rule dvd_partition)
   320      prefer 3 apply (blast dest: quotient_disj)
   321     apply (simp_all add: Union_quotient equiv_type)
   322   done
   323 
   324 lemma card_quotient_disjoint:
   325  "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
   326 apply(simp add:quotient_def)
   327 apply(subst card_UN_disjoint)
   328    apply assumption
   329   apply simp
   330  apply(fastsimp simp add:inj_on_def)
   331 apply (simp add:setsum_constant)
   332 done
   333 
   334 end