src/HOL/Library/Primes.thy
author paulson
Mon Jan 12 16:51:45 2004 +0100 (2004-01-12)
changeset 14353 79f9fbef9106
parent 13187 e5434b822a96
child 14706 71590b7733b7
permissions -rw-r--r--
Added lemmas to Ring_and_Field with slightly modified simplification rules

Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field

Consolidated integer powers
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
wenzelm@12300
    66
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
wenzelm@12300
    67
  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
paulson@11363
    68
  apply (induct m n rule: gcd_induct)
paulson@11363
    69
   apply (simp_all add: gcd_non_0)
paulson@11363
    70
  apply (blast dest: dvd_mod_imp_dvd)
paulson@11363
    71
  done
paulson@11363
    72
paulson@11363
    73
text {*
paulson@11363
    74
  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
paulson@11363
    75
  naturals, if @{term k} divides @{term m} and @{term k} divides
paulson@11363
    76
  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
paulson@11363
    77
*}
paulson@11363
    78
paulson@11363
    79
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
paulson@11363
    80
  apply (induct m n rule: gcd_induct)
paulson@11363
    81
   apply (simp_all add: gcd_non_0 dvd_mod)
paulson@11363
    82
  done
paulson@11363
    83
paulson@11363
    84
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
paulson@11363
    85
  apply (blast intro!: gcd_greatest intro: dvd_trans)
paulson@11363
    86
  done
paulson@11363
    87
paulson@11374
    88
lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
paulson@11374
    89
  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
paulson@11374
    90
paulson@11363
    91
paulson@11363
    92
text {*
paulson@11363
    93
  \medskip Function gcd yields the Greatest Common Divisor.
paulson@11363
    94
*}
paulson@11363
    95
paulson@11363
    96
lemma is_gcd: "is_gcd (gcd (m, n)) m n"
paulson@11363
    97
  apply (simp add: is_gcd_def gcd_greatest)
paulson@11363
    98
  done
paulson@11363
    99
paulson@11363
   100
text {*
paulson@11363
   101
  \medskip Uniqueness of GCDs.
paulson@11363
   102
*}
paulson@11363
   103
paulson@11363
   104
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
paulson@11363
   105
  apply (simp add: is_gcd_def)
paulson@11363
   106
  apply (blast intro: dvd_anti_sym)
paulson@11363
   107
  done
paulson@11363
   108
paulson@11363
   109
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
paulson@11363
   110
  apply (auto simp add: is_gcd_def)
paulson@11363
   111
  done
paulson@11363
   112
paulson@11363
   113
paulson@11363
   114
text {*
paulson@11363
   115
  \medskip Commutativity
paulson@11363
   116
*}
paulson@11363
   117
paulson@11363
   118
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
paulson@11363
   119
  apply (auto simp add: is_gcd_def)
paulson@11363
   120
  done
paulson@11363
   121
paulson@11363
   122
lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
paulson@11363
   123
  apply (rule is_gcd_unique)
paulson@11363
   124
   apply (rule is_gcd)
paulson@11363
   125
  apply (subst is_gcd_commute)
paulson@11363
   126
  apply (simp add: is_gcd)
paulson@11363
   127
  done
paulson@11363
   128
paulson@11363
   129
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
paulson@11363
   130
  apply (rule is_gcd_unique)
paulson@11363
   131
   apply (rule is_gcd)
paulson@11363
   132
  apply (simp add: is_gcd_def)
paulson@11363
   133
  apply (blast intro: dvd_trans)
paulson@11363
   134
  done
paulson@11363
   135
paulson@11363
   136
lemma gcd_0_left [simp]: "gcd (0, m) = m"
paulson@11363
   137
  apply (simp add: gcd_commute [of 0])
paulson@11363
   138
  done
paulson@11363
   139
wenzelm@11701
   140
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
wenzelm@11701
   141
  apply (simp add: gcd_commute [of "Suc 0"])
paulson@11363
   142
  done
paulson@11363
   143
paulson@11363
   144
paulson@11363
   145
text {*
paulson@11363
   146
  \medskip Multiplication laws
paulson@11363
   147
*}
paulson@11363
   148
paulson@11363
   149
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
wenzelm@11368
   150
    -- {* \cite[page 27]{davenport92} *}
paulson@11363
   151
  apply (induct m n rule: gcd_induct)
paulson@11363
   152
   apply simp
paulson@11363
   153
  apply (case_tac "k = 0")
paulson@11363
   154
   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
paulson@11363
   155
  done
paulson@11363
   156
paulson@11363
   157
lemma gcd_mult [simp]: "gcd (k, k * n) = k"
paulson@11363
   158
  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
paulson@11363
   159
  done
paulson@11363
   160
paulson@11363
   161
lemma gcd_self [simp]: "gcd (k, k) = k"
paulson@11363
   162
  apply (rule gcd_mult [of k 1, simplified])
paulson@11363
   163
  done
paulson@11363
   164
paulson@11363
   165
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
paulson@11363
   166
  apply (insert gcd_mult_distrib2 [of m k n])
paulson@11363
   167
  apply simp
paulson@11363
   168
  apply (erule_tac t = m in ssubst)
paulson@11363
   169
  apply simp
paulson@11363
   170
  done
paulson@11363
   171
paulson@11363
   172
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
paulson@11363
   173
  apply (blast intro: relprime_dvd_mult dvd_trans)
paulson@11363
   174
  done
paulson@11363
   175
paulson@11363
   176
lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
paulson@11363
   177
  apply (auto simp add: prime_def)
paulson@11363
   178
  apply (drule_tac x = "gcd (p, n)" in spec)
paulson@11363
   179
  apply auto
paulson@11363
   180
  apply (insert gcd_dvd2 [of p n])
paulson@11363
   181
  apply simp
paulson@11363
   182
  done
paulson@11363
   183
wenzelm@13032
   184
lemma two_is_prime: "2 \<in> prime"
wenzelm@13032
   185
  apply (auto simp add: prime_def)
wenzelm@13032
   186
  apply (case_tac m)
wenzelm@13032
   187
   apply (auto dest!: dvd_imp_le)
wenzelm@13032
   188
  done
wenzelm@13032
   189
paulson@11363
   190
text {*
paulson@11363
   191
  This theorem leads immediately to a proof of the uniqueness of
paulson@11363
   192
  factorization.  If @{term p} divides a product of primes then it is
paulson@11363
   193
  one of those primes.
paulson@11363
   194
*}
paulson@11363
   195
paulson@11363
   196
lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
wenzelm@12739
   197
  by (blast intro: relprime_dvd_mult prime_imp_relprime)
paulson@11363
   198
wenzelm@11701
   199
lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
wenzelm@12739
   200
  by (auto dest: prime_dvd_mult)
wenzelm@12739
   201
wenzelm@12739
   202
lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
paulson@14353
   203
  by (rule prime_dvd_square) (simp_all add: power2_eq_square)
wenzelm@11368
   204
paulson@11363
   205
paulson@11363
   206
text {* \medskip Addition laws *}
paulson@11363
   207
paulson@11363
   208
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
paulson@11363
   209
  apply (case_tac "n = 0")
paulson@11363
   210
   apply (simp_all add: gcd_non_0)
paulson@11363
   211
  done
paulson@11363
   212
paulson@11363
   213
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
paulson@11363
   214
  apply (rule gcd_commute [THEN trans])
paulson@11363
   215
  apply (subst add_commute)
paulson@11363
   216
  apply (simp add: gcd_add1)
paulson@11363
   217
  apply (rule gcd_commute)
paulson@11363
   218
  done
paulson@11363
   219
paulson@11363
   220
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
paulson@11363
   221
  apply (subst add_commute)
paulson@11363
   222
  apply (rule gcd_add2)
paulson@11363
   223
  done
paulson@11363
   224
paulson@11363
   225
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
paulson@11363
   226
  apply (induct k)
paulson@11363
   227
   apply (simp_all add: gcd_add2 add_assoc)
paulson@11363
   228
  done
paulson@11363
   229
paulson@11363
   230
paulson@11363
   231
text {* \medskip More multiplication laws *}
paulson@11363
   232
paulson@11363
   233
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
paulson@11363
   234
  apply (rule dvd_anti_sym)
paulson@11363
   235
   apply (rule gcd_greatest)
paulson@11363
   236
    apply (rule_tac n = k in relprime_dvd_mult)
paulson@11363
   237
     apply (simp add: gcd_assoc)
paulson@11363
   238
     apply (simp add: gcd_commute)
paulson@11363
   239
    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
paulson@11363
   240
  apply (blast intro: gcd_dvd1 dvd_trans)
paulson@11363
   241
  done
paulson@11363
   242
paulson@11363
   243
end