| changeset 71181 | 8331063570d6 |
| parent 70193 | 49a65e3f04c9 |
| child 71756 | 3d1f72d25fc3 |
--- a/src/HOL/Word/Bits_Int.thy Fri Nov 29 21:53:02 2019 +0100 +++ b/src/HOL/Word/Bits_Int.thy Wed Nov 27 16:54:33 2019 +0000 @@ -1623,7 +1623,8 @@ apply (case_tac bit, auto) done -lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" +lemma mod_BIT: + "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit proof - have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1" by (simp add: mod_mult_mult1)