equal
deleted
inserted
replaced
78 |
78 |
79 (*needed in this form in Sylow.ML*) |
79 (*needed in this form in Sylow.ML*) |
80 lemma div_combine: |
80 lemma div_combine: |
81 fixes p::nat |
81 fixes p::nat |
82 shows "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] ==> p ^ a dvd k" |
82 shows "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] ==> p ^ a dvd k" |
83 by (metis add_Suc nat_add_commute prime_power_dvd_cases) |
83 by (metis add_Suc add.commute prime_power_dvd_cases) |
84 |
84 |
85 (*Lemma for power_dvd_bound*) |
85 (*Lemma for power_dvd_bound*) |
86 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" |
86 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" |
87 apply (induct n) |
87 apply (induct n) |
88 apply (simp (no_asm_simp)) |
88 apply (simp (no_asm_simp)) |
183 |
183 |
184 |
184 |
185 text{*Main Combinatorial Argument*} |
185 text{*Main Combinatorial Argument*} |
186 |
186 |
187 lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b" |
187 lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b" |
188 by (simp add: mult_commute[of a b]) |
188 by (simp add: mult.commute[of a b]) |
189 |
189 |
190 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" |
190 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" |
191 apply (rule_tac P = "%x. x <= b * c" in subst) |
191 apply (rule_tac P = "%x. x <= b * c" in subst) |
192 apply (rule mult_1_right) |
192 apply (rule mult_1_right) |
193 apply (rule mult_le_mono, auto) |
193 apply (rule mult_le_mono, auto) |
199 apply (rule notI) |
199 apply (rule notI) |
200 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) |
200 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) |
201 apply (drule less_imp_le [of a]) |
201 apply (drule less_imp_le [of a]) |
202 apply (drule le_imp_power_dvd) |
202 apply (drule le_imp_power_dvd) |
203 apply (drule_tac b = "p ^ r" in dvd_trans, assumption) |
203 apply (drule_tac b = "p ^ r" in dvd_trans, assumption) |
204 apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2_nat gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10)) |
204 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)) |
205 done |
205 done |
206 |
206 |
207 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |] |
207 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |] |
208 ==> (p^r) dvd (p^a) - k" |
208 ==> (p^r) dvd (p^a) - k" |
209 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) |
209 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) |