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