author | paulson |
Mon, 04 Sep 2000 10:24:55 +0200 | |
changeset 9824 | c6eee0626d28 |
parent 8698 | 8812dad6ef12 |
child 9843 | cc8aa63bdad6 |
permissions | -rw-r--r-- |
1804 | 1 |
(* Title: HOL/ex/Primes.thy |
2 |
ID: $Id$ |
|
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
3376 | 6 |
The Greatest Common Divisor and Euclid's algorithm |
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3376
diff
changeset
|
7 |
|
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
8 |
See H. Davenport, "The Higher Arithmetic". 6th edition. (CUP, 1992) |
1804 | 9 |
*) |
10 |
||
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
11 |
theory Primes = Main: |
1804 | 12 |
consts |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
13 |
gcd :: "nat*nat=>nat" (*Euclid's algorithm *) |
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
14 |
|
3495
04739732b13e
New comments on how to deal with unproved termination conditions
paulson
parents:
3376
diff
changeset
|
15 |
recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)" |
3242
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
16 |
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" |
406ae5ced4e9
Renamed egcd and gcd; defined the gcd function using TFL
paulson
parents:
1804
diff
changeset
|
17 |
|
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
18 |
constdefs |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
19 |
is_gcd :: "[nat,nat,nat]=>bool" (*gcd as a relation*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
20 |
"is_gcd p m n == p dvd m & p dvd n & |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
21 |
(ALL d. d dvd m & d dvd n --> d dvd p)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
22 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
23 |
coprime :: "[nat,nat]=>bool" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
24 |
"coprime m n == gcd(m,n) = 1" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
25 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
26 |
prime :: "nat set" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
27 |
"prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
28 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
29 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
30 |
(************************************************) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
31 |
(** Greatest Common Divisor **) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
32 |
(************************************************) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
33 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
34 |
(*** Euclid's Algorithm ***) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
35 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
36 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
37 |
lemma gcd_induct: |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
38 |
"[| !!m. P m 0; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
39 |
!!m n. [| 0<n; P n (m mod n) |] ==> P m n |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
40 |
|] ==> P (m::nat) (n::nat)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
41 |
apply (rule_tac u="m" and v="n" in gcd.induct) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
42 |
apply (case_tac "n=0") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
43 |
apply (simp_all) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
44 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
45 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
46 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
47 |
lemma gcd_0 [simp]: "gcd(m,0) = m" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
48 |
apply (simp); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
49 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
50 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
51 |
lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
52 |
apply (simp) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
53 |
done; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
54 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
55 |
declare gcd.simps [simp del]; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
56 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
57 |
lemma gcd_1 [simp]: "gcd(m,1) = 1" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
58 |
apply (simp add: gcd_non_0) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
59 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
60 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
61 |
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
62 |
lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
63 |
apply (rule_tac m="m" and n="n" in gcd_induct) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
64 |
apply (simp_all add: gcd_non_0) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
65 |
apply (blast dest: dvd_mod_imp_dvd) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
66 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
67 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
68 |
lemmas gcd_dvd1 = gcd_dvd_both [THEN conjunct1]; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
69 |
lemmas gcd_dvd2 = gcd_dvd_both [THEN conjunct2]; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
70 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
71 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
72 |
(*Maximality: for all m,n,f naturals, |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
73 |
if f divides m and f divides n then f divides gcd(m,n)*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
74 |
lemma gcd_greatest [rulify]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
75 |
apply (rule_tac m="m" and n="n" in gcd_induct) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
76 |
apply (simp_all add: gcd_non_0 dvd_mod); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
77 |
done; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
78 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
79 |
(*Function gcd yields the Greatest Common Divisor*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
80 |
lemma is_gcd: "is_gcd (gcd(m,n)) m n" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
81 |
apply (simp add: is_gcd_def gcd_greatest gcd_dvd_both); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
82 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
83 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
84 |
(*uniqueness of GCDs*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
85 |
lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
86 |
apply (simp add: is_gcd_def); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
87 |
apply (blast intro: dvd_anti_sym) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
88 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
89 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
90 |
lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
91 |
apply (auto simp add: is_gcd_def); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
92 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
93 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
94 |
(** Commutativity **) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
95 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
96 |
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
97 |
apply (auto simp add: is_gcd_def); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
98 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
99 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
100 |
lemma gcd_commute: "gcd(m,n) = gcd(n,m)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
101 |
apply (rule is_gcd_unique) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
102 |
apply (rule is_gcd) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
103 |
apply (subst is_gcd_commute) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
104 |
apply (simp add: is_gcd) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
105 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
106 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
107 |
lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
108 |
apply (rule is_gcd_unique) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
109 |
apply (rule is_gcd) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
110 |
apply (simp add: is_gcd_def); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
111 |
apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans gcd_greatest); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
112 |
done |
1804 | 113 |
|
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
114 |
lemma gcd_0_left [simp]: "gcd(0,m) = m" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
115 |
apply (simp add: gcd_commute [of 0]) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
116 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
117 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
118 |
lemma gcd_1_left [simp]: "gcd(1,m) = 1" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
119 |
apply (simp add: gcd_commute [of 1]) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
120 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
121 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
122 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
123 |
(** Multiplication laws **) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
124 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
125 |
(*Davenport, page 27*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
126 |
lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
127 |
apply (rule_tac m="m" and n="n" in gcd_induct) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
128 |
apply (simp) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
129 |
apply (case_tac "k=0") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
130 |
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
131 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
132 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
133 |
lemma gcd_self [simp]: "gcd(m,m) = m" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
134 |
apply (cut_tac k="m" and m="1" and n="1" in gcd_mult_distrib2) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
135 |
apply (simp) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
136 |
(*alternative: |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
137 |
proof -; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
138 |
note gcd_mult_distrib2 [of m 1 1, simplify, THEN sym]; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
139 |
thus ?thesis; by assumption; qed; *) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
140 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
141 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
142 |
lemma gcd_mult [simp]: "gcd(k, k*n) = k" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
143 |
apply (cut_tac k="k" and m="1" and n="n" in gcd_mult_distrib2) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
144 |
apply (simp) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
145 |
(*alternative: |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
146 |
proof -; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
147 |
note gcd_mult_distrib2 [of k 1 n, simplify, THEN sym]; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
148 |
thus ?thesis; by assumption; qed; *) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
149 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
150 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
151 |
lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m"; |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
152 |
apply (subgoal_tac "k dvd gcd(m*k, m*n)") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
153 |
apply (subgoal_tac "gcd(m*k, m*n) = m") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
154 |
apply (simp) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
155 |
apply (simp add: gcd_mult_distrib2 [THEN sym]); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
156 |
apply (rule gcd_greatest) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
157 |
apply (simp_all) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
158 |
done |
1804 | 159 |
|
9824
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
160 |
lemma prime_imp_relprime: "[| p: prime; ~ p dvd n |] ==> gcd (p, n) = 1" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
161 |
apply (simp add: prime_def); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
162 |
apply (cut_tac m="p" and n="n" in gcd_dvd_both) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
163 |
apply auto |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
164 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
165 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
166 |
(*This theorem leads immediately to a proof of the uniqueness of factorization. |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
167 |
If p divides a product of primes then it is one of those primes.*) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
168 |
lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
169 |
apply (blast intro: relprime_dvd_mult prime_imp_relprime) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
170 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
171 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
172 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
173 |
(** Addition laws **) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
174 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
175 |
lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
176 |
apply (case_tac "n=0") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
177 |
apply (simp_all add: gcd_non_0) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
178 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
179 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
180 |
lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
181 |
apply (rule gcd_commute [THEN trans]) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
182 |
apply (subst add_commute) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
183 |
apply (simp add: gcd_add1) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
184 |
apply (rule gcd_commute) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
185 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
186 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
187 |
lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
188 |
apply (subst add_commute) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
189 |
apply (rule gcd_add2) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
190 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
191 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
192 |
lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
193 |
apply (induct_tac "k") |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
194 |
apply (simp_all add: gcd_add2 add_assoc) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
195 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
196 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
197 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
198 |
(** More multiplication laws **) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
199 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
200 |
lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
201 |
apply (blast intro: gcd_dvd2 gcd_dvd1 dvd_trans gcd_greatest); |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
202 |
done |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
203 |
|
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
204 |
lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)" |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
205 |
apply (rule dvd_anti_sym) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
206 |
apply (rule gcd_greatest) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
207 |
apply (rule_tac n="k" in relprime_dvd_mult) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
208 |
apply (simp add: gcd_assoc) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
209 |
apply (simp add: gcd_commute) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
210 |
apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2 gcd_dvd_gcd_mult) |
c6eee0626d28
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
paulson
parents:
8698
diff
changeset
|
211 |
done |
1804 | 212 |
|
213 |
end |