# Theory Misc_msb

theory Misc_msb
imports Reversed_Bit_Lists
```(*  Author:     Jeremy Dawson, NICTA
*)

section ‹Operation variant for the most significant bit›

theory Misc_msb
imports
Word
Reversed_Bit_Lists
begin

class msb =
fixes msb :: ‹'a ⇒ bool›

instantiation int :: msb
begin

definition ‹msb x ⟷ x < 0› for x :: int

instance ..

end

lemma msb_conv_bin_sign: "msb x ⟷ bin_sign x = -1"

lemma msb_bin_rest [simp]: "msb (bin_rest x) = msb x"

lemma int_msb_and [simp]: "msb ((x :: int) AND y) ⟷ msb x ∧ msb y"

lemma int_msb_or [simp]: "msb ((x :: int) OR y) ⟷ msb x ∨ msb y"

lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) ⟷ msb x ≠ msb y"

lemma int_msb_not [simp]: "msb (NOT (x :: int)) ⟷ ¬ msb x"

lemma msb_shiftl [simp]: "msb ((x :: int) << n) ⟷ msb x"

lemma msb_shiftr [simp]: "msb ((x :: int) >> r) ⟷ msb x"

lemma msb_bin_sc [simp]: "msb (bin_sc n b x) ⟷ msb x"

lemma msb_0 [simp]: "msb (0 :: int) = False"

lemma msb_1 [simp]: "msb (1 :: int) = False"

lemma msb_numeral [simp]:
"msb (numeral n :: int) = False"
"msb (- numeral n :: int) = True"

instantiation word :: (len) msb
begin

definition msb_word :: ‹'a word ⇒ bool›
where ‹msb a ⟷ bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1›

lemma msb_word_eq:
‹msb w ⟷ bit w (LENGTH('a) - 1)› for w :: ‹'a::len word›
by (simp add: msb_word_def bin_sign_lem bit_uint_iff)

instance ..

end

lemma msb_word_iff_bit:
‹msb w ⟷ bit w (LENGTH('a) - Suc 0)›
for w :: ‹'a::len word›
by (simp add: msb_word_def bin_sign_def bit_uint_iff)

lemma word_msb_def:
"msb a ⟷ bin_sign (sint a) = - 1"

lemma word_msb_sint: "msb w ⟷ sint w < 0"

lemma msb_word_iff_sless_0:
‹msb w ⟷ w <s 0›

lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)

lemma word_msb_numeral [simp]:
"msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
unfolding word_numeral_alt by (rule msb_word_of_int)

lemma word_msb_neg_numeral [simp]:
"msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
unfolding word_neg_numeral_alt by (rule msb_word_of_int)

lemma word_msb_0 [simp]: "¬ msb (0::'a::len word)"
by (simp add: word_msb_def bin_sign_def sint_uint sbintrunc_eq_take_bit)

lemma word_msb_1 [simp]: "msb (1::'a::len word) ⟷ LENGTH('a) = 1"
unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]

lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
for w :: "'a::len word"
by (simp add: word_msb_def sint_uint bin_sign_lem)

lemma word_msb_alt: "msb w ⟷ hd (to_bl w)"
for w :: "'a::len word"
apply (subst hd_conv_nth)
apply simp
apply (subst nth_to_bl)
apply simp
apply simp
done

lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
for w :: "'a::len word"