# HG changeset patch # User haftmann # Date 1184081443 -7200 # Node ID 315c638d58563d94c550b061a07b3fcaab4e7c82 # Parent 18d6ee42568940fafa5952c31c52a1eefd673463 moved finite lemmas to Finite_Set.thy diff -r 18d6ee425689 -r 315c638d5856 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Tue Jul 10 16:46:37 2007 +0200 +++ b/src/HOL/Equiv_Relations.thy Tue Jul 10 17:30:43 2007 +0200 @@ -6,7 +6,7 @@ header {* Equivalence Relations in Higher-Order Set Theory *} theory Equiv_Relations -imports Relation Finite_Set +imports Relation begin subsection {* Equivalence relations *} @@ -292,83 +292,4 @@ 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 3 apply (blast dest: quotient_disj) - apply (simp_all add: Union_quotient equiv_type) - done - -lemma card_quotient_disjoint: - "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A" -apply(simp add:quotient_def) -apply(subst card_UN_disjoint) - apply assumption - apply simp - apply(fastsimp simp add:inj_on_def) -apply (simp add:setsum_constant) -done -(* -ML -{* -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_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"; -*} -*) end diff -r 18d6ee425689 -r 315c638d5856 src/HOL/IntDef.thy --- a/src/HOL/IntDef.thy Tue Jul 10 16:46:37 2007 +0200 +++ b/src/HOL/IntDef.thy Tue Jul 10 17:30:43 2007 +0200 @@ -11,6 +11,7 @@ imports Equiv_Relations Nat begin + text {* the equivalence relation underlying the integers *} definition @@ -622,52 +623,6 @@ by (rule Ints_cases) auto -(* int (Suc n) = 1 + int n *) - - - -subsection{*More Properties of @{term setsum} and @{term setprod}*} - -text{*By Jeremy Avigad*} - - -lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done - -lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done - -lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto simp add: of_nat_mult) - done - -lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" - apply (cases "finite A") - apply (erule finite_induct, auto) - done - -lemma setprod_nonzero_nat: - "finite A ==> (\x \ A. f x \ (0::nat)) ==> setprod f A \ 0" - by (rule setprod_nonzero, auto) - -lemma setprod_zero_eq_nat: - "finite A ==> (setprod f A = (0::nat)) = (\x \ A. f x = 0)" - by (rule setprod_zero_eq, auto) - -lemma setprod_nonzero_int: - "finite A ==> (\x \ A. f x \ (0::int)) ==> setprod f A \ 0" - by (rule setprod_nonzero, auto) - -lemma setprod_zero_eq_int: - "finite A ==> (setprod f A = (0::int)) = (\x \ A. f x = 0)" - by (rule setprod_zero_eq, auto) - - subsection {* Further properties *} text{*Now we replace the case analysis rule by a more conventional one: @@ -766,8 +721,6 @@ lemmas int_Suc = of_nat_Suc [where ?'a_1.0=int] lemmas abs_int_eq = abs_of_nat [where 'a=int and n="?m"] lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int] -lemmas int_setsum = of_nat_setsum [where 'a=int] -lemmas int_setprod = of_nat_setprod [where 'a=int] lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric] lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq] lemmas int_eq_of_nat = TrueI