2152 fixes x :: "'a::len0 word" |
2152 fixes x :: "'a::len0 word" |
2153 shows |
2153 shows |
2154 "(x AND y) AND z = x AND y AND z" |
2154 "(x AND y) AND z = x AND y AND z" |
2155 "(x OR y) OR z = x OR y OR z" |
2155 "(x OR y) OR z = x OR y OR z" |
2156 "(x XOR y) XOR z = x XOR y XOR z" |
2156 "(x XOR y) XOR z = x XOR y XOR z" |
2157 using word_of_int_Ex [where x=x] |
2157 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2158 word_of_int_Ex [where x=y] |
|
2159 word_of_int_Ex [where x=z] |
|
2160 by (auto simp: bwsimps bbw_assocs) |
|
2161 |
2158 |
2162 lemma word_bw_comms: |
2159 lemma word_bw_comms: |
2163 fixes x :: "'a::len0 word" |
2160 fixes x :: "'a::len0 word" |
2164 shows |
2161 shows |
2165 "x AND y = y AND x" |
2162 "x AND y = y AND x" |
2166 "x OR y = y OR x" |
2163 "x OR y = y OR x" |
2167 "x XOR y = y XOR x" |
2164 "x XOR y = y XOR x" |
2168 using word_of_int_Ex [where x=x] |
2165 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2169 word_of_int_Ex [where x=y] |
|
2170 by (auto simp: bwsimps bin_ops_comm) |
|
2171 |
2166 |
2172 lemma word_bw_lcs: |
2167 lemma word_bw_lcs: |
2173 fixes x :: "'a::len0 word" |
2168 fixes x :: "'a::len0 word" |
2174 shows |
2169 shows |
2175 "y AND x AND z = x AND y AND z" |
2170 "y AND x AND z = x AND y AND z" |
2176 "y OR x OR z = x OR y OR z" |
2171 "y OR x OR z = x OR y OR z" |
2177 "y XOR x XOR z = x XOR y XOR z" |
2172 "y XOR x XOR z = x XOR y XOR z" |
2178 using word_of_int_Ex [where x=x] |
2173 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2179 word_of_int_Ex [where x=y] |
|
2180 word_of_int_Ex [where x=z] |
|
2181 by (auto simp: bwsimps) |
|
2182 |
2174 |
2183 lemma word_log_esimps [simp]: |
2175 lemma word_log_esimps [simp]: |
2184 fixes x :: "'a::len0 word" |
2176 fixes x :: "'a::len0 word" |
2185 shows |
2177 shows |
2186 "x AND 0 = 0" |
2178 "x AND 0 = 0" |
2201 lemma word_not_dist: |
2193 lemma word_not_dist: |
2202 fixes x :: "'a::len0 word" |
2194 fixes x :: "'a::len0 word" |
2203 shows |
2195 shows |
2204 "NOT (x OR y) = NOT x AND NOT y" |
2196 "NOT (x OR y) = NOT x AND NOT y" |
2205 "NOT (x AND y) = NOT x OR NOT y" |
2197 "NOT (x AND y) = NOT x OR NOT y" |
2206 using word_of_int_Ex [where x=x] |
2198 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2207 word_of_int_Ex [where x=y] |
|
2208 by (auto simp: bwsimps bbw_not_dist) |
|
2209 |
2199 |
2210 lemma word_bw_same: |
2200 lemma word_bw_same: |
2211 fixes x :: "'a::len0 word" |
2201 fixes x :: "'a::len0 word" |
2212 shows |
2202 shows |
2213 "x AND x = x" |
2203 "x AND x = x" |
2225 "y AND x OR x = x" |
2215 "y AND x OR x = x" |
2226 "(y OR x) AND x = x" |
2216 "(y OR x) AND x = x" |
2227 "x OR x AND y = x" |
2217 "x OR x AND y = x" |
2228 "(x OR y) AND x = x" |
2218 "(x OR y) AND x = x" |
2229 "x AND y OR x = x" |
2219 "x AND y OR x = x" |
2230 using word_of_int_Ex [where x=x] |
2220 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2231 word_of_int_Ex [where x=y] |
|
2232 by (auto simp: bwsimps) |
|
2233 |
2221 |
2234 lemma word_not_not [simp]: |
2222 lemma word_not_not [simp]: |
2235 "NOT NOT (x::'a::len0 word) = x" |
2223 "NOT NOT (x::'a::len0 word) = x" |
2236 using word_of_int_Ex [where x=x] |
2224 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2237 by (auto simp: bwsimps) |
|
2238 |
2225 |
2239 lemma word_ao_dist: |
2226 lemma word_ao_dist: |
2240 fixes x :: "'a::len0 word" |
2227 fixes x :: "'a::len0 word" |
2241 shows "(x OR y) AND z = x AND z OR y AND z" |
2228 shows "(x OR y) AND z = x AND z OR y AND z" |
2242 using word_of_int_Ex [where x=x] |
2229 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2243 word_of_int_Ex [where x=y] |
|
2244 word_of_int_Ex [where x=z] |
|
2245 by (auto simp: bwsimps bbw_ao_dist) |
|
2246 |
2230 |
2247 lemma word_oa_dist: |
2231 lemma word_oa_dist: |
2248 fixes x :: "'a::len0 word" |
2232 fixes x :: "'a::len0 word" |
2249 shows "x AND y OR z = (x OR z) AND (y OR z)" |
2233 shows "x AND y OR z = (x OR z) AND (y OR z)" |
2250 using word_of_int_Ex [where x=x] |
2234 by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) |
2251 word_of_int_Ex [where x=y] |
|
2252 word_of_int_Ex [where x=z] |
|
2253 by (auto simp: bwsimps bbw_oa_dist) |
|
2254 |
2235 |
2255 lemma word_add_not [simp]: |
2236 lemma word_add_not [simp]: |
2256 fixes x :: "'a::len0 word" |
2237 fixes x :: "'a::len0 word" |
2257 shows "x + NOT x = -1" |
2238 shows "x + NOT x = -1" |
2258 using word_of_int_Ex [where x=x] |
2239 using word_of_int_Ex [where x=x] |
2443 "(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n" |
2424 "(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n" |
2444 unfolding word_test_bit_def word_number_of_def word_size |
2425 unfolding word_test_bit_def word_number_of_def word_size |
2445 by (simp add : nth_bintr [symmetric] word_ubin.eq_norm) |
2426 by (simp add : nth_bintr [symmetric] word_ubin.eq_norm) |
2446 |
2427 |
2447 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" |
2428 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" |
2448 unfolding test_bit_no word_0_no by auto |
2429 unfolding word_test_bit_def by simp |
2449 |
2430 |
2450 lemma nth_sint: |
2431 lemma nth_sint: |
2451 fixes w :: "'a::len word" |
2432 fixes w :: "'a::len word" |
2452 defines "l \<equiv> len_of TYPE ('a)" |
2433 defines "l \<equiv> len_of TYPE ('a)" |
2453 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" |
2434 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" |