--- a/src/HOL/Nat.thy Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Nat.thy Thu Oct 31 11:44:20 2013 +0100
@@ -1872,12 +1872,12 @@
shows "m dvd n + q \<longleftrightarrow> m dvd n"
using assms by (simp add: dvd_plus_eq_right add_commute [of n])
-lemma less_dvd_minus:
+lemma less_eq_dvd_minus:
fixes m n :: nat
- assumes "m < n"
- shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
+ assumes "m \<le> n"
+ shows "m dvd n \<longleftrightarrow> m dvd n - m"
proof -
- from assms have "n = m + (n - m)" by arith
+ from assms have "n = m + (n - m)" by simp
then obtain q where "n = m + q" ..
then show ?thesis by (simp add: dvd_reduce add_commute [of m])
qed
--- a/src/HOL/Number_Theory/Eratosthenes.thy Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy Thu Oct 31 11:44:20 2013 +0100
@@ -75,7 +75,7 @@
lemma numbers_of_marks_mark_out:
"numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
- nth_enumerate_eq less_dvd_minus)
+ nth_enumerate_eq less_eq_dvd_minus)
text {* Auxiliary operation for efficient implementation *}
@@ -128,7 +128,7 @@
by (simp add: mark_out_aux_def)
show ?thesis2
by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
- enumerate_Suc_eq in_set_enumerate_eq less_dvd_minus)
+ enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
{ def v \<equiv> "Suc m" and w \<equiv> "Suc n"
fix q
assume "m + n \<le> q"