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)