622 |
622 |
623 lemma sbintrunc_dec: |
623 lemma sbintrunc_dec: |
624 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
624 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
625 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
625 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
626 |
626 |
627 lemmas zmod_uminus' = zmod_uminus [where b=c] for c |
627 lemmas zmod_uminus' = zminus_zmod [where m=c] for c |
628 lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k |
628 lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k |
629 |
629 |
630 lemmas brdmod1s' [symmetric] = |
630 lemmas brdmod1s' [symmetric] = |
631 mod_add_left_eq mod_add_right_eq |
631 mod_add_left_eq mod_add_right_eq |
632 zmod_zsub_left_eq zmod_zsub_right_eq |
632 mod_diff_left_eq mod_diff_right_eq |
633 mod_mult_right_eq zmod_zmult1_eq_rev |
633 mod_mult_left_eq mod_mult_right_eq |
634 |
634 |
635 lemmas brdmods' [symmetric] = |
635 lemmas brdmods' [symmetric] = |
636 zpower_zmod' [symmetric] |
636 zpower_zmod' [symmetric] |
637 trans [OF mod_add_left_eq mod_add_right_eq] |
637 trans [OF mod_add_left_eq mod_add_right_eq] |
638 trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] |
638 trans [OF mod_diff_left_eq mod_diff_right_eq] |
639 trans [OF mod_mult_right_eq zmod_zmult1_eq_rev] |
639 trans [OF mod_mult_right_eq mod_mult_left_eq] |
640 zmod_uminus' [symmetric] |
640 zmod_uminus' [symmetric] |
641 mod_add_left_eq [where b = "1::int"] |
641 mod_add_left_eq [where b = "1::int"] |
642 zmod_zsub_left_eq [where b = "1"] |
642 mod_diff_left_eq [where b = "1::int"] |
643 |
643 |
644 lemmas bintr_arith1s = |
644 lemmas bintr_arith1s = |
645 brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n |
645 brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n |
646 lemmas bintr_ariths = |
646 lemmas bintr_ariths = |
647 brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n |
647 brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n |