src/HOL/Algebra/Exponent.thy
changeset 14889 d7711d6b9014
parent 14706 71590b7733b7
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Jun 08 19:25:27 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Jun 09 11:18:51 2004 +0200
     1.3 @@ -34,29 +34,6 @@
     1.4  by (force simp add: prime_iff)
     1.5  
     1.6  
     1.7 -lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
     1.8 -apply (rule_tac P = "%x. x <= b * c" in subst)
     1.9 -apply (rule mult_1_right)
    1.10 -apply (rule mult_le_mono, auto)
    1.11 -done
    1.12 -
    1.13 -lemma insert_partition:
    1.14 -     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
    1.15 -      ==> x \<inter> \<Union> F = {}"
    1.16 -by auto
    1.17 -
    1.18 -(* main cardinality theorem *)
    1.19 -lemma card_partition [rule_format]:
    1.20 -     "finite C ==>  
    1.21 -        finite (\<Union> C) -->  
    1.22 -        (\<forall>c\<in>C. card c = k) -->   
    1.23 -        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
    1.24 -        k * card(C) = card (\<Union> C)"
    1.25 -apply (erule finite_induct, simp)
    1.26 -apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
    1.27 -       finite_subset [of _ "\<Union> (insert x F)"])
    1.28 -done
    1.29 -
    1.30  lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
    1.31  by (rule ccontr, simp)
    1.32  
    1.33 @@ -221,6 +198,12 @@
    1.34  
    1.35  subsection{*Lemmas for the Main Combinatorial Argument*}
    1.36  
    1.37 +lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
    1.38 +apply (rule_tac P = "%x. x <= b * c" in subst)
    1.39 +apply (rule mult_1_right)
    1.40 +apply (rule mult_le_mono, auto)
    1.41 +done
    1.42 +
    1.43  lemma p_fac_forw_lemma:
    1.44       "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
    1.45  apply (rule notnotD)