src/HOL/Divides.thy
 changeset 60690 a9e45c9588c3 parent 60685 cb21b7022b00 child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Divides.thy	Wed Jul 08 14:01:41 2015 +0200
1.2 +++ b/src/HOL/Divides.thy	Wed Jul 08 20:19:12 2015 +0200
1.3 @@ -118,8 +118,8 @@
1.4  lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
1.5    using mod_mult_self1 [of 0 a b] by simp
1.6
1.7 -lemma div_by_1 [simp]: "a div 1 = a"
1.8 -  using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
1.9 +lemma div_by_1: "a div 1 = a"
1.10 +  by (fact divide_1)
1.11
1.12  lemma mod_by_1 [simp]: "a mod 1 = 0"
1.13  proof -
1.14 @@ -378,20 +378,6 @@
1.15  lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
1.16    by (fact mod_mult_mult1 [symmetric])
1.17
1.18 -lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
1.19 -  assumes "c \<noteq> 0"
1.20 -  shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
1.21 -proof -
1.22 -  have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
1.23 -    using assms by (simp add: mod_mult_mult1)
1.24 -  then show ?thesis by (simp add: mod_eq_0_iff_dvd)
1.25 -qed
1.26 -
1.27 -lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
1.28 -  assumes "c \<noteq> 0"
1.29 -  shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
1.30 -  using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
1.31 -
1.32  lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
1.33    unfolding dvd_def by (auto simp add: mod_mult_mult1)
1.34
```