src/HOL/Algebra/Exponent.thy
 author haftmann Fri Apr 20 11:21:42 2007 +0200 (2007-04-20) changeset 22744 5cbe966d67a2 parent 21256 47195501ecf7 child 23976 9a1859635978 permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
 wenzelm@14706 ` 1` ```(* Title: HOL/Algebra/Exponent.thy ``` paulson@13870 ` 2` ``` ID: \$Id\$ ``` paulson@13870 ` 3` ``` Author: Florian Kammueller, with new proofs by L C Paulson ``` paulson@13870 ` 4` paulson@13870 ` 5` ``` exponent p s yields the greatest power of p that divides s. ``` paulson@13870 ` 6` ```*) ``` paulson@13870 ` 7` wenzelm@21256 ` 8` ```theory Exponent imports Main Primes Binomial begin ``` paulson@13870 ` 9` ballarin@20318 ` 10` ballarin@20318 ` 11` ```section {*The Combinatorial Argument Underlying the First Sylow Theorem*} ``` paulson@13870 ` 12` ```constdefs ``` paulson@13870 ` 13` ``` exponent :: "[nat, nat] => nat" ``` nipkow@16663 ` 14` ``` "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" ``` paulson@13870 ` 15` ballarin@20318 ` 16` paulson@13870 ` 17` ```subsection{*Prime Theorems*} ``` paulson@13870 ` 18` nipkow@16663 ` 19` ```lemma prime_imp_one_less: "prime p ==> Suc 0 < p" ``` paulson@13870 ` 20` ```by (unfold prime_def, force) ``` paulson@13870 ` 21` paulson@13870 ` 22` ```lemma prime_iff: ``` nipkow@16663 ` 23` ``` "(prime p) = (Suc 0 < p & (\a b. p dvd a*b --> (p dvd a) | (p dvd b)))" ``` paulson@13870 ` 24` ```apply (auto simp add: prime_imp_one_less) ``` paulson@13870 ` 25` ```apply (blast dest!: prime_dvd_mult) ``` paulson@13870 ` 26` ```apply (auto simp add: prime_def) ``` paulson@13870 ` 27` ```apply (erule dvdE) ``` paulson@13870 ` 28` ```apply (case_tac "k=0", simp) ``` paulson@13870 ` 29` ```apply (drule_tac x = m in spec) ``` paulson@13870 ` 30` ```apply (drule_tac x = k in spec) ``` nipkow@16733 ` 31` ```apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2) ``` paulson@13870 ` 32` ```done ``` paulson@13870 ` 33` nipkow@16663 ` 34` ```lemma zero_less_prime_power: "prime p ==> 0 < p^a" ``` paulson@13870 ` 35` ```by (force simp add: prime_iff) ``` paulson@13870 ` 36` paulson@13870 ` 37` paulson@13870 ` 38` ```lemma zero_less_card_empty: "[| finite S; S \ {} |] ==> 0 < card(S)" ``` paulson@13870 ` 39` ```by (rule ccontr, simp) ``` paulson@13870 ` 40` paulson@13870 ` 41` paulson@13870 ` 42` ```lemma prime_dvd_cases: ``` nipkow@16663 ` 43` ``` "[| p*k dvd m*n; prime p |] ``` paulson@13870 ` 44` ``` ==> (\x. k dvd x*n & m = p*x) | (\y. k dvd m*y & n = p*y)" ``` paulson@13870 ` 45` ```apply (simp add: prime_iff) ``` paulson@13870 ` 46` ```apply (frule dvd_mult_left) ``` paulson@13870 ` 47` ```apply (subgoal_tac "p dvd m | p dvd n") ``` paulson@13870 ` 48` ``` prefer 2 apply blast ``` paulson@13870 ` 49` ```apply (erule disjE) ``` paulson@13870 ` 50` ```apply (rule disjI1) ``` paulson@13870 ` 51` ```apply (rule_tac [2] disjI2) ``` paulson@13870 ` 52` ```apply (erule_tac n = m in dvdE) ``` paulson@13870 ` 53` ```apply (erule_tac [2] n = n in dvdE, auto) ``` paulson@13870 ` 54` ```apply (rule_tac [2] k = p in dvd_mult_cancel) ``` paulson@13870 ` 55` ```apply (rule_tac k = p in dvd_mult_cancel) ``` paulson@13870 ` 56` ```apply (simp_all add: mult_ac) ``` paulson@13870 ` 57` ```done ``` paulson@13870 ` 58` paulson@13870 ` 59` nipkow@16663 ` 60` ```lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p ``` paulson@13870 ` 61` ``` ==> \m n. p^c dvd m*n --> ``` paulson@13870 ` 62` ``` (\a b. a+b = Suc c --> p^a dvd m | p^b dvd n)" ``` paulson@13870 ` 63` ```apply (induct_tac "c") ``` paulson@13870 ` 64` ``` apply clarify ``` paulson@13870 ` 65` ``` apply (case_tac "a") ``` paulson@13870 ` 66` ``` apply simp ``` paulson@13870 ` 67` ``` apply simp ``` paulson@13870 ` 68` ```(*inductive step*) ``` paulson@13870 ` 69` ```apply simp ``` paulson@13870 ` 70` ```apply clarify ``` paulson@13870 ` 71` ```apply (erule prime_dvd_cases [THEN disjE], assumption, auto) ``` paulson@13870 ` 72` ```(*case 1: p dvd m*) ``` paulson@13870 ` 73` ``` apply (case_tac "a") ``` paulson@13870 ` 74` ``` apply simp ``` paulson@13870 ` 75` ``` apply clarify ``` paulson@13870 ` 76` ``` apply (drule spec, drule spec, erule (1) notE impE) ``` paulson@13870 ` 77` ``` apply (drule_tac x = nat in spec) ``` paulson@13870 ` 78` ``` apply (drule_tac x = b in spec) ``` paulson@13870 ` 79` ``` apply simp ``` paulson@13870 ` 80` ``` apply (blast intro: dvd_refl mult_dvd_mono) ``` paulson@13870 ` 81` ```(*case 2: p dvd n*) ``` paulson@13870 ` 82` ```apply (case_tac "b") ``` paulson@13870 ` 83` ``` apply simp ``` paulson@13870 ` 84` ```apply clarify ``` paulson@13870 ` 85` ```apply (drule spec, drule spec, erule (1) notE impE) ``` paulson@13870 ` 86` ```apply (drule_tac x = a in spec) ``` paulson@13870 ` 87` ```apply (drule_tac x = nat in spec, simp) ``` paulson@13870 ` 88` ```apply (blast intro: dvd_refl mult_dvd_mono) ``` paulson@13870 ` 89` ```done ``` paulson@13870 ` 90` paulson@13870 ` 91` ```(*needed in this form in Sylow.ML*) ``` paulson@13870 ` 92` ```lemma div_combine: ``` nipkow@16663 ` 93` ``` "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] ``` paulson@13870 ` 94` ``` ==> p ^ a dvd k" ``` paulson@13870 ` 95` ```by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto) ``` paulson@13870 ` 96` paulson@13870 ` 97` ```(*Lemma for power_dvd_bound*) ``` paulson@13870 ` 98` ```lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" ``` paulson@13870 ` 99` ```apply (induct_tac "n") ``` paulson@13870 ` 100` ```apply (simp (no_asm_simp)) ``` paulson@13870 ` 101` ```apply simp ``` paulson@13870 ` 102` ```apply (subgoal_tac "2 * n + 2 <= p * p^n", simp) ``` paulson@13870 ` 103` ```apply (subgoal_tac "2 * p^n <= p * p^n") ``` paulson@13870 ` 104` ```(*?arith_tac should handle all of this!*) ``` paulson@13870 ` 105` ```apply (rule order_trans) ``` paulson@13870 ` 106` ```prefer 2 apply assumption ``` paulson@13870 ` 107` ```apply (drule_tac k = 2 in mult_le_mono2, simp) ``` paulson@13870 ` 108` ```apply (rule mult_le_mono1, simp) ``` paulson@13870 ` 109` ```done ``` paulson@13870 ` 110` paulson@13870 ` 111` ```(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) ``` paulson@13870 ` 112` ```lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a" ``` paulson@13870 ` 113` ```apply (drule dvd_imp_le) ``` paulson@13870 ` 114` ```apply (drule_tac [2] n = n in Suc_le_power, auto) ``` paulson@13870 ` 115` ```done ``` paulson@13870 ` 116` paulson@13870 ` 117` paulson@13870 ` 118` ```subsection{*Exponent Theorems*} ``` paulson@13870 ` 119` paulson@13870 ` 120` ```lemma exponent_ge [rule_format]: ``` nipkow@16663 ` 121` ``` "[|p^k dvd n; prime p; 0 k <= exponent p n" ``` paulson@13870 ` 122` ```apply (simp add: exponent_def) ``` paulson@13870 ` 123` ```apply (erule Greatest_le) ``` paulson@13870 ` 124` ```apply (blast dest: prime_imp_one_less power_dvd_bound) ``` paulson@13870 ` 125` ```done ``` paulson@13870 ` 126` paulson@13870 ` 127` ```lemma power_exponent_dvd: "0 (p ^ exponent p s) dvd s" ``` paulson@13870 ` 128` ```apply (simp add: exponent_def) ``` paulson@13870 ` 129` ```apply clarify ``` paulson@13870 ` 130` ```apply (rule_tac k = 0 in GreatestI) ``` paulson@13870 ` 131` ```prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp) ``` paulson@13870 ` 132` ```done ``` paulson@13870 ` 133` paulson@13870 ` 134` ```lemma power_Suc_exponent_Not_dvd: ``` nipkow@16663 ` 135` ``` "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0" ``` paulson@13870 ` 136` ```apply (subgoal_tac "p ^ Suc (exponent p s) dvd s") ``` paulson@13870 ` 137` ``` prefer 2 apply simp ``` paulson@13870 ` 138` ```apply (rule ccontr) ``` paulson@13870 ` 139` ```apply (drule exponent_ge, auto) ``` paulson@13870 ` 140` ```done ``` paulson@13870 ` 141` nipkow@16663 ` 142` ```lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a" ``` paulson@13870 ` 143` ```apply (simp (no_asm_simp) add: exponent_def) ``` paulson@13870 ` 144` ```apply (rule Greatest_equality, simp) ``` paulson@13870 ` 145` ```apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le) ``` paulson@13870 ` 146` ```done ``` paulson@13870 ` 147` paulson@13870 ` 148` ```lemma exponent_equalityI: ``` paulson@13870 ` 149` ``` "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b" ``` paulson@13870 ` 150` ```by (simp (no_asm_simp) add: exponent_def) ``` paulson@13870 ` 151` nipkow@16663 ` 152` ```lemma exponent_eq_0 [simp]: "\ prime p ==> exponent p s = 0" ``` paulson@13870 ` 153` ```by (simp (no_asm_simp) add: exponent_def) ``` paulson@13870 ` 154` paulson@13870 ` 155` paulson@13870 ` 156` ```(* exponent_mult_add, easy inclusion. Could weaken p \ prime to Suc 0 < p *) ``` paulson@13870 ` 157` ```lemma exponent_mult_add1: ``` paulson@13870 ` 158` ``` "[| 0 < a; 0 < b |] ``` paulson@13870 ` 159` ``` ==> (exponent p a) + (exponent p b) <= exponent p (a * b)" ``` nipkow@16663 ` 160` ```apply (case_tac "prime p") ``` paulson@13870 ` 161` ```apply (rule exponent_ge) ``` paulson@13870 ` 162` ```apply (auto simp add: power_add) ``` paulson@13870 ` 163` ```apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono) ``` paulson@13870 ` 164` ```done ``` paulson@13870 ` 165` paulson@13870 ` 166` ```(* exponent_mult_add, opposite inclusion *) ``` paulson@13870 ` 167` ```lemma exponent_mult_add2: "[| 0 < a; 0 < b |] ``` paulson@13870 ` 168` ``` ==> exponent p (a * b) <= (exponent p a) + (exponent p b)" ``` nipkow@16663 ` 169` ```apply (case_tac "prime p") ``` paulson@13870 ` 170` ```apply (rule leI, clarify) ``` paulson@13870 ` 171` ```apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto) ``` paulson@13870 ` 172` ```apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b") ``` paulson@13870 ` 173` ```apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans]) ``` paulson@13870 ` 174` ``` prefer 3 apply assumption ``` paulson@13870 ` 175` ``` prefer 2 apply simp ``` paulson@13870 ` 176` ```apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases) ``` paulson@13870 ` 177` ``` apply (assumption, force, simp) ``` paulson@13870 ` 178` ```apply (blast dest: power_Suc_exponent_Not_dvd) ``` paulson@13870 ` 179` ```done ``` paulson@13870 ` 180` paulson@13870 ` 181` ```lemma exponent_mult_add: ``` paulson@13870 ` 182` ``` "[| 0 < a; 0 < b |] ``` paulson@13870 ` 183` ``` ==> exponent p (a * b) = (exponent p a) + (exponent p b)" ``` paulson@13870 ` 184` ```by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym) ``` paulson@13870 ` 185` paulson@13870 ` 186` paulson@13870 ` 187` ```lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0" ``` paulson@13870 ` 188` ```apply (case_tac "exponent p n", simp) ``` paulson@13870 ` 189` ```apply (case_tac "n", simp) ``` paulson@13870 ` 190` ```apply (cut_tac s = n and p = p in power_exponent_dvd) ``` paulson@13870 ` 191` ```apply (auto dest: dvd_mult_left) ``` paulson@13870 ` 192` ```done ``` paulson@13870 ` 193` paulson@13870 ` 194` ```lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0" ``` nipkow@16663 ` 195` ```apply (case_tac "prime p") ``` paulson@13870 ` 196` ```apply (auto simp add: prime_iff not_divides_exponent_0) ``` paulson@13870 ` 197` ```done ``` paulson@13870 ` 198` paulson@13870 ` 199` ballarin@20318 ` 200` ```subsection{*Main Combinatorial Argument*} ``` paulson@13870 ` 201` paulson@14889 ` 202` ```lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)" ``` paulson@14889 ` 203` ```apply (rule_tac P = "%x. x <= b * c" in subst) ``` paulson@14889 ` 204` ```apply (rule mult_1_right) ``` paulson@14889 ` 205` ```apply (rule mult_le_mono, auto) ``` paulson@14889 ` 206` ```done ``` paulson@14889 ` 207` paulson@13870 ` 208` ```lemma p_fac_forw_lemma: ``` paulson@13870 ` 209` ``` "[| 0 < (m::nat); 0 r <= a" ``` paulson@13870 ` 210` ```apply (rule notnotD) ``` paulson@13870 ` 211` ```apply (rule notI) ``` paulson@13870 ` 212` ```apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) ``` paulson@13870 ` 213` ```apply (drule_tac m = a in less_imp_le) ``` paulson@13870 ` 214` ```apply (drule le_imp_power_dvd) ``` paulson@13870 ` 215` ```apply (drule_tac n = "p ^ r" in dvd_trans, assumption) ``` paulson@13870 ` 216` ```apply (frule_tac m = k in less_imp_le) ``` paulson@13870 ` 217` ```apply (drule_tac c = m in le_extend_mult, assumption) ``` paulson@13870 ` 218` ```apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1) ``` paulson@13870 ` 219` ```prefer 2 apply assumption ``` paulson@13870 ` 220` ```apply (rule dvd_refl [THEN dvd_mult2]) ``` paulson@13870 ` 221` ```apply (drule_tac n = k in dvd_imp_le, auto) ``` paulson@13870 ` 222` ```done ``` paulson@13870 ` 223` paulson@13870 ` 224` ```lemma p_fac_forw: "[| 0 < (m::nat); 0 (p^r) dvd (p^a) - k" ``` paulson@13870 ` 226` ```apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto) ``` paulson@13870 ` 227` ```apply (subgoal_tac "p^r dvd p^a*m") ``` paulson@13870 ` 228` ``` prefer 2 apply (blast intro: dvd_mult2) ``` paulson@13870 ` 229` ```apply (drule dvd_diffD1) ``` paulson@13870 ` 230` ``` apply assumption ``` paulson@13870 ` 231` ``` prefer 2 apply (blast intro: dvd_diff) ``` paulson@13870 ` 232` ```apply (drule less_imp_Suc_add, auto) ``` paulson@13870 ` 233` ```done ``` paulson@13870 ` 234` paulson@13870 ` 235` paulson@13870 ` 236` ```lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a" ``` paulson@13870 ` 237` ```by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto) ``` paulson@13870 ` 238` paulson@13870 ` 239` ```lemma p_fac_backw: "[| 0 (p^r) dvd (p^a)*m - k" ``` paulson@13870 ` 241` ```apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto) ``` paulson@13870 ` 242` ```apply (subgoal_tac "p^r dvd p^a*m") ``` paulson@13870 ` 243` ``` prefer 2 apply (blast intro: dvd_mult2) ``` paulson@13870 ` 244` ```apply (drule dvd_diffD1) ``` paulson@13870 ` 245` ``` apply assumption ``` paulson@13870 ` 246` ``` prefer 2 apply (blast intro: dvd_diff) ``` paulson@13870 ` 247` ```apply (drule less_imp_Suc_add, auto) ``` paulson@13870 ` 248` ```done ``` paulson@13870 ` 249` paulson@13870 ` 250` ```lemma exponent_p_a_m_k_equation: "[| 0 exponent p (p^a * m - k) = exponent p (p^a - k)" ``` paulson@13870 ` 252` ```apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw) ``` paulson@13870 ` 253` ```done ``` paulson@13870 ` 254` paulson@13870 ` 255` ```text{*Suc rules that we have to delete from the simpset*} ``` paulson@13870 ` 256` ```lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right ``` paulson@13870 ` 257` paulson@13870 ` 258` ```(*The bound K is needed; otherwise it's too weak to be used.*) ``` paulson@13870 ` 259` ```lemma p_not_div_choose_lemma [rule_format]: ``` paulson@13870 ` 260` ``` "[| \i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] ``` paulson@13870 ` 261` ``` ==> k exponent p ((j+k) choose k) = 0" ``` nipkow@16663 ` 262` ```apply (case_tac "prime p") ``` paulson@13870 ` 263` ``` prefer 2 apply simp ``` paulson@13870 ` 264` ```apply (induct_tac "k") ``` paulson@13870 ` 265` ```apply (simp (no_asm)) ``` paulson@13870 ` 266` ```(*induction step*) ``` paulson@13870 ` 267` ```apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ") ``` paulson@13870 ` 268` ``` prefer 2 apply (simp add: zero_less_binomial_iff, clarify) ``` paulson@13870 ` 269` ```apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = ``` paulson@13870 ` 270` ``` exponent p (Suc n)") ``` paulson@13870 ` 271` ``` txt{*First, use the assumed equation. We simplify the LHS to ``` paulson@13870 ` 272` ``` @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"} ``` paulson@13870 ` 273` ``` the common terms cancel, proving the conclusion.*} ``` paulson@13870 ` 274` ``` apply (simp del: bad_Sucs add: exponent_mult_add) ``` paulson@13870 ` 275` ```txt{*Establishing the equation requires first applying ``` paulson@13870 ` 276` ``` @{text Suc_times_binomial_eq} ...*} ``` paulson@13870 ` 277` ```apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric]) ``` paulson@13870 ` 278` ```txt{*...then @{text exponent_mult_add} and the quantified premise.*} ``` paulson@13870 ` 279` ```apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add) ``` paulson@13870 ` 280` ```done ``` paulson@13870 ` 281` paulson@13870 ` 282` ```(*The lemma above, with two changes of variables*) ``` paulson@13870 ` 283` ```lemma p_not_div_choose: ``` paulson@13870 ` 284` ``` "[| kj. 0 exponent p (n - k + (K - j)) = exponent p (K - j)|] ``` paulson@13870 ` 286` ``` ==> exponent p (n choose k) = 0" ``` paulson@13870 ` 287` ```apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma) ``` paulson@13870 ` 288` ``` prefer 3 apply simp ``` paulson@13870 ` 289` ``` prefer 2 apply assumption ``` paulson@13870 ` 290` ```apply (drule_tac x = "K - Suc i" in spec) ``` paulson@13870 ` 291` ```apply (simp add: Suc_diff_le) ``` paulson@13870 ` 292` ```done ``` paulson@13870 ` 293` paulson@13870 ` 294` paulson@13870 ` 295` ```lemma const_p_fac_right: ``` paulson@13870 ` 296` ``` "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0" ``` nipkow@16663 ` 297` ```apply (case_tac "prime p") ``` paulson@13870 ` 298` ``` prefer 2 apply simp ``` paulson@13870 ` 299` ```apply (frule_tac a = a in zero_less_prime_power) ``` paulson@13870 ` 300` ```apply (rule_tac K = "p^a" in p_not_div_choose) ``` paulson@13870 ` 301` ``` apply simp ``` paulson@13870 ` 302` ``` apply simp ``` paulson@13870 ` 303` ``` apply (case_tac "m") ``` paulson@13870 ` 304` ``` apply (case_tac [2] "p^a") ``` paulson@13870 ` 305` ``` apply auto ``` paulson@13870 ` 306` ```(*now the hard case, simplified to ``` paulson@13870 ` 307` ``` exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *) ``` paulson@13870 ` 308` ```apply (subgoal_tac "0 exponent p (((p^a) * m) choose p^a) = exponent p m" ``` nipkow@16663 ` 315` ```apply (case_tac "prime p") ``` paulson@13870 ` 316` ``` prefer 2 apply simp ``` paulson@13870 ` 317` ```apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m") ``` paulson@13870 ` 318` ``` prefer 2 apply (force simp add: prime_iff) ``` paulson@13870 ` 319` ```txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}: ``` paulson@13870 ` 320` ``` insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS, ``` paulson@13870 ` 321` ``` first ``` paulson@13870 ` 322` ``` transform the binomial coefficient, then use @{text exponent_mult_add}.*} ``` paulson@13870 ` 323` ```apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = ``` paulson@13870 ` 324` ``` a + exponent p m") ``` paulson@13870 ` 325` ``` apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff) ``` paulson@13870 ` 326` ```txt{*one subgoal left!*} ``` paulson@13870 ` 327` ```apply (subst times_binomial_minus1_eq, simp, simp) ``` paulson@13870 ` 328` ```apply (subst exponent_mult_add, simp) ``` paulson@13870 ` 329` ```apply (simp (no_asm_simp) add: zero_less_binomial_iff) ``` webertj@20432 ` 330` ```apply arith ``` paulson@13870 ` 331` ```apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right) ``` paulson@13870 ` 332` ```done ``` paulson@13870 ` 333` paulson@13870 ` 334` paulson@13870 ` 335` ```end ```