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_self [simp]: "gcd(m,m) = m" |
|
138 apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym]) |
|
139 done |
|
140 |
|
141 lemma gcd_mult [simp]: "gcd(k, k*n) = k" |
|
142 apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym]) |
|
143 done |
|
144 |
|
145 lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
|
146 apply (subgoal_tac "gcd(m*k, m*n) = m") |
|
147 apply (erule_tac t="m" in subst); |
|
148 apply (simp) |
|
149 apply (simp add: gcd_mult_distrib2 [THEN sym]); |
|
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 |
|