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