added lcm, ilcm (lcm for integers) and some lemmas about them;
authorchaieb
Tue Jun 05 10:42:31 2007 +0200 (2007-06-05)
changeset 232441630951f0512
parent 23243 a37d3e6e8323
child 23245 57aee3d85ff3
added lcm, ilcm (lcm for integers) and some lemmas about them;
src/HOL/Library/GCD.thy
     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