src/HOL/Rings.thy
changeset 58647 fce800afeec7
parent 58198 099ca49b5231
child 58649 a62065b5e1e2
     1.1 --- a/src/HOL/Rings.thy	Fri Oct 10 19:55:32 2014 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 12 16:31:28 2014 +0200
     1.3 @@ -211,6 +211,35 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class semiring_dvd = comm_semiring_1 +
     1.8 +  assumes dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \<longleftrightarrow> a dvd b"
     1.9 +  assumes dvd_addD: "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c"
    1.10 +begin
    1.11 +
    1.12 +lemma dvd_add_times_triv_right_iff [simp]:
    1.13 +  "a dvd b + c * a \<longleftrightarrow> a dvd b"
    1.14 +  using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps)
    1.15 +
    1.16 +lemma dvd_add_triv_left_iff [simp]:
    1.17 +  "a dvd a + b \<longleftrightarrow> a dvd b"
    1.18 +  using dvd_add_times_triv_left_iff [of a 1 b] by simp
    1.19 +
    1.20 +lemma dvd_add_triv_right_iff [simp]:
    1.21 +  "a dvd b + a \<longleftrightarrow> a dvd b"
    1.22 +  using dvd_add_times_triv_right_iff [of a b 1] by simp
    1.23 +
    1.24 +lemma dvd_add_eq_right:
    1.25 +  assumes "a dvd b"
    1.26 +  shows "a dvd b + c \<longleftrightarrow> a dvd c"
    1.27 +  using assms by (auto dest: dvd_addD)
    1.28 +
    1.29 +lemma dvd_add_eq_left:
    1.30 +  assumes "a dvd c"
    1.31 +  shows "a dvd b + c \<longleftrightarrow> a dvd b"
    1.32 +  using assms dvd_add_eq_right [of a c b] by (simp add: ac_simps)
    1.33 +
    1.34 +end
    1.35 +
    1.36  class no_zero_divisors = zero + times +
    1.37    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.38  begin
    1.39 @@ -324,6 +353,28 @@
    1.40  subclass ring_1 ..
    1.41  subclass comm_semiring_1_cancel ..
    1.42  
    1.43 +subclass semiring_dvd
    1.44 +proof
    1.45 +  fix a b c
    1.46 +  show "a dvd c * a + b \<longleftrightarrow> a dvd b" (is "?P \<longleftrightarrow> ?Q")
    1.47 +  proof
    1.48 +    assume ?Q then show ?P by simp
    1.49 +  next
    1.50 +    assume ?P then obtain d where "c * a + b = a * d" ..
    1.51 +    then have "b = a * (d - c)" by (simp add: algebra_simps)
    1.52 +    then show ?Q ..
    1.53 +  qed
    1.54 +  assume "a dvd b + c" and "a dvd b"
    1.55 +  show "a dvd c"
    1.56 +  proof -
    1.57 +    from `a dvd b` obtain d where "b = a * d" ..
    1.58 +    moreover from `a dvd b + c` obtain e where "b + c = a * e" ..
    1.59 +    ultimately have "a * d + c = a * e" by simp
    1.60 +    then have "c = a * (e - d)" by (simp add: algebra_simps)
    1.61 +    then show "a dvd c" ..
    1.62 +  qed
    1.63 +qed
    1.64 +
    1.65  lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
    1.66  proof
    1.67    assume "x dvd - y"