equal
deleted
inserted
replaced
264 "of_int (signed a) = a" |
264 "of_int (signed a) = a" |
265 by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps) |
265 by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps) |
266 |
266 |
267 |
267 |
268 subsubsection \<open>Properties\<close> |
268 subsubsection \<open>Properties\<close> |
|
269 |
|
270 lemma exp_eq_zero_iff: |
|
271 \<open>(2 :: 'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a) \<le> n\<close> |
|
272 by transfer simp |
269 |
273 |
270 |
274 |
271 subsubsection \<open>Division\<close> |
275 subsubsection \<open>Division\<close> |
272 |
276 |
273 instantiation word :: (len0) modulo |
277 instantiation word :: (len0) modulo |