author haftmann Tue Jul 10 09:23:13 2007 +0200 (2007-07-10) changeset 23687 06884f7ffb18 parent 23686 9d5671f61b31 child 23688 7cd68def72b2
extended - convers now basic lcm properties also
 src/HOL/Library/GCD.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:12 2007 +0200
1.2 +++ b/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:13 2007 +0200
1.3 @@ -11,43 +11,64 @@
1.4  begin
1.5
1.6  text {*
1.7 -  See \cite{davenport92}.
1.8 -  \bigskip
1.9 +  See \cite{davenport92}. \bigskip
1.10  *}
1.11
1.12 -consts
1.13 -  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
1.14 -
1.15 -recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
1.16 -  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
1.17 +subsection {* Specification of GCD on nats *}
1.18
1.19  definition
1.20 -  is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *}
1.21 -  "is_gcd p m n = (p dvd m \<and> p dvd n \<and>
1.22 -    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))"
1.23 +  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
1.24 +  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
1.25 +    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
1.26 +
1.27 +text {* Uniqueness *}
1.28 +
1.29 +lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
1.30 +  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
1.31 +
1.32 +text {* Connection to divides relation *}
1.33
1.34 +lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
1.35 +  by (auto simp add: is_gcd_def)
1.36 +
1.37 +text {* Commutativity *}
1.38 +
1.39 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
1.40 +  by (auto simp add: is_gcd_def)
1.41 +
1.42 +
1.43 +subsection {* GCD on nat by Euclid's algorithm *}
1.44 +
1.45 +fun
1.46 +  gcd  :: "nat \<times> nat => nat"
1.47 +where
1.48 +  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
1.49
1.50  lemma gcd_induct:
1.51 -  "(!!m. P m 0) ==>
1.52 -    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
1.53 -  ==> P (m::nat) (n::nat)"
1.54 -  apply (induct m n rule: gcd.induct)
1.55 -  apply (case_tac "n = 0")
1.56 -   apply simp_all
1.57 -  done
1.58 -
1.59 +  fixes m n :: nat
1.60 +  assumes "\<And>m. P m 0"
1.61 +    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
1.62 +  shows "P m n"
1.63 +apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
1.64 +apply (case_tac "n = 0")
1.65 +apply simp_all
1.66 +using assms apply simp_all
1.67 +done
1.68
1.69  lemma gcd_0 [simp]: "gcd (m, 0) = m"
1.70    by simp
1.71
1.72 -lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
1.73 +lemma gcd_0_left [simp]: "gcd (0, m) = m"
1.74 +  by simp
1.75 +
1.76 +lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
1.77 +  by simp
1.78 +
1.79 +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
1.80    by simp
1.81
1.82  declare gcd.simps [simp del]
1.83
1.84 -lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
1.85 -  by (simp add: gcd_non_0)
1.86 -
1.87  text {*
1.88    \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
1.89    conjunctions don't seem provable separately.
1.90 @@ -66,45 +87,24 @@
1.91    @{term n} then @{term k} divides @{term "gcd (m, n)"}.
1.92  *}
1.93
1.94 -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
1.95 +lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
1.96    by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
1.97
1.98 -lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
1.99 -  by (blast intro!: gcd_greatest intro: dvd_trans)
1.100 -
1.101 -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
1.102 -  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
1.103 -
1.104 -
1.105  text {*
1.106    \medskip Function gcd yields the Greatest Common Divisor.
1.107  *}
1.108
1.109  lemma is_gcd: "is_gcd (gcd (m, n)) m n"
1.110 -  apply (simp add: is_gcd_def gcd_greatest)
1.111 -  done
1.112 -
1.113 -text {*
1.114 -  \medskip Uniqueness of GCDs.
1.115 -*}
1.116 -
1.117 -lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
1.118 -  apply (simp add: is_gcd_def)
1.119 -  apply (blast intro: dvd_anti_sym)
1.120 -  done
1.121 -
1.122 -lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
1.123 -  apply (auto simp add: is_gcd_def)
1.124 -  done
1.125 +  by (simp add: is_gcd_def gcd_greatest)
1.126
1.127
1.128 -text {*
1.129 -  \medskip Commutativity
1.130 -*}
1.131 +subsection {* Derived laws for GCD *}
1.132
1.133 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
1.134 -  apply (auto simp add: is_gcd_def)
1.135 -  done
1.136 +lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
1.137 +  by (blast intro!: gcd_greatest intro: dvd_trans)
1.138 +
1.139 +lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
1.140 +  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
1.141
1.142  lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
1.143    apply (rule is_gcd_unique)
1.144 @@ -120,14 +120,8 @@
1.145    apply (blast intro: dvd_trans)
1.146    done
1.147
1.148 -lemma gcd_0_left [simp]: "gcd (0, m) = m"
1.149 -  apply (simp add: gcd_commute [of 0])
1.150 -  done
1.151 -
1.152  lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
1.153 -  apply (simp add: gcd_commute [of "Suc 0"])
1.154 -  done
1.155 -
1.156 +  by (simp add: gcd_commute)
1.157
1.158  text {*
1.159    \medskip Multiplication laws
1.160 @@ -195,6 +189,8 @@
1.161  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
1.163
1.164 +lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
1.165 +  using mult_dvd_mono [of 1] by auto
1.166
1.167  text {*
1.168    \medskip Division by gcd yields rrelatively primes.
1.169 @@ -223,10 +219,115 @@
1.170    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
1.171  qed
1.172
1.173 +subsection {* LCM defined by GCD *}
1.174
1.175 -text {*
1.176 -  \medskip Gcd on integers.
1.177 -*}
1.178 +definition
1.179 +  lcm :: "nat \<times> nat \<Rightarrow> nat"
1.180 +where
1.181 +  "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
1.182 +
1.183 +lemma lcm_def:
1.184 +  "lcm (m, n) = m * n div gcd (m, n)"
1.185 +  unfolding lcm_def by simp
1.186 +
1.187 +lemma prod_gcd_lcm:
1.188 +  "m * n = gcd (m, n) * lcm (m, n)"
1.189 +  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
1.190 +
1.191 +lemma lcm_0 [simp]: "lcm (m, 0) = 0"
1.192 +  unfolding lcm_def by simp
1.193 +
1.194 +lemma lcm_1 [simp]: "lcm (m, 1) = m"
1.195 +  unfolding lcm_def by simp
1.196 +
1.197 +lemma lcm_0_left [simp]: "lcm (0, n) = 0"
1.198 +  unfolding lcm_def by simp
1.199 +
1.200 +lemma lcm_1_left [simp]: "lcm (1, m) = m"
1.201 +  unfolding lcm_def by simp
1.202 +
1.203 +lemma dvd_pos:
1.204 +  fixes n m :: nat
1.205 +  assumes "n > 0" and "m dvd n"
1.206 +  shows "m > 0"
1.207 +using assms by (cases m) auto
1.208 +
1.209 +lemma lcm_lowest:
1.210 +  assumes "m dvd k" and "n dvd k"
1.211 +  shows "lcm (m, n) dvd k"
1.212 +proof (cases k)
1.213 +  case 0 then show ?thesis by auto
1.214 +next
1.215 +  case (Suc _) then have pos_k: "k > 0" by auto
1.216 +  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
1.217 +  with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
1.218 +  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
1.219 +  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
1.220 +  from pos_k k_m have pos_p: "p > 0" by auto
1.221 +  from pos_k k_n have pos_q: "q > 0" by auto
1.222 +  have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
1.223 +    by (simp add: mult_ac gcd_mult_distrib2)
1.224 +  also have "\<dots> = k * gcd (m * p * q, n * q * p)"
1.225 +    by (simp add: k_m [symmetric] k_n [symmetric])
1.226 +  also have "\<dots> = k * p * q * gcd (m, n)"
1.227 +    by (simp add: mult_ac gcd_mult_distrib2)
1.228 +  finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
1.229 +    by (simp only: k_m [symmetric] k_n [symmetric])
1.230 +  then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
1.231 +    by (simp add: mult_ac)
1.232 +  with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
1.233 +    by simp
1.234 +  with prod_gcd_lcm [of m n]
1.235 +  have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
1.236 +    by (simp add: mult_ac)
1.237 +  with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
1.238 +  then show ?thesis using dvd_def by auto
1.239 +qed
1.240 +
1.241 +lemma lcm_dvd1 [iff]:
1.242 +  "m dvd lcm (m, n)"
1.243 +proof (cases m)
1.244 +  case 0 then show ?thesis by simp
1.245 +next
1.246 +  case (Suc _)
1.247 +  then have mpos: "m > 0" by simp
1.248 +  show ?thesis
1.249 +  proof (cases n)
1.250 +    case 0 then show ?thesis by simp
1.251 +  next
1.252 +    case (Suc _)
1.253 +    then have npos: "n > 0" by simp
1.254 +    have "gcd (m, n) dvd n" by simp
1.255 +    then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
1.256 +    then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
1.257 +    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
1.258 +    finally show ?thesis by (simp add: lcm_def)
1.259 +  qed
1.260 +qed
1.261 +
1.262 +lemma lcm_dvd2 [iff]:
1.263 +  "n dvd lcm (m, n)"
1.264 +proof (cases n)
1.265 +  case 0 then show ?thesis by simp
1.266 +next
1.267 +  case (Suc _)
1.268 +  then have npos: "n > 0" by simp
1.269 +  show ?thesis
1.270 +  proof (cases m)
1.271 +    case 0 then show ?thesis by simp
1.272 +  next
1.273 +    case (Suc _)
1.274 +    then have mpos: "m > 0" by simp
1.275 +    have "gcd (m, n) dvd m" by simp
1.276 +    then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
1.277 +    then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
1.278 +    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
1.279 +    finally show ?thesis by (simp add: lcm_def)
1.280 +  qed
1.281 +qed
1.282 +
1.283 +
1.284 +subsection {* GCD and LCM on integers *}
1.285
1.286  definition
1.287    igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
1.288 @@ -316,37 +417,9 @@
1.289    with igcd_pos show "?g' = 1" by simp
1.290  qed
1.291
1.292 -text{* LCM *}
1.293 -
1.294 -definition "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
1.295 -
1.296  definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
1.297
1.298  (* ilcm_dvd12 are needed later *)
1.299 -lemma lcm_dvd1:
1.300 -  assumes mpos: " m >0"
1.301 -  and npos: "n>0"
1.302 -  shows "m dvd (lcm(m,n))"
1.303 -proof-
1.304 -  have "gcd(m,n) dvd n" by simp
1.305 -  then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
1.306 -  then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
1.307 -  also have "\<dots> = m*k" using mpos npos gcd_zero by simp
1.308 -  finally show ?thesis by (simp add: lcm_def)
1.309 -qed
1.310 -
1.311 -lemma lcm_dvd2:
1.312 -  assumes mpos: " m >0"
1.313 -  and npos: "n>0"
1.314 -  shows "n dvd (lcm(m,n))"
1.315 -proof-
1.316 -  have "gcd(m,n) dvd m" by simp
1.317 -  then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
1.318 -  then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
1.319 -  also have "\<dots> = n*k" using mpos npos gcd_zero by simp
1.320 -  finally show ?thesis by (simp add: lcm_def)
1.321 -qed
1.322 -
1.323  lemma ilcm_dvd1:
1.324  assumes anz: "a \<noteq> 0"
1.325    and bnz: "b \<noteq> 0"
1.326 @@ -360,7 +433,6 @@
1.327    thus ?thesis by (simp add: ilcm_def dvd_int_iff)
1.328  qed
1.329
1.330 -
1.331  lemma ilcm_dvd2:
1.332  assumes anz: "a \<noteq> 0"
1.333    and bnz: "b \<noteq> 0"
1.334 @@ -389,7 +461,6 @@
1.335    assumes mpos: "m > 0"
1.336    and npos: "n>0"
1.337    shows "lcm (m,n) > 0"
1.338 -
1.339  proof(rule ccontr, simp add: lcm_def gcd_zero)
1.340  assume h:"m*n div gcd(m,n) = 0"
1.341  from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
1.342 @@ -419,5 +490,4 @@
1.343    thus ?thesis by (simp add: ilcm_def)
1.344  qed
1.345
1.346 -
1.347  end
```