author | huffman |
Wed, 07 Sep 2011 09:02:58 -0700 | |
changeset 44821 | a92f65e174cf |
parent 40461 | e876e95588ce |
child 44872 | a98ef45122f3 |
permissions | -rw-r--r-- |
32479 | 1 |
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, |
31798 | 2 |
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow |
31706 | 3 |
|
4 |
||
32479 | 5 |
This file deals with properties of primes. Definitions and lemmas are |
6 |
proved uniformly for the natural numbers and integers. |
|
31706 | 7 |
|
8 |
This file combines and revises a number of prior developments. |
|
9 |
||
10 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
11 |
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced |
|
12 |
gcd, lcm, and prime for the natural numbers. |
|
13 |
||
14 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
15 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
16 |
another extension of the notions to the integers, and added a number |
|
17 |
of results to "Primes" and "GCD". IntPrimes also defined and developed |
|
18 |
the congruence relations on the integers. The notion was extended to |
|
33718 | 19 |
the natural numbers by Chaieb. |
31706 | 20 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
21 |
Jeremy Avigad combined all of these, made everything uniform for the |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
22 |
natural numbers and the integers, and added a number of new theorems. |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
23 |
|
31798 | 24 |
Tobias Nipkow cleaned up a lot. |
21256 | 25 |
*) |
26 |
||
31706 | 27 |
|
32479 | 28 |
header {* Primes *} |
21256 | 29 |
|
32479 | 30 |
theory Primes |
37294
a2a8216999a2
absolute import -- must work with Main.thy / HOL-Proofs
haftmann
parents:
35644
diff
changeset
|
31 |
imports "~~/src/HOL/GCD" |
31706 | 32 |
begin |
33 |
||
34 |
declare One_nat_def [simp del] |
|
35 |
||
36 |
class prime = one + |
|
37 |
||
38 |
fixes |
|
39 |
prime :: "'a \<Rightarrow> bool" |
|
40 |
||
41 |
instantiation nat :: prime |
|
42 |
||
43 |
begin |
|
21256 | 44 |
|
21263 | 45 |
definition |
31706 | 46 |
prime_nat :: "nat \<Rightarrow> bool" |
47 |
where |
|
37765 | 48 |
"prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
31706 | 49 |
|
50 |
instance proof qed |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
51 |
|
31706 | 52 |
end |
53 |
||
54 |
instantiation int :: prime |
|
55 |
||
56 |
begin |
|
57 |
||
58 |
definition |
|
59 |
prime_int :: "int \<Rightarrow> bool" |
|
60 |
where |
|
37765 | 61 |
"prime_int p = prime (nat p)" |
31706 | 62 |
|
63 |
instance proof qed |
|
64 |
||
65 |
end |
|
66 |
||
67 |
||
68 |
subsection {* Set up Transfer *} |
|
69 |
||
70 |
||
32479 | 71 |
lemma transfer_nat_int_prime: |
31706 | 72 |
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" |
73 |
unfolding gcd_int_def lcm_int_def prime_int_def |
|
74 |
by auto |
|
23687
06884f7ffb18
extended - convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset
|
75 |
|
35644 | 76 |
declare transfer_morphism_nat_int[transfer add return: |
32479 | 77 |
transfer_nat_int_prime] |
31706 | 78 |
|
32479 | 79 |
lemma transfer_int_nat_prime: |
31706 | 80 |
"prime (int x) = prime x" |
81 |
by (unfold gcd_int_def lcm_int_def prime_int_def, auto) |
|
82 |
||
35644 | 83 |
declare transfer_morphism_int_nat[transfer add return: |
32479 | 84 |
transfer_int_nat_prime] |
31798 | 85 |
|
21256 | 86 |
|
32479 | 87 |
subsection {* Primes *} |
31706 | 88 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
89 |
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
31706 | 90 |
unfolding prime_nat_def |
40461 | 91 |
by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat) |
31706 | 92 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
93 |
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" |
31706 | 94 |
unfolding prime_int_def |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
95 |
apply (frule prime_odd_nat) |
31706 | 96 |
apply (auto simp add: even_nat_def) |
97 |
done |
|
98 |
||
31992 | 99 |
(* FIXME Is there a better way to handle these, rather than making them elim rules? *) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
100 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
101 |
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0" |
31706 | 102 |
by (unfold prime_nat_def, auto) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
103 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
104 |
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0" |
31706 | 105 |
by (unfold prime_nat_def, auto) |
22367 | 106 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
107 |
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1" |
31706 | 108 |
by (unfold prime_nat_def, auto) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
109 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
110 |
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1" |
31706 | 111 |
by (unfold prime_nat_def, auto) |
22367 | 112 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
113 |
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" |
31706 | 114 |
by (unfold prime_nat_def, auto) |
22367 | 115 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
116 |
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" |
31706 | 117 |
by (unfold prime_nat_def, auto) |
118 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
119 |
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" |
31706 | 120 |
by (unfold prime_nat_def, auto) |
121 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
122 |
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0" |
31992 | 123 |
by (unfold prime_int_def prime_nat_def) auto |
22367 | 124 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
125 |
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0" |
31706 | 126 |
by (unfold prime_int_def prime_nat_def, auto) |
127 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
128 |
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1" |
31706 | 129 |
by (unfold prime_int_def prime_nat_def, auto) |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
130 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
131 |
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1" |
31706 | 132 |
by (unfold prime_int_def prime_nat_def, auto) |
133 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
134 |
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2" |
31706 | 135 |
by (unfold prime_int_def prime_nat_def, auto) |
22367 | 136 |
|
31706 | 137 |
|
138 |
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow> |
|
139 |
m = 1 \<or> m = p))" |
|
140 |
using prime_nat_def [transferred] |
|
141 |
apply (case_tac "p >= 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
142 |
by (blast, auto simp add: prime_ge_0_int) |
31706 | 143 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
144 |
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
31706 | 145 |
apply (unfold prime_nat_def) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
146 |
apply (metis gcd_dvd1_nat gcd_dvd2_nat) |
31706 | 147 |
done |
148 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
149 |
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" |
31706 | 150 |
apply (unfold prime_int_altdef) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
151 |
apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
152 |
done |
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
153 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
154 |
lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
155 |
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) |
31706 | 156 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
157 |
lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
158 |
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) |
31706 | 159 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
160 |
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow> |
31706 | 161 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
162 |
by (rule iffI, rule prime_dvd_mult_nat, auto) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
163 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
164 |
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow> |
31706 | 165 |
p dvd m * n = (p dvd m \<or> p dvd n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
166 |
by (rule iffI, rule prime_dvd_mult_int, auto) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
167 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
168 |
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
31706 | 169 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
170 |
unfolding prime_nat_def dvd_def apply auto |
|
31992 | 171 |
by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
172 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
173 |
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> |
31706 | 174 |
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" |
175 |
unfolding prime_int_altdef dvd_def |
|
176 |
apply auto |
|
44821 | 177 |
by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
178 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
179 |
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) --> |
31706 | 180 |
n > 0 --> (p dvd x^n --> p dvd x)" |
181 |
by (induct n rule: nat_induct, auto) |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
182 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
183 |
lemma prime_dvd_power_int [rule_format]: "prime (p::int) --> |
31706 | 184 |
n > 0 --> (p dvd x^n --> p dvd x)" |
185 |
apply (induct n rule: nat_induct, auto) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
186 |
apply (frule prime_ge_0_int) |
31706 | 187 |
apply auto |
188 |
done |
|
189 |
||
32007 | 190 |
subsubsection{* Make prime naively executable *} |
191 |
||
192 |
lemma zero_not_prime_nat [simp]: "~prime (0::nat)" |
|
193 |
by (simp add: prime_nat_def) |
|
194 |
||
195 |
lemma zero_not_prime_int [simp]: "~prime (0::int)" |
|
196 |
by (simp add: prime_int_def) |
|
197 |
||
198 |
lemma one_not_prime_nat [simp]: "~prime (1::nat)" |
|
199 |
by (simp add: prime_nat_def) |
|
200 |
||
201 |
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" |
|
202 |
by (simp add: prime_nat_def One_nat_def) |
|
203 |
||
204 |
lemma one_not_prime_int [simp]: "~prime (1::int)" |
|
205 |
by (simp add: prime_int_def) |
|
206 |
||
37607 | 207 |
lemma prime_nat_code [code]: |
208 |
"prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" |
|
209 |
apply (simp add: Ball_def) |
|
32007 | 210 |
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat) |
211 |
done |
|
212 |
||
213 |
lemma prime_nat_simp: |
|
37607 | 214 |
"prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)" |
215 |
by (auto simp add: prime_nat_code) |
|
32007 | 216 |
|
37607 | 217 |
lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard] |
32007 | 218 |
|
37607 | 219 |
lemma prime_int_code [code]: |
220 |
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R") |
|
32007 | 221 |
proof |
222 |
assume "?L" thus "?R" |
|
44821 | 223 |
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le) |
32007 | 224 |
next |
225 |
assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int) |
|
226 |
qed |
|
227 |
||
228 |
lemma prime_int_simp: |
|
37607 | 229 |
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)" |
230 |
by (auto simp add: prime_int_code) |
|
32007 | 231 |
|
37607 | 232 |
lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard] |
32007 | 233 |
|
234 |
lemma two_is_prime_nat [simp]: "prime (2::nat)" |
|
235 |
by simp |
|
236 |
||
237 |
lemma two_is_prime_int [simp]: "prime (2::int)" |
|
238 |
by simp |
|
239 |
||
32111 | 240 |
text{* A bit of regression testing: *} |
241 |
||
242 |
lemma "prime(97::nat)" |
|
243 |
by simp |
|
244 |
||
245 |
lemma "prime(97::int)" |
|
246 |
by simp |
|
247 |
||
248 |
lemma "prime(997::nat)" |
|
249 |
by eval |
|
250 |
||
251 |
lemma "prime(997::int)" |
|
252 |
by eval |
|
253 |
||
32007 | 254 |
|
255 |
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
256 |
apply (rule coprime_exp_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
257 |
apply (subst gcd_commute_nat) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
258 |
apply (erule (1) prime_imp_coprime_nat) |
31706 | 259 |
done |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
260 |
|
32007 | 261 |
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
262 |
apply (rule coprime_exp_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
263 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
264 |
apply (erule (1) prime_imp_coprime_int) |
31706 | 265 |
done |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
266 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
267 |
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
268 |
apply (rule prime_imp_coprime_nat, assumption) |
31706 | 269 |
apply (unfold prime_nat_def, auto) |
270 |
done |
|
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
271 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
272 |
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
273 |
apply (rule prime_imp_coprime_int, assumption) |
40461 | 274 |
apply (unfold prime_int_altdef) |
44821 | 275 |
apply (metis int_one_le_iff_zero_less less_le) |
31706 | 276 |
done |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
277 |
|
32007 | 278 |
lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
279 |
by (rule coprime_exp2_nat, rule primes_coprime_nat) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
280 |
|
32007 | 281 |
lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
282 |
by (rule coprime_exp2_int, rule primes_coprime_int) |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
283 |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
284 |
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n" |
31706 | 285 |
apply (induct n rule: nat_less_induct) |
286 |
apply (case_tac "n = 0") |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
287 |
using two_is_prime_nat apply blast |
40461 | 288 |
apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less |
289 |
neq0_conv prime_nat_def) |
|
31706 | 290 |
done |
23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset
|
291 |
|
31706 | 292 |
(* An Isar version: |
293 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
294 |
lemma prime_factor_b_nat: |
31706 | 295 |
fixes n :: nat |
296 |
assumes "n \<noteq> 1" |
|
297 |
shows "\<exists>p. prime p \<and> p dvd n" |
|
23983 | 298 |
|
31706 | 299 |
using `n ~= 1` |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
300 |
proof (induct n rule: less_induct_nat) |
31706 | 301 |
fix n :: nat |
302 |
assume "n ~= 1" and |
|
303 |
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" |
|
304 |
thus "\<exists>p. prime p \<and> p dvd n" |
|
305 |
proof - |
|
306 |
{ |
|
307 |
assume "n = 0" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
308 |
moreover note two_is_prime_nat |
31706 | 309 |
ultimately have ?thesis |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
310 |
by (auto simp del: two_is_prime_nat) |
31706 | 311 |
} |
312 |
moreover |
|
313 |
{ |
|
314 |
assume "prime n" |
|
315 |
hence ?thesis by auto |
|
316 |
} |
|
317 |
moreover |
|
318 |
{ |
|
319 |
assume "n ~= 0" and "~ prime n" |
|
320 |
with `n ~= 1` have "n > 1" by auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
321 |
with `~ prime n` and not_prime_eq_prod_nat obtain m k where |
31706 | 322 |
"n = m * k" and "1 < m" and "m < n" by blast |
323 |
with ih obtain p where "prime p" and "p dvd m" by blast |
|
324 |
with `n = m * k` have ?thesis by auto |
|
325 |
} |
|
326 |
ultimately show ?thesis by blast |
|
327 |
qed |
|
23983 | 328 |
qed |
329 |
||
31706 | 330 |
*) |
331 |
||
332 |
text {* One property of coprimality is easier to prove via prime factors. *} |
|
333 |
||
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
334 |
lemma prime_divprod_pow_nat: |
31706 | 335 |
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b" |
336 |
shows "p^n dvd a \<or> p^n dvd b" |
|
337 |
proof- |
|
338 |
{assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis |
|
339 |
apply (cases "n=0", simp_all) |
|
340 |
apply (cases "a=1", simp_all) done} |
|
341 |
moreover |
|
342 |
{assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" |
|
343 |
then obtain m where m: "n = Suc m" by (cases n, auto) |
|
344 |
from n have "p dvd p^n" by (intro dvd_power, auto) |
|
345 |
also note pab |
|
346 |
finally have pab': "p dvd a * b". |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
347 |
from prime_dvd_mult_nat[OF p pab'] |
31706 | 348 |
have "p dvd a \<or> p dvd b" . |
349 |
moreover |
|
33946 | 350 |
{ assume pa: "p dvd a" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
351 |
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto |
31706 | 352 |
with p have "coprime b p" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
353 |
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) |
31706 | 354 |
hence pnb: "coprime (p^n) b" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
355 |
by (subst gcd_commute_nat, rule coprime_exp_nat) |
33946 | 356 |
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } |
31706 | 357 |
moreover |
33946 | 358 |
{ assume pb: "p dvd b" |
31706 | 359 |
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
360 |
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" |
31706 | 361 |
by auto |
362 |
with p have "coprime a p" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
363 |
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) |
31706 | 364 |
hence pna: "coprime (p^n) a" |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset
|
365 |
by (subst gcd_commute_nat, rule coprime_exp_nat) |
33946 | 366 |
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } |
31706 | 367 |
ultimately have ?thesis by blast} |
368 |
ultimately show ?thesis by blast |
|
23983 | 369 |
qed |
370 |
||
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
371 |
subsection {* Infinitely many primes *} |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
372 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
373 |
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
374 |
proof- |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
375 |
have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
376 |
from prime_factor_nat [OF f1] |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
377 |
obtain p where "prime p" and "p dvd fact n + 1" by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
378 |
hence "p \<le> fact n + 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
379 |
by (intro dvd_imp_le, auto) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
380 |
{assume "p \<le> n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
381 |
from `prime p` have "p \<ge> 1" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
382 |
by (cases p, simp_all) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
383 |
with `p <= n` have "p dvd fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
384 |
by (intro dvd_fact_nat) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
385 |
with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
386 |
by (rule dvd_diff_nat) |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
387 |
hence "p dvd 1" by simp |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
388 |
hence "p <= 1" by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
389 |
moreover from `prime p` have "p > 1" by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
390 |
ultimately have False by auto} |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
391 |
hence "n < p" by arith |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
392 |
with `prime p` and `p <= fact n + 1` show ?thesis by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
393 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
394 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
395 |
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
396 |
using next_prime_bound by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
397 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
398 |
lemma primes_infinite: "\<not> (finite {(p::nat). prime p})" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
399 |
proof |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
400 |
assume "finite {(p::nat). prime p}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
401 |
with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
402 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
403 |
then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
404 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
405 |
with bigger_prime [of b] show False by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
406 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
407 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
408 |
|
21256 | 409 |
end |