author | paulson |
Wed, 18 Jul 2007 11:43:06 +0200 | |
changeset 23839 | d9fa0f457d9a |
parent 22665 | cf152ff55d16 |
child 25593 | 0b0df6c8646a |
permissions | -rw-r--r-- |
11368 | 1 |
(* Title: HOL/Library/Primes.thy |
11363 | 2 |
ID: $Id$ |
3 |
Author: Christophe Tabacznyj and Lawrence C Paulson |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
*) |
|
6 |
||
16762 | 7 |
header {* Primality on nat *} |
11363 | 8 |
|
15131 | 9 |
theory Primes |
21256 | 10 |
imports GCD |
15131 | 11 |
begin |
11363 | 12 |
|
19086 | 13 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset
|
14 |
coprime :: "nat => nat => bool" where |
19086 | 15 |
"coprime m n = (gcd (m, n) = 1)" |
11363 | 16 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset
|
17 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21256
diff
changeset
|
18 |
prime :: "nat \<Rightarrow> bool" where |
19086 | 19 |
"prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" |
11363 | 20 |
|
21 |
||
16762 | 22 |
lemma two_is_prime: "prime 2" |
23 |
apply (auto simp add: prime_def) |
|
24 |
apply (case_tac m) |
|
25 |
apply (auto dest!: dvd_imp_le) |
|
11363 | 26 |
done |
27 |
||
16663 | 28 |
lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1" |
11363 | 29 |
apply (auto simp add: prime_def) |
23839 | 30 |
apply (metis One_nat_def gcd_dvd1 gcd_dvd2) |
11363 | 31 |
done |
32 |
||
33 |
text {* |
|
34 |
This theorem leads immediately to a proof of the uniqueness of |
|
35 |
factorization. If @{term p} divides a product of primes then it is |
|
36 |
one of those primes. |
|
37 |
*} |
|
38 |
||
16663 | 39 |
lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
12739 | 40 |
by (blast intro: relprime_dvd_mult prime_imp_relprime) |
11363 | 41 |
|
16663 | 42 |
lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" |
12739 | 43 |
by (auto dest: prime_dvd_mult) |
44 |
||
16663 | 45 |
lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m" |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13187
diff
changeset
|
46 |
by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
11368 | 47 |
|
11363 | 48 |
end |