equal
deleted
inserted
replaced
1 (* Title: HOL/Word/Misc_Arithmetic.thy *) |
1 (* Title: HOL/Word/Misc_Arithmetic.thy *) |
2 |
2 |
3 section \<open>Miscellaneous lemmas, mostly for arithmetic\<close> |
3 section \<open>Miscellaneous lemmas, mostly for arithmetic\<close> |
4 |
4 |
5 theory Misc_Arithmetic |
5 theory Misc_Arithmetic |
6 imports Misc_Auxiliary "HOL-Library.Bit" |
6 imports Misc_Auxiliary "HOL-Library.Z2" |
7 begin |
7 begin |
8 |
8 |
9 lemma one_mod_exp_eq_one [simp]: |
9 lemma one_mod_exp_eq_one [simp]: |
10 "1 mod (2 * 2 ^ n) = (1::int)" |
10 "1 mod (2 * 2 ^ n) = (1::int)" |
11 using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial) |
11 using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial) |