src/HOL/GCD.thy
author nipkow
Fri Jul 08 11:37:53 2005 +0200 (2005-07-08)
changeset 16759 668e72b1c4d7
permissions -rw-r--r--
Used to be in Library/Primes
nipkow@16759
     1
(*  Title:      HOL/GCD.thy
nipkow@16759
     2
    ID:         $Id$
nipkow@16759
     3
    Author:     Christophe Tabacznyj and Lawrence C Paulson
nipkow@16759
     4
    Copyright   1996  University of Cambridge
nipkow@16759
     5
nipkow@16759
     6
Builds on Integ/Parity mainly because that contains recdef, which we
nipkow@16759
     7
need, but also because we may want to include gcd on integers in here
nipkow@16759
     8
as well in the future.
nipkow@16759
     9
*)
nipkow@16759
    10
nipkow@16759
    11
header {* The Greatest Common Divisor *}
nipkow@16759
    12
nipkow@16759
    13
theory GCD
nipkow@16759
    14
imports Parity
nipkow@16759
    15
begin
nipkow@16759
    16
nipkow@16759
    17
text {*
nipkow@16759
    18
  See \cite{davenport92}.
nipkow@16759
    19
  \bigskip
nipkow@16759
    20
*}
nipkow@16759
    21
nipkow@16759
    22
consts
nipkow@16759
    23
  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
nipkow@16759
    24
nipkow@16759
    25
recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
nipkow@16759
    26
  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
nipkow@16759
    27
nipkow@16759
    28
constdefs
nipkow@16759
    29
  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
nipkow@16759
    30
  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
nipkow@16759
    31
    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
nipkow@16759
    32
nipkow@16759
    33
nipkow@16759
    34
lemma gcd_induct:
nipkow@16759
    35
  "(!!m. P m 0) ==>
nipkow@16759
    36
    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
nipkow@16759
    37
  ==> P (m::nat) (n::nat)"
nipkow@16759
    38
  apply (induct m n rule: gcd.induct)
nipkow@16759
    39
  apply (case_tac "n = 0")
nipkow@16759
    40
   apply simp_all
nipkow@16759
    41
  done
nipkow@16759
    42
nipkow@16759
    43
nipkow@16759
    44
lemma gcd_0 [simp]: "gcd (m, 0) = m"
nipkow@16759
    45
  apply simp
nipkow@16759
    46
  done
nipkow@16759
    47
nipkow@16759
    48
lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
nipkow@16759
    49
  apply simp
nipkow@16759
    50
  done
nipkow@16759
    51
nipkow@16759
    52
declare gcd.simps [simp del]
nipkow@16759
    53
nipkow@16759
    54
lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
nipkow@16759
    55
  apply (simp add: gcd_non_0)
nipkow@16759
    56
  done
nipkow@16759
    57
nipkow@16759
    58
text {*
nipkow@16759
    59
  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
nipkow@16759
    60
  conjunctions don't seem provable separately.
nipkow@16759
    61
*}
nipkow@16759
    62
nipkow@16759
    63
lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
nipkow@16759
    64
  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
nipkow@16759
    65
  apply (induct m n rule: gcd_induct)
nipkow@16759
    66
   apply (simp_all add: gcd_non_0)
nipkow@16759
    67
  apply (blast dest: dvd_mod_imp_dvd)
nipkow@16759
    68
  done
nipkow@16759
    69
nipkow@16759
    70
text {*
nipkow@16759
    71
  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
nipkow@16759
    72
  naturals, if @{term k} divides @{term m} and @{term k} divides
nipkow@16759
    73
  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
nipkow@16759
    74
*}
nipkow@16759
    75
nipkow@16759
    76
lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
nipkow@16759
    77
  apply (induct m n rule: gcd_induct)
nipkow@16759
    78
   apply (simp_all add: gcd_non_0 dvd_mod)
nipkow@16759
    79
  done
nipkow@16759
    80
nipkow@16759
    81
lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
nipkow@16759
    82
  apply (blast intro!: gcd_greatest intro: dvd_trans)
nipkow@16759
    83
  done
nipkow@16759
    84
nipkow@16759
    85
lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
nipkow@16759
    86
  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
nipkow@16759
    87
nipkow@16759
    88
nipkow@16759
    89
text {*
nipkow@16759
    90
  \medskip Function gcd yields the Greatest Common Divisor.
nipkow@16759
    91
*}
nipkow@16759
    92
nipkow@16759
    93
lemma is_gcd: "is_gcd (gcd (m, n)) m n"
nipkow@16759
    94
  apply (simp add: is_gcd_def gcd_greatest)
nipkow@16759
    95
  done
nipkow@16759
    96
nipkow@16759
    97
text {*
nipkow@16759
    98
  \medskip Uniqueness of GCDs.
nipkow@16759
    99
*}
nipkow@16759
   100
nipkow@16759
   101
lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
nipkow@16759
   102
  apply (simp add: is_gcd_def)
nipkow@16759
   103
  apply (blast intro: dvd_anti_sym)
nipkow@16759
   104
  done
nipkow@16759
   105
nipkow@16759
   106
lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
nipkow@16759
   107
  apply (auto simp add: is_gcd_def)
nipkow@16759
   108
  done
nipkow@16759
   109
nipkow@16759
   110
nipkow@16759
   111
text {*
nipkow@16759
   112
  \medskip Commutativity
nipkow@16759
   113
*}
nipkow@16759
   114
nipkow@16759
   115
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
nipkow@16759
   116
  apply (auto simp add: is_gcd_def)
nipkow@16759
   117
  done
nipkow@16759
   118
nipkow@16759
   119
lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
nipkow@16759
   120
  apply (rule is_gcd_unique)
nipkow@16759
   121
   apply (rule is_gcd)
nipkow@16759
   122
  apply (subst is_gcd_commute)
nipkow@16759
   123
  apply (simp add: is_gcd)
nipkow@16759
   124
  done
nipkow@16759
   125
nipkow@16759
   126
lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
nipkow@16759
   127
  apply (rule is_gcd_unique)
nipkow@16759
   128
   apply (rule is_gcd)
nipkow@16759
   129
  apply (simp add: is_gcd_def)
nipkow@16759
   130
  apply (blast intro: dvd_trans)
nipkow@16759
   131
  done
nipkow@16759
   132
nipkow@16759
   133
lemma gcd_0_left [simp]: "gcd (0, m) = m"
nipkow@16759
   134
  apply (simp add: gcd_commute [of 0])
nipkow@16759
   135
  done
nipkow@16759
   136
nipkow@16759
   137
lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
nipkow@16759
   138
  apply (simp add: gcd_commute [of "Suc 0"])
nipkow@16759
   139
  done
nipkow@16759
   140
nipkow@16759
   141
nipkow@16759
   142
text {*
nipkow@16759
   143
  \medskip Multiplication laws
nipkow@16759
   144
*}
nipkow@16759
   145
nipkow@16759
   146
lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
nipkow@16759
   147
    -- {* \cite[page 27]{davenport92} *}
nipkow@16759
   148
  apply (induct m n rule: gcd_induct)
nipkow@16759
   149
   apply simp
nipkow@16759
   150
  apply (case_tac "k = 0")
nipkow@16759
   151
   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
nipkow@16759
   152
  done
nipkow@16759
   153
nipkow@16759
   154
lemma gcd_mult [simp]: "gcd (k, k * n) = k"
nipkow@16759
   155
  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
nipkow@16759
   156
  done
nipkow@16759
   157
nipkow@16759
   158
lemma gcd_self [simp]: "gcd (k, k) = k"
nipkow@16759
   159
  apply (rule gcd_mult [of k 1, simplified])
nipkow@16759
   160
  done
nipkow@16759
   161
nipkow@16759
   162
lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
nipkow@16759
   163
  apply (insert gcd_mult_distrib2 [of m k n])
nipkow@16759
   164
  apply simp
nipkow@16759
   165
  apply (erule_tac t = m in ssubst)
nipkow@16759
   166
  apply simp
nipkow@16759
   167
  done
nipkow@16759
   168
nipkow@16759
   169
lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
nipkow@16759
   170
  apply (blast intro: relprime_dvd_mult dvd_trans)
nipkow@16759
   171
  done
nipkow@16759
   172
nipkow@16759
   173
lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
nipkow@16759
   174
  apply (rule dvd_anti_sym)
nipkow@16759
   175
   apply (rule gcd_greatest)
nipkow@16759
   176
    apply (rule_tac n = k in relprime_dvd_mult)
nipkow@16759
   177
     apply (simp add: gcd_assoc)
nipkow@16759
   178
     apply (simp add: gcd_commute)
nipkow@16759
   179
    apply (simp_all add: mult_commute)
nipkow@16759
   180
  apply (blast intro: dvd_trans)
nipkow@16759
   181
  done
nipkow@16759
   182
nipkow@16759
   183
nipkow@16759
   184
text {* \medskip Addition laws *}
nipkow@16759
   185
nipkow@16759
   186
lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
nipkow@16759
   187
  apply (case_tac "n = 0")
nipkow@16759
   188
   apply (simp_all add: gcd_non_0)
nipkow@16759
   189
  done
nipkow@16759
   190
nipkow@16759
   191
lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
nipkow@16759
   192
proof -
nipkow@16759
   193
  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
nipkow@16759
   194
  also have "... = gcd (n + m, m)" by (simp add: add_commute)
nipkow@16759
   195
  also have "... = gcd (n, m)" by simp
nipkow@16759
   196
  also have  "... = gcd (m, n)" by (rule gcd_commute) 
nipkow@16759
   197
  finally show ?thesis .
nipkow@16759
   198
qed
nipkow@16759
   199
nipkow@16759
   200
lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
nipkow@16759
   201
  apply (subst add_commute)
nipkow@16759
   202
  apply (rule gcd_add2)
nipkow@16759
   203
  done
nipkow@16759
   204
nipkow@16759
   205
lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
nipkow@16759
   206
  apply (induct k)
nipkow@16759
   207
   apply (simp_all add: add_assoc)
nipkow@16759
   208
  done
nipkow@16759
   209
nipkow@16759
   210
end