summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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