src/HOL/Number_Theory/Primes.thy
author wenzelm
Sun, 02 Nov 2014 18:21:45 +0100
changeset 58889 5b7a9633cfa8
parent 58645 94bef115c08f
child 58898 1ebf0a1f12a4
permissions -rw-r--r--
modernized header uniformly as section;
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
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 57512
diff changeset
    11
and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
31706
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
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58645
diff changeset
    28
section {* 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
37294
a2a8216999a2 absolute import -- must work with Main.thy / HOL-Proofs
haftmann
parents: 35644
diff changeset
    31
imports "~~/src/HOL/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
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
    34
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
    35
declare [[coercion_enabled]]
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    36
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
    37
definition prime :: "nat \<Rightarrow> bool"
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
    38
  where "prime 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
    39
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
    40
lemmas prime_nat_def = prime_def
31798
fe9a3043d36c Cleaned up GCD
nipkow
parents: 31766
diff changeset
    41
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
    42
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32415
diff changeset
    43
subsection {* Primes *}
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    44
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
    45
lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
58645
94bef115c08f more foundational definition for predicate even
haftmann
parents: 58623
diff changeset
    46
  apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
94bef115c08f more foundational definition for predicate even
haftmann
parents: 58623
diff changeset
    47
  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
54228
229282d53781 purely algebraic foundation for even/odd
haftmann
parents: 53598
diff changeset
    48
  done
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    49
31992
f8aed98faae7 More about gcd/lcm, and some cleaning up
nipkow
parents: 31952
diff changeset
    50
(* 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
    51
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
    52
lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
    53
  unfolding prime_nat_def by auto
22027
e4a08629c4bd A few lemmas about relative primes when dividing trough gcd
chaieb
parents: 21404
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
lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
    56
  unfolding prime_nat_def by auto
22367
6860f09242bf tuned document;
wenzelm
parents: 22027
diff changeset
    57
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
    58
lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
    59
  unfolding prime_nat_def by auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    60
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
    61
lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
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
    62
  unfolding prime_nat_def by auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    63
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
    64
lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
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
    65
  unfolding prime_nat_def by auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    66
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
    67
lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
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
    68
  unfolding prime_nat_def by auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    69
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
    70
lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    71
  apply (unfold prime_nat_def)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    72
  apply (metis gcd_dvd1_nat gcd_dvd2_nat)
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    73
  done
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    74
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
    75
lemma prime_int_altdef: 
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
    76
  "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
    77
    m = 1 \<or> m = p))"
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
    78
  apply (simp add: prime_def)
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
    79
  apply (auto simp add: )
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
    80
  apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
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
    81
  apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
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
    82
  done
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
    83
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
    84
lemma prime_imp_coprime_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
    85
  fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    86
  apply (unfold prime_int_altdef)
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    87
  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
    88
  done
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
    89
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
    90
lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    91
  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
    92
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
    93
lemma prime_dvd_mult_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
    94
  fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
    95
  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
    96
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
    97
lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
    98
    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
    99
  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
   100
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
   101
lemma prime_dvd_mult_eq_int [simp]:
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
   102
  fixes n::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
   103
  shows "prime p \<Longrightarrow> 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
   104
  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
   105
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   106
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
   107
    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
   108
  unfolding prime_nat_def dvd_def apply auto
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 55337
diff changeset
   109
  by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   110
      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
   111
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
   112
lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
53598
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   113
  by (induct n) auto
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   114
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
   115
lemma prime_dvd_power_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
   116
  fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
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
   117
  by (induct n) auto
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   118
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
   119
lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
53598
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   120
    p dvd x^n \<longleftrightarrow> p dvd x"
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   121
  by (cases n) (auto elim: prime_dvd_power_nat)
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   122
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
   123
lemma prime_dvd_power_int_iff:
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
   124
  fixes x::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
   125
  shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
53598
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   126
  by (cases n) (auto elim: prime_dvd_power_int)
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   127
2bd8d459ebae remove unneeded assumption from prime_dvd_power lemmas;
huffman
parents: 47108
diff changeset
   128
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   129
subsubsection {* Make prime naively executable *}
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   130
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   131
lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   132
  by (simp add: prime_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   133
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   134
lemma one_not_prime_nat [simp]: "~prime (1::nat)"
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   135
  by (simp add: prime_nat_def)
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   136
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   137
lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
55130
70db8d380d62 Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents: 54228
diff changeset
   138
  by (simp add: prime_nat_def)
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   139
37607
ebb8b1a79c4c tuned theory text
haftmann
parents: 37294
diff changeset
   140
lemma prime_nat_code [code]:
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
   141
    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   142
  apply (simp add: Ball_def)
55130
70db8d380d62 Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents: 54228
diff changeset
   143
  apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   144
  done
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   145
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   146
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
   147
    "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   148
  by (auto simp add: prime_nat_code)
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   149
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45605
diff changeset
   150
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   151
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   152
lemma two_is_prime_nat [simp]: "prime (2::nat)"
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   153
  by simp
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   154
32111
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   155
text{* A bit of regression testing: *}
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   156
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   157
lemma "prime(97::nat)" by simp
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   158
lemma "prime(997::nat)" by eval
32111
7c39fcfffd61 Tests for executability of "prime"
nipkow
parents: 32045
diff changeset
   159
32007
a2a3685f61c3 Made "prime" executable
nipkow
parents: 31996
diff changeset
   160
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
   161
lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
55130
70db8d380d62 Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents: 54228
diff changeset
   162
  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   163
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
   164
lemma prime_imp_power_coprime_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
   165
  fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
55130
70db8d380d62 Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents: 54228
diff changeset
   166
  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   167
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
   168
lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
55130
70db8d380d62 Restored Suc rather than +1, and using Library/Binimial
paulson <lp15@cam.ac.uk>
parents: 54228
diff changeset
   169
  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
27568
9949dc7a24de Theorem names as in IntPrimes.thy, also several theorems moved from there
chaieb
parents: 27556
diff changeset
   170
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   171
lemma primes_imp_powers_coprime_nat:
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
   172
    "prime p \<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
   173
  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
   174
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   175
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
   176
  apply (induct n rule: nat_less_induct)
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   177
  apply (case_tac "n = 0")
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   178
  using two_is_prime_nat
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   179
  apply blast
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   180
  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   181
    nat_dvd_not_less neq0_conv prime_nat_def)
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   182
  done
23244
1630951f0512 added lcm, ilcm (lcm for integers) and some lemmas about them;
chaieb
parents: 22367
diff changeset
   183
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   184
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
   185
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   186
lemma prime_divprod_pow_nat:
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
  assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   188
  shows "p^n dvd a \<or> p^n dvd b"
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   189
proof-
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   190
  { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   191
      apply (cases "n=0", simp_all)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   192
      apply (cases "a=1", simp_all)
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   193
      done }
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   194
  moreover
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   195
  { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   196
    then obtain m where m: "n = Suc m" by (cases n) auto
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   197
    from n have "p dvd p^n" apply (intro dvd_power) apply auto done
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   198
    also note pab
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   199
    finally have pab': "p dvd a * b".
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   200
    from prime_dvd_mult_nat[OF p pab']
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   201
    have "p dvd a \<or> p dvd b" .
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   202
    moreover
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   203
    { assume pa: "p dvd a"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   204
      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
   205
      with p have "coprime b p"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   206
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   207
      then have pnb: "coprime (p^n) b"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   208
        by (subst gcd_commute_nat, rule coprime_exp_nat)
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   209
      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
   210
    moreover
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   211
    { assume pb: "p dvd b"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 55337
diff changeset
   212
      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
   213
      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
   214
        by auto
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   215
      with p have "coprime a p"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   216
        by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   217
      then have pna: "coprime (p^n) a"
31952
40501bb2d57c renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents: 31814
diff changeset
   218
        by (subst gcd_commute_nat, rule coprime_exp_nat)
33946
fcc20072df9a removed redundant lemma
nipkow
parents: 33718
diff changeset
   219
      from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   220
    ultimately have ?thesis by blast }
31706
1db0c8f235fb new GCD library, courtesy of Jeremy Avigad
huffman
parents: 30738
diff changeset
   221
  ultimately show ?thesis by blast
23983
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   222
qed
79dc793bec43 Added lemmas
nipkow
parents: 23951
diff changeset
   223
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   224
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   225
subsection {* Infinitely many primes *}
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   226
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
   227
lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   228
proof-
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   229
  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
   230
  from prime_factor_nat [OF f1]
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   231
  obtain p where "prime p" and "p dvd fact n + 1" by auto
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   232
  then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   233
  { assume "p \<le> n"
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   234
    from `prime p` have "p \<ge> 1" 
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   235
      by (cases p, simp_all)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   236
    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
   237
      by (intro dvd_fact_nat)
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   238
    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
   239
      by (rule dvd_diff_nat)
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   240
    then have "p dvd 1" by simp
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   241
    then have "p <= 1" by auto
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   242
    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
   243
    ultimately have False by auto}
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   244
  then have "n < p" by presburger
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   245
  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
   246
qed
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   247
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   248
lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)" 
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   249
  using next_prime_bound by auto
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   250
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   251
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
   252
proof
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   253
  assume "finite {(p::nat). prime p}"
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   254
  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
   255
    by auto
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   256
  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
   257
    by auto
44872
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   258
  with bigger_prime [of b] show False
a98ef45122f3 misc tuning;
wenzelm
parents: 44821
diff changeset
   259
    by auto
32036
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   260
qed
8a9228872fbd Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
avigad
parents: 31952
diff changeset
   261
55215
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   262
subsection{*Powers of Primes*}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   263
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   264
text{*Versions for type nat only*}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   265
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   266
lemma prime_product: 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   267
  fixes p::nat
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   268
  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
   269
  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
   270
proof -
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   271
  from assms have 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   272
    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   273
    unfolding prime_nat_def by auto
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   274
  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   275
  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
   276
  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
   277
  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
   278
  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
   279
qed
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   280
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   281
lemma prime_exp: 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   282
  fixes p::nat
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   283
  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   284
proof(induct n)
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   285
  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
   286
next
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   287
  case (Suc n)
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   288
  {assume "p = 0" hence ?case by simp}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   289
  moreover
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   290
  {assume "p=1" hence ?case by simp}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   291
  moreover
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   292
  {assume p: "p \<noteq> 0" "p\<noteq>1"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   293
    {assume pp: "prime (p^Suc n)"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   294
      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   295
      with p have n: "n = 0"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   296
        by (metis One_nat_def nat_power_eq_Suc_0_iff)
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   297
      with pp have "prime p \<and> Suc n = 1" by simp}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   298
    moreover
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   299
    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   300
    ultimately 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
   301
  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
   302
qed
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   303
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   304
lemma prime_power_mult: 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   305
  fixes p::nat
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   306
  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
   307
  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
   308
using xy
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   309
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
   310
  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
   311
next
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   312
  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
   313
  from Suc.prems have pxy: "p dvd x*y" by auto
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   314
  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   315
  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   316
  {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
   317
    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
   318
    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
   319
    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
   320
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = 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
   321
    with d have "x = p^Suc i" by simp 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   322
    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
   323
  moreover 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   324
  {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
   325
    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
   326
    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
   327
    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
   328
    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = 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
   329
    with d have "y = p^Suc i" by simp 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   330
    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
   331
  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
   332
qed
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   333
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   334
lemma prime_power_exp: 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   335
  fixes p::nat
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   336
  assumes p: "prime p" and n: "n \<noteq> 0" 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   337
    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
   338
  using n xn
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   339
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
   340
  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
   341
next
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   342
  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
   343
  {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
   344
  moreover
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   345
  {assume n: "n \<noteq> 0"
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   346
    from prime_power_mult[OF p th] 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   347
    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
   348
    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
   349
  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
   350
qed
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   351
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   352
lemma divides_primepow:
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   353
  fixes p::nat
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   354
  assumes p: "prime p" 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   355
  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
   356
proof
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   357
  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
   358
    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
55215
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   359
  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=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
   360
  from e ij have "p^(i + j) = p^k" 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
   361
  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   362
  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
   363
  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
   364
next
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   365
  {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
   366
    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
   367
      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
   368
    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
   369
    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
   370
  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
   371
qed
b6c926e67350 Restoring some proofs from the equivalent file in Old_Number_Theory.
paulson <lp15@cam.ac.uk>
parents: 55130
diff changeset
   372
55238
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   373
subsection {*Chinese Remainder Theorem Variants*}
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   374
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   375
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
   376
  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
   377
  using bezout_nat[of a b]
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   378
by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   379
  gcd_nat.right_neutral mult_0) 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   380
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   381
lemma gcd_bezout_sum_nat:
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   382
  fixes a::nat 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   383
  assumes "a * x + b * y = d" 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   384
  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
   385
proof-
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   386
  let ?g = "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
   387
    have dv: "?g dvd a*x" "?g dvd b * y" 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   388
      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
   389
    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
   390
    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
   391
qed
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   392
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   393
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   394
text {* A binary form of the Chinese Remainder Theorem. *}
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   395
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   396
lemma chinese_remainder: 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   397
  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
   398
  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
   399
proof-
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   400
  from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   401
  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1" 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   402
    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
   403
  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
   404
    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
   405
  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
   406
  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
   407
  let ?q2 = "v * y1 + u * x2"
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   408
  from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   409
  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
   410
    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
   411
  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
   412
qed
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   413
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   414
text {* Primality *}
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   415
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   416
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
   417
  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
   418
  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
   419
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
   420
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   421
lemma bezout_prime: 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   422
  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
   423
  shows "\<exists>x y. a*x = Suc (p*y)"
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   424
proof-
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   425
  have ap: "coprime a p"
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   426
    by (metis gcd_nat.commute p pa prime_imp_coprime_nat) 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   427
  from coprime_bezout_strong[OF ap] show ?thesis
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   428
    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa) 
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   429
qed
7ddb889e23bd Added material from Old_Number_Theory related to the Chinese Remainder Theorem
paulson <lp15@cam.ac.uk>
parents: 55215
diff changeset
   430
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents:
diff changeset
   431
end