author | haftmann |
Thu, 06 Apr 2017 21:37:13 +0200 | |
changeset 65417 | fc41a5650fb1 |
parent 65025 | src/HOL/Number_Theory/Primes.thy@8c32ce2a01c6 |
child 65435 | 378175f44328 |
permissions | -rw-r--r-- |
32479 | 1 |
(* Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb, |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
2 |
Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
3 |
Manuel Eberl |
31706 | 4 |
|
5 |
||
32479 | 6 |
This file deals with properties of primes. Definitions and lemmas are |
7 |
proved uniformly for the natural numbers and integers. |
|
31706 | 8 |
|
9 |
This file combines and revises a number of prior developments. |
|
10 |
||
11 |
The original theories "GCD" and "Primes" were by Christophe Tabacznyj |
|
58623 | 12 |
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced |
31706 | 13 |
gcd, lcm, and prime for the natural numbers. |
14 |
||
15 |
The original theory "IntPrimes" was by Thomas M. Rasmussen, and |
|
16 |
extended gcd, lcm, primes to the integers. Amine Chaieb provided |
|
17 |
another extension of the notions to the integers, and added a number |
|
18 |
of results to "Primes" and "GCD". IntPrimes also defined and developed |
|
19 |
the congruence relations on the integers. The notion was extended to |
|
33718 | 20 |
the natural numbers by Chaieb. |
31706 | 21 |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
|
31798 | 25 |
Tobias Nipkow cleaned up a lot. |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
26 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
31 |
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
|
32 |
Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray. |
21256 | 33 |
*) |
34 |
||
31706 | 35 |
|
60526 | 36 |
section \<open>Primes\<close> |
21256 | 37 |
|
32479 | 38 |
theory Primes |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
39 |
imports "~~/src/HOL/Binomial" Euclidean_Algorithm |
31706 | 40 |
begin |
41 |
||
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
42 |
(* As a simp or intro rule, |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
43 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
44 |
prime p \<Longrightarrow> p > 0 |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
45 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
46 |
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
|
47 |
leads to the backchaining |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
48 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
49 |
x > 0 |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
50 |
prime x |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
51 |
x \<in># M which is, unfortunately, |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
52 |
count M x > 0 |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
53 |
*) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
54 |
|
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
|
55 |
declare [[coercion int]] |
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
|
56 |
declare [[coercion_enabled]] |
31706 | 57 |
|
63633 | 58 |
lemma prime_elem_nat_iff: |
59 |
"prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. 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
|
60 |
proof safe |
63633 | 61 |
assume *: "prime_elem n" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
62 |
from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+ |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
63 |
thus "n > 1" by (cases n) simp_all |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
64 |
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
|
65 |
from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m" |
63633 | 66 |
by (intro irreducibleD' prime_elem_imp_irreducible) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
67 |
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
|
68 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
69 |
assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n" |
63633 | 70 |
thus "prime_elem n" |
71 |
by (auto simp: prime_elem_iff_irreducible irreducible_altdef) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
72 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
73 |
|
63633 | 74 |
lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n" |
75 |
by (simp add: prime_def) |
|
31706 | 76 |
|
63633 | 77 |
lemma prime_nat_iff: |
78 |
"prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))" |
|
79 |
by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff) |
|
31706 | 80 |
|
63633 | 81 |
lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
82 |
proof |
63633 | 83 |
assume "prime_elem n" |
84 |
thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
85 |
next |
63633 | 86 |
assume "prime_elem (nat (abs n))" |
87 |
thus "prime_elem n" |
|
88 |
by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
89 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
90 |
|
63633 | 91 |
lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n" |
92 |
by (auto simp: prime_elem_int_nat_transfer) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
93 |
|
63633 | 94 |
lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n" |
95 |
by (auto simp: prime_elem_int_nat_transfer prime_def) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
96 |
|
63633 | 97 |
lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)" |
98 |
by (auto simp: prime_elem_int_nat_transfer prime_def) |
|
31706 | 99 |
|
63633 | 100 |
lemma prime_int_iff: |
101 |
"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
|
102 |
proof (intro iffI conjI allI impI; (elim conjE)?) |
63633 | 103 |
assume *: "prime n" |
104 |
hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible) |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
105 |
from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1" |
63633 | 106 |
by (auto simp: prime_def zabs_def not_less split: if_splits) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
107 |
thus "n > 1" by presburger |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
113 |
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
|
114 |
hence "nat n > 1" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
115 |
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
|
116 |
proof (intro allI impI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
117 |
fix m assume "m dvd nat n" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
118 |
with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
119 |
with n(2) have "int m = 1 \<or> int m = n" by auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
120 |
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
|
121 |
qed |
63633 | 122 |
ultimately show "prime n" |
123 |
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
|
124 |
qed |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
125 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
126 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
127 |
lemma prime_nat_not_dvd: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
128 |
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
|
129 |
shows "\<not>n dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
130 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
131 |
assume "n dvd p" |
63633 | 132 |
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
|
133 |
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
|
134 |
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
|
135 |
qed |
22027
e4a08629c4bd
A few lemmas about relative primes when dividing trough gcd
chaieb
parents:
21404
diff
changeset
|
136 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
137 |
lemma prime_int_not_dvd: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
138 |
assumes "prime p" "p > n" "n > (1::int)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
139 |
shows "\<not>n dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
140 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
141 |
assume "n dvd p" |
63633 | 142 |
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
|
143 |
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
|
144 |
by (auto dest!: zdvd_imp_le) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
145 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
146 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
147 |
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
|
148 |
by (intro prime_nat_not_dvd) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
149 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
150 |
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
|
151 |
by (intro prime_int_not_dvd) auto |
22367 | 152 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
153 |
lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)" |
63633 | 154 |
unfolding prime_int_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
155 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
156 |
lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)" |
63633 | 157 |
unfolding prime_nat_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
158 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
159 |
lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)" |
63633 | 160 |
unfolding prime_int_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
161 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
162 |
lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)" |
63633 | 163 |
unfolding prime_nat_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
164 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
165 |
lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0" |
63633 | 166 |
unfolding prime_nat_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
167 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
168 |
lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)" |
63633 | 169 |
unfolding prime_int_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
170 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
171 |
lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)" |
63633 | 172 |
unfolding prime_nat_iff by auto |
31706 | 173 |
|
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
|
174 |
lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0" |
63633 | 175 |
unfolding prime_nat_iff by auto |
31706 | 176 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
177 |
lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)" |
63633 | 178 |
unfolding prime_int_iff by auto |
31706 | 179 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
180 |
lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)" |
63633 | 181 |
unfolding prime_nat_iff by auto |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
182 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
183 |
lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)" |
63633 | 184 |
unfolding prime_int_iff by auto |
31706 | 185 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
186 |
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
|
187 |
"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
|
188 |
m = 1 \<or> m = p))" |
63633 | 189 |
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
|
190 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62429
diff
changeset
|
191 |
lemma not_prime_eq_prod_nat: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
192 |
assumes "m > 1" "\<not>prime (m::nat)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
193 |
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
|
194 |
using assms irreducible_altdef[of m] |
63633 | 195 |
by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef) |
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset
|
196 |
|
64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
197 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
198 |
subsection\<open>Largest exponent of a prime factor\<close> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
199 |
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
|
200 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
201 |
lemma prime_power_cancel_less: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
202 |
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
|
203 |
shows False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
204 |
proof - |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
205 |
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
|
206 |
using less less_imp_add_positive by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
207 |
have "m = m * (p ^ k) div (p ^ k)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
208 |
using \<open>prime p\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
209 |
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
|
210 |
using eq by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
211 |
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
|
212 |
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
|
213 |
also have "... = m' * (p ^ l)" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
214 |
using \<open>prime p\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
215 |
finally have "p dvd m" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
216 |
using \<open>l > 0\<close> by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
217 |
with assms show False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
218 |
by simp |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
219 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
220 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
221 |
lemma prime_power_cancel: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
222 |
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
|
223 |
shows "k = k'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
224 |
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
|
225 |
by (metis linorder_neqE_nat) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
226 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
227 |
lemma prime_power_cancel2: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
228 |
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
|
229 |
obtains "m = m'" "k = k'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
230 |
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
|
231 |
|
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
232 |
lemma prime_power_canonical: |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
233 |
fixes m::nat |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
234 |
assumes "prime p" "m > 0" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
235 |
shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
236 |
using \<open>m > 0\<close> |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
237 |
proof (induction m rule: less_induct) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
238 |
case (less m) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
239 |
show ?case |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
240 |
proof (cases "p dvd m") |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
241 |
case True |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
242 |
then obtain m' where m': "m = p * m'" |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
243 |
using dvdE by blast |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
244 |
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
|
245 |
using less.prems prime_nat_iff by auto |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
246 |
with m' less show ?thesis |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
247 |
by (metis power_Suc mult.left_commute) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
248 |
next |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
249 |
case False |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
250 |
then show ?thesis |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
251 |
by (metis mult.right_neutral power_0) |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
252 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
253 |
qed |
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64590
diff
changeset
|
254 |
|
53598
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset
|
255 |
|
60526 | 256 |
subsubsection \<open>Make prime naively executable\<close> |
32007 | 257 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
258 |
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" |
63633 | 259 |
unfolding One_nat_def [symmetric] by (rule not_prime_1) |
32007 | 260 |
|
63633 | 261 |
lemma prime_nat_iff': |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
262 |
"prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
263 |
proof safe |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
264 |
assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p" |
63633 | 265 |
show "prime p" unfolding prime_nat_iff |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
266 |
proof (intro conjI allI impI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
267 |
fix m assume "m dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
268 |
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
|
269 |
hence "m \<ge> 1" by simp |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
qed fact+ |
63633 | 274 |
qed (auto simp: prime_nat_iff) |
32007 | 275 |
|
63633 | 276 |
lemma prime_int_iff': |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
277 |
"prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)" (is "?lhs = ?rhs") |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
278 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
279 |
assume "?lhs" |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
280 |
thus "?rhs" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
281 |
by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff') |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
282 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
283 |
assume "?rhs" |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
284 |
thus "?lhs" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
285 |
by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff') |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
286 |
qed |
32007 | 287 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
288 |
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
|
289 |
"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
|
290 |
by (simp add: prime_int_nat_transfer) |
32007 | 291 |
|
63635 | 292 |
lemma two_is_prime_nat [simp]: "prime (2::nat)" |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
293 |
by (simp add: prime_nat_iff') |
32007 | 294 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
295 |
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
|
296 |
"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
|
297 |
(1::nat) < numeral m \<and> |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
298 |
(\<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
|
299 |
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
|
300 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
301 |
|
60526 | 302 |
text\<open>A bit of regression testing:\<close> |
32111 | 303 |
|
58954
18750e86d5b8
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
haftmann
parents:
58898
diff
changeset
|
304 |
lemma "prime(97::nat)" by simp |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
305 |
lemma "prime(97::int)" by simp |
31706 | 306 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
307 |
lemma prime_factor_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
308 |
"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
|
309 |
using prime_divisor_exists[of n] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
310 |
by (cases "n = 0") (auto intro: exI[of _ "2::nat"]) |
23983 | 311 |
|
44872 | 312 |
|
60526 | 313 |
subsection \<open>Infinitely many primes\<close> |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
314 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
315 |
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
|
316 |
proof- |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset
|
317 |
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
|
318 |
from prime_factor_nat [OF f1] |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
319 |
obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto |
44872 | 320 |
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done |
321 |
{ assume "p \<le> n" |
|
60526 | 322 |
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
|
323 |
by (cases p, simp_all) |
60526 | 324 |
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
|
325 |
by (intro dvd_fact) |
60526 | 326 |
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
|
327 |
by (rule dvd_diff_nat) |
44872 | 328 |
then have "p dvd 1" by simp |
329 |
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
|
330 |
moreover from \<open>prime p\<close> have "p > 1" |
63633 | 331 |
using prime_nat_iff by blast |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
332 |
ultimately have False by auto} |
44872 | 333 |
then have "n < p" by presburger |
60526 | 334 |
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
|
335 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
336 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
337 |
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" |
44872 | 338 |
using next_prime_bound by auto |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
339 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
340 |
lemma 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
|
341 |
proof |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
342 |
assume "finite {(p::nat). prime p}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
343 |
with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
344 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
345 |
then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
346 |
by auto |
44872 | 347 |
with bigger_prime [of b] show False |
348 |
by auto |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
349 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
350 |
|
60526 | 351 |
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
|
352 |
|
60526 | 353 |
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
|
354 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
355 |
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
|
356 |
fixes p::nat |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
357 |
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
|
358 |
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
|
359 |
proof - |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
360 |
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
|
361 |
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q" |
63633 | 362 |
unfolding prime_nat_iff by auto |
60526 | 363 |
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
|
364 |
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
|
365 |
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
|
366 |
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
|
367 |
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
|
368 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
369 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
370 |
(* TODO: Generalise? *) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
371 |
lemma prime_power_mult_nat: |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
372 |
fixes p::nat |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
373 |
assumes p: "prime p" and xy: "x * y = p ^ k" |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
374 |
shows "\<exists>i j. x = p ^i \<and> y = p^ j" |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
375 |
using xy |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
376 |
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
|
377 |
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
|
378 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
379 |
case (Suc k x y) |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
380 |
from Suc.prems have pxy: "p dvd x*y" by auto |
63633 | 381 |
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
|
382 |
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
|
383 |
{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
|
384 |
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
|
385 |
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
|
386 |
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
|
387 |
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
|
388 |
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
|
389 |
with ij(2) have ?case by blast} |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
390 |
moreover |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
391 |
{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
|
392 |
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
|
393 |
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
|
394 |
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
|
395 |
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
|
396 |
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
|
397 |
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
|
398 |
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
|
399 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
400 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
401 |
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
|
402 |
fixes p::nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
403 |
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
|
404 |
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
|
405 |
using n xn |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
406 |
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
|
407 |
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
|
408 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
409 |
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
|
410 |
{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
|
411 |
moreover |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
412 |
{assume n: "n \<noteq> 0" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
413 |
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
|
414 |
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
|
415 |
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
|
416 |
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
|
417 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
418 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
419 |
lemma divides_primepow_nat: |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
420 |
fixes p::nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
421 |
assumes p: "prime p" |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
422 |
shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)" |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
423 |
proof |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
424 |
assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset
|
425 |
unfolding dvd_def apply (auto simp add: mult.commute) by blast |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
426 |
from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
427 |
from e ij have "p^(i + j) = p^k" by (simp add: power_add) |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
428 |
hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
429 |
hence "i \<le> k" by arith |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
430 |
with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
431 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
432 |
{fix i assume H: "i \<le> k" "d = p^i" |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
433 |
then obtain j where j: "k = i + j" |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
434 |
by (metis le_add_diff_inverse) |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
435 |
hence "p^k = p^j*d" using H(2) by (simp add: power_add) |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
436 |
hence "d dvd p^k" unfolding dvd_def by auto} |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
437 |
thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
438 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
439 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
440 |
|
60526 | 441 |
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
|
442 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
443 |
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
|
444 |
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
|
445 |
using bezout_nat[of a b] |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62410
diff
changeset
|
446 |
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
|
447 |
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
|
448 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
449 |
lemma gcd_bezout_sum_nat: |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
450 |
fixes a::nat |
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
451 |
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
|
452 |
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
|
453 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
454 |
let ?g = "gcd a b" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
455 |
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
|
456 |
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
|
457 |
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
|
458 |
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
|
459 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
460 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
461 |
|
60526 | 462 |
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
|
463 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
464 |
(* TODO: Generalise? *) |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
465 |
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
|
466 |
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
|
467 |
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
|
468 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
469 |
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
|
470 |
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
|
471 |
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
472 |
then have d12: "d1 = 1" "d2 =1" |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
473 |
by (metis ab coprime_nat)+ |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
474 |
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
|
475 |
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
|
476 |
let ?q2 = "v * y1 + u * x2" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
477 |
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
|
478 |
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
|
479 |
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
|
480 |
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
|
481 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
482 |
|
60526 | 483 |
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
|
484 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
485 |
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
|
486 |
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
|
487 |
shows "\<exists>x y. a * x = b * y + 1" |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
488 |
by (metis assms bezout_nat gcd_nat.left_neutral) |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
489 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
490 |
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
|
491 |
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
|
492 |
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
|
493 |
proof - |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
494 |
have ap: "coprime a p" |
63633 | 495 |
by (metis gcd.commute p pa prime_imp_coprime) |
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
496 |
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
|
497 |
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
|
498 |
by (rule coprime_bezout_strong) |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
499 |
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
|
500 |
qed |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
501 |
(* 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
|
502 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
503 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
504 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
505 |
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
|
506 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
507 |
lemma prime_factors_gt_0_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
508 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::nat)" |
63905 | 509 |
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
|
510 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
511 |
lemma prime_factors_gt_0_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
512 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::int)" |
63905 | 513 |
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
|
514 |
|
63905 | 515 |
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
|
516 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
517 |
shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0" |
63905 | 518 |
by (drule prime_factors_gt_0_int) simp |
519 |
||
63830 | 520 |
lemma prod_mset_prime_factorization_int: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
521 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
522 |
assumes "n > 0" |
63830 | 523 |
shows "prod_mset (prime_factorization n) = n" |
524 |
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
|
525 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
526 |
lemma prime_factorization_exists_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
527 |
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))" |
63633 | 528 |
using prime_factorization_exists[of n] by (auto simp: prime_def) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
529 |
|
63830 | 530 |
lemma prod_mset_prime_factorization_nat [simp]: |
531 |
"(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n" |
|
532 |
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
|
533 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
534 |
lemma prime_factorization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
535 |
"n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 536 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
537 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
538 |
lemma prime_factorization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
539 |
"n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 540 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
541 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
542 |
lemma prime_factorization_unique_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
543 |
fixes f :: "nat \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
544 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
545 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
546 |
and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 547 |
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
|
548 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
549 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
550 |
lemma prime_factorization_unique_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
551 |
fixes f :: "int \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
552 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
553 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
554 |
and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 555 |
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
|
556 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
557 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
558 |
lemma prime_factors_characterization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
559 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
560 |
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
|
561 |
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
|
562 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
563 |
lemma prime_factors_characterization'_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
564 |
"finite {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
565 |
(\<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
|
566 |
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
|
567 |
by (rule prime_factors_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
568 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
569 |
lemma prime_factors_characterization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
570 |
"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
|
571 |
\<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
|
572 |
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
|
573 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
574 |
(* TODO Move *) |
64272 | 575 |
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
|
576 |
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
|
577 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
578 |
lemma primes_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
579 |
"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
|
580 |
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}" |
64272 | 581 |
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
|
582 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
583 |
lemma multiplicity_characterization_nat: |
63633 | 584 |
"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
|
585 |
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
|
586 |
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
|
587 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
588 |
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> |
63633 | 589 |
(\<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
|
590 |
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
|
591 |
by (intro impI, rule multiplicity_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
592 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
593 |
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
63633 | 594 |
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
|
595 |
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) |
64272 | 596 |
(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
|
597 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
598 |
lemma multiplicity_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
599 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> |
63633 | 600 |
(\<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
|
601 |
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
|
602 |
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
|
603 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
604 |
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
|
605 |
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
|
606 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
607 |
lemma multiplicity_eq_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
608 |
fixes x and y::nat |
63633 | 609 |
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
|
610 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
611 |
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
|
612 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
613 |
lemma multiplicity_eq_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
614 |
fixes x y :: int |
63633 | 615 |
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
|
616 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
617 |
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
|
618 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
619 |
lemma multiplicity_prod_prime_powers: |
63633 | 620 |
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
|
621 |
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
|
622 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
623 |
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
|
624 |
define A where "A = Abs_multiset g" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
625 |
have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
626 |
from finite_subset[OF this assms(1)] have [simp]: "g : multiset" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
627 |
by (simp add: multiset_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
628 |
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
|
629 |
by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
630 |
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
|
631 |
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
|
632 |
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
|
633 |
from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) " |
64272 | 634 |
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
|
635 |
also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)" |
64272 | 636 |
by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A) |
63830 | 637 |
also have "\<dots> = prod_mset A" |
64272 | 638 |
by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong) |
63830 | 639 |
also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)" |
640 |
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
|
641 |
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
|
642 |
by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime) |
63830 | 643 |
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
|
644 |
finally show ?thesis . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
645 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
646 |
|
63904 | 647 |
lemma prime_factorization_prod_mset: |
648 |
assumes "0 \<notin># A" |
|
649 |
shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)" |
|
650 |
using assms by (induct A) (auto simp add: prime_factorization_mult) |
|
651 |
||
64272 | 652 |
lemma prime_factors_prod: |
63904 | 653 |
assumes "finite A" and "0 \<notin> f ` A" |
64272 | 654 |
shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)" |
655 |
using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset) |
|
63904 | 656 |
|
657 |
lemma prime_factors_fact: |
|
658 |
"prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N") |
|
659 |
proof (rule set_eqI) |
|
660 |
fix p |
|
661 |
{ fix m :: nat |
|
662 |
assume "p \<in> prime_factors m" |
|
663 |
then have "prime p" and "p dvd m" by auto |
|
664 |
moreover assume "m > 0" |
|
665 |
ultimately have "2 \<le> p" and "p \<le> m" |
|
666 |
by (auto intro: prime_ge_2_nat dest: dvd_imp_le) |
|
667 |
moreover assume "m \<le> n" |
|
668 |
ultimately have "2 \<le> p" and "p \<le> n" |
|
669 |
by (auto intro: order_trans) |
|
670 |
} note * = this |
|
671 |
show "p \<in> ?M \<longleftrightarrow> p \<in> ?N" |
|
64272 | 672 |
by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *) |
63904 | 673 |
qed |
674 |
||
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
675 |
lemma prime_dvd_fact_iff: |
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
676 |
assumes "prime p" |
63904 | 677 |
shows "p dvd fact n \<longleftrightarrow> p \<le> n" |
678 |
using assms |
|
679 |
by (auto simp add: prime_factorization_subset_iff_dvd [symmetric] |
|
63905 | 680 |
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
|
681 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
682 |
(* TODO Legacy names *) |
63633 | 683 |
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat] |
684 |
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int] |
|
685 |
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
686 |
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int] |
|
687 |
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
688 |
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int] |
|
689 |
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat] |
|
690 |
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int] |
|
691 |
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat] |
|
692 |
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int] |
|
693 |
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat] |
|
694 |
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
|
695 |
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
|
696 |
lemmas primes_coprime_int = primes_coprime[where ?'a = nat] |
63633 | 697 |
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat] |
698 |
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
|
699 |
|
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
700 |
text \<open>Code generation\<close> |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
701 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
702 |
context |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
703 |
begin |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
704 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
705 |
qualified definition prime_nat :: "nat \<Rightarrow> bool" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
706 |
where [simp, code_abbrev]: "prime_nat = prime" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
707 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
708 |
lemma prime_nat_naive [code]: |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
709 |
"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
|
710 |
by (auto simp add: prime_nat_iff') |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
711 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
712 |
qualified definition prime_int :: "int \<Rightarrow> bool" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
713 |
where [simp, code_abbrev]: "prime_int = prime" |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
714 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
715 |
lemma prime_int_naive [code]: |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
716 |
"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
|
717 |
by (auto simp add: prime_int_iff') |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
718 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
719 |
lemma "prime(997::nat)" by eval |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
720 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
721 |
lemma "prime(997::int)" by eval |
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
722 |
|
63635 | 723 |
end |
65025
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
724 |
|
8c32ce2a01c6
explicit operations for executable primality checks
haftmann
parents:
64911
diff
changeset
|
725 |
end |