partial tidy-up of Sylow's theorem
authorpaulson <lp15@cam.ac.uk>
Thu Feb 25 16:49:00 2016 +0000 (2016-02-25)
changeset 624102fc7a8d9c529
parent 62408 86f27b264d3d
child 62411 994b8bab5a99
partial tidy-up of Sylow's theorem
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Feb 25 13:58:48 2016 +0000
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Feb 25 16:49:00 2016 +0000
     1.3 @@ -11,304 +11,237 @@
     1.4  
     1.5  section \<open>Sylow's Theorem\<close>
     1.6  
     1.7 -subsection \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
     1.8 +text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
     1.9 +
    1.10 +
    1.11 +subsection\<open>Prime Theorems\<close>
    1.12 +
    1.13 +lemma prime_dvd_cases:
    1.14 +  assumes pk: "p*k dvd m*n" and p: "prime p"
    1.15 +  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
    1.16 +proof -
    1.17 +  have "p dvd m*n" using dvd_mult_left pk by blast
    1.18 +  then consider "p dvd m" | "p dvd n"
    1.19 +    using p prime_dvd_mult_eq_nat by blast
    1.20 +  then show ?thesis
    1.21 +  proof cases
    1.22 +    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
    1.23 +      then have "\<exists>x. k dvd x * n \<and> m = p * x"
    1.24 +        using p pk by auto
    1.25 +    then show ?thesis ..
    1.26 +  next
    1.27 +    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
    1.28 +      then have "\<exists>y. k dvd m*y \<and> n = p*y"
    1.29 +        using p pk by auto
    1.30 +    then show ?thesis ..
    1.31 +  qed
    1.32 +qed
    1.33 +
    1.34 +lemma prime_power_dvd_prod:
    1.35 +  assumes pc: "p^c dvd m*n" and p: "prime p"
    1.36 +  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
    1.37 +using pc
    1.38 +proof (induct c arbitrary: m n)
    1.39 +  case 0 show ?case by simp
    1.40 +next
    1.41 +  case (Suc c)
    1.42 +  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
    1.43 +    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
    1.44 +  then show ?case
    1.45 +  proof cases
    1.46 +    case (1 x) 
    1.47 +      with Suc.hyps [of x n] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
    1.48 +      by force
    1.49 +  next
    1.50 +    case (2 y) 
    1.51 +      with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
    1.52 +      by force
    1.53 +  qed
    1.54 +qed
    1.55 +
    1.56 +lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
    1.57 +  by arith
    1.58 +
    1.59 +lemma prime_power_dvd_cases:
    1.60 +     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
    1.61 +  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
    1.62 +
    1.63 +text\<open>needed in this form to prove Sylow's theorem\<close>
    1.64 +corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
    1.65 +  by (metis add_Suc_right mult.commute prime_power_dvd_cases)
    1.66 +
    1.67 +
    1.68 +subsection\<open>The Exponent Function\<close>
    1.69  
    1.70  definition
    1.71    exponent :: "nat => nat => nat"
    1.72    where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
    1.73  
    1.74 +lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
    1.75 +  by (simp add: exponent_def)
    1.76  
    1.77 -text\<open>Prime Theorems\<close>
    1.78 +lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
    1.79 +  by (induct n) (auto simp: Suc_le_eq le_less_trans)
    1.80 +
    1.81 +text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
    1.82 +lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
    1.83 +  by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
    1.84  
    1.85 -lemma prime_iff:
    1.86 -  "prime p \<longleftrightarrow> Suc 0 < p \<and> (\<forall>a b. p dvd a * b \<longrightarrow> p dvd a \<or> p dvd b)"
    1.87 -  by (auto simp add: prime_gt_Suc_0_nat)
    1.88 -    (metis One_nat_def Suc_lessD dvd_refl nat_dvd_not_less not_prime_eq_prod_nat)
    1.89 -  
    1.90 -lemma zero_less_prime_power:
    1.91 -  fixes p::nat shows "prime p ==> 0 < p^a"
    1.92 -by (force simp add: prime_iff)
    1.93 +lemma exponent_ge:
    1.94 +  assumes "p ^ k dvd n" "prime p" "0 < n"
    1.95 +    shows "k \<le> exponent p n"
    1.96 +proof -
    1.97 +  have "Suc 0 < p"
    1.98 +    using \<open>prime p\<close> by (simp add: prime_def)
    1.99 +  with assms show ?thesis
   1.100 +    by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
   1.101 +qed
   1.102  
   1.103 -lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
   1.104 -by (rule ccontr, simp)
   1.105 +lemma power_exponent_dvd: "p ^ exponent p s dvd s"
   1.106 +proof (cases "s = 0")
   1.107 +  case True then show ?thesis by simp
   1.108 +next
   1.109 +  case False then show ?thesis 
   1.110 +    apply (simp add: exponent_def, clarify)
   1.111 +    apply (rule GreatestI [where k = 0])
   1.112 +    apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
   1.113 +    done
   1.114 +qed
   1.115 +
   1.116 +lemma power_Suc_exponent_Not_dvd:
   1.117 +    "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
   1.118 +  by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
   1.119  
   1.120 +lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
   1.121 +  apply (simp add: exponent_def)
   1.122 +  apply (rule Greatest_equality, simp)
   1.123 +  apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
   1.124 +  done
   1.125  
   1.126 -lemma prime_dvd_cases:
   1.127 -  fixes p::nat
   1.128 -  shows "[| p*k dvd m*n;  prime p |]
   1.129 -   ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
   1.130 -apply (simp add: prime_iff)
   1.131 -apply (frule dvd_mult_left)
   1.132 -apply (subgoal_tac "p dvd m | p dvd n")
   1.133 - prefer 2 apply blast
   1.134 -apply (erule disjE)
   1.135 -apply (rule disjI1)
   1.136 -apply (rule_tac [2] disjI2)
   1.137 -apply (auto elim!: dvdE)
   1.138 -done
   1.139 +lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   1.140 +  apply (case_tac "prime p")
   1.141 +  apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
   1.142 +  apply simp
   1.143 +  done
   1.144 +
   1.145 +lemma exponent_equalityI:
   1.146 +  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
   1.147 +  by (simp add: exponent_def)
   1.148 +
   1.149 +lemma exponent_mult_add: 
   1.150 +  assumes "a > 0" "b > 0"
   1.151 +    shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.152 +proof (cases "prime p")
   1.153 +  case False then show ?thesis by simp
   1.154 +next
   1.155 +  case True show ?thesis
   1.156 +  proof (rule order_antisym)
   1.157 +    show "exponent p a + exponent p b \<le> exponent p (a * b)"
   1.158 +      by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> assms)
   1.159 +  next
   1.160 +    { assume "exponent p a + exponent p b < exponent p (a * b)"
   1.161 +      then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b"
   1.162 +        by (meson Suc_le_eq power_exponent_dvd power_le_dvd)
   1.163 +      with prime_power_dvd_cases [where  a = "Suc (exponent p a)" and b = "Suc (exponent p b)"] 
   1.164 +      have False 
   1.165 +        by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge)
   1.166 +    } 
   1.167 +  then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
   1.168 +  qed
   1.169 +qed
   1.170 +
   1.171 +lemma not_divides_exponent_0: "~ (p dvd n) \<Longrightarrow> exponent p n = 0"
   1.172 +  apply (case_tac "exponent p n", simp)
   1.173 +  by (metis dvd_mult_left power_Suc power_exponent_dvd)
   1.174  
   1.175  
   1.176 -lemma prime_power_dvd_cases [rule_format (no_asm)]:
   1.177 -fixes p::nat
   1.178 -  shows "prime p
   1.179 -  ==> \<forall>m n. p^c dvd m*n -->
   1.180 -        (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
   1.181 -apply (induct c)
   1.182 -apply (metis dvd_1_left nat_power_eq_Suc_0_iff one_is_add)
   1.183 -(*inductive step*)
   1.184 -apply simp
   1.185 -apply clarify
   1.186 -apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
   1.187 -(*case 1: p dvd m*)
   1.188 - apply (case_tac "a")
   1.189 -  apply simp
   1.190 - apply clarify
   1.191 - apply (drule spec, drule spec, erule (1) notE impE)
   1.192 - apply (drule_tac x = nat in spec)
   1.193 - apply (drule_tac x = b in spec)
   1.194 - apply simp
   1.195 -(*case 2: p dvd n*)
   1.196 -apply (case_tac "b")
   1.197 - apply simp
   1.198 -apply clarify
   1.199 -apply (drule spec, drule spec, erule (1) notE impE)
   1.200 -apply (drule_tac x = a in spec)
   1.201 -apply (drule_tac x = nat in spec, simp)
   1.202 -done
   1.203 -
   1.204 -(*needed in this form in Sylow.ML*)
   1.205 -lemma div_combine:
   1.206 -  fixes p::nat
   1.207 -  shows "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] ==> p ^ a dvd k"
   1.208 -by (metis add_Suc add.commute prime_power_dvd_cases)
   1.209 -
   1.210 -(*Lemma for power_dvd_bound*)
   1.211 -lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
   1.212 -apply (induct n)
   1.213 -apply (simp (no_asm_simp))
   1.214 -apply simp
   1.215 -apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
   1.216 -apply (subgoal_tac "2 * p^n <= p * p^n")
   1.217 -apply arith
   1.218 -apply (drule_tac k = 2 in mult_le_mono2, simp)
   1.219 -done
   1.220 -
   1.221 -(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
   1.222 -lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a > 0|] ==> n < a"
   1.223 -apply (drule dvd_imp_le)
   1.224 -apply (drule_tac [2] n = n in Suc_le_power, auto)
   1.225 -done
   1.226 -
   1.227 -
   1.228 -text\<open>Exponent Theorems\<close>
   1.229 +subsection\<open>The Main Combinatorial Argument\<close>
   1.230  
   1.231 -lemma exponent_ge [rule_format]:
   1.232 -  "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
   1.233 -apply (simp add: exponent_def)
   1.234 -apply (erule Greatest_le)
   1.235 -apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound)
   1.236 -done
   1.237 -
   1.238 -lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
   1.239 -apply (simp add: exponent_def)
   1.240 -apply clarify
   1.241 -apply (rule_tac k = 0 in GreatestI)
   1.242 -prefer 2 apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound, simp)
   1.243 -done
   1.244 -
   1.245 -lemma power_Suc_exponent_Not_dvd:
   1.246 -  "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
   1.247 -apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
   1.248 - prefer 2 apply simp
   1.249 -apply (rule ccontr)
   1.250 -apply (drule exponent_ge, auto)
   1.251 -done
   1.252 -
   1.253 -lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a"
   1.254 -apply (simp add: exponent_def)
   1.255 -apply (rule Greatest_equality, simp)
   1.256 -apply (simp (no_asm_simp) add: prime_gt_Suc_0_nat power_dvd_imp_le)
   1.257 -done
   1.258 +lemma exponent_p_a_m_k_equation: 
   1.259 +  assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a" 
   1.260 +    shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.261 +proof (rule exponent_equalityI [OF iffI])
   1.262 +  fix r
   1.263 +  assume *: "p ^ r dvd p ^ a * m - k" 
   1.264 +  show "p ^ r dvd p ^ a - k"
   1.265 +  proof -
   1.266 +    have "k \<le> p ^ a * m" using assms
   1.267 +      by (meson nat_dvd_not_less dvd_triv_left leI mult_pos_pos order.strict_trans)
   1.268 +    then have "r \<le> a"
   1.269 +      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)
   1.270 +    then have "p^r dvd p^a * m" by (simp add: le_imp_power_dvd)
   1.271 +    thus ?thesis
   1.272 +      by (meson \<open>k \<le> p ^ a * m\<close> \<open>r \<le> a\<close> * dvd_diffD1 dvd_diff_nat le_imp_power_dvd)
   1.273 +  qed
   1.274 +next
   1.275 +  fix r
   1.276 +  assume *: "p ^ r dvd p ^ a - k" 
   1.277 +  with assms have "r \<le> a"
   1.278 +    by (metis diff_diff_cancel less_imp_le_nat nat_dvd_not_less nat_le_linear power_le_dvd zero_less_diff)
   1.279 +  show "p ^ r dvd p ^ a * m - k"
   1.280 +  proof -
   1.281 +    have "p^r dvd p^a*m"
   1.282 +      by (simp add: \<open>r \<le> a\<close> le_imp_power_dvd)
   1.283 +    then show ?thesis
   1.284 +      by (meson assms * dvd_diffD1 dvd_diff_nat le_imp_power_dvd less_imp_le_nat \<open>r \<le> a\<close>)
   1.285 +  qed
   1.286 +qed
   1.287  
   1.288 -lemma exponent_equalityI:
   1.289 -  "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   1.290 -by (simp (no_asm_simp) add: exponent_def)
   1.291 -
   1.292 -lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
   1.293 -by (simp (no_asm_simp) add: exponent_def)
   1.294 -
   1.295 +lemma p_not_div_choose_lemma: 
   1.296 +  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
   1.297 +      and "k < K"
   1.298 +    shows "exponent p (j + k choose k) = 0"
   1.299 +proof (cases "prime p")
   1.300 +  case False then show ?thesis by simp
   1.301 +next
   1.302 +  case True show ?thesis using \<open>k < K\<close> 
   1.303 +  proof (induction k)
   1.304 +    case 0 then show ?case by simp
   1.305 +  next
   1.306 +    case (Suc k)
   1.307 +    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
   1.308 +    then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
   1.309 +      by (metis Suc.IH Suc.prems Suc_lessD Suc_times_binomial_eq add.comm_neutral eeq exponent_mult_add 
   1.310 +                mult_pos_pos zero_less_Suc zero_less_mult_pos)
   1.311 +    then show ?case
   1.312 +      by (metis * add.commute add_Suc_right add_eq_self_zero exponent_mult_add zero_less_Suc)
   1.313 +  qed
   1.314 +qed
   1.315  
   1.316 -(* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
   1.317 -lemma exponent_mult_add1: "[| a > 0; b > 0 |]
   1.318 -  ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   1.319 -apply (case_tac "prime p")
   1.320 -apply (rule exponent_ge)
   1.321 -apply (auto simp add: power_add)
   1.322 -by (metis mult_dvd_mono power_exponent_dvd)
   1.323 -
   1.324 -(* exponent_mult_add, opposite inclusion *)
   1.325 -lemma exponent_mult_add2: "[| a > 0; b > 0 |]
   1.326 -  ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   1.327 -apply (case_tac "prime p")
   1.328 -apply (rule leI, clarify)
   1.329 -apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
   1.330 -apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
   1.331 -apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
   1.332 -  prefer 3 apply assumption
   1.333 - prefer 2 apply simp
   1.334 -apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
   1.335 - apply (assumption, force, simp)
   1.336 -apply (blast dest: power_Suc_exponent_Not_dvd)
   1.337 +text\<open>The lemma above, with two changes of variables\<close>
   1.338 +lemma p_not_div_choose:
   1.339 +  assumes "k < K" and "k \<le> n" 
   1.340 +      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)"
   1.341 +    shows "exponent p (n choose k) = 0"
   1.342 +apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
   1.343 +apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
   1.344 +apply (rule TrueI)
   1.345  done
   1.346  
   1.347 -lemma exponent_mult_add: "[| a > 0; b > 0 |]
   1.348 -   ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.349 -by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
   1.350 -
   1.351 -
   1.352 -lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
   1.353 -apply (case_tac "exponent p n", simp)
   1.354 -apply (case_tac "n", simp)
   1.355 -apply (cut_tac s = n and p = p in power_exponent_dvd)
   1.356 -apply (auto dest: dvd_mult_left)
   1.357 -done
   1.358 -
   1.359 -lemma exponent_1_eq_0 [simp]:
   1.360 -  fixes p::nat
   1.361 -  shows "exponent p (Suc 0) = 0"
   1.362 -apply (case_tac "prime p")
   1.363 -apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
   1.364 -apply (simp add: prime_iff not_divides_exponent_0)
   1.365 -done
   1.366 -
   1.367 -
   1.368 -text\<open>Main Combinatorial Argument\<close>
   1.369 -
   1.370 -lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
   1.371 -by (simp add: mult.commute[of a b])
   1.372 -
   1.373 -lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
   1.374 -apply (rule_tac P = "%x. x <= b * c" in subst)
   1.375 -apply (rule mult_1_right)
   1.376 -apply (rule mult_le_mono, auto)
   1.377 -done
   1.378 -
   1.379 -lemma p_fac_forw_lemma:
   1.380 -  "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   1.381 -apply (rule notnotD)
   1.382 -apply (rule notI)
   1.383 -apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
   1.384 -apply (drule less_imp_le [of a])
   1.385 -apply (drule le_imp_power_dvd)
   1.386 -apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
   1.387 -apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10))
   1.388 -done
   1.389 -
   1.390 -lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
   1.391 -  ==> (p^r) dvd (p^a) - k"
   1.392 -apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
   1.393 -apply (subgoal_tac "p^r dvd p^a*m")
   1.394 - prefer 2 apply (blast intro: dvd_mult2)
   1.395 -apply (drule dvd_diffD1)
   1.396 -  apply assumption
   1.397 - prefer 2 apply (blast intro: dvd_diff_nat)
   1.398 -apply (drule gr0_implies_Suc, auto)
   1.399 -done
   1.400 -
   1.401 -
   1.402 -lemma r_le_a_forw:
   1.403 -  "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
   1.404 -by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
   1.405 -
   1.406 -lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]
   1.407 -  ==> (p^r) dvd (p^a)*m - k"
   1.408 -apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
   1.409 -apply (subgoal_tac "p^r dvd p^a*m")
   1.410 - prefer 2 apply (blast intro: dvd_mult2)
   1.411 -apply (drule dvd_diffD1)
   1.412 -  apply assumption
   1.413 - prefer 2 apply (blast intro: dvd_diff_nat)
   1.414 -apply (drule less_imp_Suc_add, auto)
   1.415 -done
   1.416 -
   1.417 -lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]
   1.418 -  ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.419 -apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   1.420 -done
   1.421 -
   1.422 -text\<open>Suc rules that we have to delete from the simpset\<close>
   1.423 -lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
   1.424 -
   1.425 -(*The bound K is needed; otherwise it's too weak to be used.*)
   1.426 -lemma p_not_div_choose_lemma [rule_format]:
   1.427 -  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
   1.428 -   ==> k<K --> exponent p ((j+k) choose k) = 0"
   1.429 -apply (cases "prime p")
   1.430 - prefer 2 apply simp
   1.431 -apply (induct k)
   1.432 -apply (simp (no_asm))
   1.433 -(*induction step*)
   1.434 -apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
   1.435 - prefer 2 apply (simp, clarify)
   1.436 -apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
   1.437 -                    exponent p (Suc k)")
   1.438 - txt\<open>First, use the assumed equation.  We simplify the LHS to
   1.439 -  @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
   1.440 -  the common terms cancel, proving the conclusion.\<close>
   1.441 - apply (simp del: bad_Sucs add: exponent_mult_add)
   1.442 -apply (simp del: bad_Sucs add: mult_ac Suc_times_binomial exponent_mult_add)
   1.443 -
   1.444 -done
   1.445 -
   1.446 -(*The lemma above, with two changes of variables*)
   1.447 -lemma p_not_div_choose:
   1.448 -  "[| k<K;  k<=n;
   1.449 -      \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
   1.450 -   ==> exponent p (n choose k) = 0"
   1.451 -apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
   1.452 -  prefer 3 apply simp
   1.453 - prefer 2 apply assumption
   1.454 -apply (drule_tac x = "K - Suc i" in spec)
   1.455 -apply (simp add: Suc_diff_le)
   1.456 -done
   1.457 -
   1.458 -
   1.459 -lemma const_p_fac_right:
   1.460 -  "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.461 -apply (case_tac "prime p")
   1.462 - prefer 2 apply simp
   1.463 -apply (frule_tac a = a in zero_less_prime_power)
   1.464 -apply (rule_tac K = "p^a" in p_not_div_choose)
   1.465 -   apply simp
   1.466 -  apply simp
   1.467 - apply (case_tac "m")
   1.468 -  apply (case_tac [2] "p^a")
   1.469 -   apply auto
   1.470 -(*now the hard case, simplified to
   1.471 -    exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
   1.472 -apply (subgoal_tac "0<p")
   1.473 - prefer 2 apply (force dest!: prime_gt_Suc_0_nat)
   1.474 -apply (subst exponent_p_a_m_k_equation, auto)
   1.475 -done
   1.476 -
   1.477 -lemma const_p_fac:
   1.478 -  "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.479 -apply (case_tac "prime p")
   1.480 - prefer 2 apply simp
   1.481 -apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   1.482 - prefer 2 apply (force simp add: prime_iff)
   1.483 -txt\<open>A similar trick to the one used in @{text p_not_div_choose_lemma}:
   1.484 -  insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   1.485 -  first
   1.486 -  transform the binomial coefficient, then use @{text exponent_mult_add}.\<close>
   1.487 -apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
   1.488 -                    a + exponent p m")
   1.489 - apply (simp add: exponent_mult_add)
   1.490 -txt\<open>one subgoal left!\<close>
   1.491 -apply (auto simp: mult_ac)
   1.492 -apply (subst times_binomial_minus1_eq, simp)
   1.493 -apply (simp add: diff_le_mono exponent_mult_add)
   1.494 -apply (metis const_p_fac_right mult.commute)
   1.495 -done
   1.496 +proposition const_p_fac:
   1.497 +  assumes "m>0"
   1.498 +    shows "exponent p (p^a * m choose p^a) = exponent p m"
   1.499 +proof (cases "prime p")
   1.500 +  case False then show ?thesis by auto
   1.501 +next
   1.502 +  case True 
   1.503 +  with assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
   1.504 +    by (auto simp: prime_gt_0_nat) 
   1.505 +  have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
   1.506 +    apply (rule p_not_div_choose [where K = "p^a"])
   1.507 +    using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono)
   1.508 +  have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
   1.509 +  proof -
   1.510 +    have "p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1)) = p ^ a * (p ^ a * m choose p ^ a)"
   1.511 +      using p One_nat_def times_binomial_minus1_eq by presburger
   1.512 +    moreover have "exponent p (p ^ a) = a"
   1.513 +      by (meson True exponent_power_eq)
   1.514 +    ultimately show ?thesis
   1.515 +      using * p 
   1.516 +      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)
   1.517 +  qed
   1.518 +  then show ?thesis
   1.519 +    using True p exponent_mult_add by auto
   1.520 +qed
   1.521  
   1.522  end
     2.1 --- a/src/HOL/Algebra/Sylow.thy	Thu Feb 25 13:58:48 2016 +0000
     2.2 +++ b/src/HOL/Algebra/Sylow.thy	Thu Feb 25 16:49:00 2016 +0000
     2.3 @@ -12,6 +12,10 @@
     2.4  
     2.5  text\<open>The combinatorial argument is in theory Exponent\<close>
     2.6  
     2.7 +lemma le_extend_mult: 
     2.8 +  fixes c::nat shows "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
     2.9 +by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero)
    2.10 +
    2.11  locale sylow = group +
    2.12    fixes p and a and m and calM and RelM
    2.13    assumes prime_p:   "prime p"
    2.14 @@ -20,13 +24,14 @@
    2.15    defines "calM == {s. s \<subseteq> carrier(G) & card(s) = p^a}"
    2.16        and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
    2.17                               (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
    2.18 +begin
    2.19  
    2.20 -lemma (in sylow) RelM_refl_on: "refl_on calM RelM"
    2.21 +lemma RelM_refl_on: "refl_on calM RelM"
    2.22  apply (auto simp add: refl_on_def RelM_def calM_def)
    2.23  apply (blast intro!: coset_mult_one [symmetric])
    2.24  done
    2.25  
    2.26 -lemma (in sylow) RelM_sym: "sym RelM"
    2.27 +lemma RelM_sym: "sym RelM"
    2.28  proof (unfold sym_def RelM_def, clarify)
    2.29    fix y g
    2.30    assume   "y \<in> calM"
    2.31 @@ -35,19 +40,20 @@
    2.32    thus "\<exists>g'\<in>carrier G. y = y #> g #> g'" by (blast intro: g)
    2.33  qed
    2.34  
    2.35 -lemma (in sylow) RelM_trans: "trans RelM"
    2.36 +lemma RelM_trans: "trans RelM"
    2.37  by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
    2.38  
    2.39 -lemma (in sylow) RelM_equiv: "equiv calM RelM"
    2.40 +lemma RelM_equiv: "equiv calM RelM"
    2.41  apply (unfold equiv_def)
    2.42  apply (blast intro: RelM_refl_on RelM_sym RelM_trans)
    2.43  done
    2.44  
    2.45 -lemma (in sylow) M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
    2.46 +lemma M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
    2.47  apply (unfold RelM_def)
    2.48  apply (blast elim!: quotientE)
    2.49  done
    2.50  
    2.51 +end
    2.52  
    2.53  subsection\<open>Main Part of the Proof\<close>
    2.54  
    2.55 @@ -58,102 +64,87 @@
    2.56        and M1_in_M:    "M1 \<in> M"
    2.57    defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
    2.58  
    2.59 -lemma (in sylow_central) M_subset_calM: "M \<subseteq> calM"
    2.60 -by (rule M_in_quot [THEN M_subset_calM_prep])
    2.61 +begin
    2.62  
    2.63 -lemma (in sylow_central) card_M1: "card(M1) = p^a"
    2.64 -apply (cut_tac M_subset_calM M1_in_M)
    2.65 -apply (simp add: calM_def, blast)
    2.66 -done
    2.67 +lemma M_subset_calM: "M \<subseteq> calM"
    2.68 +  by (rule M_in_quot [THEN M_subset_calM_prep])
    2.69  
    2.70 -lemma card_nonempty: "0 < card(S) ==> S \<noteq> {}"
    2.71 -by force
    2.72 +lemma card_M1: "card(M1) = p^a"
    2.73 +  using M1_in_M M_subset_calM calM_def by blast
    2.74 + 
    2.75 +lemma exists_x_in_M1: "\<exists>x. x \<in> M1"
    2.76 +using prime_p [THEN prime_gt_Suc_0_nat] card_M1
    2.77 +by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI)
    2.78  
    2.79 -lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
    2.80 -apply (subgoal_tac "0 < card M1")
    2.81 - apply (blast dest: card_nonempty)
    2.82 -apply (cut_tac prime_p [THEN prime_gt_Suc_0_nat])
    2.83 -apply (simp (no_asm_simp) add: card_M1)
    2.84 -done
    2.85 +lemma M1_subset_G [simp]: "M1 \<subseteq> carrier G"
    2.86 +  using M1_in_M  M_subset_calM calM_def mem_Collect_eq subsetCE by blast
    2.87  
    2.88 -lemma (in sylow_central) M1_subset_G [simp]: "M1 \<subseteq> carrier G"
    2.89 -apply (rule subsetD [THEN PowD])
    2.90 -apply (rule_tac [2] M1_in_M)
    2.91 -apply (rule M_subset_calM [THEN subset_trans])
    2.92 -apply (auto simp add: calM_def)
    2.93 -done
    2.94 -
    2.95 -lemma (in sylow_central) M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
    2.96 -  proof -
    2.97 -    from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
    2.98 -    have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
    2.99 -    show ?thesis
   2.100 -    proof
   2.101 -      show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
   2.102 -        by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
   2.103 -      show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
   2.104 -      proof (rule restrictI)
   2.105 -        fix z assume zH: "z \<in> H"
   2.106 -        show "m1 \<otimes> z \<in> M1"
   2.107 -        proof -
   2.108 -          from zH
   2.109 -          have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
   2.110 -            by (auto simp add: H_def)
   2.111 -          show ?thesis
   2.112 -            by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
   2.113 -        qed
   2.114 +lemma M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
   2.115 +proof -
   2.116 +  from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
   2.117 +  have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
   2.118 +  show ?thesis
   2.119 +  proof
   2.120 +    show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
   2.121 +      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
   2.122 +    show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
   2.123 +    proof (rule restrictI)
   2.124 +      fix z assume zH: "z \<in> H"
   2.125 +      show "m1 \<otimes> z \<in> M1"
   2.126 +      proof -
   2.127 +        from zH
   2.128 +        have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
   2.129 +          by (auto simp add: H_def)
   2.130 +        show ?thesis
   2.131 +          by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
   2.132        qed
   2.133      qed
   2.134    qed
   2.135 +qed
   2.136  
   2.137 +end
   2.138  
   2.139  subsection\<open>Discharging the Assumptions of @{text sylow_central}\<close>
   2.140  
   2.141 -lemma (in sylow) EmptyNotInEquivSet: "{} \<notin> calM // RelM"
   2.142 +context sylow
   2.143 +begin
   2.144 +
   2.145 +lemma EmptyNotInEquivSet: "{} \<notin> calM // RelM"
   2.146  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
   2.147  
   2.148 -lemma (in sylow) existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
   2.149 -apply (subgoal_tac "M \<noteq> {}")
   2.150 - apply blast
   2.151 -apply (cut_tac EmptyNotInEquivSet, blast)
   2.152 -done
   2.153 +lemma existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
   2.154 +  using RelM_equiv equiv_Eps_in by blast
   2.155  
   2.156 -lemma (in sylow) zero_less_o_G: "0 < order(G)"
   2.157 -apply (unfold order_def)
   2.158 -apply (blast intro: zero_less_card_empty)
   2.159 -done
   2.160 +lemma zero_less_o_G: "0 < order(G)"
   2.161 +  by (simp add: order_def card_gt_0_iff carrier_not_empty)
   2.162  
   2.163 -lemma (in sylow) zero_less_m: "m > 0"
   2.164 -apply (cut_tac zero_less_o_G)
   2.165 -apply (simp add: order_G)
   2.166 -done
   2.167 +lemma zero_less_m: "m > 0"
   2.168 +  using zero_less_o_G by (simp add: order_G)
   2.169  
   2.170 -lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
   2.171 +lemma card_calM: "card(calM) = (p^a) * m choose p^a"
   2.172  by (simp add: calM_def n_subsets order_G [symmetric] order_def)
   2.173  
   2.174 -lemma (in sylow) zero_less_card_calM: "card calM > 0"
   2.175 +lemma zero_less_card_calM: "card calM > 0"
   2.176  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
   2.177  
   2.178 -lemma (in sylow) max_p_div_calM:
   2.179 +lemma max_p_div_calM:
   2.180       "~ (p ^ Suc(exponent p m) dvd card(calM))"
   2.181 -apply (subgoal_tac "exponent p m = exponent p (card calM) ")
   2.182 - apply (cut_tac zero_less_card_calM prime_p)
   2.183 - apply (force dest: power_Suc_exponent_Not_dvd)
   2.184 -apply (simp add: card_calM zero_less_m [THEN const_p_fac])
   2.185 -done
   2.186 +proof -
   2.187 +  have "exponent p m = exponent p (card calM)"
   2.188 +    by (simp add: card_calM const_p_fac zero_less_m)
   2.189 +  then show ?thesis
   2.190 +    by (metis Suc_n_not_le_n exponent_ge prime_p zero_less_card_calM)
   2.191 +qed
   2.192  
   2.193 -lemma (in sylow) finite_calM: "finite calM"
   2.194 -apply (unfold calM_def)
   2.195 -apply (rule_tac B = "Pow (carrier G) " in finite_subset)
   2.196 -apply auto
   2.197 -done
   2.198 +lemma finite_calM: "finite calM"
   2.199 +  unfolding calM_def
   2.200 +  by (rule_tac B = "Pow (carrier G) " in finite_subset) auto
   2.201  
   2.202 -lemma (in sylow) lemma_A1:
   2.203 +lemma lemma_A1:
   2.204       "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
   2.205 -apply (rule max_p_div_calM [THEN contrapos_np])
   2.206 -apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv])
   2.207 -done
   2.208 +  using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast
   2.209  
   2.210 +end
   2.211  
   2.212  subsubsection\<open>Introduction and Destruct Rules for @{term H}\<close>
   2.213  
   2.214 @@ -196,11 +187,7 @@
   2.215  by (rule finite_subset [OF M1_subset_G finite_G])
   2.216  
   2.217  lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)"
   2.218 -apply (rule finite_subset)
   2.219 -apply (rule subsetI)
   2.220 -apply (erule rcosetGM1g_subset_G, assumption)
   2.221 -apply (rule finite_G)
   2.222 -done
   2.223 +  using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast
   2.224  
   2.225  lemma (in sylow_central) M1_cardeq_rcosetGM1g:
   2.226       "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
   2.227 @@ -242,7 +229,7 @@
   2.228       "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
   2.229    by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
   2.230  
   2.231 -lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M"
   2.232 +lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
   2.233  apply (rule bexI)
   2.234  apply (rule_tac [2] M_funcset_rcosets_H)
   2.235  apply (rule inj_onI, simp)
     3.1 --- a/src/HOL/Number_Theory/Primes.thy	Thu Feb 25 13:58:48 2016 +0000
     3.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Feb 25 16:49:00 2016 +0000
     3.3 @@ -40,9 +40,7 @@
     3.4  subsection \<open>Primes\<close>
     3.5  
     3.6  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
     3.7 -  apply (auto simp add: prime_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
     3.8 -  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
     3.9 -  done
    3.10 +  using nat_dvd_1_iff_1 odd_one prime_def by blast
    3.11  
    3.12  lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
    3.13    unfolding prime_def by auto