generalised lemma
authorhaftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 5422224874b4024d1
parent 54221 56587960e444
child 54223 85705ba18add
generalised lemma
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Nat.thy
src/HOL/Number_Theory/Eratosthenes.thy
     1.1 --- a/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -1872,12 +1872,12 @@
     1.4    shows "m dvd n + q \<longleftrightarrow> m dvd n"
     1.5    using assms by (simp add: dvd_plus_eq_right add_commute [of n])
     1.6  
     1.7 -lemma less_dvd_minus:
     1.8 +lemma less_eq_dvd_minus:
     1.9    fixes m n :: nat
    1.10 -  assumes "m < n"
    1.11 -  shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
    1.12 +  assumes "m \<le> n"
    1.13 +  shows "m dvd n \<longleftrightarrow> m dvd n - m"
    1.14  proof -
    1.15 -  from assms have "n = m + (n - m)" by arith
    1.16 +  from assms have "n = m + (n - m)" by simp
    1.17    then obtain q where "n = m + q" ..
    1.18    then show ?thesis by (simp add: dvd_reduce add_commute [of m])
    1.19  qed
     2.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Thu Oct 31 11:44:20 2013 +0100
     2.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Thu Oct 31 11:44:20 2013 +0100
     2.3 @@ -75,7 +75,7 @@
     2.4  lemma numbers_of_marks_mark_out:
     2.5    "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
     2.6    by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
     2.7 -    nth_enumerate_eq less_dvd_minus)
     2.8 +    nth_enumerate_eq less_eq_dvd_minus)
     2.9  
    2.10  
    2.11  text {* Auxiliary operation for efficient implementation  *}
    2.12 @@ -128,7 +128,7 @@
    2.13      by (simp add: mark_out_aux_def)
    2.14    show ?thesis2
    2.15      by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
    2.16 -      enumerate_Suc_eq in_set_enumerate_eq less_dvd_minus)
    2.17 +      enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus)
    2.18    { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
    2.19      fix q
    2.20      assume "m + n \<le> q"