1 (* Title: ZF/ex/Primes.thy
3 Author: Christophe Tabacznyj and Lawrence C Paulson
4 Copyright 1996 University of Cambridge
7 header{*The Divides Relation and Euclid's algorithm for the GCD*}
11 divides :: "[i,i]=>o" (infixl "dvd" 50)
12 "m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
14 is_gcd :: "[i,i,i]=>o" --{*definition of great common divisor*}
15 "is_gcd(p,m,n) == ((p dvd m) & (p dvd n)) &
16 (\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
18 gcd :: "[i,i]=>i" --{*Euclid's algorithm for the gcd*}
19 "gcd(m,n) == transrec(natify(n),
20 %n f. \<lambda>m \<in> nat.
21 if n=0 then m else f`(m mod n)`n) ` natify(m)"
23 coprime :: "[i,i]=>o" --{*the coprime relation*}
24 "coprime(m,n) == gcd(m,n) = 1"
26 prime :: i --{*the set of prime numbers*}
27 "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
30 subsection{*The Divides Relation*}
32 lemma dvdD: "m dvd n ==> m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
33 by (unfold divides_def, assumption)
36 "[|m dvd n; !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P"
37 by (blast dest!: dvdD)
39 lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard]
40 lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard]
43 lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0"
44 apply (simp add: divides_def)
45 apply (fast intro: nat_0I mult_0_right [symmetric])
48 lemma dvd_0_left: "0 dvd m ==> m = 0"
49 by (simp add: divides_def)
51 lemma dvd_refl [simp]: "m \<in> nat ==> m dvd m"
52 apply (simp add: divides_def)
53 apply (fast intro: nat_1I mult_1_right [symmetric])
56 lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p"
57 by (auto simp add: divides_def intro: mult_assoc mult_type)
59 lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n"
60 apply (simp add: divides_def)
61 apply (force dest: mult_eq_self_implies_10
62 simp add: mult_assoc mult_eq_1_iff)
65 lemma dvd_mult_left: "[|(i#*j) dvd k; i \<in> nat|] ==> i dvd k"
66 by (auto simp add: divides_def mult_assoc)
68 lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
69 apply (simp add: divides_def, clarify)
70 apply (rule_tac x = "i#*k" in bexI)
71 apply (simp add: mult_ac)
72 apply (rule mult_type)
76 subsection{*Euclid's Algorithm for the GCD*}
78 lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
79 apply (simp add: gcd_def)
80 apply (subst transrec, simp)
83 lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)"
84 by (simp add: gcd_def)
86 lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)"
87 by (simp add: gcd_def)
90 "[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
91 apply (simp add: gcd_def)
92 apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
93 apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
94 mod_less_divisor [THEN ltD])
97 lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)"
98 apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw)
102 lemma gcd_1 [simp]: "gcd(m,1) = 1"
103 by (simp (no_asm_simp) add: gcd_non_0)
105 lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)"
106 apply (simp add: divides_def)
107 apply (fast intro: add_mult_distrib_left [symmetric] add_type)
110 lemma dvd_mult: "k dvd n ==> k dvd (m #* n)"
111 apply (simp add: divides_def)
112 apply (fast intro: mult_left_commute mult_type)
115 lemma dvd_mult2: "k dvd m ==> k dvd (m #* n)"
116 apply (subst mult_commute)
117 apply (blast intro: dvd_mult)
121 lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard]
122 lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard]
124 lemma dvd_mod_imp_dvd_raw:
125 "[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
126 apply (case_tac "b=0")
127 apply (simp add: DIVISION_BY_ZERO_MOD)
128 apply (blast intro: mod_div_equality [THEN subst]
130 intro!: dvd_add dvd_mult mult_type mod_type div_type)
133 lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a \<in> nat |] ==> k dvd a"
134 apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw)
136 apply (simp add: divides_def)
140 lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n \<in> nat;
141 \<forall>m \<in> nat. P(m,0);
142 \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]
143 ==> \<forall>m \<in> nat. P (m,n)"
144 apply (erule_tac i = n in complete_induct)
145 apply (case_tac "x=0")
146 apply (simp (no_asm_simp))
148 apply (drule_tac x1 = m and x = x in bspec [THEN bspec])
149 apply (simp_all add: Ord_0_lt_iff)
150 apply (blast intro: mod_less_divisor [THEN ltD])
153 lemma gcd_induct: "!!P. [| m \<in> nat; n \<in> nat;
154 !!m. m \<in> nat ==> P(m,0);
155 !!m n. [|m \<in> nat; n \<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |]
157 by (blast intro: gcd_induct_lemma)
160 subsection{*Basic Properties of @{term gcd}*}
163 lemma gcd_type [simp,TC]: "gcd(m, n) \<in> nat"
164 apply (subgoal_tac "gcd (natify (m), natify (n)) \<in> nat")
166 apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct)
168 apply (simp add: gcd_non_0)
172 text{* Property 1: gcd(a,b) divides a and b *}
175 "[| m \<in> nat; n \<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n"
176 apply (rule_tac m = m and n = n in gcd_induct)
177 apply (simp_all add: gcd_non_0)
178 apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt])
181 lemma gcd_dvd1 [simp]: "m \<in> nat ==> gcd(m,n) dvd m"
182 apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
186 lemma gcd_dvd2 [simp]: "n \<in> nat ==> gcd(m,n) dvd n"
187 apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
191 text{* if f divides a and b then f divides gcd(a,b) *}
193 lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
194 apply (simp add: divides_def)
195 apply (case_tac "b=0")
196 apply (simp add: DIVISION_BY_ZERO_MOD, auto)
197 apply (blast intro: mod_mult_distrib2 [symmetric])
200 text{* Property 2: for all a,b,f naturals,
201 if f divides a and f divides b then f divides gcd(a,b)*}
203 lemma gcd_greatest_raw [rule_format]:
204 "[| m \<in> nat; n \<in> nat; f \<in> nat |]
205 ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
206 apply (rule_tac m = m and n = n in gcd_induct)
207 apply (simp_all add: gcd_non_0 dvd_mod)
210 lemma gcd_greatest: "[| f dvd m; f dvd n; f \<in> nat |] ==> f dvd gcd(m,n)"
211 apply (rule gcd_greatest_raw)
212 apply (auto simp add: divides_def)
215 lemma gcd_greatest_iff [simp]: "[| k \<in> nat; m \<in> nat; n \<in> nat |]
216 ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)"
217 by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
220 subsection{*The Greatest Common Divisor*}
222 text{*The GCD exists and function gcd computes it.*}
224 lemma is_gcd: "[| m \<in> nat; n \<in> nat |] ==> is_gcd(gcd(m,n), m, n)"
225 by (simp add: is_gcd_def)
227 text{*The GCD is unique*}
229 lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m\<in>nat; n\<in>nat|] ==> m=n"
230 apply (simp add: is_gcd_def)
231 apply (blast intro: dvd_anti_sym)
234 lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
235 by (simp add: is_gcd_def, blast)
237 lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)"
238 apply (rule is_gcd_unique)
240 apply (rule_tac [3] is_gcd_commute [THEN iffD1])
241 apply (rule_tac [3] is_gcd, auto)
244 lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
245 apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw)
249 lemma gcd_assoc_raw: "[| k \<in> nat; m \<in> nat; n \<in> nat |]
250 ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
251 apply (rule is_gcd_unique)
253 apply (simp_all add: is_gcd_def)
254 apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans)
257 lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
258 apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
263 lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)"
264 by (simp add: gcd_commute [of 0])
266 lemma gcd_1_left [simp]: "gcd (1, m) = 1"
267 by (simp add: gcd_commute [of 1])
270 subsection{*Addition laws*}
272 lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
273 apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
275 apply (case_tac "natify (n) = 0")
276 apply (auto simp add: Ord_0_lt_iff gcd_non_0)
279 lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
280 apply (rule gcd_commute [THEN trans])
281 apply (subst add_commute, simp)
282 apply (rule gcd_commute)
285 lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
286 by (subst add_commute, rule gcd_add2)
288 lemma gcd_add_mult_raw: "k \<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
289 apply (erule nat_induct)
290 apply (auto simp add: gcd_add2 add_assoc)
293 lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
294 apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
299 subsection{* Multiplication Laws*}
301 lemma gcd_mult_distrib2_raw:
302 "[| k \<in> nat; m \<in> nat; n \<in> nat |]
303 ==> k #* gcd (m, n) = gcd (k #* m, k #* n)"
304 apply (erule_tac m = m and n = n in gcd_induct, assumption)
306 apply (case_tac "k = 0", simp)
307 apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff)
310 lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)"
311 apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
312 in gcd_mult_distrib2_raw)
316 lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)"
317 by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto)
319 lemma gcd_self [simp]: "gcd (k, k) = natify(k)"
320 by (cut_tac k = k and n = 1 in gcd_mult, auto)
322 lemma relprime_dvd_mult:
323 "[| gcd (k,n) = 1; k dvd (m #* n); m \<in> nat |] ==> k dvd m"
324 apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto)
325 apply (erule_tac b = m in ssubst)
326 apply (simp add: dvd_imp_nat1)
329 lemma relprime_dvd_mult_iff:
330 "[| gcd (k,n) = 1; m \<in> nat |] ==> k dvd (m #* n) <-> k dvd m"
331 by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)
333 lemma prime_imp_relprime:
334 "[| p \<in> prime; ~ (p dvd n); n \<in> nat |] ==> gcd (p, n) = 1"
335 apply (simp add: prime_def, clarify)
336 apply (drule_tac x = "gcd (p,n)" in bspec)
338 apply (cut_tac m = p and n = n in gcd_dvd2, auto)
341 lemma prime_into_nat: "p \<in> prime ==> p \<in> nat"
342 by (simp add: prime_def)
344 lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p\<noteq>0"
345 by (auto simp add: prime_def)
348 text{*This theorem leads immediately to a proof of the uniqueness of
349 factorization. If @{term p} divides a product of primes then it is
350 one of those primes.*}
352 lemma prime_dvd_mult:
353 "[|p dvd m #* n; p \<in> prime; m \<in> nat; n \<in> nat |] ==> p dvd m \<or> p dvd n"
354 by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat)
357 lemma gcd_mult_cancel_raw:
358 "[|gcd (k,n) = 1; m \<in> nat; n \<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)"
359 apply (rule dvd_anti_sym)
360 apply (rule gcd_greatest)
361 apply (rule relprime_dvd_mult [of _ k])
362 apply (simp add: gcd_assoc)
363 apply (simp add: gcd_commute)
364 apply (simp_all add: mult_commute)
365 apply (blast intro: dvdI1 gcd_dvd1 dvd_trans)
368 lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)"
369 apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw)
374 subsection{*The Square Root of a Prime is Irrational: Key Lemma*}
376 lemma prime_dvd_other_side:
377 "\<lbrakk>n#*n = p#*(k#*k); p \<in> prime; n \<in> nat\<rbrakk> \<Longrightarrow> p dvd n"
378 apply (subgoal_tac "p dvd n#*n")
379 apply (blast dest: prime_dvd_mult)
380 apply (rule_tac j = "k#*k" in dvd_mult_left)
381 apply (auto simp add: prime_def)
385 "\<lbrakk>k#*k = p#*(j#*j); p \<in> prime; 0 < k; j \<in> nat; k \<in> nat\<rbrakk>
386 \<Longrightarrow> k < p#*j & 0 < j"
388 apply (simp add: not_lt_iff_le prime_into_nat)
390 apply (frule mult_le_mono, assumption+)
391 apply (simp add: mult_ac)
392 apply (auto dest!: natify_eqE
393 simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1)
394 apply (simp add: prime_def)
395 apply (blast dest: lt_trans1)
398 lemma rearrange: "j #* (p#*j) = k#*k \<Longrightarrow> k#*k = p#*(j#*j)"
399 by (simp add: mult_ac)
401 lemma prime_not_square:
402 "\<lbrakk>m \<in> nat; p \<in> prime\<rbrakk> \<Longrightarrow> \<forall>k \<in> nat. 0<k \<longrightarrow> m#*m \<noteq> p#*(k#*k)"
403 apply (erule complete_induct, clarify)
404 apply (frule prime_dvd_other_side, assumption)
407 apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat)
408 apply (blast dest: rearrange reduction ltD)