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