author paulson Thu Feb 25 16:49:00 2016 +0000 (2016-02-25) changeset 62410 2fc7a8d9c529 parent 62408 86f27b264d3d child 62411 994b8bab5a99
partial tidy-up of Sylow's theorem
 src/HOL/Algebra/Exponent.thy file | annotate | diff | revisions src/HOL/Algebra/Sylow.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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.310 +                mult_pos_pos zero_less_Suc zero_less_mult_pos)
1.311 +    then show ?case
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.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.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.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.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.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.490 -txt\<open>one subgoal left!\<close>
1.491 -apply (auto simp: mult_ac)
1.492 -apply (subst times_binomial_minus1_eq, simp)
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.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
```