--- a/src/HOL/Rings.thy Fri Oct 10 19:55:32 2014 +0200
+++ b/src/HOL/Rings.thy Sun Oct 12 16:31:28 2014 +0200
@@ -211,6 +211,35 @@
end
+class semiring_dvd = comm_semiring_1 +
+ assumes dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
+ assumes dvd_addD: "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
+begin
+
+lemma dvd_add_times_triv_right_iff [simp]:
+ "a dvd b + c * a \<longleftrightarrow> a dvd b"
+ using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
+
+lemma dvd_add_triv_left_iff [simp]:
+ "a dvd a + b \<longleftrightarrow> a dvd b"
+ using dvd_add_times_triv_left_iff [of a 1 b] by simp
+
+lemma dvd_add_triv_right_iff [simp]:
+ "a dvd b + a \<longleftrightarrow> a dvd b"
+ using dvd_add_times_triv_right_iff [of a b 1] by simp
+
+lemma dvd_add_eq_right:
+ assumes "a dvd b"
+ shows "a dvd b + c \<longleftrightarrow> a dvd c"
+ using assms by (auto dest: dvd_addD)
+
+lemma dvd_add_eq_left:
+ assumes "a dvd c"
+ shows "a dvd b + c \<longleftrightarrow> a dvd b"
+ using assms dvd_add_eq_right [of a c b] by (simp add: ac_simps)
+
+end
+
class no_zero_divisors = zero + times +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
begin
@@ -324,6 +353,28 @@
subclass ring_1 ..
subclass comm_semiring_1_cancel ..
+subclass semiring_dvd
+proof
+ fix a b c
+ show "a dvd c * a + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
+ proof
+ assume ?Q then show ?P by simp
+ next
+ assume ?P then obtain d where "c * a + b = a * d" ..
+ then have "b = a * (d - c)" by (simp add: algebra_simps)
+ then show ?Q ..
+ qed
+ assume "a dvd b + c" and "a dvd b"
+ show "a dvd c"
+ proof -
+ from `a dvd b` obtain d where "b = a * d" ..
+ moreover from `a dvd b + c` obtain e where "b + c = a * e" ..
+ ultimately have "a * d + c = a * e" by simp
+ then have "c = a * (e - d)" by (simp add: algebra_simps)
+ then show "a dvd c" ..
+ qed
+qed
+
lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
proof
assume "x dvd - y"