author | haftmann |
Sat, 17 Dec 2016 15:22:13 +0100 | |
changeset 64590 | 6621d91d3c8a |
parent 64272 | f76b6dda2e56 |
child 64773 | 223b2ebdda79 |
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 |
|
2bd8d459ebae
remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents:
47108
diff
changeset
|
197 |
|
60526 | 198 |
subsubsection \<open>Make prime naively executable\<close> |
32007 | 199 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
200 |
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)" |
63633 | 201 |
unfolding One_nat_def [symmetric] by (rule not_prime_1) |
32007 | 202 |
|
63633 | 203 |
lemma prime_nat_iff': |
63535 | 204 |
"prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
205 |
proof safe |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
206 |
assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p" |
63633 | 207 |
show "prime p" unfolding prime_nat_iff |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
208 |
proof (intro conjI allI impI) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
209 |
fix m assume "m dvd p" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
210 |
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
|
211 |
hence "m \<ge> 1" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
212 |
moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
qed fact+ |
63633 | 216 |
qed (auto simp: prime_nat_iff) |
32007 | 217 |
|
63535 | 218 |
lemma prime_nat_code [code_unfold]: |
219 |
"(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" |
|
63633 | 220 |
by (rule ext, rule prime_nat_iff') |
63535 | 221 |
|
63633 | 222 |
lemma prime_int_iff': |
63535 | 223 |
"prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs") |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
224 |
proof |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
225 |
assume "?lhs" |
63633 | 226 |
thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
227 |
next |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
228 |
assume "?rhs" |
63633 | 229 |
thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
230 |
qed |
32007 | 231 |
|
63535 | 232 |
lemma prime_int_code [code_unfold]: |
233 |
"(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))" |
|
63633 | 234 |
by (rule ext, rule prime_int_iff') |
63535 | 235 |
|
32007 | 236 |
lemma prime_nat_simp: |
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
|
237 |
"prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)" |
44872 | 238 |
by (auto simp add: prime_nat_code) |
32007 | 239 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
240 |
lemma prime_int_simp: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
241 |
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
242 |
by (auto simp add: prime_int_code) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
243 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
244 |
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
|
245 |
"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
|
246 |
by (simp add: prime_int_nat_transfer) |
32007 | 247 |
|
63635 | 248 |
lemma two_is_prime_nat [simp]: "prime (2::nat)" |
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
249 |
by (simp add: prime_nat_simp) |
32007 | 250 |
|
64590
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
251 |
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
|
252 |
"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
|
253 |
(1::nat) < numeral m \<and> |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
254 |
(\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)" |
6621d91d3c8a
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
haftmann
parents:
64272
diff
changeset
|
255 |
by (fact prime_nat_simp) -- \<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
|
256 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
257 |
|
60526 | 258 |
text\<open>A bit of regression testing:\<close> |
32111 | 259 |
|
58954
18750e86d5b8
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
haftmann
parents:
58898
diff
changeset
|
260 |
lemma "prime(97::nat)" by simp |
44872 | 261 |
lemma "prime(997::nat)" by eval |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
262 |
lemma "prime(97::int)" by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
263 |
lemma "prime(997::int)" by eval |
31706 | 264 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
265 |
lemma prime_factor_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
266 |
"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
|
267 |
using prime_divisor_exists[of n] |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
268 |
by (cases "n = 0") (auto intro: exI[of _ "2::nat"]) |
23983 | 269 |
|
44872 | 270 |
|
60526 | 271 |
subsection \<open>Infinitely many primes\<close> |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
272 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
273 |
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
|
274 |
proof- |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset
|
275 |
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
|
276 |
from prime_factor_nat [OF f1] |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
277 |
obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto |
44872 | 278 |
then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done |
279 |
{ assume "p \<le> n" |
|
60526 | 280 |
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
|
281 |
by (cases p, simp_all) |
60526 | 282 |
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
|
283 |
by (intro dvd_fact) |
60526 | 284 |
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
|
285 |
by (rule dvd_diff_nat) |
44872 | 286 |
then have "p dvd 1" by simp |
287 |
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
|
288 |
moreover from \<open>prime p\<close> have "p > 1" |
63633 | 289 |
using prime_nat_iff by blast |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
290 |
ultimately have False by auto} |
44872 | 291 |
then have "n < p" by presburger |
60526 | 292 |
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
|
293 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
294 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
295 |
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" |
44872 | 296 |
using next_prime_bound by auto |
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
297 |
|
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
298 |
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
|
299 |
proof |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
300 |
assume "finite {(p::nat). prime p}" |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
301 |
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
|
302 |
by auto |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
303 |
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
|
304 |
by auto |
44872 | 305 |
with bigger_prime [of b] show False |
306 |
by auto |
|
32036
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
307 |
qed |
8a9228872fbd
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents:
31952
diff
changeset
|
308 |
|
60526 | 309 |
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
|
310 |
|
60526 | 311 |
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
|
312 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
313 |
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
|
314 |
fixes p::nat |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
315 |
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
|
316 |
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
|
317 |
proof - |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
318 |
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
|
319 |
"1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q" |
63633 | 320 |
unfolding prime_nat_iff by auto |
60526 | 321 |
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
|
322 |
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
|
323 |
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
|
324 |
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
|
325 |
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
|
326 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
327 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
328 |
(* TODO: Generalise? *) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
329 |
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
|
330 |
fixes p::nat |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
331 |
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
|
332 |
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
|
333 |
using xy |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
334 |
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
|
335 |
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
|
336 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
337 |
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
|
338 |
from Suc.prems have pxy: "p dvd x*y" by auto |
63633 | 339 |
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
|
340 |
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
|
341 |
{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
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
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
|
347 |
with ij(2) have ?case by blast} |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
348 |
moreover |
55215
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
349 |
{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
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
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
|
354 |
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
|
355 |
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
|
356 |
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
|
357 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
358 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
359 |
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
|
360 |
fixes p::nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
361 |
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
|
362 |
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
|
363 |
using n xn |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
364 |
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
|
365 |
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
|
366 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
367 |
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
|
368 |
{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
|
369 |
moreover |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
370 |
{assume n: "n \<noteq> 0" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
371 |
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
|
372 |
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
|
373 |
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
|
374 |
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
|
375 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
376 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
377 |
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
|
378 |
fixes p::nat |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
379 |
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
|
380 |
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
|
381 |
proof |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
382 |
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
|
383 |
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
|
384 |
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
|
385 |
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
|
386 |
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
|
387 |
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
|
388 |
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
|
389 |
next |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
390 |
{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
|
391 |
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
|
392 |
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
|
393 |
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
|
394 |
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
|
395 |
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
|
396 |
qed |
b6c926e67350
Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
397 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
398 |
|
60526 | 399 |
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
|
400 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
401 |
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
|
402 |
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
|
403 |
using bezout_nat[of a b] |
62429
25271ff79171
Tuned Euclidean Rings/GCD rings
Manuel Eberl <eberlm@in.tum.de>
parents:
62410
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
407 |
lemma gcd_bezout_sum_nat: |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
408 |
fixes a::nat |
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
409 |
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
|
410 |
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
|
411 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
412 |
let ?g = "gcd a b" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
413 |
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
|
414 |
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
|
415 |
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
|
416 |
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
|
417 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
418 |
|
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
419 |
|
60526 | 420 |
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
|
421 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
422 |
(* TODO: Generalise? *) |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
423 |
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
|
424 |
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
|
425 |
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
|
426 |
proof- |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
427 |
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
|
428 |
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
|
429 |
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
|
430 |
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
|
431 |
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
|
432 |
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
|
433 |
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
|
434 |
let ?q2 = "v * y1 + u * x2" |
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
435 |
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
|
436 |
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
|
437 |
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
|
438 |
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
|
439 |
qed |
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
440 |
|
60526 | 441 |
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
|
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 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
|
444 |
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
|
445 |
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
|
446 |
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
|
447 |
|
59669
de7792ea4090
renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
448 |
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
|
449 |
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
|
450 |
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
|
451 |
proof - |
55238
7ddb889e23bd
Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents:
55215
diff
changeset
|
452 |
have ap: "coprime a p" |
63633 | 453 |
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
|
454 |
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
|
455 |
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
|
456 |
by (rule coprime_bezout_strong) |
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
62348
diff
changeset
|
457 |
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
|
458 |
qed |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
459 |
(* 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
|
460 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
461 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
462 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
463 |
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
|
464 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
465 |
lemma prime_factors_gt_0_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
466 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::nat)" |
63905 | 467 |
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
|
468 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
469 |
lemma prime_factors_gt_0_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
470 |
"p \<in> prime_factors x \<Longrightarrow> p > (0::int)" |
63905 | 471 |
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
|
472 |
|
63905 | 473 |
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
|
474 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
475 |
shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0" |
63905 | 476 |
by (drule prime_factors_gt_0_int) simp |
477 |
||
63830 | 478 |
lemma prod_mset_prime_factorization_int: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
479 |
fixes n :: int |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
480 |
assumes "n > 0" |
63830 | 481 |
shows "prod_mset (prime_factorization n) = n" |
482 |
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
|
483 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
484 |
lemma prime_factorization_exists_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
485 |
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))" |
63633 | 486 |
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
|
487 |
|
63830 | 488 |
lemma prod_mset_prime_factorization_nat [simp]: |
489 |
"(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n" |
|
490 |
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
|
491 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
492 |
lemma prime_factorization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
493 |
"n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 494 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
495 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
496 |
lemma prime_factorization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
497 |
"n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)" |
64272 | 498 |
by (simp add: prod_prime_factors) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
499 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
500 |
lemma prime_factorization_unique_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
501 |
fixes f :: "nat \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
502 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
503 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
504 |
and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 505 |
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
|
506 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
507 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
508 |
lemma prime_factorization_unique_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
509 |
fixes f :: "int \<Rightarrow> _" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
510 |
assumes S_eq: "S = {p. 0 < f p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
511 |
and "finite S" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
512 |
and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)" |
63633 | 513 |
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
|
514 |
using assms by (intro prime_factorization_unique'') auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
515 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
516 |
lemma prime_factors_characterization_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
517 |
"S = {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
518 |
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
|
519 |
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
|
520 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
521 |
lemma prime_factors_characterization'_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
522 |
"finite {p. 0 < f (p::nat)} \<Longrightarrow> |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
523 |
(\<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
|
524 |
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
|
525 |
by (rule prime_factors_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
526 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
527 |
lemma prime_factors_characterization_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
528 |
"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
|
529 |
\<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
|
530 |
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
|
531 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
532 |
(* TODO Move *) |
64272 | 533 |
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
|
534 |
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
|
535 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
536 |
lemma primes_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
537 |
"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
|
538 |
prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}" |
64272 | 539 |
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
|
540 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
541 |
lemma multiplicity_characterization_nat: |
63633 | 542 |
"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
|
543 |
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
|
544 |
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
|
545 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
546 |
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow> |
63633 | 547 |
(\<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
|
548 |
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
|
549 |
by (intro impI, rule multiplicity_characterization_nat) auto |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
550 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
551 |
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> |
63633 | 552 |
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
|
553 |
by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) |
64272 | 554 |
(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
|
555 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
556 |
lemma multiplicity_characterization'_int [rule_format]: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
557 |
"finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> |
63633 | 558 |
(\<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
|
559 |
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
|
560 |
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
|
561 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
562 |
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
|
563 |
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
|
564 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
565 |
lemma multiplicity_eq_nat: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
566 |
fixes x and y::nat |
63633 | 567 |
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
|
568 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
569 |
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
|
570 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
571 |
lemma multiplicity_eq_int: |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
572 |
fixes x y :: int |
63633 | 573 |
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
|
574 |
shows "x = y" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
575 |
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
|
576 |
|
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
577 |
lemma multiplicity_prod_prime_powers: |
63633 | 578 |
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
|
579 |
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
|
580 |
proof - |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
581 |
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
|
582 |
define A where "A = Abs_multiset g" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
583 |
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
|
584 |
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
|
585 |
by (simp add: multiset_def) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
586 |
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
|
587 |
by simp |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
588 |
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
|
589 |
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
|
590 |
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
|
591 |
from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) " |
64272 | 592 |
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
|
593 |
also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)" |
64272 | 594 |
by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A) |
63830 | 595 |
also have "\<dots> = prod_mset A" |
64272 | 596 |
by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong) |
63830 | 597 |
also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)" |
598 |
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
|
599 |
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
|
600 |
by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime) |
63830 | 601 |
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
|
602 |
finally show ?thesis . |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
603 |
qed |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
604 |
|
63904 | 605 |
lemma prime_factorization_prod_mset: |
606 |
assumes "0 \<notin># A" |
|
607 |
shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)" |
|
608 |
using assms by (induct A) (auto simp add: prime_factorization_mult) |
|
609 |
||
64272 | 610 |
lemma prime_factors_prod: |
63904 | 611 |
assumes "finite A" and "0 \<notin> f ` A" |
64272 | 612 |
shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)" |
613 |
using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset) |
|
63904 | 614 |
|
615 |
lemma prime_factors_fact: |
|
616 |
"prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N") |
|
617 |
proof (rule set_eqI) |
|
618 |
fix p |
|
619 |
{ fix m :: nat |
|
620 |
assume "p \<in> prime_factors m" |
|
621 |
then have "prime p" and "p dvd m" by auto |
|
622 |
moreover assume "m > 0" |
|
623 |
ultimately have "2 \<le> p" and "p \<le> m" |
|
624 |
by (auto intro: prime_ge_2_nat dest: dvd_imp_le) |
|
625 |
moreover assume "m \<le> n" |
|
626 |
ultimately have "2 \<le> p" and "p \<le> n" |
|
627 |
by (auto intro: order_trans) |
|
628 |
} note * = this |
|
629 |
show "p \<in> ?M \<longleftrightarrow> p \<in> ?N" |
|
64272 | 630 |
by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *) |
63904 | 631 |
qed |
632 |
||
63766
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
633 |
lemma prime_dvd_fact_iff: |
695d60817cb1
Some facts about factorial and binomial coefficients
Manuel Eberl <eberlm@in.tum.de>
parents:
63635
diff
changeset
|
634 |
assumes "prime p" |
63904 | 635 |
shows "p dvd fact n \<longleftrightarrow> p \<le> n" |
636 |
using assms |
|
637 |
by (auto simp add: prime_factorization_subset_iff_dvd [symmetric] |
|
63905 | 638 |
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
|
639 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
62481
diff
changeset
|
640 |
(* TODO Legacy names *) |
63633 | 641 |
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat] |
642 |
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int] |
|
643 |
lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
644 |
lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int] |
|
645 |
lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat] |
|
646 |
lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int] |
|
647 |
lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat] |
|
648 |
lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int] |
|
649 |
lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat] |
|
650 |
lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int] |
|
651 |
lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat] |
|
652 |
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
|
653 |
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
|
654 |
lemmas primes_coprime_int = primes_coprime[where ?'a = nat] |
63633 | 655 |
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat] |
656 |
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
|
657 |
|
63635 | 658 |
end |