author | nipkow |
Fri, 08 Jul 2005 11:39:08 +0200 | |
changeset 16762 | aafd23b47a5d |
parent 16663 | 13e9c402308b |
child 19086 | 1b3780be6cc2 |
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 |
15140 | 10 |
imports Main |
15131 | 11 |
begin |
11363 | 12 |
|
13 |
constdefs |
|
14 |
coprime :: "nat => nat => bool" |
|
15 |
"coprime m n == gcd (m, n) = 1" |
|
16 |
||
16663 | 17 |
prime :: "nat \<Rightarrow> bool" |
18 |
"prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)" |
|
11363 | 19 |
|
20 |
||
16762 | 21 |
lemma two_is_prime: "prime 2" |
22 |
apply (auto simp add: prime_def) |
|
23 |
apply (case_tac m) |
|
24 |
apply (auto dest!: dvd_imp_le) |
|
11363 | 25 |
done |
26 |
||
16663 | 27 |
lemma prime_imp_relprime: "prime p ==> \<not> p dvd n ==> gcd (p, n) = 1" |
11363 | 28 |
apply (auto simp add: prime_def) |
29 |
apply (drule_tac x = "gcd (p, n)" in spec) |
|
30 |
apply auto |
|
31 |
apply (insert gcd_dvd2 [of p n]) |
|
32 |
apply simp |
|
33 |
done |
|
34 |
||
35 |
text {* |
|
36 |
This theorem leads immediately to a proof of the uniqueness of |
|
37 |
factorization. If @{term p} divides a product of primes then it is |
|
38 |
one of those primes. |
|
39 |
*} |
|
40 |
||
16663 | 41 |
lemma prime_dvd_mult: "prime p ==> p dvd m * n ==> p dvd m \<or> p dvd n" |
12739 | 42 |
by (blast intro: relprime_dvd_mult prime_imp_relprime) |
11363 | 43 |
|
16663 | 44 |
lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" |
12739 | 45 |
by (auto dest: prime_dvd_mult) |
46 |
||
16663 | 47 |
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
|
48 |
by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
11368 | 49 |
|
11363 | 50 |
|
51 |
end |