src/HOL/Library/Primes.thy
author paulson
Sat Jun 09 08:41:25 2001 +0200 (2001-06-09)
changeset 11363 a548865b1b6a
child 11368 9c1995c73383
permissions -rw-r--r--
moved Primes.thy from NumberTheory to Library
paulson@11363
     1
(*  Title:      HOL/NumberTheory/Primes.thy
paulson@11363
     2
    ID:         $Id$
paulson@11363
     3
    Author:     Christophe Tabacznyj and Lawrence C Paulson
paulson@11363
     4
    Copyright   1996  University of Cambridge
paulson@11363
     5
*)
paulson@11363
     6
paulson@11363
     7
header {* The Greatest Common Divisor and Euclid's algorithm *}
paulson@11363
     8
paulson@11363
     9
theory Primes = Main:
paulson@11363
    10
paulson@11363
    11
text {*
paulson@11363
    12
  (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
paulson@11363
    13
paulson@11363
    14
  \bigskip
paulson@11363
    15
*}
paulson@11363
    16
paulson@11363
    17
consts
paulson@11363
    18
  gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
paulson@11363
    19
paulson@11363
    20
recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
paulson@11363
    21
  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
paulson@11363
    22
paulson@11363
    23
constdefs
paulson@11363
    24
  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
paulson@11363
    25
  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
paulson@11363
    26
    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
paulson@11363
    27
paulson@11363
    28
  coprime :: "nat => nat => bool"
paulson@11363
    29
  "coprime m n == gcd (m, n) = 1"
paulson@11363
    30
paulson@11363
    31
  prime :: "nat set"
paulson@11363
    32
  "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
paulson@11363
    33
paulson@11363
    34
paulson@11363
    35
lemma gcd_induct:
paulson@11363
    36
  "(!!m. P m 0) ==>
paulson@11363
    37
    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
paulson@11363
    38
  ==> P (m::nat) (n::nat)"
paulson@11363
    39
  apply (induct m n rule: gcd.induct)
paulson@11363
    40
  apply (case_tac "n = 0")
paulson@11363
    41
   apply simp_all
paulson@11363
    42
  done
paulson@11363
    43
paulson@11363
    44
paulson@11363
    45
lemma gcd_0 [simp]: "gcd (m, 0) = m"
paulson@11363
    46
  apply simp
paulson@11363
    47
  done
paulson@11363
    48
paulson@11363
    49
lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
paulson@11363
    50
  apply simp
paulson@11363
    51
  done
paulson@11363
    52
paulson@11363
    53
declare gcd.simps [simp del]
paulson@11363
    54
paulson@11363
    55
lemma gcd_1 [simp]: "gcd (m, 1) = 1"
paulson@11363
    56
  apply (simp add: gcd_non_0)
paulson@11363
    57
  done
paulson@11363
    58
paulson@11363
    59
text {*
paulson@11363
    60
  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
paulson@11363
    61
  conjunctions don't seem provable separately.
paulson@11363
    62
*}
paulson@11363
    63
paulson@11363
    64
lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
paulson@11363
    65
  apply (induct m n rule: gcd_induct)
paulson@11363
    66
   apply (simp_all add: gcd_non_0)
paulson@11363
    67
  apply (blast dest: dvd_mod_imp_dvd)
paulson@11363
    68
  done
paulson@11363
    69
paulson@11363
    70
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
paulson@11363
    71
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
paulson@11363
    72
paulson@11363
    73
paulson@11363
    74
text {*
paulson@11363
    75
  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
paulson@11363
    76
  naturals, if @{term k} divides @{term m} and @{term k} divides
paulson@11363
    77
  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
paulson@11363
    78
*}
paulson@11363
    79
paulson@11363
    80
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
paulson@11363
    81
  apply (induct m n rule: gcd_induct)
paulson@11363
    82
   apply (simp_all add: gcd_non_0 dvd_mod)
paulson@11363
    83
  done
paulson@11363
    84
paulson@11363
    85
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
paulson@11363
    86
  apply (blast intro!: gcd_greatest intro: dvd_trans)
paulson@11363
    87
  done
paulson@11363
    88
paulson@11363
    89
paulson@11363
    90
text {*
paulson@11363
    91
  \medskip Function gcd yields the Greatest Common Divisor.
paulson@11363
    92
*}
paulson@11363
    93
paulson@11363
    94
lemma is_gcd: "is_gcd (gcd (m, n)) m n"
paulson@11363
    95
  apply (simp add: is_gcd_def gcd_greatest)
paulson@11363
    96
  done
paulson@11363
    97
paulson@11363
    98
text {*
paulson@11363
    99
  \medskip Uniqueness of GCDs.
paulson@11363
   100
*}
paulson@11363
   101
paulson@11363
   102
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
paulson@11363
   103
  apply (simp add: is_gcd_def)
paulson@11363
   104
  apply (blast intro: dvd_anti_sym)
paulson@11363
   105
  done
paulson@11363
   106
paulson@11363
   107
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
paulson@11363
   108
  apply (auto simp add: is_gcd_def)
paulson@11363
   109
  done
paulson@11363
   110
paulson@11363
   111
paulson@11363
   112
text {*
paulson@11363
   113
  \medskip Commutativity
paulson@11363
   114
*}
paulson@11363
   115
paulson@11363
   116
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
paulson@11363
   117
  apply (auto simp add: is_gcd_def)
paulson@11363
   118
  done
paulson@11363
   119
paulson@11363
   120
lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
paulson@11363
   121
  apply (rule is_gcd_unique)
paulson@11363
   122
   apply (rule is_gcd)
paulson@11363
   123
  apply (subst is_gcd_commute)
paulson@11363
   124
  apply (simp add: is_gcd)
paulson@11363
   125
  done
paulson@11363
   126
paulson@11363
   127
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
paulson@11363
   128
  apply (rule is_gcd_unique)
paulson@11363
   129
   apply (rule is_gcd)
paulson@11363
   130
  apply (simp add: is_gcd_def)
paulson@11363
   131
  apply (blast intro: dvd_trans)
paulson@11363
   132
  done
paulson@11363
   133
paulson@11363
   134
lemma gcd_0_left [simp]: "gcd (0, m) = m"
paulson@11363
   135
  apply (simp add: gcd_commute [of 0])
paulson@11363
   136
  done
paulson@11363
   137
paulson@11363
   138
lemma gcd_1_left [simp]: "gcd (1, m) = 1"
paulson@11363
   139
  apply (simp add: gcd_commute [of 1])
paulson@11363
   140
  done
paulson@11363
   141
paulson@11363
   142
paulson@11363
   143
text {*
paulson@11363
   144
  \medskip Multiplication laws
paulson@11363
   145
*}
paulson@11363
   146
paulson@11363
   147
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
paulson@11363
   148
    -- {* Davenport, page 27 *}
paulson@11363
   149
  apply (induct m n rule: gcd_induct)
paulson@11363
   150
   apply simp
paulson@11363
   151
  apply (case_tac "k = 0")
paulson@11363
   152
   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
paulson@11363
   153
  done
paulson@11363
   154
paulson@11363
   155
lemma gcd_mult [simp]: "gcd (k, k * n) = k"
paulson@11363
   156
  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
paulson@11363
   157
  done
paulson@11363
   158
paulson@11363
   159
lemma gcd_self [simp]: "gcd (k, k) = k"
paulson@11363
   160
  apply (rule gcd_mult [of k 1, simplified])
paulson@11363
   161
  done
paulson@11363
   162
paulson@11363
   163
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
paulson@11363
   164
  apply (insert gcd_mult_distrib2 [of m k n])
paulson@11363
   165
  apply simp
paulson@11363
   166
  apply (erule_tac t = m in ssubst)
paulson@11363
   167
  apply simp
paulson@11363
   168
  done
paulson@11363
   169
paulson@11363
   170
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
paulson@11363
   171
  apply (blast intro: relprime_dvd_mult dvd_trans)
paulson@11363
   172
  done
paulson@11363
   173
paulson@11363
   174
lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
paulson@11363
   175
  apply (auto simp add: prime_def)
paulson@11363
   176
  apply (drule_tac x = "gcd (p, n)" in spec)
paulson@11363
   177
  apply auto
paulson@11363
   178
  apply (insert gcd_dvd2 [of p n])
paulson@11363
   179
  apply simp
paulson@11363
   180
  done
paulson@11363
   181
paulson@11363
   182
text {*
paulson@11363
   183
  This theorem leads immediately to a proof of the uniqueness of
paulson@11363
   184
  factorization.  If @{term p} divides a product of primes then it is
paulson@11363
   185
  one of those primes.
paulson@11363
   186
*}
paulson@11363
   187
paulson@11363
   188
lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
paulson@11363
   189
  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
paulson@11363
   190
  done
paulson@11363
   191
paulson@11363
   192
paulson@11363
   193
text {* \medskip Addition laws *}
paulson@11363
   194
paulson@11363
   195
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
paulson@11363
   196
  apply (case_tac "n = 0")
paulson@11363
   197
   apply (simp_all add: gcd_non_0)
paulson@11363
   198
  done
paulson@11363
   199
paulson@11363
   200
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
paulson@11363
   201
  apply (rule gcd_commute [THEN trans])
paulson@11363
   202
  apply (subst add_commute)
paulson@11363
   203
  apply (simp add: gcd_add1)
paulson@11363
   204
  apply (rule gcd_commute)
paulson@11363
   205
  done
paulson@11363
   206
paulson@11363
   207
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
paulson@11363
   208
  apply (subst add_commute)
paulson@11363
   209
  apply (rule gcd_add2)
paulson@11363
   210
  done
paulson@11363
   211
paulson@11363
   212
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
paulson@11363
   213
  apply (induct k)
paulson@11363
   214
   apply (simp_all add: gcd_add2 add_assoc)
paulson@11363
   215
  done
paulson@11363
   216
paulson@11363
   217
paulson@11363
   218
text {* \medskip More multiplication laws *}
paulson@11363
   219
paulson@11363
   220
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
paulson@11363
   221
  apply (rule dvd_anti_sym)
paulson@11363
   222
   apply (rule gcd_greatest)
paulson@11363
   223
    apply (rule_tac n = k in relprime_dvd_mult)
paulson@11363
   224
     apply (simp add: gcd_assoc)
paulson@11363
   225
     apply (simp add: gcd_commute)
paulson@11363
   226
    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
paulson@11363
   227
  apply (blast intro: gcd_dvd1 dvd_trans)
paulson@11363
   228
  done
paulson@11363
   229
paulson@11363
   230
end