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