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