author haftmann Thu Oct 31 11:44:20 2013 +0100 (2013-10-31) changeset 54222 24874b4024d1 parent 54221 56587960e444 child 54223 85705ba18add
generalised lemma
 src/HOL/Decision_Procs/Rat_Pair.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Number_Theory/Eratosthenes.thy file | annotate | diff | revisions
```     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.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.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 @@