src/HOL/Library/GCD.thy
 changeset 23244 1630951f0512 parent 22367 6860f09242bf child 23365 f31794033ae1
```     1.1 --- a/src/HOL/Library/GCD.thy	Tue Jun 05 09:56:19 2007 +0200
1.2 +++ b/src/HOL/Library/GCD.thy	Tue Jun 05 10:42:31 2007 +0200
1.3 @@ -316,4 +316,108 @@
1.4    with igcd_pos show "?g' = 1" by simp
1.5  qed
1.6
1.7 +text{* LCM *}
1.8 +
1.9 +definition "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
1.10 +
1.11 +definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
1.12 +
1.13 +(* ilcm_dvd12 are needed later *)
1.14 +lemma lcm_dvd1:
1.15 +  assumes mpos: " m >0"
1.16 +  and npos: "n>0"
1.17 +  shows "m dvd (lcm(m,n))"
1.18 +proof-
1.19 +  have "gcd(m,n) dvd n" by simp
1.20 +  then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
1.21 +  then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
1.22 +  also have "\<dots> = m*k" using mpos npos gcd_zero by simp
1.23 +  finally show ?thesis by (simp add: lcm_def)
1.24 +qed
1.25 +
1.26 +lemma lcm_dvd2:
1.27 +  assumes mpos: " m >0"
1.28 +  and npos: "n>0"
1.29 +  shows "n dvd (lcm(m,n))"
1.30 +proof-
1.31 +  have "gcd(m,n) dvd m" by simp
1.32 +  then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
1.33 +  then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
1.34 +  also have "\<dots> = n*k" using mpos npos gcd_zero by simp
1.35 +  finally show ?thesis by (simp add: lcm_def)
1.36 +qed
1.37 +
1.38 +lemma ilcm_dvd1:
1.39 +assumes anz: "a \<noteq> 0"
1.40 +  and bnz: "b \<noteq> 0"
1.41 +  shows "a dvd (ilcm a b)"
1.42 +proof-
1.43 +  let ?na = "nat (abs a)"
1.44 +  let ?nb = "nat (abs b)"
1.45 +  have nap: "?na >0" using anz by simp
1.46 +  have nbp: "?nb >0" using bnz by simp
1.47 +  from nap nbp have "?na dvd lcm(?na,?nb)" using lcm_dvd1 by simp
1.48 +  thus ?thesis by (simp add: ilcm_def dvd_int_iff)
1.49 +qed
1.50 +
1.51 +
1.52 +lemma ilcm_dvd2:
1.53 +assumes anz: "a \<noteq> 0"
1.54 +  and bnz: "b \<noteq> 0"
1.55 +  shows "b dvd (ilcm a b)"
1.56 +proof-
1.57 +  let ?na = "nat (abs a)"
1.58 +  let ?nb = "nat (abs b)"
1.59 +  have nap: "?na >0" using anz by simp
1.60 +  have nbp: "?nb >0" using bnz by simp
1.61 +  from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp
1.62 +  thus ?thesis by (simp add: ilcm_def dvd_int_iff)
1.63 +qed
1.64 +
1.65 +lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
1.66 +by (case_tac "d <0", simp_all)
1.67 +
1.68 +lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
1.69 +by (case_tac "d<0", simp_all)
1.70 +
1.71 +lemma zdvd_abs1: "((d::int) dvd t) = ((abs d) dvd t)"
1.72 + by (cases "d < 0") simp_all
1.73 +
1.74 +(* lcm a b is positive for positive a and b *)
1.75 +
1.76 +lemma lcm_pos:
1.77 +  assumes mpos: "m > 0"
1.78 +  and npos: "n>0"
1.79 +  shows "lcm (m,n) > 0"
1.80 +
1.81 +proof(rule ccontr, simp add: lcm_def gcd_zero)
1.82 +assume h:"m*n div gcd(m,n) = 0"
1.83 +from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
1.84 +hence gcdp: "gcd(m,n) > 0" by simp
1.85 +with h
1.86 +have "m*n < gcd(m,n)"
1.87 +  by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
1.88 +moreover
1.89 +have "gcd(m,n) dvd m" by simp
1.90 + with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
1.91 + with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
1.92 + have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
1.93 + with t1 have "gcd(m,n) \<le> m*n" by arith
1.94 +ultimately show "False" by simp
1.95 +qed
1.96 +
1.97 +lemma ilcm_pos:
1.98 +  assumes apos: " 0 < a"
1.99 +  and bpos: "0 < b"
1.100 +  shows "0 < ilcm  a b"
1.101 +proof-
1.102 +  let ?na = "nat (abs a)"
1.103 +  let ?nb = "nat (abs b)"
1.104 +  have nap: "?na >0" using apos by simp
1.105 +  have nbp: "?nb >0" using bpos by simp
1.106 +  have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
1.107 +  thus ?thesis by (simp add: ilcm_def)
1.108 +qed
1.109 +
1.110 +
1.111  end
```