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