72000
|
1 |
(* Author: Jeremy Dawson, NICTA
|
|
2 |
*)
|
|
3 |
|
|
4 |
section \<open>Operation variant for the least significant bit\<close>
|
|
5 |
|
|
6 |
theory Misc_lsb
|
|
7 |
imports Word
|
|
8 |
begin
|
|
9 |
|
|
10 |
class lsb = semiring_bits +
|
|
11 |
fixes lsb :: \<open>'a \<Rightarrow> bool\<close>
|
|
12 |
assumes lsb_odd: \<open>lsb = odd\<close>
|
|
13 |
|
|
14 |
instantiation int :: lsb
|
|
15 |
begin
|
|
16 |
|
|
17 |
definition lsb_int :: \<open>int \<Rightarrow> bool\<close>
|
|
18 |
where \<open>lsb i = i !! 0\<close> for i :: int
|
|
19 |
|
|
20 |
instance
|
|
21 |
by standard (simp add: fun_eq_iff lsb_int_def)
|
|
22 |
|
|
23 |
end
|
|
24 |
|
|
25 |
lemma bin_last_conv_lsb: "bin_last = lsb"
|
|
26 |
by (simp add: lsb_odd)
|
|
27 |
|
|
28 |
lemma int_lsb_numeral [simp]:
|
|
29 |
"lsb (0 :: int) = False"
|
|
30 |
"lsb (1 :: int) = True"
|
|
31 |
"lsb (Numeral1 :: int) = True"
|
|
32 |
"lsb (- 1 :: int) = True"
|
|
33 |
"lsb (- Numeral1 :: int) = True"
|
|
34 |
"lsb (numeral (num.Bit0 w) :: int) = False"
|
|
35 |
"lsb (numeral (num.Bit1 w) :: int) = True"
|
|
36 |
"lsb (- numeral (num.Bit0 w) :: int) = False"
|
|
37 |
"lsb (- numeral (num.Bit1 w) :: int) = True"
|
|
38 |
by (simp_all add: lsb_int_def)
|
|
39 |
|
|
40 |
instantiation word :: (len) lsb
|
|
41 |
begin
|
|
42 |
|
|
43 |
definition lsb_word :: \<open>'a word \<Rightarrow> bool\<close>
|
|
44 |
where word_lsb_def: \<open>lsb a \<longleftrightarrow> odd (uint a)\<close> for a :: \<open>'a word\<close>
|
|
45 |
|
|
46 |
instance
|
|
47 |
apply standard
|
|
48 |
apply (simp add: fun_eq_iff word_lsb_def)
|
|
49 |
apply transfer apply simp
|
|
50 |
done
|
|
51 |
|
|
52 |
end
|
|
53 |
|
|
54 |
lemma lsb_word_eq:
|
|
55 |
\<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
|
|
56 |
by (fact lsb_odd)
|
|
57 |
|
|
58 |
lemma word_lsb_alt: "lsb w = test_bit w 0"
|
|
59 |
for w :: "'a::len word"
|
|
60 |
by (auto simp: word_test_bit_def word_lsb_def)
|
|
61 |
|
|
62 |
lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
|
|
63 |
unfolding word_lsb_def uint_eq_0 uint_1 by simp
|
|
64 |
|
|
65 |
lemma word_lsb_last:
|
|
66 |
\<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
|
|
67 |
for w :: \<open>'a::len word\<close>
|
|
68 |
using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w]
|
|
69 |
by (simp add: lsb_odd last_conv_nth)
|
|
70 |
|
|
71 |
lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
|
|
72 |
apply (simp add: lsb_odd flip: odd_iff_mod_2_eq_one)
|
|
73 |
apply transfer
|
|
74 |
apply simp
|
|
75 |
done
|
|
76 |
|
|
77 |
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
|
|
78 |
|
|
79 |
lemma word_lsb_numeral [simp]:
|
|
80 |
"lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
|
|
81 |
unfolding word_lsb_alt test_bit_numeral by simp
|
|
82 |
|
|
83 |
lemma word_lsb_neg_numeral [simp]:
|
|
84 |
"lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
|
|
85 |
by (simp add: word_lsb_alt)
|
|
86 |
|
|
87 |
end
|