diff -r 37adca7fd48f -r 651ea265d568 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Tue Mar 10 15:20:40 2015 +0000
@@ -6,7 +6,7 @@
 *)
 
 theory Exponent
-imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Number_Theory/Binomial"
+imports Main "~~/src/HOL/Number_Theory/Primes"
 begin
 
 section {*Sylow's Theorem*}
@@ -35,7 +35,7 @@
 
 lemma prime_dvd_cases:
   fixes p::nat
-  shows "[| p*k dvd m*n;  prime p |]  
+  shows "[| p*k dvd m*n;  prime p |]
    ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
 apply (simp add: prime_iff)
 apply (frule dvd_mult_left)
@@ -48,10 +48,10 @@
 done
 
 
-lemma prime_power_dvd_cases [rule_format (no_asm)]: 
+lemma prime_power_dvd_cases [rule_format (no_asm)]:
 fixes p::nat
   shows "prime p
-  ==> \<forall>m n. p^c dvd m*n -->  
+  ==> \<forall>m n. p^c dvd m*n -->
         (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
 apply (induct c)
 apply (metis dvd_1_left nat_power_eq_Suc_0_iff one_is_add)
@@ -119,7 +119,7 @@
 lemma power_Suc_exponent_Not_dvd:
   "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
- prefer 2 apply simp 
+ prefer 2 apply simp
 apply (rule ccontr)
 apply (drule exponent_ge, auto)
 done
@@ -147,7 +147,7 @@
 by (metis mult_dvd_mono power_exponent_dvd)
 
 (* exponent_mult_add, opposite inclusion *)
-lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
+lemma exponent_mult_add2: "[| a > 0; b > 0 |]
   ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
 apply (case_tac "prime p")
 apply (rule leI, clarify)
@@ -155,7 +155,7 @@
 apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
   prefer 3 apply assumption
- prefer 2 apply simp 
+ prefer 2 apply simp
 apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
  apply (assumption, force, simp)
 apply (blast dest: power_Suc_exponent_Not_dvd)
@@ -185,7 +185,7 @@
 text{*Main Combinatorial Argument*}
 
 lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
-by (simp add: mult.commute[of a b]) 
+by (simp add: mult.commute[of a b])
 
 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
 apply (rule_tac P = "%x. x <= b * c" in subst)
@@ -204,7 +204,7 @@
 apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2_nat gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10))
 done
 
-lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
+lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
   ==> (p^r) dvd (p^a) - k"
 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
@@ -220,7 +220,7 @@
   "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
 
-lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
+lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]
   ==> (p^r) dvd (p^a)*m - k"
 apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
@@ -231,7 +231,7 @@
 apply (drule less_imp_Suc_add, auto)
 done
 
-lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
+lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]
   ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
 done
@@ -241,16 +241,16 @@
 
 (*The bound K is needed; otherwise it's too weak to be used.*)
 lemma p_not_div_choose_lemma [rule_format]:
-  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
+  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
    ==> k<K --> exponent p ((j+k) choose k) = 0"
 apply (cases "prime p")
- prefer 2 apply simp 
+ prefer 2 apply simp
 apply (induct k)
 apply (simp (no_asm))
 (*induction step*)
 apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
  prefer 2 apply (simp, clarify)
-apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
+apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
                     exponent p (Suc k)")
  txt{*First, use the assumed equation.  We simplify the LHS to
   @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
@@ -276,7 +276,7 @@
 lemma const_p_fac_right:
   "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
 apply (case_tac "prime p")
- prefer 2 apply simp 
+ prefer 2 apply simp
 apply (frule_tac a = a in zero_less_prime_power)
 apply (rule_tac K = "p^a" in p_not_div_choose)
    apply simp
@@ -294,14 +294,14 @@
 lemma const_p_fac:
   "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
 apply (case_tac "prime p")
- prefer 2 apply simp 
+ prefer 2 apply simp
 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
  prefer 2 apply (force simp add: prime_iff)
 txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
   insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   first
   transform the binomial coefficient, then use @{text exponent_mult_add}.*}
-apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
+apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
                     a + exponent p m")
  apply (simp add: exponent_mult_add)
 txt{*one subgoal left!*}