# HG changeset patch # User paulson # Date 1086772731 -7200 # Node ID d7711d6b901448f9bf256e1d648f4ca5a7fe414d # Parent 99ac3eb0f84ee7e5313a4272293225d98ceabd98 moved some cardinality results into main HOL diff -r 99ac3eb0f84e -r d7711d6b9014 src/HOL/Algebra/Exponent.thy --- a/src/HOL/Algebra/Exponent.thy Tue Jun 08 19:25:27 2004 +0200 +++ b/src/HOL/Algebra/Exponent.thy Wed Jun 09 11:18:51 2004 +0200 @@ -34,29 +34,6 @@ by (force simp add: prime_iff) -lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)" -apply (rule_tac P = "%x. x <= b * c" in subst) -apply (rule mult_1_right) -apply (rule mult_le_mono, auto) -done - -lemma insert_partition: - "[| x \ F; \c1\insert x F. \c2 \ insert x F. c1 \ c2 --> c1 \ c2 = {}|] - ==> x \ \ F = {}" -by auto - -(* main cardinality theorem *) -lemma card_partition [rule_format]: - "finite C ==> - finite (\ C) --> - (\c\C. card c = k) --> - (\c1 \ C. \c2 \ C. c1 \ c2 --> c1 \ c2 = {}) --> - k * card(C) = card (\ C)" -apply (erule finite_induct, simp) -apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition - finite_subset [of _ "\ (insert x F)"]) -done - lemma zero_less_card_empty: "[| finite S; S \ {} |] ==> 0 < card(S)" by (rule ccontr, simp) @@ -221,6 +198,12 @@ subsection{*Lemmas for the Main Combinatorial Argument*} +lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)" +apply (rule_tac P = "%x. x <= b * c" in subst) +apply (rule mult_1_right) +apply (rule mult_le_mono, auto) +done + lemma p_fac_forw_lemma: "[| 0 < (m::nat); 0 r <= a" apply (rule notnotD) diff -r 99ac3eb0f84e -r d7711d6b9014 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Jun 08 19:25:27 2004 +0200 +++ b/src/HOL/Finite_Set.thy Wed Jun 09 11:18:51 2004 +0200 @@ -496,6 +496,23 @@ lemma card_psubset: "finite B ==> A \ B ==> card A < card B ==> A < B" by (erule psubsetI, blast) +lemma insert_partition: + "[| x \ F; \c1\insert x F. \c2 \ insert x F. c1 \ c2 --> c1 \ c2 = {}|] + ==> x \ \ F = {}" +by auto + +(* main cardinality theorem *) +lemma card_partition [rule_format]: + "finite C ==> + finite (\ C) --> + (\c\C. card c = k) --> + (\c1 \ C. \c2 \ C. c1 \ c2 --> c1 \ c2 = {}) --> + k * card(C) = card (\ C)" +apply (erule finite_induct, simp) +apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition + finite_subset [of _ "\ (insert x F)"]) +done + subsubsection {* Cardinality of image *}