equal
deleted
inserted
replaced
2153 lemma test_bit_no [simp]: |
2153 lemma test_bit_no [simp]: |
2154 "(number_of w :: 'a::len0 word) !! n \<longleftrightarrow> |
2154 "(number_of w :: 'a::len0 word) !! n \<longleftrightarrow> |
2155 n < len_of TYPE('a) \<and> bin_nth (number_of w) n" |
2155 n < len_of TYPE('a) \<and> bin_nth (number_of w) n" |
2156 unfolding word_number_of_alt test_bit_wi .. |
2156 unfolding word_number_of_alt test_bit_wi .. |
2157 |
2157 |
|
2158 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0" |
|
2159 unfolding word_1_wi test_bit_wi by auto |
|
2160 |
2158 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" |
2161 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" |
2159 unfolding word_test_bit_def by simp |
2162 unfolding word_test_bit_def by simp |
2160 |
2163 |
2161 (* get from commutativity, associativity etc of int_and etc |
2164 (* get from commutativity, associativity etc of int_and etc |
2162 to same for word_and etc *) |
2165 to same for word_and etc *) |