src/HOL/Library/GCD.thy

   with igcd_pos show "?g' = 1" by simp
 qed
 
 definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
 
-(* ilcm_dvd12 are needed later *)
+lemma dvd_ilcm_self1[simp]: "i dvd ilcm i j"
+by(simp add:ilcm_def dvd_int_iff)
+
+lemma dvd_ilcm_self2[simp]: "j dvd ilcm i j"
+by(simp add:ilcm_def dvd_int_iff)
+
 lemma ilcm_dvd1: 
 assumes anz: "a \<noteq> 0" 
   and bnz: "b \<noteq> 0"
   shows "a dvd (ilcm a b)"
 proof-

   let ?nb = "nat (abs b)"
   have nap: "?na >0" using anz by simp
   have nbp: "?nb >0" using bnz by simp
   from nap nbp have "?nb dvd lcm(?na,?nb)" using lcm_dvd2 by simp
   thus ?thesis by (simp add: ilcm_def dvd_int_iff)
+qed
+
+lemma dvd_imp_dvd_ilcm1:
+  assumes "k dvd i" shows "k dvd (ilcm i j)"
+proof -
+  have "nat(abs k) dvd nat(abs i)" using `k dvd i`
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric]IntDiv.zdvd_abs1)
+  thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
+qed
+
+lemma dvd_imp_dvd_ilcm2:
+  assumes "k dvd j" shows "k dvd (ilcm i j)"
+proof -
+  have "nat(abs k) dvd nat(abs j)" using `k dvd j`
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric]IntDiv.zdvd_abs1)
+  thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
 
 lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
 by (case_tac "d <0", simp_all)
 

  with t1 have "gcd(m,n) \<le> m*n" by arith
 ultimately show "False" by simp
 qed
 
 lemma ilcm_pos: 
-  assumes apos: " 0 < a"
-  and bpos: "0 < b" 
-  shows "0 < ilcm  a b"
+  assumes anz: "a \<noteq> 0"
+  and bnz: "b \<noteq> 0" 
+  shows "0 < ilcm a b"
 proof-
   let ?na = "nat (abs a)"
   let ?nb = "nat (abs b)"
-  have nap: "?na >0" using apos by simp
-  have nbp: "?nb >0" using bpos by simp
+  have nap: "?na >0" using anz by simp
+  have nbp: "?nb >0" using bnz by simp
   have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
   thus ?thesis by (simp add: ilcm_def)
 qed
 
 end