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