# HG changeset patch # User wenzelm # Date 1028843261 -7200 # Node ID 2bb7200a99cf70a6c41cd45ee8341e4fe905cb5e # Parent 796a5b766c2ef0cb152912833de67e58fa85781d converted; diff -r 796a5b766c2e -r 2bb7200a99cf src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Thu Aug 08 23:46:51 2002 +0200 +++ b/src/HOL/Integ/Equiv.ML Thu Aug 08 23:47:41 2002 +0200 @@ -1,262 +1,38 @@ -(* Title: Equiv.ML - ID: $Id$ - Authors: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge -Equivalence relations in HOL Set Theory -*) - -(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***) - -(** first half: equiv A r ==> r^-1 O r = r **) - -Goalw [trans_def,sym_def,converse_def] - "[| sym(r); trans(r) |] ==> r^-1 O r <= r"; -by (Blast_tac 1); -qed "sym_trans_comp_subset"; - -Goalw [refl_def] "refl A r ==> r <= r^-1 O r"; -by (Blast_tac 1); -qed "refl_comp_subset"; - -Goalw [equiv_def] "equiv A r ==> r^-1 O r = r"; -by (Clarify_tac 1); -by (rtac equalityI 1); -by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1)); -qed "equiv_comp_eq"; - -(*second half*) -Goalw [equiv_def,refl_def,sym_def,trans_def] - "[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r"; -by (etac equalityE 1); -by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1); -by (ALLGOALS Fast_tac); -qed "comp_equivI"; - -(** Equivalence classes **) - -(*Lemma for the next result*) -Goalw [equiv_def,trans_def,sym_def] - "[| equiv A r; (a,b): r |] ==> r``{a} <= r``{b}"; -by (Blast_tac 1); -qed "equiv_class_subset"; - -Goal "[| equiv A r; (a,b): r |] ==> r``{a} = r``{b}"; -by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); -by (rewrite_goals_tac [equiv_def,sym_def]); -by (Blast_tac 1); -qed "equiv_class_eq"; - -Goalw [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r``{a}"; -by (Blast_tac 1); -qed "equiv_class_self"; - -(*Lemma for the next result*) -Goalw [equiv_def,refl_def] - "[| equiv A r; r``{b} <= r``{a}; b: A |] ==> (a,b): r"; -by (Blast_tac 1); -qed "subset_equiv_class"; - -Goal "[| r``{a} = r``{b}; equiv A r; b: A |] ==> (a,b): r"; -by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1)); -qed "eq_equiv_class"; - -(*thus r``{a} = r``{b} as well*) -Goalw [equiv_def,trans_def,sym_def] - "[| equiv A r; x: (r``{a} Int r``{b}) |] ==> (a,b): r"; -by (Blast_tac 1); -qed "equiv_class_nondisjoint"; - -Goalw [equiv_def,refl_def] "equiv A r ==> r <= A <*> A"; -by (Blast_tac 1); -qed "equiv_type"; - -Goal "equiv A r ==> ((x,y): r) = (r``{x} = r``{y} & x:A & y:A)"; -by (blast_tac (claset() addSIs [equiv_class_eq] - addDs [eq_equiv_class, equiv_type]) 1); -qed "equiv_class_eq_iff"; - -Goal "[| equiv A r; x: A; y: A |] ==> (r``{x} = r``{y}) = ((x,y): r)"; -by (blast_tac (claset() addSIs [equiv_class_eq] - addDs [eq_equiv_class, equiv_type]) 1); -qed "eq_equiv_class_iff"; - -(*** Quotients ***) - -(** Introduction/elimination rules -- needed? **) - -Goalw [quotient_def] "x:A ==> r``{x}: A//r"; -by (Blast_tac 1); -qed "quotientI"; - -val [major,minor] = Goalw [quotient_def] - "[| X:(A//r); !!x. [| X = r``{x}; x:A |] ==> P |] \ -\ ==> P"; -by (resolve_tac [major RS UN_E] 1); -by (rtac minor 1); -by (assume_tac 2); -by (Fast_tac 1); (*Blast_tac FAILS to prove it*) -qed "quotientE"; - -Goalw [equiv_def,refl_def,quotient_def] - "equiv A r ==> Union(A//r) = A"; -by (Blast_tac 1); -qed "Union_quotient"; - -Goalw [quotient_def] - "[| equiv A r; X: A//r; Y: A//r |] ==> X=Y | (X Int Y = {})"; -by (Clarify_tac 1); -by (rtac equiv_class_eq 1); -by (assume_tac 1); -by (rewrite_goals_tac [equiv_def,trans_def,sym_def]); -by (Blast_tac 1); -qed "quotient_disj"; - - -(**** Defining unary operations upon equivalence classes ****) - -(* theorem needed to prove UN_equiv_class *) -Goal "[| a:A; ALL y:A. b(y)=c |] ==> (UN y:A. b(y))=c"; -by Auto_tac; -qed "UN_constant_eq"; - - -(** Could introduce a LOCALE with the assumptions - equiv A r; congruent r b -**) +(* legacy ML bindings *) -(*Conversion rule*) -Goal "[| equiv A r; congruent r b; a: A |] \ -\ ==> (UN x:r``{a}. b(x)) = b(a)"; -by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1)); -by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); -by (blast_tac (claset() delrules [equalityI]) 1); -qed "UN_equiv_class"; - -(*type checking of UN x:r`{a}. b(x) *) -val prems = Goalw [quotient_def] - "[| equiv A r; congruent r b; X: A//r; \ -\ !!x. x : A ==> b(x) : B |] \ -\ ==> (UN x:X. b(x)) : B"; -by (cut_facts_tac prems 1); -by (Clarify_tac 1); -by (stac UN_equiv_class 1); -by (REPEAT (ares_tac prems 1)); -qed "UN_equiv_class_type"; - -(*Sufficient conditions for injectiveness. Could weaken premises! - major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B -*) -val prems = Goalw [quotient_def] - "[| equiv A r; congruent r b; \ -\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A//r; Y: A//r; \ -\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] \ -\ ==> X=Y"; -by (cut_facts_tac prems 1); -by (Clarify_tac 1); -by (rtac equiv_class_eq 1); -by (REPEAT (ares_tac prems 1)); -by (etac box_equals 1); -by (REPEAT (ares_tac [UN_equiv_class] 1)); -qed "UN_equiv_class_inject"; - - -(**** Defining binary operations upon equivalence classes ****) - - -Goalw [congruent_def,congruent2_def,equiv_def,refl_def] - "[| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)"; -by (Blast_tac 1); -qed "congruent2_implies_congruent"; - -Goalw [congruent_def] - "[| equiv A r; congruent2 r b; a: A |] ==> \ -\ congruent r (%x1. UN x2:r``{a}. b x1 x2)"; -by (Clarify_tac 1); -by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1)); -by (asm_simp_tac (simpset() addsimps [UN_equiv_class, - congruent2_implies_congruent]) 1); -by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]); -by (blast_tac (claset() delrules [equalityI]) 1); -qed "congruent2_implies_congruent_UN"; - -Goal "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ -\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b x1 x2) = b a1 a2"; -by (asm_simp_tac (simpset() addsimps [UN_equiv_class, - congruent2_implies_congruent, - congruent2_implies_congruent_UN]) 1); -qed "UN_equiv_class2"; - -(*type checking*) -val prems = Goalw [quotient_def] - "[| equiv A r; congruent2 r b; \ -\ X1: A//r; X2: A//r; \ -\ !!x1 x2. [| x1: A; x2: A |] ==> b x1 x2 : B |] \ -\ ==> (UN x1:X1. UN x2:X2. b x1 x2) : B"; -by (cut_facts_tac prems 1); -by (Clarify_tac 1); -by (REPEAT (ares_tac (prems@[UN_equiv_class_type, - congruent2_implies_congruent_UN, - congruent2_implies_congruent, quotientI]) 1)); -qed "UN_equiv_class_type2"; - -(*Allows a natural expression of binary operators, without explicit calls - to "split"*) -Goal "(UN (x1,x2):X. UN (y1,y2):Y. A x1 x2 y1 y2) = \ -\ (UN x:X. UN y:Y. (%(x1, x2). (%(y1, y2). A x1 x2 y1 y2) y) x)"; -by Auto_tac; -qed "UN_UN_split_split_eq"; - -(*Suggested by John Harrison -- the two subproofs may be MUCH simpler - than the direct proof*) -val prems = Goalw [congruent2_def,equiv_def,refl_def] - "[| equiv A r; \ -\ !! y z w. [| w: A; (y,z) : r |] ==> b y w = b z w; \ -\ !! y z w. [| w: A; (y,z) : r |] ==> b w y = b w z \ -\ |] ==> congruent2 r b"; -by (cut_facts_tac prems 1); -by (Clarify_tac 1); -by (blast_tac (claset() addIs (trans::prems)) 1); -qed "congruent2I"; - -val [equivA,commute,congt] = Goal - "[| equiv A r; \ -\ !! y z. [| y: A; z: A |] ==> b y z = b z y; \ -\ !! y z w. [| w: A; (y,z): r |] ==> b w y = b w z \ -\ |] ==> congruent2 r b"; -by (resolve_tac [equivA RS congruent2I] 1); -by (rtac (commute RS trans) 1); -by (rtac (commute RS trans RS sym) 3); -by (rtac sym 5); -by (REPEAT (ares_tac [congt] 1 - ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1)); -qed "congruent2_commuteI"; - - -(*** Cardinality results suggested by Florian Kammueller ***) - -(*Recall that equiv A r implies r <= A <*> A (equiv_type) *) -Goal "[| finite A; r <= A <*> A |] ==> finite (A//r)"; -by (rtac finite_subset 1); -by (etac (finite_Pow_iff RS iffD2) 2); -by (rewtac quotient_def); -by (Blast_tac 1); -qed "finite_quotient"; - -Goalw [quotient_def] - "[| finite A; r <= A <*> A; X : A//r |] ==> finite X"; -by (rtac finite_subset 1); -by (assume_tac 2); -by (Blast_tac 1); -qed "finite_equiv_class"; - -Goal "[| finite A; equiv A r; ALL X : A//r. k dvd card(X) |] \ -\ ==> k dvd card(A)"; -by (rtac (Union_quotient RS subst) 1); -by (assume_tac 1); -by (rtac dvd_partition 1); -by (blast_tac (claset() addDs [quotient_disj]) 4); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [Union_quotient, equiv_type, - finite_quotient]))); -qed "equiv_imp_dvd_card"; +val UN_UN_split_split_eq = thm "UN_UN_split_split_eq"; +val UN_constant_eq = thm "UN_constant_eq"; +val UN_equiv_class = thm "UN_equiv_class"; +val UN_equiv_class2 = thm "UN_equiv_class2"; +val UN_equiv_class_inject = thm "UN_equiv_class_inject"; +val UN_equiv_class_type = thm "UN_equiv_class_type"; +val UN_equiv_class_type2 = thm "UN_equiv_class_type2"; +val Union_quotient = thm "Union_quotient"; +val comp_equivI = thm "comp_equivI"; +val congruent2I = thm "congruent2I"; +val congruent2_commuteI = thm "congruent2_commuteI"; +val congruent2_def = thm "congruent2_def"; +val congruent2_implies_congruent = thm "congruent2_implies_congruent"; +val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN"; +val congruent_def = thm "congruent_def"; +val eq_equiv_class = thm "eq_equiv_class"; +val eq_equiv_class_iff = thm "eq_equiv_class_iff"; +val equiv_class_eq = thm "equiv_class_eq"; +val equiv_class_eq_iff = thm "equiv_class_eq_iff"; +val equiv_class_nondisjoint = thm "equiv_class_nondisjoint"; +val equiv_class_self = thm "equiv_class_self"; +val equiv_class_subset = thm "equiv_class_subset"; +val equiv_comp_eq = thm "equiv_comp_eq"; +val equiv_def = thm "equiv_def"; +val equiv_imp_dvd_card = thm "equiv_imp_dvd_card"; +val equiv_type = thm "equiv_type"; +val finite_equiv_class = thm "finite_equiv_class"; +val finite_quotient = thm "finite_quotient"; +val quotientE = thm "quotientE"; +val quotientI = thm "quotientI"; +val quotient_def = thm "quotient_def"; +val quotient_disj = thm "quotient_disj"; +val refl_comp_subset = thm "refl_comp_subset"; +val subset_equiv_class = thm "subset_equiv_class"; +val sym_trans_comp_subset = thm "sym_trans_comp_subset"; diff -r 796a5b766c2e -r 2bb7200a99cf src/HOL/Integ/Equiv.thy --- a/src/HOL/Integ/Equiv.thy Thu Aug 08 23:46:51 2002 +0200 +++ b/src/HOL/Integ/Equiv.thy Thu Aug 08 23:47:41 2002 +0200 @@ -1,23 +1,273 @@ -(* Title: Equiv.thy +(* Title: HOL/Integ/Equiv.thy ID: $Id$ Authors: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge - -Equivalence relations in Higher-Order Set Theory *) -Equiv = Relation + Finite_Set + +header {* Equivalence relations in Higher-Order Set Theory *} + +theory Equiv = Relation + Finite_Set: + +subsection {* Equiv relations *} + +locale equiv = + fixes A and r + assumes refl: "refl A r" + and sym: "sym r" + and trans: "trans r" + +text {* + Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\ O + r = r"}. + + First half: @{text "equiv A r ==> r\ O r = r"}. +*} + +lemma sym_trans_comp_subset: + "sym r ==> trans r ==> r\ O r \ r" + by (unfold trans_def sym_def converse_def) blast + +lemma refl_comp_subset: "refl A r ==> r \ r\ O r" + by (unfold refl_def) blast + +lemma equiv_comp_eq: "equiv A r ==> r\ O r = r" + apply (unfold equiv_def) + apply clarify + apply (rule equalityI) + apply (rules intro: sym_trans_comp_subset refl_comp_subset)+ + done + +text {* + Second half. +*} + +lemma comp_equivI: + "r\ O r = r ==> Domain r = A ==> equiv A r" + apply (unfold equiv_def refl_def sym_def trans_def) + apply (erule equalityE) + apply (subgoal_tac "\x y. (x, y) \ r --> (y, x) \ r") + apply fast + apply fast + done + + +subsection {* Equivalence classes *} + +lemma equiv_class_subset: + "equiv A r ==> (a, b) \ r ==> r``{a} \ r``{b}" + -- {* lemma for the next result *} + by (unfold equiv_def trans_def sym_def) blast + +lemma equiv_class_eq: "equiv A r ==> (a, b) \ r ==> r``{a} = r``{b}" + apply (assumption | rule equalityI equiv_class_subset)+ + apply (unfold equiv_def sym_def) + apply blast + done + +lemma equiv_class_self: "equiv A r ==> a \ A ==> a \ r``{a}" + by (unfold equiv_def refl_def) blast + +lemma subset_equiv_class: + "equiv A r ==> r``{b} \ r``{a} ==> b \ A ==> (a,b) \ r" + -- {* lemma for the next result *} + by (unfold equiv_def refl_def) blast + +lemma eq_equiv_class: + "r``{a} = r``{b} ==> equiv A r ==> b \ A ==> (a, b) \ r" + by (rules intro: equalityD2 subset_equiv_class) + +lemma equiv_class_nondisjoint: + "equiv A r ==> x \ (r``{a} \ r``{b}) ==> (a, b) \ r" + by (unfold equiv_def trans_def sym_def) blast + +lemma equiv_type: "equiv A r ==> r \ A \ A" + by (unfold equiv_def refl_def) blast + +lemma equiv_class_eq_iff: + "equiv A r ==> ((x, y) \ r) = (r``{x} = r``{y} & x \ A & y \ A)" + by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) + +lemma eq_equiv_class_iff: + "equiv A r ==> x \ A ==> y \ A ==> (r``{x} = r``{y}) = ((x, y) \ r)" + by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type) + + +subsection {* Quotients *} + constdefs - equiv :: "['a set, ('a*'a) set] => bool" - "equiv A r == refl A r & sym(r) & trans(r)" + quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) + "A//r == \x \ A. {r``{x}}" -- {* set of equiv classes *} + +lemma quotientI: "x \ A ==> r``{x} \ A//r" + by (unfold quotient_def) blast + +lemma quotientE: + "X \ A//r ==> (!!x. X = r``{x} ==> x \ A ==> P) ==> P" + by (unfold quotient_def) blast + +lemma Union_quotient: "equiv A r ==> Union (A//r) = A" + by (unfold equiv_def refl_def quotient_def) blast - quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) - "A//r == UN x:A. {r``{x}}" (*set of equiv classes*) +lemma quotient_disj: + "equiv A r ==> X \ A//r ==> Y \ A//r ==> X = Y | (X \ Y = {})" + apply (unfold quotient_def) + apply clarify + apply (rule equiv_class_eq) + apply assumption + apply (unfold equiv_def trans_def sym_def) + apply blast + done + + +subsection {* Defining unary operations upon equivalence classes *} + +locale congruent = + fixes r and b + assumes congruent: "(y, z) \ r ==> b y = b z" + +lemma UN_constant_eq: "a \ A ==> \y \ A. b y = c ==> (\y \ A. b(y))=c" + -- {* lemma required to prove @{text UN_equiv_class} *} + by auto + +lemma UN_equiv_class: + "equiv A r ==> congruent r b ==> a \ A + ==> (\x \ r``{a}. b x) = b a" + -- {* Conversion rule *} + apply (rule equiv_class_self [THEN UN_constant_eq], assumption+) + apply (unfold equiv_def congruent_def sym_def) + apply (blast del: equalityI) + done - congruent :: "[('a*'a) set, 'a=>'b] => bool" - "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" +lemma UN_equiv_class_type: + "equiv A r ==> congruent r b ==> X \ A//r ==> + (!!x. x \ A ==> b x : B) ==> (\x \ X. b x) : B" + apply (unfold quotient_def) + apply clarify + apply (subst UN_equiv_class) + apply auto + done + +text {* + Sufficient conditions for injectiveness. Could weaken premises! + major premise could be an inclusion; bcong could be @{text "!!y. y \ + A ==> b y \ B"}. +*} + +lemma UN_equiv_class_inject: + "equiv A r ==> congruent r b ==> + (\x \ X. b x) = (\y \ Y. b y) ==> X \ A//r ==> Y \ A//r + ==> (!!x y. x \ A ==> y \ A ==> b x = b y ==> (x, y) \ r) + ==> X = Y" + apply (unfold quotient_def) + apply clarify + apply (rule equiv_class_eq) + apply assumption + apply (subgoal_tac "b x = b xa") + apply blast + apply (erule box_equals) + apply (assumption | rule UN_equiv_class)+ + done + + +subsection {* Defining binary operations upon equivalence classes *} + +locale congruent2 = + fixes r and b + assumes congruent2: + "(y1, z1) \ r ==> (y2, z2) \ r ==> b y1 y2 = b z1 z2" + +lemma congruent2_implies_congruent: + "equiv A r ==> congruent2 r b ==> a \ A ==> congruent r (b a)" + by (unfold congruent_def congruent2_def equiv_def refl_def) blast + +lemma congruent2_implies_congruent_UN: + "equiv A r ==> congruent2 r b ==> a \ A ==> + congruent r (\x1. \x2 \ r``{a}. b x1 x2)" + apply (unfold congruent_def) + apply clarify + apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) + apply (simp add: UN_equiv_class congruent2_implies_congruent) + apply (unfold congruent2_def equiv_def refl_def) + apply (blast del: equalityI) + done + +lemma UN_equiv_class2: + "equiv A r ==> congruent2 r b ==> a1 \ A ==> a2 \ A + ==> (\x1 \ r``{a1}. \x2 \ r``{a2}. b x1 x2) = b a1 a2" + by (simp add: UN_equiv_class congruent2_implies_congruent + congruent2_implies_congruent_UN) - congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool" - "congruent2 r b == ALL y1 z1 y2 z2. - (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" +lemma UN_equiv_class_type2: + "equiv A r ==> congruent2 r b ==> X1 \ A//r ==> X2 \ A//r + ==> (!!x1 x2. x1 \ A ==> x2 \ A ==> b x1 x2 \ B) + ==> (\x1 \ X1. \x2 \ X2. b x1 x2) \ B" + apply (unfold quotient_def) + apply clarify + apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN + congruent2_implies_congruent quotientI) + done + +lemma UN_UN_split_split_eq: + "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) = + (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)" + -- {* Allows a natural expression of binary operators, *} + -- {* without explicit calls to @{text split} *} + by auto + +lemma congruent2I: + "equiv A r + ==> (!!y z w. w \ A ==> (y, z) \ r ==> b y w = b z w) + ==> (!!y z w. w \ A ==> (y, z) \ r ==> b w y = b w z) + ==> congruent2 r b" + -- {* Suggested by John Harrison -- the two subproofs may be *} + -- {* \emph{much} simpler than the direct proof. *} + apply (unfold congruent2_def equiv_def refl_def) + apply clarify + apply (blast intro: trans) + done + +lemma congruent2_commuteI: + assumes equivA: "equiv A r" + and commute: "!!y z. y \ A ==> z \ A ==> b y z = b z y" + and congt: "!!y z w. w \ A ==> (y, z) \ r ==> b w y = b w z" + shows "congruent2 r b" + apply (rule equivA [THEN congruent2I]) + apply (rule commute [THEN trans]) + apply (rule_tac [3] commute [THEN trans, symmetric]) + apply (rule_tac [5] sym) + apply (assumption | rule congt | + erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+ + done + + +subsection {* Cardinality results *} + +text {* (suggested by Florian Kammüller) *} + +lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)" + -- {* recall @{thm equiv_type} *} + apply (rule finite_subset) + apply (erule_tac [2] finite_Pow_iff [THEN iffD2]) + apply (unfold quotient_def) + apply blast + done + +lemma finite_equiv_class: + "finite A ==> r \ A \ A ==> X \ A//r ==> finite X" + apply (unfold quotient_def) + apply (rule finite_subset) + prefer 2 apply assumption + apply blast + done + +lemma equiv_imp_dvd_card: + "finite A ==> equiv A r ==> \X \ A//r. k dvd card X + ==> k dvd card A" + apply (rule Union_quotient [THEN subst]) + apply assumption + apply (rule dvd_partition) + prefer 4 apply (blast dest: quotient_disj) + apply (simp_all add: Union_quotient equiv_type finite_quotient) + done + end