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