--- a/src/HOL/Library/Word.thy Wed Jun 20 05:06:56 2007 +0200
+++ b/src/HOL/Library/Word.thy Wed Jun 20 05:18:39 2007 +0200
@@ -927,12 +927,12 @@
next
fix xs
assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
- show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
+ show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
proof (rule bit_list_cases [of xs], simp_all)
fix ys
assume [simp]: "xs = \<one>#ys"
from ind
- show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
+ show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
by simp
qed
qed
@@ -945,9 +945,9 @@
by (simp add: int_nat_two_exp)
next
fix bs
- have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp
+ have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
also have "... < 2 ^ length bs" by (induct bs) simp_all
- finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" .
+ finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
qed
lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
@@ -959,7 +959,7 @@
next
fix bs
from bv_to_nat_upper_range [of "bv_not bs"]
- show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
+ show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
by (simp add: int_nat_two_exp)
qed