--- 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!*}