# HG changeset patch
# User haftmann
# Date 1267017593 -3600
# Node ID 45a193f0ed0c94dcba5e24ec9bf2b80eea06ff9a
# Parent  6d474096698c6beee976d5443d18162bc70396f3
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult

diff -r 6d474096698c -r 45a193f0ed0c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Feb 24 14:19:52 2010 +0100
+++ b/src/HOL/Divides.thy	Wed Feb 24 14:19:53 2010 +0100
@@ -309,6 +309,15 @@
   apply (simp add: no_zero_divisors)
   done
 
+lemma div_mult_swap:
+  assumes "c dvd b"
+  shows "a * (b div c) = (a * b) div c"
+proof -
+  from assms have "b div c * (a div 1) = b * a div (c * 1)"
+    by (simp only: div_mult_div_if_dvd one_dvd)
+  then show ?thesis by (simp add: mult_commute)
+qed
+   
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   by (drule div_mult_mult1) (simp add: mult_commute)
@@ -347,6 +356,24 @@
 apply(simp add: div_mult_div_if_dvd dvd_power_same)
 done
 
+lemma dvd_div_eq_mult:
+  assumes "a \<noteq> 0" and "a dvd b"  
+  shows "b div a = c \<longleftrightarrow> b = c * a"
+proof
+  assume "b = c * a"
+  then show "b div a = c" by (simp add: assms)
+next
+  assume "b div a = c"
+  then have "b div a * a = c * a" by simp
+  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
+  ultimately show "b = c * a" by simp
+qed
+   
+lemma dvd_div_div_eq_mult:
+  assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
+  shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
+  using assms by (auto simp add: mult_commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
+
 end
 
 class ring_div = semiring_div + idom