|
1 (* Title: HOL/NumberTheory/Primes.thy |
|
2 ID: $Id$ |
|
3 Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 Copyright 1996 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* The Greatest Common Divisor and Euclid's algorithm *} |
|
8 |
|
9 theory Primes = Main: |
|
10 |
|
11 text {* |
|
12 (See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992)) |
|
13 |
|
14 \bigskip |
|
15 *} |
|
16 |
|
17 consts |
|
18 gcd :: "nat * nat => nat" -- {* Euclid's algorithm *} |
|
19 |
|
20 recdef gcd "measure ((\<lambda>(m, n). n) :: nat * nat => nat)" |
|
21 "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))" |
|
22 |
|
23 constdefs |
|
24 is_gcd :: "nat => nat => nat => bool" -- {* @{term gcd} as a relation *} |
|
25 "is_gcd p m n == p dvd m \<and> p dvd n \<and> |
|
26 (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)" |
|
27 |
|
28 coprime :: "nat => nat => bool" |
|
29 "coprime m n == gcd (m, n) = 1" |
|
30 |
|
31 prime :: "nat set" |
|
32 "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}" |
|
33 |
|
34 |
|
35 lemma gcd_induct: |
|
36 "(!!m. P m 0) ==> |
|
37 (!!m n. 0 < n ==> P n (m mod n) ==> P m n) |
|
38 ==> P (m::nat) (n::nat)" |
|
39 apply (induct m n rule: gcd.induct) |
|
40 apply (case_tac "n = 0") |
|
41 apply simp_all |
|
42 done |
|
43 |
|
44 |
|
45 lemma gcd_0 [simp]: "gcd (m, 0) = m" |
|
46 apply simp |
|
47 done |
|
48 |
|
49 lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)" |
|
50 apply simp |
|
51 done |
|
52 |
|
53 declare gcd.simps [simp del] |
|
54 |
|
55 lemma gcd_1 [simp]: "gcd (m, 1) = 1" |
|
56 apply (simp add: gcd_non_0) |
|
57 done |
|
58 |
|
59 text {* |
|
60 \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}. The |
|
61 conjunctions don't seem provable separately. |
|
62 *} |
|
63 |
|
64 lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n" |
|
65 apply (induct m n rule: gcd_induct) |
|
66 apply (simp_all add: gcd_non_0) |
|
67 apply (blast dest: dvd_mod_imp_dvd) |
|
68 done |
|
69 |
|
70 lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard] |
|
71 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard] |
|
72 |
|
73 |
|
74 text {* |
|
75 \medskip Maximality: for all @{term m}, @{term n}, @{term k} |
|
76 naturals, if @{term k} divides @{term m} and @{term k} divides |
|
77 @{term n} then @{term k} divides @{term "gcd (m, n)"}. |
|
78 *} |
|
79 |
|
80 lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" |
|
81 apply (induct m n rule: gcd_induct) |
|
82 apply (simp_all add: gcd_non_0 dvd_mod) |
|
83 done |
|
84 |
|
85 lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)" |
|
86 apply (blast intro!: gcd_greatest intro: dvd_trans) |
|
87 done |
|
88 |
|
89 |
|
90 text {* |
|
91 \medskip Function gcd yields the Greatest Common Divisor. |
|
92 *} |
|
93 |
|
94 lemma is_gcd: "is_gcd (gcd (m, n)) m n" |
|
95 apply (simp add: is_gcd_def gcd_greatest) |
|
96 done |
|
97 |
|
98 text {* |
|
99 \medskip Uniqueness of GCDs. |
|
100 *} |
|
101 |
|
102 lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" |
|
103 apply (simp add: is_gcd_def) |
|
104 apply (blast intro: dvd_anti_sym) |
|
105 done |
|
106 |
|
107 lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" |
|
108 apply (auto simp add: is_gcd_def) |
|
109 done |
|
110 |
|
111 |
|
112 text {* |
|
113 \medskip Commutativity |
|
114 *} |
|
115 |
|
116 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" |
|
117 apply (auto simp add: is_gcd_def) |
|
118 done |
|
119 |
|
120 lemma gcd_commute: "gcd (m, n) = gcd (n, m)" |
|
121 apply (rule is_gcd_unique) |
|
122 apply (rule is_gcd) |
|
123 apply (subst is_gcd_commute) |
|
124 apply (simp add: is_gcd) |
|
125 done |
|
126 |
|
127 lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" |
|
128 apply (rule is_gcd_unique) |
|
129 apply (rule is_gcd) |
|
130 apply (simp add: is_gcd_def) |
|
131 apply (blast intro: dvd_trans) |
|
132 done |
|
133 |
|
134 lemma gcd_0_left [simp]: "gcd (0, m) = m" |
|
135 apply (simp add: gcd_commute [of 0]) |
|
136 done |
|
137 |
|
138 lemma gcd_1_left [simp]: "gcd (1, m) = 1" |
|
139 apply (simp add: gcd_commute [of 1]) |
|
140 done |
|
141 |
|
142 |
|
143 text {* |
|
144 \medskip Multiplication laws |
|
145 *} |
|
146 |
|
147 lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" |
|
148 -- {* Davenport, page 27 *} |
|
149 apply (induct m n rule: gcd_induct) |
|
150 apply simp |
|
151 apply (case_tac "k = 0") |
|
152 apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
|
153 done |
|
154 |
|
155 lemma gcd_mult [simp]: "gcd (k, k * n) = k" |
|
156 apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) |
|
157 done |
|
158 |
|
159 lemma gcd_self [simp]: "gcd (k, k) = k" |
|
160 apply (rule gcd_mult [of k 1, simplified]) |
|
161 done |
|
162 |
|
163 lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" |
|
164 apply (insert gcd_mult_distrib2 [of m k n]) |
|
165 apply simp |
|
166 apply (erule_tac t = m in ssubst) |
|
167 apply simp |
|
168 done |
|
169 |
|
170 lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" |
|
171 apply (blast intro: relprime_dvd_mult dvd_trans) |
|
172 done |
|
173 |
|
174 lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1" |
|
175 apply (auto simp add: prime_def) |
|
176 apply (drule_tac x = "gcd (p, n)" in spec) |
|
177 apply auto |
|
178 apply (insert gcd_dvd2 [of p n]) |
|
179 apply simp |
|
180 done |
|
181 |
|
182 text {* |
|
183 This theorem leads immediately to a proof of the uniqueness of |
|
184 factorization. If @{term p} divides a product of primes then it is |
|
185 one of those primes. |
|
186 *} |
|
187 |
|
188 lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
|
189 apply (blast intro: relprime_dvd_mult prime_imp_relprime) |
|
190 done |
|
191 |
|
192 |
|
193 text {* \medskip Addition laws *} |
|
194 |
|
195 lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" |
|
196 apply (case_tac "n = 0") |
|
197 apply (simp_all add: gcd_non_0) |
|
198 done |
|
199 |
|
200 lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" |
|
201 apply (rule gcd_commute [THEN trans]) |
|
202 apply (subst add_commute) |
|
203 apply (simp add: gcd_add1) |
|
204 apply (rule gcd_commute) |
|
205 done |
|
206 |
|
207 lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" |
|
208 apply (subst add_commute) |
|
209 apply (rule gcd_add2) |
|
210 done |
|
211 |
|
212 lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" |
|
213 apply (induct k) |
|
214 apply (simp_all add: gcd_add2 add_assoc) |
|
215 done |
|
216 |
|
217 |
|
218 text {* \medskip More multiplication laws *} |
|
219 |
|
220 lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" |
|
221 apply (rule dvd_anti_sym) |
|
222 apply (rule gcd_greatest) |
|
223 apply (rule_tac n = k in relprime_dvd_mult) |
|
224 apply (simp add: gcd_assoc) |
|
225 apply (simp add: gcd_commute) |
|
226 apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2) |
|
227 apply (blast intro: gcd_dvd1 dvd_trans) |
|
228 done |
|
229 |
|
230 end |