src/HOL/Divides.thy
changeset 35367 45a193f0ed0c
parent 35216 7641e8d831d2
child 35644 d20cf282342e
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 24 14:19:52 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 24 14:19:53 2010 +0100
     1.3 @@ -309,6 +309,15 @@
     1.4    apply (simp add: no_zero_divisors)
     1.5    done
     1.6  
     1.7 +lemma div_mult_swap:
     1.8 +  assumes "c dvd b"
     1.9 +  shows "a * (b div c) = (a * b) div c"
    1.10 +proof -
    1.11 +  from assms have "b div c * (a div 1) = b * a div (c * 1)"
    1.12 +    by (simp only: div_mult_div_if_dvd one_dvd)
    1.13 +  then show ?thesis by (simp add: mult_commute)
    1.14 +qed
    1.15 +   
    1.16  lemma div_mult_mult2 [simp]:
    1.17    "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
    1.18    by (drule div_mult_mult1) (simp add: mult_commute)
    1.19 @@ -347,6 +356,24 @@
    1.20  apply(simp add: div_mult_div_if_dvd dvd_power_same)
    1.21  done
    1.22  
    1.23 +lemma dvd_div_eq_mult:
    1.24 +  assumes "a \<noteq> 0" and "a dvd b"  
    1.25 +  shows "b div a = c \<longleftrightarrow> b = c * a"
    1.26 +proof
    1.27 +  assume "b = c * a"
    1.28 +  then show "b div a = c" by (simp add: assms)
    1.29 +next
    1.30 +  assume "b div a = c"
    1.31 +  then have "b div a * a = c * a" by simp
    1.32 +  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
    1.33 +  ultimately show "b = c * a" by simp
    1.34 +qed
    1.35 +   
    1.36 +lemma dvd_div_div_eq_mult:
    1.37 +  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
    1.38 +  shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
    1.39 +  using assms by (auto simp add: mult_commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
    1.40 +
    1.41  end
    1.42  
    1.43  class ring_div = semiring_div + idom