src/HOL/Algebra/Exponent.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (20 months ago) changeset 67003 49850a679c2c parent 66453 cc19f7ca2ed6 permissions -rw-r--r--
more robust sorted_entries;
```     1 (*  Title:      HOL/Algebra/Exponent.thy
```
```     2     Author:     Florian Kammueller
```
```     3     Author:     L C Paulson
```
```     4
```
```     5 exponent p s   yields the greatest power of p that divides s.
```
```     6 *)
```
```     7
```
```     8 theory Exponent
```
```     9 imports Main "HOL-Computational_Algebra.Primes"
```
```    10 begin
```
```    11
```
```    12 section \<open>Sylow's Theorem\<close>
```
```    13
```
```    14 text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
```
```    15
```
```    16 text\<open>needed in this form to prove Sylow's theorem\<close>
```
```    17 corollary (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
```
```    21 lemma 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)"
```
```    25 proof (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
```
```    38 next
```
```    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
```
```    50 qed
```
```    51
```
```    52 lemma 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>
```
```    58 proof (induction k)
```
```    59   case 0 then show ?case by simp
```
```    60 next
```
```    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
```
```    68 qed
```
```    69
```
```    70 text\<open>The lemma above, with two changes of variables\<close>
```
```    71 lemma 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"
```
```    75 apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
```
```    76 apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
```
```    77 apply (rule TrueI)+
```
```    78 done
```
```    79
```
```    80 proposition const_p_fac:
```
```    81   assumes "m>0" and prime: "prime p"
```
```    82   shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
```
```    83 proof-
```
```    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
```
```   103 qed
```
```   104
```
```   105 end
```