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