author | Manuel Eberl <eberlm@in.tum.de> |
Mon, 04 Jan 2021 19:41:38 +0100 | |
changeset 73047 | ab9e27da0e85 |
parent 69597 | ff784d5a5bfb |
child 73270 | e2d03448d5b5 |
permissions | -rw-r--r-- |
65435 | 1 |
(* Title: HOL/Computational_Algebra/Primes.thy |
2 |
Author: Christophe Tabacznyj |
|
3 |
Author: Lawrence C. Paulson |
|
4 |
Author: Amine Chaieb |
|
5 |
Author: Thomas M. Rasmussen |
|
6 |
Author: Jeremy Avigad |
|
7 |
Author: Tobias Nipkow |
|
8 |
Author: Manuel Eberl |
|
31706 | 9 |
|
65435 | 10 |
This theory deals with properties of primes. Definitions and lemmas are |
32479 | 11 |
proved uniformly for the natural numbers and integers. |
31706 | 12 |
|
13 |
This file combines and revises a number of prior developments. |
|
14 |
||
15 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
58623 | 16 |
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced |
31706 | 17 |
gcd, lcm, and prime for the natural numbers. |
18 |
||
19 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
20 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
21 |
another extension of the notions to the integers, and added a number |
|
22 |
of results to "Primes" and "GCD". IntPrimes also defined and developed |
|
23 |
the congruence relations on the integers. The notion was extended to |
|
33718 | 24 |
the natural numbers by Chaieb. |
31706 | 25 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
26 |
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
|
27 |
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
|
28 |
|
31798 | 29 |
Tobias Nipkow cleaned up a lot. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
30 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
31 |
Florian Haftmann and Manuel Eberl put primality and prime factorisation |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
32 |
onto an algebraic foundation and thus generalised these concepts to |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
33 |
other rings, such as polynomials. (see also the Factorial_Ring theory). |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
34 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
35 |
There were also previous formalisations of unique factorisation by |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
36 |
Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray. |
21256 | 37 |
*) |
38 |
||
60526 | 39 |
section \<open>Primes\<close> |
21256 | 40 |
|
32479 | 41 |
theory Primes |
68623 | 42 |
imports Euclidean_Algorithm |
31706 | 43 |
begin |
44 |
||
69597 | 45 |
subsection \<open>Primes on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> |
67117 | 46 |
|
47 |
lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)" |
|
48 |
using not_prime_1 [where ?'a = nat] by simp |
|
49 |
||
50 |
lemma prime_ge_2_nat: |
|
51 |
"p \<ge> 2" if "prime p" for p :: nat |
|
52 |
proof - |
|
53 |
from that have "p \<noteq> 0" and "p \<noteq> 1" |
|
54 |
by (auto dest: prime_elem_not_zeroI prime_elem_not_unit) |
|
55 |
then show ?thesis |
|
56 |
by simp |
|
57 |
qed |
|
58 |
||
59 |
lemma prime_ge_2_int: |
|
60 |
"p \<ge> 2" if "prime p" for p :: int |
|
61 |
proof - |
|
62 |
from that have "prime_elem p" and "\<bar>p\<bar> = p" |
|
63 |
by (auto dest: normalize_prime) |
|
64 |
then have "p \<noteq> 0" and "\<bar>p\<bar> \<noteq> 1" and "p \<ge> 0" |
|
65 |
by (auto dest: prime_elem_not_zeroI prime_elem_not_unit) |
|
66 |
then show ?thesis |
|
67 |
by simp |
|
68 |
qed |
|
69 |
||
70 |
lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)" |
|
71 |
using prime_ge_2_int [of p] by simp |
|
72 |
||
73 |
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)" |
|
74 |
using prime_ge_2_nat [of p] by simp |
|
75 |
||
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
76 |
(* As a simp or intro rule, |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
77 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
78 |
prime p \<Longrightarrow> p > 0 |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
79 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
80 |
wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
81 |
leads to the backchaining |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
82 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
83 |
x > 0 |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
84 |
prime x |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
85 |
x \<in># M which is, unfortunately, |
67117 | 86 |
count M x > 0 FIXME no, this is obsolete |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
87 |
*) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
88 |
|
67117 | 89 |
lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)" |
90 |
using prime_ge_2_int [of p] by simp |
|
91 |
||
92 |
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)" |
|
93 |
using prime_ge_2_nat [of p] by simp |
|
94 |
||
95 |
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0" |
|
96 |
using prime_ge_1_nat [of p] by simp |
|
97 |
||
98 |
lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)" |
|
99 |
using prime_ge_2_int [of p] by simp |
|
31706 | 100 |
|
67117 | 101 |
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)" |
102 |
using prime_ge_2_nat [of p] by simp |
|
103 |
||
104 |
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0" |
|
105 |
using prime_gt_1_nat [of p] by simp |
|
106 |
||
107 |
lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)" |
|
108 |
using prime_ge_2_int [of p] by simp |
|
109 |
||
110 |
lemma prime_natI: |
|
111 |
"prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: nat |
|
112 |
using that by (auto intro!: primeI prime_elemI) |
|
113 |
||
114 |
lemma prime_intI: |
|
115 |
"prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: int |
|
116 |
using that by (auto intro!: primeI prime_elemI) |
|
66837 | 117 |
|
67118 | 118 |
lemma prime_elem_nat_iff [simp]: |
67117 | 119 |
"prime_elem n \<longleftrightarrow> prime n" for n :: nat |
120 |
by (simp add: prime_def) |
|
121 |
||
67118 | 122 |
lemma prime_elem_iff_prime_abs [simp]: |
67117 | 123 |
"prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int |
124 |
by (auto intro: primeI) |
|
125 |
||
126 |
lemma prime_nat_int_transfer [simp]: |
|
127 |
"prime (int n) \<longleftrightarrow> prime n" (is "?P \<longleftrightarrow> ?Q") |
|
128 |
proof |
|
129 |
assume ?P |
|
130 |
then have "n \<ge> 2" |
|
131 |
by (auto dest: prime_ge_2_int) |
|
132 |
then show ?Q |
|
133 |
proof (rule prime_natI) |
|
134 |
fix r s |
|
135 |
assume "n dvd r * s" |
|
67118 | 136 |
with of_nat_dvd_iff [of n "r * s"] have "int n dvd int r * int s" |
67117 | 137 |
by simp |
138 |
with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s" |
|
67118 | 139 |
using prime_dvd_mult_iff [of "int n" "int r" "int s"] |
140 |
by simp |
|
67117 | 141 |
then show "n dvd r \<or> n dvd s" |
67118 | 142 |
by simp |
67117 | 143 |
qed |
144 |
next |
|
145 |
assume ?Q |
|
146 |
then have "int n \<ge> 2" |
|
147 |
by (auto dest: prime_ge_2_nat) |
|
148 |
then show ?P |
|
149 |
proof (rule prime_intI) |
|
150 |
fix r s |
|
151 |
assume "int n dvd r * s" |
|
152 |
then have "n dvd nat \<bar>r * s\<bar>" |
|
67118 | 153 |
by simp |
67117 | 154 |
then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>" |
155 |
by (simp add: nat_abs_mult_distrib) |
|
156 |
with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>" |
|
67118 | 157 |
using prime_dvd_mult_iff [of "n" "nat \<bar>r\<bar>" "nat \<bar>s\<bar>"] |
158 |
by simp |
|
67117 | 159 |
then show "int n dvd r \<or> int n dvd s" |
67118 | 160 |
by simp |
67117 | 161 |
qed |
162 |
qed |
|
163 |
||
67118 | 164 |
lemma prime_nat_iff_prime [simp]: |
67117 | 165 |
"prime (nat k) \<longleftrightarrow> prime k" |
166 |
proof (cases "k \<ge> 0") |
|
167 |
case True |
|
168 |
then show ?thesis |
|
169 |
using prime_nat_int_transfer [of "nat k"] by simp |
|
170 |
next |
|
171 |
case False |
|
172 |
then show ?thesis |
|
173 |
by (auto dest: prime_ge_2_int) |
|
174 |
qed |
|
175 |
||
176 |
lemma prime_int_nat_transfer: |
|
177 |
"prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)" |
|
67118 | 178 |
by (auto dest: prime_ge_2_int) |
67117 | 179 |
|
180 |
lemma prime_nat_naiveI: |
|
181 |
"prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat |
|
182 |
proof (rule primeI, rule prime_elemI) |
|
183 |
fix m n :: nat |
|
184 |
assume "p dvd m * n" |
|
185 |
then obtain r s where "p = r * s" "r dvd m" "s dvd n" |
|
186 |
by (blast dest: division_decomp) |
|
187 |
moreover have "r = 1 \<or> r = p" |
|
188 |
using \<open>r dvd m\<close> \<open>p = r * s\<close> dvd [of r] by simp |
|
189 |
ultimately show "p dvd m \<or> p dvd n" |
|
190 |
by auto |
|
191 |
qed (use \<open>p \<ge> 2\<close> in simp_all) |
|
192 |
||
193 |
lemma prime_int_naiveI: |
|
194 |
"prime p" if "p \<ge> 2" and dvd: "\<And>k. k dvd p \<Longrightarrow> \<bar>k\<bar> = 1 \<or> \<bar>k\<bar> = p" for p :: int |
|
195 |
proof - |
|
196 |
from \<open>p \<ge> 2\<close> have "nat p \<ge> 2" |
|
197 |
by simp |
|
198 |
then have "prime (nat p)" |
|
199 |
proof (rule prime_nat_naiveI) |
|
200 |
fix n |
|
201 |
assume "n dvd nat p" |
|
202 |
with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>" |
|
203 |
by simp |
|
204 |
then have "int n dvd p" |
|
67118 | 205 |
by simp |
67117 | 206 |
with dvd [of "int n"] show "n = 1 \<or> n = nat p" |
207 |
by auto |
|
208 |
qed |
|
209 |
then show ?thesis |
|
67118 | 210 |
by simp |
67117 | 211 |
qed |
212 |
||
213 |
lemma prime_nat_iff: |
|
214 |
"prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))" |
|
215 |
proof (safe intro!: prime_gt_1_nat) |
|
216 |
assume "prime n" |
|
217 |
then have *: "prime_elem n" |
|
218 |
by simp |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
219 |
fix m assume m: "m dvd n" "m \<noteq> n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
220 |
from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m" |
63633 | 221 |
by (intro irreducibleD' prime_elem_imp_irreducible) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
222 |
with m show "m = 1" by (auto dest: dvd_antisym) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
223 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
224 |
assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n" |
67117 | 225 |
then show "prime n" |
226 |
using prime_nat_naiveI [of n] by auto |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
227 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
228 |
|
63633 | 229 |
lemma prime_int_iff: |
230 |
"prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))" |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
231 |
proof (intro iffI conjI allI impI; (elim conjE)?) |
63633 | 232 |
assume *: "prime n" |
67118 | 233 |
hence irred: "irreducible n" by (auto intro: prime_elem_imp_irreducible) |
234 |
from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" |
|
235 |
by (auto simp add: prime_ge_0_int) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
236 |
thus "n > 1" by presburger |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
237 |
fix m assume "m dvd n" \<open>m \<ge> 0\<close> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
238 |
with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
239 |
with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
240 |
using associated_iff_dvd[of m n] by auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
241 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
242 |
assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
243 |
hence "nat n > 1" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
244 |
moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
245 |
proof (intro allI impI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
246 |
fix m assume "m dvd nat n" |
67118 | 247 |
with \<open>n > 1\<close> have "m dvd nat \<bar>n\<bar>" |
248 |
by simp |
|
249 |
then have "int m dvd n" |
|
250 |
by simp |
|
65583
8d53b3bebab4
Further new material. The simprule status of some exp and ln identities was reverted.
paulson <lp15@cam.ac.uk>
parents:
65435
diff
changeset
|
251 |
with n(2) have "int m = 1 \<or> int m = n" |
8d53b3bebab4
Further new material. The simprule status of some exp and ln identities was reverted.
paulson <lp15@cam.ac.uk>
parents:
65435
diff
changeset
|
252 |
using of_nat_0_le_iff by blast |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
253 |
thus "m = 1 \<or> m = nat n" by auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
254 |
qed |
63633 | 255 |
ultimately show "prime n" |
256 |
unfolding prime_int_nat_transfer prime_nat_iff by auto |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
257 |
qed |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
258 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
259 |
lemma prime_nat_not_dvd: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
260 |
assumes "prime p" "p > n" "n \<noteq> (1::nat)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
261 |
shows "\<not>n dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
262 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
263 |
assume "n dvd p" |
63633 | 264 |
from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
265 |
from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
266 |
by (cases "n = 0") (auto dest!: dvd_imp_le) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
267 |
qed |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
268 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
269 |
lemma prime_int_not_dvd: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
270 |
assumes "prime p" "p > n" "n > (1::int)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
271 |
shows "\<not>n dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
272 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
273 |
assume "n dvd p" |
67118 | 274 |
from assms(1) have "irreducible p" by (auto intro: prime_elem_imp_irreducible) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
275 |
from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
276 |
by (auto dest!: zdvd_imp_le) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
277 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
278 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
279 |
lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
280 |
by (intro prime_nat_not_dvd) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
281 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
282 |
lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
283 |
by (intro prime_int_not_dvd) auto |
22367 | 284 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
285 |
lemma prime_int_altdef: |
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset
|
286 |
"prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow> |
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55238
diff
changeset
|
287 |
m = 1 \<or> m = p))" |
63633 | 288 |
unfolding prime_int_iff by blast |
27568
9949dc7a24de
Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents:
27556
diff
changeset
|
289 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62429
diff
changeset
|
290 |
lemma not_prime_eq_prod_nat: |
67118 | 291 |
assumes "m > 1" "\<not> prime (m::nat)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
292 |
shows "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
293 |
using assms irreducible_altdef[of m] |
67118 | 294 |
by (auto simp: prime_elem_iff_irreducible irreducible_altdef) |
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset
|
295 |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
296 |
|
67117 | 297 |
subsection \<open>Largest exponent of a prime factor\<close> |
298 |
||
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
299 |
text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
300 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
301 |
lemma prime_power_cancel_less: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
302 |
assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
303 |
shows False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
304 |
proof - |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
305 |
obtain l where l: "k' = k + l" and "l > 0" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
306 |
using less less_imp_add_positive by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
307 |
have "m = m * (p ^ k) div (p ^ k)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
308 |
using \<open>prime p\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
309 |
also have "\<dots> = m' * (p ^ k') div (p ^ k)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
310 |
using eq by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
311 |
also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
312 |
by (simp add: l mult.commute mult.left_commute power_add) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
313 |
also have "... = m' * (p ^ l)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
314 |
using \<open>prime p\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
315 |
finally have "p dvd m" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
316 |
using \<open>l > 0\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
317 |
with assms show False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
318 |
by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
319 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
320 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
321 |
lemma prime_power_cancel: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
322 |
assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
323 |
shows "k = k'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
324 |
using prime_power_cancel_less [OF \<open>prime p\<close>] assms |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
325 |
by (metis linorder_neqE_nat) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
326 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
327 |
lemma prime_power_cancel2: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
328 |
assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
329 |
obtains "m = m'" "k = k'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
330 |
using prime_power_cancel [OF assms] assms by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
331 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
332 |
lemma prime_power_canonical: |
67051 | 333 |
fixes m :: nat |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
334 |
assumes "prime p" "m > 0" |
67051 | 335 |
shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k" |
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
336 |
using \<open>m > 0\<close> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
337 |
proof (induction m rule: less_induct) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
338 |
case (less m) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
339 |
show ?case |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
340 |
proof (cases "p dvd m") |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
341 |
case True |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
342 |
then obtain m' where m': "m = p * m'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
343 |
using dvdE by blast |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
344 |
with \<open>prime p\<close> have "0 < m'" "m' < m" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
345 |
using less.prems prime_nat_iff by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
346 |
with m' less show ?thesis |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
347 |
by (metis power_Suc mult.left_commute) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
348 |
next |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
349 |
case False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
350 |
then show ?thesis |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
351 |
by (metis mult.right_neutral power_0) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
352 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
353 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
354 |
|
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset
|
355 |
|
60526 | 356 |
subsubsection \<open>Make prime naively executable\<close> |
32007 | 357 |
|
63633 | 358 |
lemma prime_nat_iff': |
67091 | 359 |
"prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
360 |
proof safe |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
361 |
assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p" |
63633 | 362 |
show "prime p" unfolding prime_nat_iff |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
363 |
proof (intro conjI allI impI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
364 |
fix m assume "m dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
365 |
with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
366 |
hence "m \<ge> 1" by simp |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
367 |
moreover from \<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
368 |
with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
369 |
ultimately show "m = 1 \<or> m = p" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
370 |
qed fact+ |
63633 | 371 |
qed (auto simp: prime_nat_iff) |
32007 | 372 |
|
63633 | 373 |
lemma prime_int_iff': |
67118 | 374 |
"prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q") |
375 |
proof (cases "p \<ge> 0") |
|
376 |
case True |
|
377 |
have "?P \<longleftrightarrow> prime (nat p)" |
|
378 |
by simp |
|
379 |
also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)" |
|
380 |
using True by (simp add: prime_nat_iff') |
|
381 |
also have "{2..<nat p} = nat ` {2..<p}" |
|
382 |
using True int_eq_iff by fastforce |
|
383 |
finally show "?P \<longleftrightarrow> ?Q" by simp |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
384 |
next |
67118 | 385 |
case False |
386 |
then show ?thesis |
|
387 |
by (auto simp add: prime_ge_0_int) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
388 |
qed |
32007 | 389 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
390 |
lemma prime_int_numeral_eq [simp]: |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
391 |
"prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)" |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
392 |
by (simp add: prime_int_nat_transfer) |
32007 | 393 |
|
63635 | 394 |
lemma two_is_prime_nat [simp]: "prime (2::nat)" |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
395 |
by (simp add: prime_nat_iff') |
32007 | 396 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
397 |
lemma prime_nat_numeral_eq [simp]: |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
398 |
"prime (numeral m :: nat) \<longleftrightarrow> |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
399 |
(1::nat) < numeral m \<and> |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
400 |
(\<forall>n::nat \<in> set [2..<numeral m]. \<not> n dvd numeral m)" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
401 |
by (simp only: prime_nat_iff' set_upt) \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close> |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
402 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
403 |
|
60526 | 404 |
text\<open>A bit of regression testing:\<close> |
32111 | 405 |
|
58954
18750e86d5b8
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
haftmann
parents:
58898
diff
changeset
|
406 |
lemma "prime(97::nat)" by simp |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
407 |
lemma "prime(97::int)" by simp |
31706 | 408 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
409 |
lemma prime_factor_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
410 |
"n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
411 |
using prime_divisor_exists[of n] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
412 |
by (cases "n = 0") (auto intro: exI[of _ "2::nat"]) |
23983 | 413 |
|
67118 | 414 |
lemma prime_factor_int: |
415 |
fixes k :: int |
|
416 |
assumes "\<bar>k\<bar> \<noteq> 1" |
|
417 |
obtains p where "prime p" "p dvd k" |
|
418 |
proof (cases "k = 0") |
|
419 |
case True |
|
420 |
then have "prime (2::int)" and "2 dvd k" |
|
421 |
by simp_all |
|
422 |
with that show thesis |
|
423 |
by blast |
|
424 |
next |
|
425 |
case False |
|
426 |
with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k" |
|
427 |
by auto |
|
428 |
with that show thesis |
|
429 |
by blast |
|
430 |
qed |
|
431 |
||
44872 | 432 |
|
60526 | 433 |
subsection \<open>Infinitely many primes\<close> |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
434 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
435 |
lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
436 |
proof- |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset
|
437 |
have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
438 |
from prime_factor_nat [OF f1] |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
439 |
obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto |
44872 | 440 |
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done |
441 |
{ assume "p \<le> n" |
|
60526 | 442 |
from \<open>prime p\<close> have "p \<ge> 1" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
443 |
by (cases p, simp_all) |
60526 | 444 |
with \<open>p <= n\<close> have "p dvd fact n" |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset
|
445 |
by (intro dvd_fact) |
60526 | 446 |
with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
447 |
by (rule dvd_diff_nat) |
44872 | 448 |
then have "p dvd 1" by simp |
449 |
then have "p <= 1" by auto |
|
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
60804
diff
changeset
|
450 |
moreover from \<open>prime p\<close> have "p > 1" |
63633 | 451 |
using prime_nat_iff by blast |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
452 |
ultimately have False by auto} |
44872 | 453 |
then have "n < p" by presburger |
60526 | 454 |
with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
455 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
456 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
457 |
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" |
44872 | 458 |
using next_prime_bound by auto |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
459 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
460 |
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
|
461 |
proof |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
462 |
assume "finite {(p::nat). prime p}" |
67091 | 463 |
with Max_ge have "(\<exists>b. (\<forall>x \<in> {(p::nat). prime p}. x \<le> b))" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
464 |
by auto |
67091 | 465 |
then obtain b where "\<forall>(x::nat). prime x \<longrightarrow> x \<le> b" |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
466 |
by auto |
44872 | 467 |
with bigger_prime [of b] show False |
468 |
by auto |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
469 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
470 |
|
67117 | 471 |
subsection \<open>Powers of Primes\<close> |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
472 |
|
60526 | 473 |
text\<open>Versions for type nat only\<close> |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
474 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
475 |
lemma prime_product: |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
476 |
fixes p::nat |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
477 |
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
|
478 |
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
|
479 |
proof - |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
480 |
from assms have |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
481 |
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q" |
63633 | 482 |
unfolding prime_nat_iff by auto |
60526 | 483 |
from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
484 |
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
|
485 |
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
|
486 |
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
|
487 |
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
|
488 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
489 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
490 |
(* TODO: Generalise? *) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
491 |
lemma prime_power_mult_nat: |
67051 | 492 |
fixes p :: nat |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
493 |
assumes p: "prime p" and xy: "x * y = p ^ k" |
67051 | 494 |
shows "\<exists>i j. x = p ^ i \<and> y = p^ j" |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
495 |
using xy |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
496 |
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
|
497 |
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
|
498 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
499 |
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
|
500 |
from Suc.prems have pxy: "p dvd x*y" by auto |
63633 | 501 |
from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" . |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
502 |
from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
503 |
{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
|
504 |
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
|
505 |
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
|
506 |
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
|
507 |
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
508 |
with d have "x = p^Suc i" by simp |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
509 |
with ij(2) have ?case by blast} |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
510 |
moreover |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
511 |
{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
|
512 |
then obtain d where d: "y = p*d" unfolding dvd_def by blast |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset
|
513 |
from Suc.prems d have "p*d*x = p^Suc k" by (simp add: mult.commute) |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
514 |
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
|
515 |
from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
516 |
with d have "y = p^Suc i" by simp |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
517 |
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
|
518 |
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
|
519 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
520 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
521 |
lemma prime_power_exp_nat: |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
522 |
fixes p::nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
523 |
assumes p: "prime p" and n: "n \<noteq> 0" |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
524 |
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
|
525 |
using n xn |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
526 |
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
|
527 |
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
|
528 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
529 |
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
|
530 |
{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
|
531 |
moreover |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
532 |
{assume n: "n \<noteq> 0" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
533 |
from prime_power_mult_nat[OF p th] |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
534 |
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
|
535 |
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
|
536 |
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
|
537 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
538 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
539 |
lemma divides_primepow_nat: |
67051 | 540 |
fixes p :: nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
541 |
assumes p: "prime p" |
67051 | 542 |
shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)" |
543 |
using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd) |
|
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
544 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
545 |
|
60526 | 546 |
subsection \<open>Chinese Remainder Theorem Variants\<close> |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
547 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
548 |
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
|
549 |
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
|
550 |
using bezout_nat[of a b] |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62410
diff
changeset
|
551 |
by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
552 |
gcd_nat.right_neutral mult_0) |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
553 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
554 |
lemma gcd_bezout_sum_nat: |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
555 |
fixes a::nat |
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
556 |
assumes "a * x + b * y = d" |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
557 |
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
|
558 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
559 |
let ?g = "gcd a b" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
560 |
have dv: "?g dvd a*x" "?g dvd b * y" |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
561 |
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
|
562 |
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
|
563 |
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
|
564 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
565 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
566 |
|
60526 | 567 |
text \<open>A binary form of the Chinese Remainder Theorem.\<close> |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
568 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
569 |
(* TODO: Generalise? *) |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
570 |
lemma chinese_remainder: |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
571 |
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
|
572 |
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
|
573 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
574 |
from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a] |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
575 |
obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
576 |
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast |
67051 | 577 |
then have d12: "d1 = 1" "d2 = 1" |
578 |
using ab coprime_common_divisor_nat [of a b] by blast+ |
|
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
579 |
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
|
580 |
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
|
581 |
let ?q2 = "v * y1 + u * x2" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
582 |
from dxy2(3)[simplified d12] dxy1(3)[simplified d12] |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
583 |
have "?x = u + ?q1 * a" "?x = v + ?q2 * b" |
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
584 |
by algebra+ |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
585 |
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
|
586 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
587 |
|
60526 | 588 |
text \<open>Primality\<close> |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
589 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
590 |
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
|
591 |
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
|
592 |
shows "\<exists>x y. a * x = b * y + 1" |
67051 | 593 |
by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left) |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
594 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
595 |
lemma bezout_prime: |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
596 |
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
|
597 |
shows "\<exists>x y. a*x = Suc (p*y)" |
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
598 |
proof - |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
599 |
have ap: "coprime a p" |
67051 | 600 |
using coprime_commute p pa prime_imp_coprime by auto |
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
601 |
moreover from p have "p \<noteq> 1" by auto |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
602 |
ultimately have "\<exists>x y. a * x = p * y + 1" |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
603 |
by (rule coprime_bezout_strong) |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
604 |
then show ?thesis by simp |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
605 |
qed |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
606 |
(* END TODO *) |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
607 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
608 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
609 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
610 |
subsection \<open>Multiplicity and primality for natural numbers and integers\<close> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
611 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
612 |
lemma prime_factors_gt_0_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
613 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::nat)" |
63905 | 614 |
by (simp add: in_prime_factors_imp_prime prime_gt_0_nat) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
615 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
616 |
lemma prime_factors_gt_0_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
617 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::int)" |
63905 | 618 |
by (simp add: in_prime_factors_imp_prime prime_gt_0_int) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
619 |
|
63905 | 620 |
lemma prime_factors_ge_0_int [elim]: (* FIXME !? *) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
621 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
622 |
shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0" |
63905 | 623 |
by (drule prime_factors_gt_0_int) simp |
624 |
||
63830 | 625 |
lemma prod_mset_prime_factorization_int: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
626 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
627 |
assumes "n > 0" |
63830 | 628 |
shows "prod_mset (prime_factorization n) = n" |
629 |
using assms by (simp add: prod_mset_prime_factorization) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
630 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
631 |
lemma prime_factorization_exists_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
632 |
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))" |
67118 | 633 |
using prime_factorization_exists[of n] by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
634 |
|
63830 | 635 |
lemma prod_mset_prime_factorization_nat [simp]: |
636 |
"(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n" |
|
637 |
by (subst prod_mset_prime_factorization) simp_all |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
638 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
639 |
lemma prime_factorization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
640 |
"n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 641 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
642 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
643 |
lemma prime_factorization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
644 |
"n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 645 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
646 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
647 |
lemma prime_factorization_unique_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
648 |
fixes f :: "nat \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
649 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
650 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
651 |
and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 652 |
shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
653 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
654 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
655 |
lemma prime_factorization_unique_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
656 |
fixes f :: "int \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
657 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
658 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
659 |
and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 660 |
shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
661 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
662 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
663 |
lemma prime_factors_characterization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
664 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
665 |
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
666 |
by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric]) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
667 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
668 |
lemma prime_factors_characterization'_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
669 |
"finite {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
670 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
671 |
prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
672 |
by (rule prime_factors_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
673 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
674 |
lemma prime_factors_characterization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
675 |
"S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
676 |
\<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
677 |
by (rule prime_factorization_unique_int [THEN conjunct1, symmetric]) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
678 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
679 |
(* TODO Move *) |
64272 | 680 |
lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
681 |
by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
682 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
683 |
lemma primes_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
684 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
685 |
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}" |
64272 | 686 |
by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
687 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
688 |
lemma multiplicity_characterization_nat: |
63633 | 689 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
690 |
n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
691 |
by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
692 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
693 |
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> |
63633 | 694 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow> |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
695 |
multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
696 |
by (intro impI, rule multiplicity_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
697 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
698 |
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
63633 | 699 |
finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
700 |
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) |
64272 | 701 |
(auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
702 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
703 |
lemma multiplicity_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
704 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> |
63633 | 705 |
(\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow> |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
706 |
multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
707 |
by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
708 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
709 |
lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
710 |
unfolding One_nat_def [symmetric] by (rule multiplicity_one) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
711 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
712 |
lemma multiplicity_eq_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
713 |
fixes x and y::nat |
63633 | 714 |
assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
715 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
716 |
using multiplicity_eq_imp_eq[of x y] assms by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
717 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
718 |
lemma multiplicity_eq_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
719 |
fixes x y :: int |
63633 | 720 |
assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
721 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
722 |
using multiplicity_eq_imp_eq[of x y] assms by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
723 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
724 |
lemma multiplicity_prod_prime_powers: |
63633 | 725 |
assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
726 |
shows "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
727 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
728 |
define g where "g = (\<lambda>x. if x \<in> S then f x else 0)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
729 |
define A where "A = Abs_multiset g" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
730 |
have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def) |
67613 | 731 |
from finite_subset[OF this assms(1)] have [simp]: "g \<in> multiset" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
732 |
by (simp add: multiset_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
733 |
from assms have count_A: "count A x = g x" for x unfolding A_def |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
734 |
by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
735 |
have set_mset_A: "set_mset A = {x\<in>S. f x > 0}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
736 |
unfolding set_mset_def count_A by (auto simp: g_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
737 |
with assms have prime: "prime x" if "x \<in># A" for x using that by auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
738 |
from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) " |
64272 | 739 |
by (intro prod.cong) (auto simp: g_def) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
740 |
also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)" |
64272 | 741 |
by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A) |
63830 | 742 |
also have "\<dots> = prod_mset A" |
64272 | 743 |
by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong) |
63830 | 744 |
also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)" |
745 |
by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
746 |
also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
747 |
by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime) |
63830 | 748 |
also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
749 |
finally show ?thesis . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
750 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
751 |
|
63904 | 752 |
lemma prime_factorization_prod_mset: |
753 |
assumes "0 \<notin># A" |
|
73047
ab9e27da0e85
HOL-Library: Changed notation for sum_mset
Manuel Eberl <eberlm@in.tum.de>
parents:
69597
diff
changeset
|
754 |
shows "prime_factorization (prod_mset A) = \<Sum>\<^sub>#(image_mset prime_factorization A)" |
63904 | 755 |
using assms by (induct A) (auto simp add: prime_factorization_mult) |
756 |
||
64272 | 757 |
lemma prime_factors_prod: |
63904 | 758 |
assumes "finite A" and "0 \<notin> f ` A" |
69313 | 759 |
shows "prime_factors (prod f A) = \<Union>((prime_factors \<circ> f) ` A)" |
64272 | 760 |
using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset) |
63904 | 761 |
|
762 |
lemma prime_factors_fact: |
|
763 |
"prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N") |
|
764 |
proof (rule set_eqI) |
|
765 |
fix p |
|
766 |
{ fix m :: nat |
|
767 |
assume "p \<in> prime_factors m" |
|
768 |
then have "prime p" and "p dvd m" by auto |
|
769 |
moreover assume "m > 0" |
|
770 |
ultimately have "2 \<le> p" and "p \<le> m" |
|
771 |
by (auto intro: prime_ge_2_nat dest: dvd_imp_le) |
|
772 |
moreover assume "m \<le> n" |
|
773 |
ultimately have "2 \<le> p" and "p \<le> n" |
|
774 |
by (auto intro: order_trans) |
|
775 |
} note * = this |
|
776 |
show "p \<in> ?M \<longleftrightarrow> p \<in> ?N" |
|
64272 | 777 |
by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *) |
63904 | 778 |
qed |
779 |
||
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
780 |
lemma prime_dvd_fact_iff: |
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
781 |
assumes "prime p" |
63904 | 782 |
shows "p dvd fact n \<longleftrightarrow> p \<le> n" |
783 |
using assms |
|
784 |
by (auto simp add: prime_factorization_subset_iff_dvd [symmetric] |
|
63905 | 785 |
prime_factorization_prime prime_factors_fact prime_ge_2_nat) |
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
786 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
787 |
(* TODO Legacy names *) |
63633 | 788 |
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat] |
789 |
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int] |
|
790 |
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
791 |
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int] |
|
792 |
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
793 |
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int] |
|
794 |
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat] |
|
795 |
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int] |
|
796 |
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat] |
|
797 |
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int] |
|
798 |
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat] |
|
799 |
lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int] |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
800 |
lemmas primes_coprime_nat = primes_coprime[where ?'a = nat] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
801 |
lemmas primes_coprime_int = primes_coprime[where ?'a = nat] |
63633 | 802 |
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat] |
803 |
lemmas prime_exp = prime_elem_power_iff[where ?'a = nat] |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
804 |
|
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
805 |
text \<open>Code generation\<close> |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
806 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
807 |
context |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
808 |
begin |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
809 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
810 |
qualified definition prime_nat :: "nat \<Rightarrow> bool" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
811 |
where [simp, code_abbrev]: "prime_nat = prime" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
812 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
813 |
lemma prime_nat_naive [code]: |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
814 |
"prime_nat p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
815 |
by (auto simp add: prime_nat_iff') |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
816 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
817 |
qualified definition prime_int :: "int \<Rightarrow> bool" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
818 |
where [simp, code_abbrev]: "prime_int = prime" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
819 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
820 |
lemma prime_int_naive [code]: |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
821 |
"prime_int p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
822 |
by (auto simp add: prime_int_iff') |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
823 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
824 |
lemma "prime(997::nat)" by eval |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
825 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
826 |
lemma "prime(997::int)" by eval |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
827 |
|
63635 | 828 |
end |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
829 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
830 |
end |