Used to be in Library/Primes
authornipkow
Fri Jul 08 11:37:53 2005 +0200 (2005-07-08)
changeset 16759668e72b1c4d7
parent 16758 c32334d98fcd
child 16760 5c5f051aaaaa
Used to be in Library/Primes
src/HOL/GCD.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/GCD.thy	Fri Jul 08 11:37:53 2005 +0200
     1.3 @@ -0,0 +1,210 @@
     1.4 +(*  Title:      HOL/GCD.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Builds on Integ/Parity mainly because that contains recdef, which we
    1.10 +need, but also because we may want to include gcd on integers in here
    1.11 +as well in the future.
    1.12 +*)
    1.13 +
    1.14 +header {* The Greatest Common Divisor *}
    1.15 +
    1.16 +theory GCD
    1.17 +imports Parity
    1.18 +begin
    1.19 +
    1.20 +text {*
    1.21 +  See \cite{davenport92}.
    1.22 +  \bigskip
    1.23 +*}
    1.24 +
    1.25 +consts
    1.26 +  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
    1.27 +
    1.28 +recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
    1.29 +  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    1.30 +
    1.31 +constdefs
    1.32 +  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
    1.33 +  "is_gcd p m n == p dvd m \<and> p dvd n \<and>
    1.34 +    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
    1.35 +
    1.36 +
    1.37 +lemma gcd_induct:
    1.38 +  "(!!m. P m 0) ==>
    1.39 +    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    1.40 +  ==> P (m::nat) (n::nat)"
    1.41 +  apply (induct m n rule: gcd.induct)
    1.42 +  apply (case_tac "n = 0")
    1.43 +   apply simp_all
    1.44 +  done
    1.45 +
    1.46 +
    1.47 +lemma gcd_0 [simp]: "gcd (m, 0) = m"
    1.48 +  apply simp
    1.49 +  done
    1.50 +
    1.51 +lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    1.52 +  apply simp
    1.53 +  done
    1.54 +
    1.55 +declare gcd.simps [simp del]
    1.56 +
    1.57 +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    1.58 +  apply (simp add: gcd_non_0)
    1.59 +  done
    1.60 +
    1.61 +text {*
    1.62 +  \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    1.63 +  conjunctions don't seem provable separately.
    1.64 +*}
    1.65 +
    1.66 +lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
    1.67 +  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
    1.68 +  apply (induct m n rule: gcd_induct)
    1.69 +   apply (simp_all add: gcd_non_0)
    1.70 +  apply (blast dest: dvd_mod_imp_dvd)
    1.71 +  done
    1.72 +
    1.73 +text {*
    1.74 +  \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    1.75 +  naturals, if @{term k} divides @{term m} and @{term k} divides
    1.76 +  @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    1.77 +*}
    1.78 +
    1.79 +lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    1.80 +  apply (induct m n rule: gcd_induct)
    1.81 +   apply (simp_all add: gcd_non_0 dvd_mod)
    1.82 +  done
    1.83 +
    1.84 +lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    1.85 +  apply (blast intro!: gcd_greatest intro: dvd_trans)
    1.86 +  done
    1.87 +
    1.88 +lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
    1.89 +  by (simp only: dvd_0_left_iff [THEN sym] gcd_greatest_iff)
    1.90 +
    1.91 +
    1.92 +text {*
    1.93 +  \medskip Function gcd yields the Greatest Common Divisor.
    1.94 +*}
    1.95 +
    1.96 +lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    1.97 +  apply (simp add: is_gcd_def gcd_greatest)
    1.98 +  done
    1.99 +
   1.100 +text {*
   1.101 +  \medskip Uniqueness of GCDs.
   1.102 +*}
   1.103 +
   1.104 +lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   1.105 +  apply (simp add: is_gcd_def)
   1.106 +  apply (blast intro: dvd_anti_sym)
   1.107 +  done
   1.108 +
   1.109 +lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   1.110 +  apply (auto simp add: is_gcd_def)
   1.111 +  done
   1.112 +
   1.113 +
   1.114 +text {*
   1.115 +  \medskip Commutativity
   1.116 +*}
   1.117 +
   1.118 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   1.119 +  apply (auto simp add: is_gcd_def)
   1.120 +  done
   1.121 +
   1.122 +lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   1.123 +  apply (rule is_gcd_unique)
   1.124 +   apply (rule is_gcd)
   1.125 +  apply (subst is_gcd_commute)
   1.126 +  apply (simp add: is_gcd)
   1.127 +  done
   1.128 +
   1.129 +lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   1.130 +  apply (rule is_gcd_unique)
   1.131 +   apply (rule is_gcd)
   1.132 +  apply (simp add: is_gcd_def)
   1.133 +  apply (blast intro: dvd_trans)
   1.134 +  done
   1.135 +
   1.136 +lemma gcd_0_left [simp]: "gcd (0, m) = m"
   1.137 +  apply (simp add: gcd_commute [of 0])
   1.138 +  done
   1.139 +
   1.140 +lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
   1.141 +  apply (simp add: gcd_commute [of "Suc 0"])
   1.142 +  done
   1.143 +
   1.144 +
   1.145 +text {*
   1.146 +  \medskip Multiplication laws
   1.147 +*}
   1.148 +
   1.149 +lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   1.150 +    -- {* \cite[page 27]{davenport92} *}
   1.151 +  apply (induct m n rule: gcd_induct)
   1.152 +   apply simp
   1.153 +  apply (case_tac "k = 0")
   1.154 +   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   1.155 +  done
   1.156 +
   1.157 +lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   1.158 +  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   1.159 +  done
   1.160 +
   1.161 +lemma gcd_self [simp]: "gcd (k, k) = k"
   1.162 +  apply (rule gcd_mult [of k 1, simplified])
   1.163 +  done
   1.164 +
   1.165 +lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   1.166 +  apply (insert gcd_mult_distrib2 [of m k n])
   1.167 +  apply simp
   1.168 +  apply (erule_tac t = m in ssubst)
   1.169 +  apply simp
   1.170 +  done
   1.171 +
   1.172 +lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   1.173 +  apply (blast intro: relprime_dvd_mult dvd_trans)
   1.174 +  done
   1.175 +
   1.176 +lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   1.177 +  apply (rule dvd_anti_sym)
   1.178 +   apply (rule gcd_greatest)
   1.179 +    apply (rule_tac n = k in relprime_dvd_mult)
   1.180 +     apply (simp add: gcd_assoc)
   1.181 +     apply (simp add: gcd_commute)
   1.182 +    apply (simp_all add: mult_commute)
   1.183 +  apply (blast intro: dvd_trans)
   1.184 +  done
   1.185 +
   1.186 +
   1.187 +text {* \medskip Addition laws *}
   1.188 +
   1.189 +lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   1.190 +  apply (case_tac "n = 0")
   1.191 +   apply (simp_all add: gcd_non_0)
   1.192 +  done
   1.193 +
   1.194 +lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   1.195 +proof -
   1.196 +  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
   1.197 +  also have "... = gcd (n + m, m)" by (simp add: add_commute)
   1.198 +  also have "... = gcd (n, m)" by simp
   1.199 +  also have  "... = gcd (m, n)" by (rule gcd_commute) 
   1.200 +  finally show ?thesis .
   1.201 +qed
   1.202 +
   1.203 +lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   1.204 +  apply (subst add_commute)
   1.205 +  apply (rule gcd_add2)
   1.206 +  done
   1.207 +
   1.208 +lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   1.209 +  apply (induct k)
   1.210 +   apply (simp_all add: add_assoc)
   1.211 +  done
   1.212 +
   1.213 +end