src/HOL/Algebra/Exponent.thy
author eberlm
Fri, 17 Jun 2016 11:33:52 +0200
changeset 63319 bc8793d7bd21
parent 62410 2fc7a8d9c529
child 63534 523b488b15c9
permissions -rw-r--r--
fps_from_poly → fps_of_poly
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 13870
diff changeset
     1
(*  Title:      HOL/Algebra/Exponent.thy
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     2
    Author:     Florian Kammueller
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     3
    Author:     L C Paulson
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     4
35849
b5522b51cb1e standard headers;
wenzelm
parents: 35848
diff changeset
     5
exponent p s   yields the greatest power of p that divides s.
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     6
*)
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
     7
27105
5f139027c365 slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents: 25162
diff changeset
     8
theory Exponent
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 58917
diff changeset
     9
imports Main "~~/src/HOL/Number_Theory/Primes"
27105
5f139027c365 slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents: 25162
diff changeset
    10
begin
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20282
diff changeset
    11
61382
efac889fccbc isabelle update_cartouches;
wenzelm
parents: 59667
diff changeset
    12
section \<open>Sylow's Theorem\<close>
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27651
diff changeset
    13
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    14
text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    15
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    16
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    17
subsection\<open>Prime Theorems\<close>
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    18
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    19
lemma prime_dvd_cases:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    20
  assumes pk: "p*k dvd m*n" and p: "prime p"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    21
  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    22
proof -
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    23
  have "p dvd m*n" using dvd_mult_left pk by blast
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    24
  then consider "p dvd m" | "p dvd n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    25
    using p prime_dvd_mult_eq_nat by blast
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    26
  then show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    27
  proof cases
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    28
    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    29
      then have "\<exists>x. k dvd x * n \<and> m = p * x"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    30
        using p pk by auto
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    31
    then show ?thesis ..
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    32
  next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    33
    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    34
      then have "\<exists>y. k dvd m*y \<and> n = p*y"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    35
        using p pk by auto
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    36
    then show ?thesis ..
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    37
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    38
qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    39
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    40
lemma prime_power_dvd_prod:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    41
  assumes pc: "p^c dvd m*n" and p: "prime p"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    42
  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    43
using pc
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    44
proof (induct c arbitrary: m n)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    45
  case 0 show ?case by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    46
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    47
  case (Suc c)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    48
  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    49
    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    50
  then show ?case
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    51
  proof cases
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    52
    case (1 x) 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    53
      with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    54
      by force
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    55
  next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    56
    case (2 y) 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    57
      with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    58
      by force
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    59
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    60
qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    61
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    62
lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    63
  by arith
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    64
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    65
lemma prime_power_dvd_cases:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    66
     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    67
  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    68
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    69
text\<open>needed in this form to prove Sylow's theorem\<close>
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    70
corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    71
  by (metis add_Suc_right mult.commute prime_power_dvd_cases)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    72
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    73
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    74
subsection\<open>The Exponent Function\<close>
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 27651
diff changeset
    75
35848
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 32946
diff changeset
    76
definition
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 32946
diff changeset
    77
  exponent :: "nat => nat => nat"
5443079512ea slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents: 32946
diff changeset
    78
  where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    79
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    80
lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    81
  by (simp add: exponent_def)
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20282
diff changeset
    82
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    83
lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    84
  by (induct n) (auto simp: Suc_le_eq le_less_trans)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    85
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    86
text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    87
lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    88
  by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    89
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    90
lemma exponent_ge:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    91
  assumes "p ^ k dvd n" "prime p" "0 < n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    92
    shows "k \<le> exponent p n"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    93
proof -
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    94
  have "Suc 0 < p"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    95
    using \<open>prime p\<close> by (simp add: prime_def)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    96
  with assms show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    97
    by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
    98
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
    99
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   100
lemma power_exponent_dvd: "p ^ exponent p s dvd s"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   101
proof (cases "s = 0")
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   102
  case True then show ?thesis by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   103
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   104
  case False then show ?thesis 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   105
    apply (simp add: exponent_def, clarify)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   106
    apply (rule GreatestI [where k = 0])
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   107
    apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   108
    done
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   109
qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   110
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   111
lemma power_Suc_exponent_Not_dvd:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   112
    "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   113
  by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   114
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   115
lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   116
  apply (simp add: exponent_def)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   117
  apply (rule Greatest_equality, simp)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   118
  apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   119
  done
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   120
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   121
lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   122
  apply (case_tac "prime p")
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   123
  apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   124
  apply simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   125
  done
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   126
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   127
lemma exponent_equalityI:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   128
  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   129
  by (simp add: exponent_def)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   130
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   131
lemma exponent_mult_add: 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   132
  assumes "a > 0" "b > 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   133
    shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   134
proof (cases "prime p")
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   135
  case False then show ?thesis by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   136
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   137
  case True show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   138
  proof (rule order_antisym)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   139
    show "exponent p a + exponent p b \<le> exponent p (a * b)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   140
      by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> assms)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   141
  next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   142
    { assume "exponent p a + exponent p b < exponent p (a * b)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   143
      then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   144
        by (meson Suc_le_eq power_exponent_dvd power_le_dvd)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   145
      with prime_power_dvd_cases [where  a = "Suc (exponent p a)" and b = "Suc (exponent p b)"] 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   146
      have False 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   147
        by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   148
    } 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   149
  then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   150
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   151
qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   152
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   153
lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   154
  apply (case_tac "exponent p n", simp)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   155
  by (metis dvd_mult_left power_Suc power_exponent_dvd)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   156
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   157
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   158
subsection\<open>The Main Combinatorial Argument\<close>
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   159
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   160
lemma exponent_p_a_m_k_equation: 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   161
  assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   162
    shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   163
proof (rule exponent_equalityI [OF iffI])
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   164
  fix r
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   165
  assume *: "p ^ r dvd p ^ a * m - k" 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   166
  show "p ^ r dvd p ^ a - k"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   167
  proof -
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   168
    have "k \<le> p ^ a * m" using assms
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   169
      by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   170
    then have "r \<le> a"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   171
      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)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   172
    then have "p^r dvd p^a * m" by (simp add: le_imp_power_dvd)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   173
    thus ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   174
      by (meson \<open>k \<le> p ^ a * m\<close> \<open>r \<le> a\<close> * dvd_diffD1 dvd_diff_nat le_imp_power_dvd)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   175
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   176
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   177
  fix r
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   178
  assume *: "p ^ r dvd p ^ a - k" 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   179
  with assms have "r \<le> a"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   180
    by (metis diff_diff_cancel less_imp_le_nat nat_dvd_not_less nat_le_linear power_le_dvd zero_less_diff)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   181
  show "p ^ r dvd p ^ a * m - k"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   182
  proof -
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   183
    have "p^r dvd p^a*m"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   184
      by (simp add: \<open>r \<le> a\<close> le_imp_power_dvd)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   185
    then show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   186
      by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \<open>r \<le> a\<close>)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   187
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   188
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   189
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   190
lemma p_not_div_choose_lemma: 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   191
  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   192
      and "k < K"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   193
    shows "exponent p (j + k choose k) = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   194
proof (cases "prime p")
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   195
  case False then show ?thesis by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   196
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   197
  case True show ?thesis using \<open>k < K\<close> 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   198
  proof (induction k)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   199
    case 0 then show ?case by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   200
  next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   201
    case (Suc k)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   202
    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   203
    then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   204
      by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   205
                mult_pos_pos zero_less_Suc zero_less_mult_pos)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   206
    then show ?case
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   207
      by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   208
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   209
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   210
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   211
text\<open>The lemma above, with two changes of variables\<close>
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   212
lemma p_not_div_choose:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   213
  assumes "k < K" and "k \<le> n" 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   214
      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   215
    shows "exponent p (n choose k) = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   216
apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   217
apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   218
apply (rule TrueI)
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   219
done
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   220
62410
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   221
proposition const_p_fac:
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   222
  assumes "m>0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   223
    shows "exponent p (p^a * m choose p^a) = exponent p m"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   224
proof (cases "prime p")
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   225
  case False then show ?thesis by auto
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   226
next
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   227
  case True 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   228
  with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   229
    by (auto simp: prime_gt_0_nat) 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   230
  have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   231
    apply (rule p_not_div_choose [where K = "p^a"])
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   232
    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   233
  have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   234
  proof -
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   235
    have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   236
      using p One_nat_def times_binomial_minus1_eq by presburger
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   237
    moreover have "exponent p (p ^ a) = a"
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   238
      by (meson True exponent_power_eq)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   239
    ultimately show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   240
      using * p 
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   241
      by (metis (no_types, lifting) One_nat_def exponent_1_eq_0 exponent_mult_add mult.commute mult.right_neutral nat_0_less_mult_iff zero_less_binomial)
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   242
  qed
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   243
  then show ?thesis
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   244
    using True p exponent_mult_add by auto
2fc7a8d9c529 partial tidy-up of Sylow's theorem
paulson <lp15@cam.ac.uk>
parents: 62349
diff changeset
   245
qed
13870
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   246
cf947d1ec5ff moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff changeset
   247
end