equal
deleted
inserted
replaced
243 lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n" |
243 lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n" |
244 by (fact take_bit_eq_mod) |
244 by (fact take_bit_eq_mod) |
245 |
245 |
246 abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
246 abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
247 where \<open>sbintrunc \<equiv> signed_take_bit\<close> |
247 where \<open>sbintrunc \<equiv> signed_take_bit\<close> |
|
248 |
|
249 abbreviation (input) norm_sint :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
|
250 where \<open>norm_sint n \<equiv> signed_take_bit (n - 1)\<close> |
248 |
251 |
249 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n" |
252 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n" |
250 by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift) |
253 by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift) |
251 |
254 |
252 lemma sbintrunc_eq_take_bit: |
255 lemma sbintrunc_eq_take_bit: |