src/HOL/Number_Theory/Primes.thy
author haftmann
Mon, 01 Mar 2010 13:40:23 +0100
changeset 35416 d8d7d1b785af
parent 33946 fcc20072df9a
child 35644 d20cf282342e
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
     1
(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
31798
fe9a3043d36c Cleaned up GCD
nipkow
parents: 31766
diff changeset
     2
                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
     3
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
     4
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
     5
This file deals with properties of primes. Definitions and lemmas are
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
     6
proved uniformly for the natural numbers and integers.
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
     7
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
     8
This file combines and revises a number of prior developments.
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
     9
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    10
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    11
and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    12
gcd, lcm, and prime for the natural numbers.
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    13
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    14
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    15
extended gcd, lcm, primes to the integers. Amine Chaieb provided
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    16
another extension of the notions to the integers, and added a number
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    17
of results to "Primes" and "GCD". IntPrimes also defined and developed
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    18
the congruence relations on the integers. The notion was extended to
33718
06e9aff51d17 Fixed a typo in a comment.
webertj
parents: 32479
diff changeset
    19
the natural numbers by Chaieb.
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    20
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
    21
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
    22
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
    23
31798
fe9a3043d36c Cleaned up GCD
nipkow
parents: 31766
diff changeset
    24
Tobias Nipkow cleaned up a lot.
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    25
*)
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    26
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    27
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    28
header {* Primes *}
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    29
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    30
theory Primes
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    31
imports GCD
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    32
begin
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    33
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    34
declare One_nat_def [simp del]
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    35
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    36
class prime = one +
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    37
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    38
fixes
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    39
  prime :: "'a \<Rightarrow> bool"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    40
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    41
instantiation nat :: prime
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    42
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    43
begin
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    44
21263
wenzelm
parents: 21256
diff changeset
    45
definition
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    46
  prime_nat :: "nat \<Rightarrow> bool"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    47
where
31709
061f01ee9978 more [code del] declarations
huffman
parents: 31706
diff changeset
    48
  [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    49
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    50
instance proof qed
23687
06884f7ffb18 extended - convers now basic lcm properties also
haftmann
parents: 23431
diff changeset
    51
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    52
end
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    53
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    54
instantiation int :: prime
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    55
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    56
begin
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    57
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    58
definition
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    59
  prime_int :: "int \<Rightarrow> bool"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    60
where
31709
061f01ee9978 more [code del] declarations
huffman
parents: 31706
diff changeset
    61
  [code del]: "prime_int p = prime (nat p)"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    62
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    63
instance proof qed
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    64
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    65
end
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    66
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    67
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    68
subsection {* Set up Transfer *}
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    69
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    70
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    71
lemma transfer_nat_int_prime:
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    72
  "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    73
  unfolding gcd_int_def lcm_int_def prime_int_def
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    74
  by auto
23687
06884f7ffb18 extended - convers now basic lcm properties also
haftmann
parents: 23431
diff changeset
    75
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    76
declare TransferMorphism_nat_int[transfer add return:
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    77
    transfer_nat_int_prime]
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    78
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    79
lemma transfer_int_nat_prime:
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    80
  "prime (int x) = prime x"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    81
  by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    82
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    83
declare TransferMorphism_int_nat[transfer add return:
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    84
    transfer_int_nat_prime]
31798
fe9a3043d36c Cleaned up GCD
nipkow
parents: 31766
diff changeset
    85
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    86
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    87
subsection {* Primes *}
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    88
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    89
lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    90
  unfolding prime_nat_def
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    91
  apply (subst even_mult_two_ex)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    92
  apply clarify
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    93
  apply (drule_tac x = 2 in spec)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    94
  apply auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    95
done
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    96
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    97
lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    98
  unfolding prime_int_def
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    99
  apply (frule prime_odd_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   100
  apply (auto simp add: even_nat_def)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   101
done
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   102
31992
f8aed98faae7 More about gcd/lcm, and some cleaning up
nipkow
parents: 31952
diff changeset
   103
(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
22027
e4a08629c4bd A few lemmas about relative primes when dividing trough gcd
chaieb
parents: 21404
diff changeset
   104
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   105
lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   106
  by (unfold prime_nat_def, auto)
22027
e4a08629c4bd A few lemmas about relative primes when dividing trough gcd
chaieb
parents: 21404
diff changeset
   107
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   108
lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   109
  by (unfold prime_nat_def, auto)
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
   110
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   111
lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   112
  by (unfold prime_nat_def, auto)
22027
e4a08629c4bd A few lemmas about relative primes when dividing trough gcd
chaieb
parents: 21404
diff changeset
   113
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   114
lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   115
  by (unfold prime_nat_def, auto)
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
   116
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   117
lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   118
  by (unfold prime_nat_def, auto)
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
   119
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   120
lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   121
  by (unfold prime_nat_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   122
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   123
lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   124
  by (unfold prime_nat_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   125
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   126
lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
31992
f8aed98faae7 More about gcd/lcm, and some cleaning up
nipkow
parents: 31952
diff changeset
   127
  by (unfold prime_int_def prime_nat_def) auto
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
   128
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   129
lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   130
  by (unfold prime_int_def prime_nat_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   131
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   132
lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   133
  by (unfold prime_int_def prime_nat_def, auto)
22027
e4a08629c4bd A few lemmas about relative primes when dividing trough gcd
chaieb
parents: 21404
diff changeset
   134
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   135
lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   136
  by (unfold prime_int_def prime_nat_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   137
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   138
lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   139
  by (unfold prime_int_def prime_nat_def, auto)
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
   140
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   141
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   142
lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   143
    m = 1 \<or> m = p))"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   144
  using prime_nat_def [transferred]
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   145
    apply (case_tac "p >= 0")
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   146
    by (blast, auto simp add: prime_ge_0_int)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   147
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   148
lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   149
  apply (unfold prime_nat_def)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   150
  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   151
  done
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   152
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   153
lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   154
  apply (unfold prime_int_altdef)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   155
  apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   156
  done
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   157
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   158
lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   159
  by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   160
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   161
lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   162
  by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   163
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   164
lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   165
    p dvd m * n = (p dvd m \<or> p dvd n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   166
  by (rule iffI, rule prime_dvd_mult_nat, auto)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   167
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   168
lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   169
    p dvd m * n = (p dvd m \<or> p dvd n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   170
  by (rule iffI, rule prime_dvd_mult_int, auto)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   171
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   172
lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   173
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   174
  unfolding prime_nat_def dvd_def apply auto
31992
f8aed98faae7 More about gcd/lcm, and some cleaning up
nipkow
parents: 31952
diff changeset
   175
  by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   176
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   177
lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   178
    EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   179
  unfolding prime_int_altdef dvd_def
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   180
  apply auto
31992
f8aed98faae7 More about gcd/lcm, and some cleaning up
nipkow
parents: 31952
diff changeset
   181
  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   182
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   183
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   184
    n > 0 --> (p dvd x^n --> p dvd x)"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   185
  by (induct n rule: nat_induct, auto)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   186
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   187
lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   188
    n > 0 --> (p dvd x^n --> p dvd x)"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   189
  apply (induct n rule: nat_induct, auto)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   190
  apply (frule prime_ge_0_int)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   191
  apply auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   192
done
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   193
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   194
subsubsection{* Make prime naively executable *}
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   195
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   196
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   197
  by (simp add: prime_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   198
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   199
lemma zero_not_prime_int [simp]: "~prime (0::int)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   200
  by (simp add: prime_int_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   201
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   202
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   203
  by (simp add: prime_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   204
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   205
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   206
  by (simp add: prime_nat_def One_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   207
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   208
lemma one_not_prime_int [simp]: "~prime (1::int)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   209
  by (simp add: prime_int_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   210
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   211
lemma prime_nat_code[code]:
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   212
 "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   213
apply(simp add: Ball_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   214
apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   215
done
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   216
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   217
lemma prime_nat_simp:
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   218
 "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   219
apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   220
apply(simp add:nat_number One_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   221
done
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   222
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   223
lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   224
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   225
lemma prime_int_code[code]:
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   226
  "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   227
proof
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   228
  assume "?L" thus "?R"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   229
    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   230
next
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   231
    assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   232
qed
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   233
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   234
lemma prime_int_simp:
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   235
  "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   236
apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   237
apply simp
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   238
done
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   239
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   240
lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   241
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   242
lemma two_is_prime_nat [simp]: "prime (2::nat)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   243
by simp
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   244
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   245
lemma two_is_prime_int [simp]: "prime (2::int)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   246
by simp
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   247
32111
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   248
text{* A bit of regression testing: *}
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   249
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   250
lemma "prime(97::nat)"
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   251
by simp
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   252
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   253
lemma "prime(97::int)"
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   254
by simp
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   255
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   256
lemma "prime(997::nat)"
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   257
by eval
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   258
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   259
lemma "prime(997::int)"
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   260
by eval
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   261
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   262
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   263
lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   264
  apply (rule coprime_exp_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   265
  apply (subst gcd_commute_nat)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   266
  apply (erule (1) prime_imp_coprime_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   267
done
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   268
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   269
lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   270
  apply (rule coprime_exp_int)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   271
  apply (subst gcd_commute_int)
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   272
  apply (erule (1) prime_imp_coprime_int)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   273
done
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   274
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   275
lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   276
  apply (rule prime_imp_coprime_nat, assumption)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   277
  apply (unfold prime_nat_def, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   278
done
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   279
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   280
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   281
  apply (rule prime_imp_coprime_int, assumption)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   282
  apply (unfold prime_int_altdef, clarify)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   283
  apply (drule_tac x = q in spec)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   284
  apply (drule_tac x = p in spec)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   285
  apply auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   286
done
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   287
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   288
lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   289
  by (rule coprime_exp2_nat, rule primes_coprime_nat)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   290
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   291
lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   292
  by (rule coprime_exp2_int, rule primes_coprime_int)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   293
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   294
lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   295
  apply (induct n rule: nat_less_induct)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   296
  apply (case_tac "n = 0")
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   297
  using two_is_prime_nat apply blast
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   298
  apply (case_tac "prime n")
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   299
  apply blast
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   300
  apply (subgoal_tac "n > 1")
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   301
  apply (frule (1) not_prime_eq_prod_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   302
  apply (auto intro: dvd_mult dvd_mult2)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   303
done
23244
1630951f0512 added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents: 22367
diff changeset
   304
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   305
(* An Isar version:
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   306
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   307
lemma prime_factor_b_nat:
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   308
  fixes n :: nat
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   309
  assumes "n \<noteq> 1"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   310
  shows "\<exists>p. prime p \<and> p dvd n"
23983
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   311
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   312
using `n ~= 1`
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   313
proof (induct n rule: less_induct_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   314
  fix n :: nat
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   315
  assume "n ~= 1" and
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   316
    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   317
  thus "\<exists>p. prime p \<and> p dvd n"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   318
  proof -
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   319
  {
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   320
    assume "n = 0"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   321
    moreover note two_is_prime_nat
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   322
    ultimately have ?thesis
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   323
      by (auto simp del: two_is_prime_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   324
  }
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   325
  moreover
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   326
  {
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   327
    assume "prime n"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   328
    hence ?thesis by auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   329
  }
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   330
  moreover
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   331
  {
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   332
    assume "n ~= 0" and "~ prime n"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   333
    with `n ~= 1` have "n > 1" by auto
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   334
    with `~ prime n` and not_prime_eq_prod_nat obtain m k where
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   335
      "n = m * k" and "1 < m" and "m < n" by blast
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   336
    with ih obtain p where "prime p" and "p dvd m" by blast
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   337
    with `n = m * k` have ?thesis by auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   338
  }
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   339
  ultimately show ?thesis by blast
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   340
  qed
23983
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   341
qed
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   342
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   343
*)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   344
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   345
text {* One property of coprimality is easier to prove via prime factors. *}
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   346
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   347
lemma prime_divprod_pow_nat:
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   348
  assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   349
  shows "p^n dvd a \<or> p^n dvd b"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   350
proof-
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   351
  {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   352
      apply (cases "n=0", simp_all)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   353
      apply (cases "a=1", simp_all) done}
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   354
  moreover
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   355
  {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   356
    then obtain m where m: "n = Suc m" by (cases n, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   357
    from n have "p dvd p^n" by (intro dvd_power, auto)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   358
    also note pab
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   359
    finally have pab': "p dvd a * b".
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   360
    from prime_dvd_mult_nat[OF p pab']
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   361
    have "p dvd a \<or> p dvd b" .
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   362
    moreover
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   363
    { assume pa: "p dvd a"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   364
      from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   365
      with p have "coprime b p"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   366
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   367
      hence pnb: "coprime (p^n) b"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   368
        by (subst gcd_commute_nat, rule coprime_exp_nat)
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   369
      from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   370
    moreover
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   371
    { assume pb: "p dvd b"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   372
      have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   373
      from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   374
        by auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   375
      with p have "coprime a p"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   376
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   377
      hence pna: "coprime (p^n) a"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   378
        by (subst gcd_commute_nat, rule coprime_exp_nat)
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   379
      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   380
    ultimately have ?thesis by blast}
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   381
  ultimately show ?thesis by blast
23983
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   382
qed
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   383
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   384
subsection {* Infinitely many primes *}
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   385
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   386
lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   387
proof-
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   388
  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   389
  from prime_factor_nat [OF f1]
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   390
      obtain p where "prime p" and "p dvd fact n + 1" by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   391
  hence "p \<le> fact n + 1" 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   392
    by (intro dvd_imp_le, auto)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   393
  {assume "p \<le> n"
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   394
    from `prime p` have "p \<ge> 1" 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   395
      by (cases p, simp_all)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   396
    with `p <= n` have "p dvd fact n" 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   397
      by (intro dvd_fact_nat)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   398
    with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   399
      by (rule dvd_diff_nat)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   400
    hence "p dvd 1" by simp
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   401
    hence "p <= 1" by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   402
    moreover from `prime p` have "p > 1" by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   403
    ultimately have False by auto}
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   404
  hence "n < p" by arith
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   405
  with `prime p` and `p <= fact n + 1` show ?thesis by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   406
qed
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   407
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   408
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   409
using next_prime_bound by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   410
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   411
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
   412
proof
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   413
  assume "finite {(p::nat). prime p}"
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   414
  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
   415
    by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   416
  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
   417
    by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   418
  with bigger_prime [of b] show False by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   419
qed
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   420
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   421
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
   422
end