author  haftmann 
Mon, 01 Mar 2010 13:40:23 +0100  
changeset 35416  d8d7d1b785af 
parent 33946  fcc20072df9a 
child 35644  d20cf282342e 
permissions  rwrr 
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 
31 
imports 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 

31709  48 
[code del]: "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 

31709  61 
[code del]: "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 

32479  76 
declare TransferMorphism_nat_int[transfer add return: 
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 

83 
declare TransferMorphism_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 
91 
apply (subst even_mult_two_ex) 

92 
apply clarify 

93 
apply (drule_tac x = 2 in spec) 

94 
apply auto 

95 
done 

96 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

97 
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
31706  98 
unfolding prime_int_def 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

99 
apply (frule prime_odd_nat) 
31706  100 
apply (auto simp add: even_nat_def) 
101 
done 

102 

31992  103 
(* 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

104 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

105 
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0" 
31706  106 
by (unfold prime_nat_def, auto) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

107 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

108 
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0" 
31706  109 
by (unfold prime_nat_def, auto) 
22367  110 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

111 
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1" 
31706  112 
by (unfold prime_nat_def, auto) 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

113 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

114 
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1" 
31706  115 
by (unfold prime_nat_def, auto) 
22367  116 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

117 
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" 
31706  118 
by (unfold prime_nat_def, auto) 
22367  119 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

120 
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" 
31706  121 
by (unfold prime_nat_def, auto) 
122 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

123 
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" 
31706  124 
by (unfold prime_nat_def, auto) 
125 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

126 
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0" 
31992  127 
by (unfold prime_int_def prime_nat_def) auto 
22367  128 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

129 
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0" 
31706  130 
by (unfold prime_int_def prime_nat_def, auto) 
131 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

132 
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1" 
31706  133 
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

134 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

135 
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1" 
31706  136 
by (unfold prime_int_def prime_nat_def, auto) 
137 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

138 
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2" 
31706  139 
by (unfold prime_int_def prime_nat_def, auto) 
22367  140 

31706  141 

142 
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow> 

143 
m = 1 \<or> m = p))" 

144 
using prime_nat_def [transferred] 

145 
apply (case_tac "p >= 0") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

146 
by (blast, auto simp add: prime_ge_0_int) 
31706  147 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

148 
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" 
31706  149 
apply (unfold prime_nat_def) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

150 
apply (metis gcd_dvd1_nat gcd_dvd2_nat) 
31706  151 
done 
152 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

153 
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n" 
31706  154 
apply (unfold prime_int_altdef) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

155 
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

156 
done 
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

157 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

158 
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

159 
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) 
31706  160 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

161 
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

162 
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) 
31706  163 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

164 
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<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_nat, 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 prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow> 
31706  169 
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

170 
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

171 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

172 
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> 
31706  173 
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" 
174 
unfolding prime_nat_def dvd_def apply auto 

31992  175 
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

176 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

177 
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow> 
31706  178 
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" 
179 
unfolding prime_int_altdef dvd_def 

180 
apply auto 

31992  181 
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 zless_le) 
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_nat [rule_format]: "prime (p::nat) > 
31706  184 
n > 0 > (p dvd x^n > p dvd x)" 
185 
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

186 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

187 
lemma prime_dvd_power_int [rule_format]: "prime (p::int) > 
31706  188 
n > 0 > (p dvd x^n > p dvd x)" 
189 
apply (induct n rule: nat_induct, auto) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

190 
apply (frule prime_ge_0_int) 
31706  191 
apply auto 
192 
done 

193 

32007  194 
subsubsection{* Make prime naively executable *} 
195 

196 
lemma zero_not_prime_nat [simp]: "~prime (0::nat)" 

197 
by (simp add: prime_nat_def) 

198 

199 
lemma zero_not_prime_int [simp]: "~prime (0::int)" 

200 
by (simp add: prime_int_def) 

201 

202 
lemma one_not_prime_nat [simp]: "~prime (1::nat)" 

203 
by (simp add: prime_nat_def) 

204 

205 
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" 

206 
by (simp add: prime_nat_def One_nat_def) 

207 

208 
lemma one_not_prime_int [simp]: "~prime (1::int)" 

209 
by (simp add: prime_int_def) 

210 

211 
lemma prime_nat_code[code]: 

212 
"prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" 

213 
apply(simp add: Ball_def) 

214 
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat) 

215 
done 

216 

217 
lemma prime_nat_simp: 

218 
"prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))" 

219 
apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt) 

220 
apply(simp add:nat_number One_nat_def) 

221 
done 

222 

223 
lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard] 

224 

225 
lemma prime_int_code[code]: 

226 
"prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R") 

227 
proof 

228 
assume "?L" thus "?R" 

229 
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le) 

230 
next 

231 
assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int) 

232 
qed 

233 

234 
lemma prime_int_simp: 

235 
"prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p  1]))" 

236 
apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto) 

237 
apply simp 

238 
done 

239 

240 
lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard] 

241 

242 
lemma two_is_prime_nat [simp]: "prime (2::nat)" 

243 
by simp 

244 

245 
lemma two_is_prime_int [simp]: "prime (2::int)" 

246 
by simp 

247 

32111  248 
text{* A bit of regression testing: *} 
249 

250 
lemma "prime(97::nat)" 

251 
by simp 

252 

253 
lemma "prime(97::int)" 

254 
by simp 

255 

256 
lemma "prime(997::nat)" 

257 
by eval 

258 

259 
lemma "prime(997::int)" 

260 
by eval 

261 

32007  262 

263 
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

264 
apply (rule coprime_exp_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

265 
apply (subst gcd_commute_nat) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

266 
apply (erule (1) prime_imp_coprime_nat) 
31706  267 
done 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

268 

32007  269 
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

270 
apply (rule coprime_exp_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

271 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

272 
apply (erule (1) prime_imp_coprime_int) 
31706  273 
done 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

274 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

275 
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

276 
apply (rule prime_imp_coprime_nat, assumption) 
31706  277 
apply (unfold prime_nat_def, auto) 
278 
done 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

279 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

280 
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

281 
apply (rule prime_imp_coprime_int, assumption) 
31706  282 
apply (unfold prime_int_altdef, clarify) 
283 
apply (drule_tac x = q in spec) 

284 
apply (drule_tac x = p in spec) 

285 
apply auto 

286 
done 

27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

287 

32007  288 
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

289 
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

290 

32007  291 
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

292 
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

293 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

294 
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n" 
31706  295 
apply (induct n rule: nat_less_induct) 
296 
apply (case_tac "n = 0") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

297 
using two_is_prime_nat apply blast 
31706  298 
apply (case_tac "prime n") 
299 
apply blast 

300 
apply (subgoal_tac "n > 1") 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

301 
apply (frule (1) not_prime_eq_prod_nat) 
31706  302 
apply (auto intro: dvd_mult dvd_mult2) 
303 
done 

23244
1630951f0512
added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents:
22367
diff
changeset

304 

31706  305 
(* An Isar version: 
306 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

307 
lemma prime_factor_b_nat: 
31706  308 
fixes n :: nat 
309 
assumes "n \<noteq> 1" 

310 
shows "\<exists>p. prime p \<and> p dvd n" 

23983  311 

31706  312 
using `n ~= 1` 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

313 
proof (induct n rule: less_induct_nat) 
31706  314 
fix n :: nat 
315 
assume "n ~= 1" and 

316 
ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)" 

317 
thus "\<exists>p. prime p \<and> p dvd n" 

318 
proof  

319 
{ 

320 
assume "n = 0" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

321 
moreover note two_is_prime_nat 
31706  322 
ultimately have ?thesis 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

323 
by (auto simp del: two_is_prime_nat) 
31706  324 
} 
325 
moreover 

326 
{ 

327 
assume "prime n" 

328 
hence ?thesis by auto 

329 
} 

330 
moreover 

331 
{ 

332 
assume "n ~= 0" and "~ prime n" 

333 
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

334 
with `~ prime n` and not_prime_eq_prod_nat obtain m k where 
31706  335 
"n = m * k" and "1 < m" and "m < n" by blast 
336 
with ih obtain p where "prime p" and "p dvd m" by blast 

337 
with `n = m * k` have ?thesis by auto 

338 
} 

339 
ultimately show ?thesis by blast 

340 
qed 

23983  341 
qed 
342 

31706  343 
*) 
344 

345 
text {* One property of coprimality is easier to prove via prime factors. *} 

346 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

347 
lemma prime_divprod_pow_nat: 
31706  348 
assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b" 
349 
shows "p^n dvd a \<or> p^n dvd b" 

350 
proof 

351 
{assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis 

352 
apply (cases "n=0", simp_all) 

353 
apply (cases "a=1", simp_all) done} 

354 
moreover 

355 
{assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" 

356 
then obtain m where m: "n = Suc m" by (cases n, auto) 

357 
from n have "p dvd p^n" by (intro dvd_power, auto) 

358 
also note pab 

359 
finally have pab': "p dvd a * b". 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

360 
from prime_dvd_mult_nat[OF p pab'] 
31706  361 
have "p dvd a \<or> p dvd b" . 
362 
moreover 

33946  363 
{ assume pa: "p dvd a" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

364 
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto 
31706  365 
with p have "coprime b p" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

366 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
31706  367 
hence pnb: "coprime (p^n) b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

368 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  369 
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } 
31706  370 
moreover 
33946  371 
{ assume pb: "p dvd b" 
31706  372 
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

373 
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" 
31706  374 
by auto 
375 
with p have "coprime a p" 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

376 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
31706  377 
hence pna: "coprime (p^n) a" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

378 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  379 
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } 
31706  380 
ultimately have ?thesis by blast} 
381 
ultimately show ?thesis by blast 

23983  382 
qed 
383 

32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

384 
subsection {* Infinitely many primes *} 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

385 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

386 
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

387 
proof 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

388 
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

389 
from prime_factor_nat [OF f1] 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

390 
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

391 
hence "p \<le> fact n + 1" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

392 
by (intro dvd_imp_le, auto) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

393 
{assume "p \<le> n" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

394 
from `prime p` have "p \<ge> 1" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

395 
by (cases p, simp_all) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

396 
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

397 
by (intro dvd_fact_nat) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

398 
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

399 
by (rule dvd_diff_nat) 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

400 
hence "p dvd 1" by simp 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

401 
hence "p <= 1" by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

402 
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

403 
ultimately have False by auto} 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

404 
hence "n < p" by arith 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

405 
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

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 
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

409 
using next_prime_bound by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

410 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

411 
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

412 
proof 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

413 
assume "finite {(p::nat). prime p}" 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

414 
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

415 
by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

416 
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

417 
by auto 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

418 
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

419 
qed 
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

420 

8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

421 

21256  422 
end 