author | wenzelm |
Sun, 13 Jan 2002 21:14:14 +0100 | |
changeset 12739 | 1fce8f51034d |
parent 12300 | 9fbce4042034 |
child 13032 | 1ec445c51931 |
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 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
57 |
lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1" |
11363 | 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 |
||
12300 | 66 |
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m" |
67 |
and gcd_dvd2 [iff]: "gcd (m, n) dvd n" |
|
11363 | 68 |
apply (induct m n rule: gcd_induct) |
69 |
apply (simp_all add: gcd_non_0) |
|
70 |
apply (blast dest: dvd_mod_imp_dvd) |
|
71 |
done |
|
72 |
||
73 |
text {* |
|
74 |
\medskip Maximality: for all @{term m}, @{term n}, @{term k} |
|
75 |
naturals, if @{term k} divides @{term m} and @{term k} divides |
|
76 |
@{term n} then @{term k} divides @{term "gcd (m, n)"}. |
|
77 |
*} |
|
78 |
||
79 |
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)" |
|
80 |
apply (induct m n rule: gcd_induct) |
|
81 |
apply (simp_all add: gcd_non_0 dvd_mod) |
|
82 |
done |
|
83 |
||
84 |
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)" |
|
85 |
apply (blast intro!: gcd_greatest intro: dvd_trans) |
|
86 |
done |
|
87 |
||
11374
2badb9b2a8ec
New proof of gcd_zero after a change to Divides.ML made the old one fail
paulson
parents:
11369
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
|
11363 | 91 |
|
92 |
text {* |
|
93 |
\medskip Function gcd yields the Greatest Common Divisor. |
|
94 |
*} |
|
95 |
||
96 |
lemma is_gcd: "is_gcd (gcd (m, n)) m n" |
|
97 |
apply (simp add: is_gcd_def gcd_greatest) |
|
98 |
done |
|
99 |
||
100 |
text {* |
|
101 |
\medskip Uniqueness of GCDs. |
|
102 |
*} |
|
103 |
||
104 |
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n" |
|
105 |
apply (simp add: is_gcd_def) |
|
106 |
apply (blast intro: dvd_anti_sym) |
|
107 |
done |
|
108 |
||
109 |
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m" |
|
110 |
apply (auto simp add: is_gcd_def) |
|
111 |
done |
|
112 |
||
113 |
||
114 |
text {* |
|
115 |
\medskip Commutativity |
|
116 |
*} |
|
117 |
||
118 |
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" |
|
119 |
apply (auto simp add: is_gcd_def) |
|
120 |
done |
|
121 |
||
122 |
lemma gcd_commute: "gcd (m, n) = gcd (n, m)" |
|
123 |
apply (rule is_gcd_unique) |
|
124 |
apply (rule is_gcd) |
|
125 |
apply (subst is_gcd_commute) |
|
126 |
apply (simp add: is_gcd) |
|
127 |
done |
|
128 |
||
129 |
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))" |
|
130 |
apply (rule is_gcd_unique) |
|
131 |
apply (rule is_gcd) |
|
132 |
apply (simp add: is_gcd_def) |
|
133 |
apply (blast intro: dvd_trans) |
|
134 |
done |
|
135 |
||
136 |
lemma gcd_0_left [simp]: "gcd (0, m) = m" |
|
137 |
apply (simp add: gcd_commute [of 0]) |
|
138 |
done |
|
139 |
||
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
140 |
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1" |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
141 |
apply (simp add: gcd_commute [of "Suc 0"]) |
11363 | 142 |
done |
143 |
||
144 |
||
145 |
text {* |
|
146 |
\medskip Multiplication laws |
|
147 |
*} |
|
148 |
||
149 |
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)" |
|
11368 | 150 |
-- {* \cite[page 27]{davenport92} *} |
11363 | 151 |
apply (induct m n rule: gcd_induct) |
152 |
apply simp |
|
153 |
apply (case_tac "k = 0") |
|
154 |
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
|
155 |
done |
|
156 |
||
157 |
lemma gcd_mult [simp]: "gcd (k, k * n) = k" |
|
158 |
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric]) |
|
159 |
done |
|
160 |
||
161 |
lemma gcd_self [simp]: "gcd (k, k) = k" |
|
162 |
apply (rule gcd_mult [of k 1, simplified]) |
|
163 |
done |
|
164 |
||
165 |
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m" |
|
166 |
apply (insert gcd_mult_distrib2 [of m k n]) |
|
167 |
apply simp |
|
168 |
apply (erule_tac t = m in ssubst) |
|
169 |
apply simp |
|
170 |
done |
|
171 |
||
172 |
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)" |
|
173 |
apply (blast intro: relprime_dvd_mult dvd_trans) |
|
174 |
done |
|
175 |
||
176 |
lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1" |
|
177 |
apply (auto simp add: prime_def) |
|
178 |
apply (drule_tac x = "gcd (p, n)" in spec) |
|
179 |
apply auto |
|
180 |
apply (insert gcd_dvd2 [of p n]) |
|
181 |
apply simp |
|
182 |
done |
|
183 |
||
184 |
text {* |
|
185 |
This theorem leads immediately to a proof of the uniqueness of |
|
186 |
factorization. If @{term p} divides a product of primes then it is |
|
187 |
one of those primes. |
|
188 |
*} |
|
189 |
||
190 |
lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
|
12739 | 191 |
by (blast intro: relprime_dvd_mult prime_imp_relprime) |
11363 | 192 |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11464
diff
changeset
|
193 |
lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m" |
12739 | 194 |
by (auto dest: prime_dvd_mult) |
195 |
||
196 |
lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m" |
|
197 |
by (rule prime_dvd_square) (simp_all add: power_two) |
|
11368 | 198 |
|
11363 | 199 |
|
200 |
text {* \medskip Addition laws *} |
|
201 |
||
202 |
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)" |
|
203 |
apply (case_tac "n = 0") |
|
204 |
apply (simp_all add: gcd_non_0) |
|
205 |
done |
|
206 |
||
207 |
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)" |
|
208 |
apply (rule gcd_commute [THEN trans]) |
|
209 |
apply (subst add_commute) |
|
210 |
apply (simp add: gcd_add1) |
|
211 |
apply (rule gcd_commute) |
|
212 |
done |
|
213 |
||
214 |
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)" |
|
215 |
apply (subst add_commute) |
|
216 |
apply (rule gcd_add2) |
|
217 |
done |
|
218 |
||
219 |
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)" |
|
220 |
apply (induct k) |
|
221 |
apply (simp_all add: gcd_add2 add_assoc) |
|
222 |
done |
|
223 |
||
224 |
||
225 |
text {* \medskip More multiplication laws *} |
|
226 |
||
227 |
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)" |
|
228 |
apply (rule dvd_anti_sym) |
|
229 |
apply (rule gcd_greatest) |
|
230 |
apply (rule_tac n = k in relprime_dvd_mult) |
|
231 |
apply (simp add: gcd_assoc) |
|
232 |
apply (simp add: gcd_commute) |
|
233 |
apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2) |
|
234 |
apply (blast intro: gcd_dvd1 dvd_trans) |
|
235 |
done |
|
236 |
||
237 |
end |