# HG changeset patch
# User huffman
# Date 1326203322 -3600
# Node ID c06e868dc339aba8442ed9751bdfb77208dce40d
# Parent  1b2e882f42d2f12146d614c359dc47d775bc4f98
add simp rule test_bit_1

diff -r 1b2e882f42d2 -r c06e868dc339 src/HOL/Word/Examples/WordExamples.thy
--- 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)
diff -r 1b2e882f42d2 -r c06e868dc339 src/HOL/Word/Word.thy
--- 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