1(* Title: HOL/Algebra/Exponent.thy 2 Author: Florian Kammueller 3 Author: L C Paulson 4 5exponent p s yields the greatest power of p that divides s. 6*) 7 8theory Exponent 9imports Main "HOL-Computational_Algebra.Primes" 10begin 11 12section \<open>Sylow's Theorem\<close> 13 14text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close> 15 16text\<open>needed in this form to prove Sylow's theorem\<close> 17corollary (in algebraic_semidom) div_combine: 18 "\<lbrakk>prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k" 19 by (metis add_Suc_right mult.commute prime_elem_power_dvd_cases) 20 21lemma exponent_p_a_m_k_equation: 22 fixes p :: nat 23 assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 24 shows "multiplicity p (p^a * m - k) = multiplicity p (p^a - k)" 25proof (rule multiplicity_cong [OF iffI]) 26 fix r 27 assume *: "p ^ r dvd p ^ a * m - k" 28 show "p ^ r dvd p ^ a - k" 29 proof - 30 have "k \<le> p ^ a * m" using assms 31 by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans) 32 then have "r \<le> a" 33 by (meson "*" \<open>0 < k\<close> \<open>k < p^a\<close> dvd_diffD1 dvd_triv_left leI less_imp_le_nat nat_dvd_not_less power_le_dvd) 34 then have "p^r dvd p^a * m" by (simp add: le_imp_power_dvd) 35 thus ?thesis 36 by (meson \<open>k \<le> p ^ a * m\<close> \<open>r \<le> a\<close> * dvd_diffD1 dvd_diff_nat le_imp_power_dvd) 37 qed 38next 39 fix r 40 assume *: "p ^ r dvd p ^ a - k" 41 with assms have "r \<le> a" 42 by (metis diff_diff_cancel less_imp_le_nat nat_dvd_not_less nat_le_linear power_le_dvd zero_less_diff) 43 show "p ^ r dvd p ^ a * m - k" 44 proof - 45 have "p^r dvd p^a*m" 46 by (simp add: \<open>r \<le> a\<close> le_imp_power_dvd) 47 then show ?thesis 48 by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \<open>r \<le> a\<close>) 49 qed 50qed 51 52lemma p_not_div_choose_lemma: 53 fixes p :: nat 54 assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> multiplicity p (Suc i) = multiplicity p (Suc (j + i))" 55 and "k < K" and p: "prime p" 56 shows "multiplicity p (j + k choose k) = 0" 57 using \<open>k < K\<close> 58proof (induction k) 59 case 0 then show ?case by simp 60next 61 case (Suc k) 62 then have *: "(Suc (j+k) choose Suc k) > 0" by simp 63 then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)" 64 by (subst Suc_times_binomial_eq [symmetric], subst prime_elem_multiplicity_mult_distrib) 65 (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH) 66 with p * show ?case 67 by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all 68qed 69 70text\<open>The lemma above, with two changes of variables\<close> 71lemma p_not_div_choose: 72 assumes "k < K" and "k \<le> n" 73 and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p" 74 shows "multiplicity p (n choose k) = 0" 75apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1]) 76apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff) 77apply (rule TrueI)+ 78done 79 80proposition const_p_fac: 81 assumes "m>0" and prime: "prime p" 82 shows "multiplicity p (p^a * m choose p^a) = multiplicity p m" 83proof- 84 from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m" 85 by (auto simp: prime_gt_0_nat) 86 have *: "multiplicity p ((p^a * m - 1) choose (p^a - 1)) = 0" 87 apply (rule p_not_div_choose [where K = "p^a"]) 88 using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono prime) 89 have "multiplicity p ((p ^ a * m choose p ^ a) * p ^ a) = a + multiplicity p m" 90 proof - 91 have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))" 92 (is "_ = ?rhs") using prime 93 by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat) 94 also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith 95 with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)" 96 by (subst prime_elem_multiplicity_mult_distrib) auto 97 also have "\<dots> = a + multiplicity p m" 98 using prime p by (subst prime_elem_multiplicity_mult_distrib) simp_all 99 finally show ?thesis . 100 qed 101 then show ?thesis 102 using prime p by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all 103qed 104 105end 106