equal
deleted
inserted
replaced
1931 by simp |
1931 by simp |
1932 then show ?thesis |
1932 then show ?thesis |
1933 by (simp add: of_nat_mod) |
1933 by (simp add: of_nat_mod) |
1934 qed |
1934 qed |
1935 |
1935 |
1936 lemma range_mod_exp: |
1936 lemma mask_mod_exp: |
1937 \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close> |
1937 \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close> |
1938 proof - |
1938 proof - |
1939 have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>) |
1939 have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>) |
1940 proof (cases \<open>n \<le> m\<close>) |
1940 proof (cases \<open>n \<le> m\<close>) |
1941 case True |
1941 case True |