--- a/src/HOL/Word/Examples/WordExamples.thy Tue Jan 10 10:48:39 2012 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy Tue Jan 10 14:48:42 2012 +0100
@@ -109,7 +109,7 @@
lemma "(0b0010 :: 4 word) !! 1" by simp
lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
-lemma "\<not> (1 :: 3 word) !! 2" apply simp? oops
+lemma "\<not> (1 :: 3 word) !! 2" by simp
lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
--- a/src/HOL/Word/Word.thy Tue Jan 10 10:48:39 2012 +0100
+++ b/src/HOL/Word/Word.thy Tue Jan 10 14:48:42 2012 +0100
@@ -2155,6 +2155,9 @@
n < len_of TYPE('a) \<and> bin_nth (number_of w) n"
unfolding word_number_of_alt test_bit_wi ..
+lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
+ unfolding word_1_wi test_bit_wi by auto
+
lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
unfolding word_test_bit_def by simp