author  wenzelm 
Sat, 10 Sep 2011 23:27:32 +0200  
changeset 44872  a98ef45122f3 
parent 44821  a92f65e174cf 
child 45605  a89b4bc311a5 
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 
37294
a2a8216999a2
absolute import  must work with Main.thy / HOLProofs
haftmann
parents:
35644
diff
changeset

31 
imports "~~/src/HOL/GCD" 
31706  32 
begin 
33 

34 
class prime = one + 

44872  35 
fixes prime :: "'a \<Rightarrow> bool" 
31706  36 

37 
instantiation nat :: prime 

38 
begin 

21256  39 

44872  40 
definition prime_nat :: "nat \<Rightarrow> bool" 
41 
where "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p))" 

31706  42 

44872  43 
instance .. 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

44 

31706  45 
end 
46 

47 
instantiation int :: prime 

48 
begin 

49 

44872  50 
definition prime_int :: "int \<Rightarrow> bool" 
51 
where "prime_int p = prime (nat p)" 

31706  52 

44872  53 
instance .. 
31706  54 

55 
end 

56 

57 

58 
subsection {* Set up Transfer *} 

59 

32479  60 
lemma transfer_nat_int_prime: 
31706  61 
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" 
44872  62 
unfolding gcd_int_def lcm_int_def prime_int_def by auto 
23687
06884f7ffb18
extended  convers now basic lcm properties also
haftmann
parents:
23431
diff
changeset

63 

35644  64 
declare transfer_morphism_nat_int[transfer add return: 
32479  65 
transfer_nat_int_prime] 
31706  66 

44872  67 
lemma transfer_int_nat_prime: "prime (int x) = prime x" 
68 
unfolding gcd_int_def lcm_int_def prime_int_def by auto 

31706  69 

35644  70 
declare transfer_morphism_int_nat[transfer add return: 
32479  71 
transfer_int_nat_prime] 
31798  72 

21256  73 

32479  74 
subsection {* Primes *} 
31706  75 

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

76 
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
31706  77 
unfolding prime_nat_def 
40461  78 
by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat) 
31706  79 

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

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

82 
apply (frule prime_odd_nat) 
31706  83 
apply (auto simp add: even_nat_def) 
44872  84 
done 
31706  85 

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

87 

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

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

90 

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

91 
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0" 
44872  92 
unfolding prime_nat_def by auto 
22367  93 

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

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

96 

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

97 
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1" 
44872  98 
unfolding prime_nat_def by auto 
22367  99 

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

100 
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" 
44872  101 
unfolding prime_nat_def by auto 
22367  102 

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

103 
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" 
44872  104 
unfolding prime_nat_def by auto 
31706  105 

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

106 
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" 
44872  107 
unfolding prime_nat_def by auto 
31706  108 

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

109 
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0" 
44872  110 
unfolding prime_int_def prime_nat_def by auto 
22367  111 

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

112 
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0" 
44872  113 
unfolding prime_int_def prime_nat_def by auto 
31706  114 

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

115 
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1" 
44872  116 
unfolding prime_int_def prime_nat_def by auto 
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset

117 

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

118 
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1" 
44872  119 
unfolding prime_int_def prime_nat_def by auto 
31706  120 

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

121 
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2" 
44872  122 
unfolding prime_int_def prime_nat_def by auto 
22367  123 

31706  124 

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

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

127 
using prime_nat_def [transferred] 

44872  128 
apply (cases "p >= 0") 
129 
apply blast 

130 
apply (auto simp add: prime_ge_0_int) 

131 
done 

31706  132 

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

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

135 
apply (metis gcd_dvd1_nat gcd_dvd2_nat) 
31706  136 
done 
137 

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

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

140 
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

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

142 

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

143 
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

144 
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) 
31706  145 

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

146 
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

147 
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) 
31706  148 

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

149 
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow> 
31706  150 
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

151 
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

152 

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

153 
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow> 
31706  154 
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

155 
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

156 

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

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

44872  160 
by (metis mult_commute linorder_neq_iff linorder_not_le mult_1 
161 
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

162 

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

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

166 
apply auto 

44872  167 
by (metis div_mult_self1_is_id div_mult_self2_is_id 
168 
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

169 

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

170 
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) > 
31706  171 
n > 0 > (p dvd x^n > p dvd x)" 
44872  172 
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

173 

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

174 
lemma prime_dvd_power_int [rule_format]: "prime (p::int) > 
31706  175 
n > 0 > (p dvd x^n > p dvd x)" 
44872  176 
apply (induct n rule: nat_induct) 
177 
apply auto 

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

178 
apply (frule prime_ge_0_int) 
31706  179 
apply auto 
44872  180 
done 
31706  181 

44872  182 
subsubsection {* Make prime naively executable *} 
32007  183 

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

185 
by (simp add: prime_nat_def) 

186 

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

188 
by (simp add: prime_int_def) 

189 

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

191 
by (simp add: prime_nat_def) 

192 

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

194 
by (simp add: prime_nat_def One_nat_def) 

195 

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

197 
by (simp add: prime_int_def) 

198 

37607  199 
lemma prime_nat_code [code]: 
44872  200 
"prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" 
201 
apply (simp add: Ball_def) 

202 
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat) 

203 
done 

32007  204 

205 
lemma prime_nat_simp: 

44872  206 
"prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)" 
207 
by (auto simp add: prime_nat_code) 

32007  208 

37607  209 
lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard] 
32007  210 

37607  211 
lemma prime_int_code [code]: 
212 
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R") 

32007  213 
proof 
44872  214 
assume "?L" 
215 
then show "?R" 

44821  216 
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le) 
32007  217 
next 
44872  218 
assume "?R" 
219 
then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int) 

32007  220 
qed 
221 

44872  222 
lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p  1]. ~ n dvd p)" 
223 
by (auto simp add: prime_int_code) 

32007  224 

37607  225 
lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard] 
32007  226 

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

44872  228 
by simp 
32007  229 

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

44872  231 
by simp 
32007  232 

32111  233 
text{* A bit of regression testing: *} 
234 

44872  235 
lemma "prime(97::nat)" by simp 
236 
lemma "prime(97::int)" by simp 

237 
lemma "prime(997::nat)" by eval 

238 
lemma "prime(997::int)" by eval 

32111  239 

32007  240 

241 
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

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

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

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

246 

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

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

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

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

252 

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

253 
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

254 
apply (rule prime_imp_coprime_nat, assumption) 
44872  255 
apply (unfold prime_nat_def) 
256 
apply auto 

257 
done 

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

258 

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

259 
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

260 
apply (rule prime_imp_coprime_int, assumption) 
40461  261 
apply (unfold prime_int_altdef) 
44821  262 
apply (metis int_one_le_iff_zero_less less_le) 
44872  263 
done 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

264 

44872  265 
lemma primes_imp_powers_coprime_nat: 
266 
"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

267 
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

268 

44872  269 
lemma primes_imp_powers_coprime_int: 
270 
"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

271 
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

272 

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

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

44872  276 
using two_is_prime_nat 
277 
apply blast 

278 
apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat 

279 
nat_dvd_not_less neq0_conv prime_nat_def) 

280 
done 

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

281 

31706  282 
(* An Isar version: 
283 

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

284 
lemma prime_factor_b_nat: 
31706  285 
fixes n :: nat 
286 
assumes "n \<noteq> 1" 

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

23983  288 

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

290 
proof (induct n rule: less_induct_nat) 
31706  291 
fix n :: nat 
292 
assume "n ~= 1" and 

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

44872  294 
then show "\<exists>p. prime p \<and> p dvd n" 
31706  295 
proof  
296 
{ 

297 
assume "n = 0" 

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

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

300 
by (auto simp del: two_is_prime_nat) 
31706  301 
} 
302 
moreover 

303 
{ 

304 
assume "prime n" 

44872  305 
then have ?thesis by auto 
31706  306 
} 
307 
moreover 

308 
{ 

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

310 
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

311 
with `~ prime n` and not_prime_eq_prod_nat obtain m k where 
31706  312 
"n = m * k" and "1 < m" and "m < n" by blast 
313 
with ih obtain p where "prime p" and "p dvd m" by blast 

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

315 
} 

316 
ultimately show ?thesis by blast 

317 
qed 

23983  318 
qed 
319 

31706  320 
*) 
321 

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

323 

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

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

327 
proof 

44872  328 
{ assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis 
31706  329 
apply (cases "n=0", simp_all) 
44872  330 
apply (cases "a=1", simp_all) 
331 
done } 

31706  332 
moreover 
44872  333 
{ assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1" 
334 
then obtain m where m: "n = Suc m" by (cases n) auto 

335 
from n have "p dvd p^n" apply (intro dvd_power) apply auto done 

31706  336 
also note pab 
337 
finally have pab': "p dvd a * b". 

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

338 
from prime_dvd_mult_nat[OF p pab'] 
31706  339 
have "p dvd a \<or> p dvd b" . 
340 
moreover 

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

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

344 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
44872  345 
then have pnb: "coprime (p^n) b" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

346 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  347 
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } 
31706  348 
moreover 
33946  349 
{ assume pb: "p dvd b" 
31706  350 
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

351 
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" 
31706  352 
by auto 
353 
with p have "coprime a p" 

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

354 
by (subst gcd_commute_nat, intro prime_imp_coprime_nat) 
44872  355 
then have pna: "coprime (p^n) a" 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31814
diff
changeset

356 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  357 
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } 
44872  358 
ultimately have ?thesis by blast } 
31706  359 
ultimately show ?thesis by blast 
23983  360 
qed 
361 

44872  362 

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

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

364 

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

365 
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

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

367 
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

368 
from prime_factor_nat [OF f1] 
44872  369 
obtain p where "prime p" and "p dvd fact n + 1" by auto 
370 
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done 

371 
{ assume "p \<le> n" 

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

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

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

374 
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

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

376 
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

377 
by (rule dvd_diff_nat) 
44872  378 
then have "p dvd 1" by simp 
379 
then have "p <= 1" by auto 

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

380 
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

381 
ultimately have False by auto} 
44872  382 
then have "n < p" by presburger 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

383 
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

384 
qed 
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 bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
44872  387 
using next_prime_bound by auto 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

388 

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

389 
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

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

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

392 
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

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

394 
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

395 
by auto 
44872  396 
with bigger_prime [of b] show False 
397 
by auto 

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

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

399 

21256  400 
end 