src/HOL/GCD.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 16759 668e72b1c4d7
permissions -rw-r--r--
simplified code generator setup
     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