--- a/src/HOL/Word/Bit_Representation.thy Tue Mar 27 21:48:55 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Tue Mar 27 21:58:41 2012 +0200
@@ -613,8 +613,7 @@
lemma sb_dec_lem:
"(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
- by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k",
- simplified zless2p, OF _ TrueI, simplified])
+ by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified])
lemma sb_dec_lem':
"(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
--- a/src/HOL/Word/Misc_Numeric.thy Tue Mar 27 21:48:55 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Tue Mar 27 21:58:41 2012 +0200
@@ -172,11 +172,11 @@
lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
-lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
- by (rule zmod_le_nonneg_dividend)
+lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+ by (fact zmod_le_nonneg_dividend) (* FIXME: delete *)
-lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
- by (rule int_mod_le [where a = "b - n" and n = n, simplified])
+lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
+ using zmod_le_nonneg_dividend [of "b - n" "n"] by simp
lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
apply (cases "0 <= a")