72000
|
1 |
(* Author: Jeremy Dawson, NICTA
|
|
2 |
*)
|
|
3 |
|
|
4 |
section \<open>Operation variant for the most significant bit\<close>
|
|
5 |
|
|
6 |
theory Misc_msb
|
|
7 |
imports Word
|
|
8 |
begin
|
|
9 |
|
|
10 |
class msb =
|
|
11 |
fixes msb :: \<open>'a \<Rightarrow> bool\<close>
|
|
12 |
|
|
13 |
instantiation int :: msb
|
|
14 |
begin
|
|
15 |
|
|
16 |
definition \<open>msb x \<longleftrightarrow> x < 0\<close> for x :: int
|
|
17 |
|
|
18 |
instance ..
|
|
19 |
|
|
20 |
end
|
|
21 |
|
|
22 |
lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1"
|
|
23 |
by(simp add: bin_sign_def not_le msb_int_def)
|
|
24 |
|
|
25 |
lemma msb_bin_rest [simp]: "msb (bin_rest x) = msb x"
|
|
26 |
by(simp add: msb_int_def)
|
|
27 |
|
|
28 |
lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y"
|
|
29 |
by(simp add: msb_int_def)
|
|
30 |
|
|
31 |
lemma int_msb_or [simp]: "msb ((x :: int) OR y) \<longleftrightarrow> msb x \<or> msb y"
|
|
32 |
by(simp add: msb_int_def)
|
|
33 |
|
|
34 |
lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y"
|
|
35 |
by(simp add: msb_int_def)
|
|
36 |
|
|
37 |
lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x"
|
|
38 |
by(simp add: msb_int_def not_less)
|
|
39 |
|
|
40 |
lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x"
|
|
41 |
by(simp add: msb_int_def)
|
|
42 |
|
|
43 |
lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x"
|
|
44 |
by(simp add: msb_int_def)
|
|
45 |
|
|
46 |
lemma msb_bin_sc [simp]: "msb (bin_sc n b x) \<longleftrightarrow> msb x"
|
|
47 |
by(simp add: msb_conv_bin_sign)
|
|
48 |
|
|
49 |
lemma msb_0 [simp]: "msb (0 :: int) = False"
|
|
50 |
by(simp add: msb_int_def)
|
|
51 |
|
|
52 |
lemma msb_1 [simp]: "msb (1 :: int) = False"
|
|
53 |
by(simp add: msb_int_def)
|
|
54 |
|
|
55 |
lemma msb_numeral [simp]:
|
|
56 |
"msb (numeral n :: int) = False"
|
|
57 |
"msb (- numeral n :: int) = True"
|
|
58 |
by(simp_all add: msb_int_def)
|
|
59 |
|
|
60 |
instantiation word :: (len) msb
|
|
61 |
begin
|
|
62 |
|
|
63 |
definition msb_word :: \<open>'a word \<Rightarrow> bool\<close>
|
|
64 |
where \<open>msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1\<close>
|
|
65 |
|
|
66 |
lemma msb_word_eq:
|
|
67 |
\<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
|
|
68 |
by (simp add: msb_word_def bin_sign_lem bit_uint_iff)
|
|
69 |
|
|
70 |
instance ..
|
|
71 |
|
|
72 |
end
|
|
73 |
|
|
74 |
lemma word_msb_def:
|
|
75 |
"msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
|
|
76 |
by (simp add: msb_word_def sint_uint)
|
|
77 |
|
|
78 |
lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
|
|
79 |
by (simp add: msb_word_eq bit_last_iff)
|
|
80 |
|
|
81 |
lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
|
|
82 |
by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
|
|
83 |
|
|
84 |
lemma word_msb_numeral [simp]:
|
|
85 |
"msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
|
|
86 |
unfolding word_numeral_alt by (rule msb_word_of_int)
|
|
87 |
|
|
88 |
lemma word_msb_neg_numeral [simp]:
|
|
89 |
"msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
|
|
90 |
unfolding word_neg_numeral_alt by (rule msb_word_of_int)
|
|
91 |
|
|
92 |
lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
|
|
93 |
by (simp add: word_msb_def bin_sign_def sint_uint sbintrunc_eq_take_bit)
|
|
94 |
|
|
95 |
lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
|
|
96 |
unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
|
|
97 |
by (simp add: Suc_le_eq)
|
|
98 |
|
|
99 |
lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
|
|
100 |
for w :: "'a::len word"
|
|
101 |
by (simp add: word_msb_def sint_uint bin_sign_lem)
|
|
102 |
|
|
103 |
lemma word_msb_alt: "msb w \<longleftrightarrow> hd (to_bl w)"
|
|
104 |
for w :: "'a::len word"
|
|
105 |
apply (simp add: msb_word_eq)
|
|
106 |
apply (subst hd_conv_nth)
|
|
107 |
apply simp
|
|
108 |
apply (subst nth_to_bl)
|
|
109 |
apply simp
|
|
110 |
apply simp
|
|
111 |
done
|
|
112 |
|
|
113 |
lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
|
|
114 |
for w :: "'a::len word"
|
|
115 |
by (simp add: word_msb_nth word_test_bit_def)
|
|
116 |
|
|
117 |
lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
|
|
118 |
by (simp add: msb_word_eq exp_eq_zero_iff not_le)
|
|
119 |
|
|
120 |
lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
|
|
121 |
for w :: "'a::len word"
|
|
122 |
by (simp add: msb_word_eq shiftr_word_eq bit_iff_odd_drop_bit drop_bit_eq_zero_iff_not_bit_last)
|
|
123 |
|
|
124 |
lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
|
|
125 |
|
|
126 |
end
|