src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Wed Mar 04 10:45:52 2009 +0100
@@ -147,10 +147,10 @@
 lemma one_dvd [simp]: "1 dvd a"
 by (auto intro!: dvdI)
 
-lemma dvd_mult: "a dvd c \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult[simp]: "a dvd c \<Longrightarrow> a dvd (b * c)"
 by (auto intro!: mult_left_commute dvdI elim!: dvdE)
 
-lemma dvd_mult2: "a dvd b \<Longrightarrow> a dvd (b * c)"
+lemma dvd_mult2[simp]: "a dvd b \<Longrightarrow> a dvd (b * c)"
   apply (subst mult_commute)
   apply (erule dvd_mult)
   done
@@ -162,12 +162,12 @@
 by (rule dvd_mult2) (rule dvd_refl)
 
 lemma mult_dvd_mono:
-  assumes ab: "a dvd b"
-    and "cd": "c dvd d"
+  assumes "a dvd b"
+    and "c dvd d"
   shows "a * c dvd b * d"
 proof -
-  from ab obtain b' where "b = a * b'" ..
-  moreover from "cd" obtain d' where "d = c * d'" ..
+  from `a dvd b` obtain b' where "b = a * b'" ..
+  moreover from `c dvd d` obtain d' where "d = c * d'" ..
   ultimately have "b * d = (a * c) * (b' * d')" by (simp add: mult_ac)
   then show ?thesis ..
 qed
@@ -310,8 +310,8 @@
   then show "- x dvd y" ..
 qed
 
-lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
-by (simp add: diff_minus dvd_add dvd_minus_iff)
+lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+by (simp add: diff_minus dvd_minus_iff)
 
 end
 
@@ -384,6 +384,26 @@
   then show "a * a = b * b" by auto
 qed
 
+lemma dvd_mult_cancel_right [simp]:
+  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
+qed
+
+lemma dvd_mult_cancel_left [simp]:
+  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
+qed
+
 end
 
 class division_ring = ring_1 + inverse +