author  paulson <lp15@cam.ac.uk> 
Sat, 01 Feb 2014 20:38:29 +0000  
changeset 55238  7ddb889e23bd 
parent 55215  b6c926e67350 
child 55242  413ec965f95d 
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 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

34 
declare One_nat_def [simp] 
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

35 

31706  36 
class prime = one + 
44872  37 
fixes prime :: "'a \<Rightarrow> bool" 
31706  38 

39 
instantiation nat :: prime 

40 
begin 

21256  41 

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

31706  44 

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

46 

31706  47 
end 
48 

49 
instantiation int :: prime 

50 
begin 

51 

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

31706  54 

44872  55 
instance .. 
31706  56 

57 
end 

58 

59 

60 
subsection {* Set up Transfer *} 

61 

32479  62 
lemma transfer_nat_int_prime: 
31706  63 
"(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x" 
44872  64 
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

65 

35644  66 
declare transfer_morphism_nat_int[transfer add return: 
32479  67 
transfer_nat_int_prime] 
31706  68 

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

31706  71 

35644  72 
declare transfer_morphism_int_nat[transfer add return: 
32479  73 
transfer_int_nat_prime] 
31798  74 

21256  75 

32479  76 
subsection {* Primes *} 
31706  77 

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

78 
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p" 
54228  79 
apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0) 
80 
apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral) 

81 
done 

31706  82 

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

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

85 
apply (frule prime_odd_nat) 
31706  86 
apply (auto simp add: even_nat_def) 
44872  87 
done 
31706  88 

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

90 

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

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

93 

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

94 
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0" 
44872  95 
unfolding prime_nat_def by auto 
22367  96 

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

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

99 

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

100 
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1" 
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_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0" 
44872  104 
unfolding prime_nat_def by auto 
22367  105 

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

106 
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0" 
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_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2" 
44872  110 
unfolding prime_nat_def by auto 
31706  111 

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

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

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

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

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

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

120 

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

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

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

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

31706  127 

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

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

130 
using prime_nat_def [transferred] 

44872  131 
apply (cases "p >= 0") 
132 
apply blast 

133 
apply (auto simp add: prime_ge_0_int) 

134 
done 

31706  135 

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

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

138 
apply (metis gcd_dvd1_nat gcd_dvd2_nat) 
31706  139 
done 
140 

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

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

143 
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

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

145 

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

146 
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

147 
by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat) 
31706  148 

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

149 
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

150 
by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int) 
31706  151 

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

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

154 
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

155 

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

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

158 
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

159 

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

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

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

165 

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

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

169 
apply auto 

44872  170 
by (metis div_mult_self1_is_id div_mult_self2_is_id 
171 
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

172 

53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

173 
lemma prime_dvd_power_nat: "prime (p::nat) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

174 
by (induct n) auto 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

175 

53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

176 
lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

177 
by (induct n) (auto simp: prime_ge_0_int) 
31706  178 

53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

179 
lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow> 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

180 
p dvd x^n \<longleftrightarrow> p dvd x" 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

181 
by (cases n) (auto elim: prime_dvd_power_nat) 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

182 

2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

183 
lemma prime_dvd_power_int_iff: "prime (p::int) \<Longrightarrow> n > 0 \<Longrightarrow> 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

184 
p dvd x^n \<longleftrightarrow> p dvd x" 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

185 
by (cases n) (auto elim: prime_dvd_power_int) 
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

186 

2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset

187 

44872  188 
subsubsection {* Make prime naively executable *} 
32007  189 

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

191 
by (simp add: prime_nat_def) 

192 

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

194 
by (simp add: prime_int_def) 

195 

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

197 
by (simp add: prime_nat_def) 

198 

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

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

200 
by (simp add: prime_nat_def) 
32007  201 

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

203 
by (simp add: prime_int_def) 

204 

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

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

208 
apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat) 
44872  209 
done 
32007  210 

211 
lemma prime_nat_simp: 

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

32007  214 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset

215 
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m 
32007  216 

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

32007  219 
proof 
44872  220 
assume "?L" 
221 
then show "?R" 

44821  222 
by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le) 
32007  223 
next 
44872  224 
assume "?R" 
225 
then show "?L" by (clarsimp simp: Ball_def) (metis dvdI not_prime_eq_prod_int) 

32007  226 
qed 
227 

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

32007  230 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset

231 
lemmas prime_int_simp_numeral [simp] = prime_int_simp [of "numeral m"] for m 
32007  232 

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

44872  234 
by simp 
32007  235 

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

44872  237 
by simp 
32007  238 

32111  239 
text{* A bit of regression testing: *} 
240 

44872  241 
lemma "prime(97::nat)" by simp 
242 
lemma "prime(97::int)" by simp 

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

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

32111  245 

32007  246 

247 
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" 

55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

248 
by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

249 

32007  250 
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

251 
by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int) 
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" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

254 
by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

255 

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

256 
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q" 
55130
70db8d380d62
Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents:
54228
diff
changeset

257 
by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef) 
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset

258 

44872  259 
lemma primes_imp_powers_coprime_nat: 
260 
"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

261 
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

262 

44872  263 
lemma primes_imp_powers_coprime_int: 
264 
"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

265 
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

266 

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

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

44872  270 
using two_is_prime_nat 
271 
apply blast 

272 
apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat 

273 
nat_dvd_not_less neq0_conv prime_nat_def) 

274 
done 

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

275 

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

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

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

281 
proof 

44872  282 
{ assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis 
31706  283 
apply (cases "n=0", simp_all) 
44872  284 
apply (cases "a=1", simp_all) 
285 
done } 

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

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

31706  290 
also note pab 
291 
finally have pab': "p dvd a * b". 

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

292 
from prime_dvd_mult_nat[OF p pab'] 
31706  293 
have "p dvd a \<or> p dvd b" . 
294 
moreover 

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

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

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

300 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  301 
from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast } 
31706  302 
moreover 
33946  303 
{ assume pb: "p dvd b" 
31706  304 
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

305 
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a" 
31706  306 
by auto 
307 
with p have "coprime a p" 

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

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

310 
by (subst gcd_commute_nat, rule coprime_exp_nat) 
33946  311 
from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast } 
44872  312 
ultimately have ?thesis by blast } 
31706  313 
ultimately show ?thesis by blast 
23983  314 
qed 
315 

44872  316 

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

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

318 

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

319 
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

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

321 
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

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

325 
{ assume "p \<le> n" 

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

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

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

328 
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

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

330 
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

331 
by (rule dvd_diff_nat) 
44872  332 
then have "p dvd 1" by simp 
333 
then have "p <= 1" by auto 

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

334 
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

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

337 
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

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

339 

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

340 
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
44872  341 
using next_prime_bound by auto 
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset

342 

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

343 
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

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

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

346 
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

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

348 
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

349 
by auto 
44872  350 
with bigger_prime [of b] show False 
351 
by auto 

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

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

353 

55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

354 
subsection{*Powers of Primes*} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

355 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

356 
text{*Versions for type nat only*} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

357 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

358 
lemma prime_product: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

359 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

360 
assumes "prime (p * q)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

361 
shows "p = 1 \<or> q = 1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

362 
proof  
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

363 
from assms have 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

364 
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

365 
unfolding prime_nat_def by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

366 
from `1 < p * q` have "p \<noteq> 0" by (cases p) auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

367 
then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

368 
have "p dvd p * q" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

369 
then have "p = 1 \<or> p = p * q" by (rule P) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

370 
then show ?thesis by (simp add: Q) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

371 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

372 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

373 
lemma prime_exp: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

374 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

375 
shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

376 
proof(induct n) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

377 
case 0 thus ?case by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

378 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

379 
case (Suc n) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

380 
{assume "p = 0" hence ?case by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

381 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

382 
{assume "p=1" hence ?case by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

383 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

384 
{assume p: "p \<noteq> 0" "p\<noteq>1" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

385 
{assume pp: "prime (p^Suc n)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

386 
hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

387 
with p have n: "n = 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

388 
by (metis One_nat_def nat_power_eq_Suc_0_iff) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

389 
with pp have "prime p \<and> Suc n = 1" by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

390 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

391 
{assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

392 
ultimately have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

393 
ultimately show ?case by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

394 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

395 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

396 
lemma prime_power_mult: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

397 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

398 
assumes p: "prime p" and xy: "x * y = p ^ k" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

399 
shows "\<exists>i j. x = p ^i \<and> y = p^ j" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

400 
using xy 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

401 
proof(induct k arbitrary: x y) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

402 
case 0 thus ?case apply simp by (rule exI[where x="0"], simp) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

403 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

404 
case (Suc k x y) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

405 
from Suc.prems have pxy: "p dvd x*y" by auto 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

406 
from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" . 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

407 
from p have p0: "p \<noteq> 0" by  (rule ccontr, simp) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

408 
{assume px: "p dvd x" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

409 
then obtain d where d: "x = p*d" unfolding dvd_def by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

410 
from Suc.prems d have "p*d*y = p^Suc k" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

411 
hence th: "d*y = p^k" using p0 by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

412 
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

413 
with d have "x = p^Suc i" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

414 
with ij(2) have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

415 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

416 
{assume px: "p dvd y" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

417 
then obtain d where d: "y = p*d" unfolding dvd_def by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

418 
from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult_commute) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

419 
hence th: "d*x = p^k" using p0 by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

420 
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

421 
with d have "y = p^Suc i" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

422 
with ij(2) have ?case by blast} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

423 
ultimately show ?case using pxyc by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

424 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

425 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

426 
lemma prime_power_exp: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

427 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

428 
assumes p: "prime p" and n: "n \<noteq> 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

429 
and xn: "x^n = p^k" shows "\<exists>i. x = p^i" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

430 
using n xn 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

431 
proof(induct n arbitrary: k) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

432 
case 0 thus ?case by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

433 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

434 
case (Suc n k) hence th: "x*x^n = p^k" by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

435 
{assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

436 
moreover 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

437 
{assume n: "n \<noteq> 0" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

438 
from prime_power_mult[OF p th] 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

439 
obtain i j where ij: "x = p^i" "x^n = p^j"by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

440 
from Suc.hyps[OF n ij(2)] have ?case .} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

441 
ultimately show ?case by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

442 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

443 

b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

444 
lemma divides_primepow: 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

445 
fixes p::nat 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

446 
assumes p: "prime p" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

447 
shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

448 
proof 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

449 
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

450 
unfolding dvd_def apply (auto simp add: mult_commute) by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

451 
from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

452 
from e ij have "p^(i + j) = p^k" by (simp add: power_add) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

453 
hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

454 
hence "i \<le> k" by arith 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

455 
with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

456 
next 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

457 
{fix i assume H: "i \<le> k" "d = p^i" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

458 
then obtain j where j: "k = i + j" 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

459 
by (metis le_add_diff_inverse) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

460 
hence "p^k = p^j*d" using H(2) by (simp add: power_add) 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

461 
hence "d dvd p^k" unfolding dvd_def by auto} 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

462 
thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

463 
qed 
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset

464 

55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

465 
subsection {*Chinese Remainder Theorem Variants*} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

466 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

467 
lemma bezout_gcd_nat: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

468 
fixes a::nat shows "\<exists>x y. a * x  b * y = gcd a b \<or> b * x  a * y = gcd a b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

469 
using bezout_nat[of a b] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

470 
by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

471 
gcd_nat.right_neutral mult_0) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

472 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

473 
lemma gcd_bezout_sum_nat: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

474 
fixes a::nat 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

475 
assumes "a * x + b * y = d" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

476 
shows "gcd a b dvd d" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

477 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

478 
let ?g = "gcd a b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

479 
have dv: "?g dvd a*x" "?g dvd b * y" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

480 
by simp_all 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

481 
from dvd_add[OF dv] assms 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

482 
show ?thesis by auto 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

483 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

484 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

485 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

486 
text {* A binary form of the Chinese Remainder Theorem. *} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

487 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

488 
lemma chinese_remainder: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

489 
fixes a::nat assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

490 
shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

491 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

492 
from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

493 
obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

494 
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

495 
then have d12: "d1 = 1" "d2 =1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

496 
by (metis ab coprime_nat)+ 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

497 
let ?x = "v * a * x1 + u * b * x2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

498 
let ?q1 = "v * x1 + u * y2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

499 
let ?q2 = "v * y1 + u * x2" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

500 
from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

501 
have "?x = u + ?q1 * a" "?x = v + ?q2 * b" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

502 
apply (auto simp add: algebra_simps) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

503 
apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+ 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

504 
done 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

505 
thus ?thesis by blast 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

506 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

507 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

508 
text {* Primality *} 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

509 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

510 
lemma coprime_bezout_strong: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

511 
fixes a::nat assumes "coprime a b" "b \<noteq> 1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

512 
shows "\<exists>x y. a * x = b * y + 1" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

513 
by (metis assms bezout_nat gcd_nat.left_neutral) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

514 

7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

515 
lemma bezout_prime: 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

516 
assumes p: "prime p" and pa: "\<not> p dvd a" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

517 
shows "\<exists>x y. a*x = Suc (p*y)" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

518 
proof 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

519 
have ap: "coprime a p" 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

520 
by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

521 
from coprime_bezout_strong[OF ap] show ?thesis 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

522 
by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

523 
qed 
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset

524 

21256  525 
end 