src/HOL/Divides.thy
changeset 63499 9c9a59949887
parent 63417 c184ec919c70
child 63834 6a757f36997e
     1.1 --- a/src/HOL/Divides.thy	Wed Jul 13 15:46:52 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Jul 14 14:43:09 2016 +0200
     1.3 @@ -128,12 +128,12 @@
     1.4    "a mod a = 0"
     1.5    using mod_mult_self2_is_0 [of 1] by simp
     1.6  
     1.7 -lemma div_add_self1 [simp]:
     1.8 +lemma div_add_self1:
     1.9    assumes "b \<noteq> 0"
    1.10    shows "(b + a) div b = a div b + 1"
    1.11    using assms div_mult_self1 [of b a 1] by (simp add: add.commute)
    1.12  
    1.13 -lemma div_add_self2 [simp]:
    1.14 +lemma div_add_self2:
    1.15    assumes "b \<noteq> 0"
    1.16    shows "(a + b) div b = a div b + 1"
    1.17    using assms div_add_self1 [of b a] by (simp add: add.commute)
    1.18 @@ -1116,7 +1116,7 @@
    1.19  proof -
    1.20    from \<open>m \<ge> n\<close> obtain q where "m = n + q"
    1.21      by (auto simp add: le_iff_add)
    1.22 -  with \<open>n > 0\<close> show ?thesis by simp
    1.23 +  with \<open>n > 0\<close> show ?thesis by (simp add: div_add_self1)
    1.24  qed
    1.25  
    1.26  lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0"
    1.27 @@ -2154,7 +2154,7 @@
    1.28  proof -
    1.29    have "k = (k - l) + l" by simp
    1.30    then obtain j where k: "k = j + l" ..
    1.31 -  with assms show ?thesis by simp
    1.32 +  with assms show ?thesis by (simp add: div_add_self2)
    1.33  qed
    1.34  
    1.35  lemma mod_pos_geq: