equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 context semiring_bits |
12 context semiring_bits |
13 begin |
13 begin |
14 |
14 |
15 (*lemma even_mask_div_iff: |
|
16 \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close> |
|
17 sorry |
|
18 |
|
19 lemma bit_mask_iff: |
15 lemma bit_mask_iff: |
20 \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close> |
16 \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close> |
21 by (simp add: bit_def even_mask_div_iff not_le)*) |
17 by (simp add: bit_def even_mask_div_iff not_le) |
22 |
18 |
23 end |
19 end |
24 |
20 |
25 context semiring_bit_shifts |
21 context semiring_bit_shifts |
26 begin |
22 begin |