equal
deleted
inserted
replaced
370 done |
370 done |
371 qed |
371 qed |
372 |
372 |
373 lemma sbintrunc_inc: |
373 lemma sbintrunc_inc: |
374 \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close> |
374 \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close> |
375 using that by (fact signed_take_bit_greater_eq) |
375 using that by (fact signed_take_bit_int_greater_eq) |
376 |
376 |
377 lemma sbintrunc_dec: |
377 lemma sbintrunc_dec: |
378 \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close> |
378 \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close> |
379 using that by (fact signed_take_bit_less_eq) |
379 using that by (fact signed_take_bit_int_less_eq) |
380 |
380 |
381 lemma bintr_ge0: "0 \<le> bintrunc n w" |
381 lemma bintr_ge0: "0 \<le> bintrunc n w" |
382 by (simp add: bintrunc_mod2p) |
382 by (simp add: bintrunc_mod2p) |
383 |
383 |
384 lemma bintr_lt2p: "bintrunc n w < 2 ^ n" |
384 lemma bintr_lt2p: "bintrunc n w < 2 ^ n" |