306 apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq) |
306 apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq) |
307 done |
307 done |
308 |
308 |
309 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n" |
309 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n" |
310 apply (induct n arbitrary: w) |
310 apply (induct n arbitrary: w) |
311 apply simp |
311 apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE) |
312 apply (subst mod_add_left_eq) |
312 apply (smt pos_zmod_mult_2 zle2p) |
313 apply (simp add: bin_last_def) |
313 apply (simp add: mult_mod_right) |
314 apply arith |
314 done |
315 apply (simp add: bin_last_def bin_rest_def Bit_def) |
315 |
316 apply (clarsimp simp: mod_mult_mult1 [symmetric] |
|
317 mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) |
|
318 apply (rule trans [symmetric, OF _ emep1]) |
|
319 apply auto |
|
320 done |
|
321 |
316 |
322 subsection "Simplifications for (s)bintrunc" |
317 subsection "Simplifications for (s)bintrunc" |
323 |
318 |
324 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0" |
319 lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0" |
325 by (induct n) auto |
320 by (induct n) auto |
645 |
640 |
646 lemma sbintrunc_dec: |
641 lemma sbintrunc_dec: |
647 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
642 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
648 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
643 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
649 |
644 |
650 lemmas zmod_uminus' = zminus_zmod [where m=c] for c |
|
651 lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k |
|
652 |
|
653 lemmas brdmod1s' [symmetric] = |
|
654 mod_add_left_eq mod_add_right_eq |
|
655 mod_diff_left_eq mod_diff_right_eq |
|
656 mod_mult_left_eq mod_mult_right_eq |
|
657 |
|
658 lemmas brdmods' [symmetric] = |
|
659 zpower_zmod' [symmetric] |
|
660 trans [OF mod_add_left_eq mod_add_right_eq] |
|
661 trans [OF mod_diff_left_eq mod_diff_right_eq] |
|
662 trans [OF mod_mult_right_eq mod_mult_left_eq] |
|
663 zmod_uminus' [symmetric] |
|
664 mod_add_left_eq [where b = "1::int"] |
|
665 mod_diff_left_eq [where b = "1::int"] |
|
666 |
|
667 lemmas bintr_arith1s = |
|
668 brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n |
|
669 lemmas bintr_ariths = |
|
670 brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n |
|
671 |
|
672 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] |
645 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] |
673 |
646 |
674 lemma bintr_ge0: "0 \<le> bintrunc n w" |
647 lemma bintr_ge0: "0 \<le> bintrunc n w" |
675 by (simp add: bintrunc_mod2p) |
648 by (simp add: bintrunc_mod2p) |
676 |
649 |