new lemmas and tuning
authornipkow
Sat Jun 20 01:53:39 2009 +0200 (2009-06-20)
changeset 31729b9299916d618
parent 31728 60317e5211a2
child 31730 d74830dc3e4a
new lemmas and tuning
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Fri Jun 19 22:49:38 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sat Jun 20 01:53:39 2009 +0200
     1.3 @@ -1421,6 +1421,18 @@
     1.4  lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
     1.5    by (subst int_lcm_commute, rule int_lcm_dvd1)
     1.6  
     1.7 +lemma dvd_lcm_if_dvd1_nat: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
     1.8 +by(metis nat_lcm_dvd1 dvd_trans)
     1.9 +
    1.10 +lemma dvd_lcm_if_dvd2_nat: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
    1.11 +by(metis nat_lcm_dvd2 dvd_trans)
    1.12 +
    1.13 +lemma dvd_lcm_if_dvd1_int: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
    1.14 +by(metis int_lcm_dvd1 dvd_trans)
    1.15 +
    1.16 +lemma dvd_lcm_if_dvd2_int: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
    1.17 +by(metis int_lcm_dvd2 dvd_trans)
    1.18 +
    1.19  lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
    1.20      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.21    by (auto intro: dvd_anti_sym nat_lcm_least)