src/HOL/Rings.thy
 changeset 60690 a9e45c9588c3 parent 60688 01488b559910 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
1.2 +++ b/src/HOL/Rings.thy	Wed Jul 08 20:19:12 2015 +0200
1.3 @@ -629,6 +629,44 @@
1.4    then show ?thesis by simp
1.5  qed
1.6
1.7 +lemma divide_1 [simp]:
1.8 +  "a div 1 = a"
1.9 +  using nonzero_mult_divide_cancel_left [of 1 a] by simp
1.10 +
1.11 +lemma dvd_times_left_cancel_iff [simp]:
1.12 +  assumes "a \<noteq> 0"
1.13 +  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.14 +proof
1.15 +  assume ?P then obtain d where "a * c = a * b * d" ..
1.16 +  with assms have "c = b * d" by (simp add: ac_simps)
1.17 +  then show ?Q ..
1.18 +next
1.19 +  assume ?Q then obtain d where "c = b * d" ..
1.20 +  then have "a * c = a * b * d" by (simp add: ac_simps)
1.21 +  then show ?P ..
1.22 +qed
1.23 +
1.24 +lemma dvd_times_right_cancel_iff [simp]:
1.25 +  assumes "a \<noteq> 0"
1.26 +  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.27 +using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
1.28 +
1.29 +lemma div_dvd_iff_mult:
1.30 +  assumes "b \<noteq> 0" and "b dvd a"
1.31 +  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
1.32 +proof -
1.33 +  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
1.34 +  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
1.35 +qed
1.36 +
1.37 +lemma dvd_div_iff_mult:
1.38 +  assumes "c \<noteq> 0" and "c dvd b"
1.39 +  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
1.40 +proof -
1.41 +  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
1.42 +  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
1.43 +qed
1.44 +
1.45  end
1.46
1.47  class idom_divide = idom + semidom_divide
```