Theory Misc_lsb

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

section ‹Operation variant for the least significant bit›

theory Misc_lsb
  imports
    Word
    Reversed_Bit_Lists
begin

class lsb = semiring_bits +
  fixes lsb :: ‹'a ⇒ bool›
  assumes lsb_odd: ‹lsb = odd›

instantiation int :: lsb
begin

definition lsb_int :: ‹int ⇒ bool›
  where ‹lsb i = i !! 0› for i :: int

instance
  by standard (simp add: fun_eq_iff lsb_int_def)

end

lemma bin_last_conv_lsb: "bin_last = lsb"
  by (simp add: lsb_odd)

lemma int_lsb_numeral [simp]:
  "lsb (0 :: int) = False"
  "lsb (1 :: int) = True"
  "lsb (Numeral1 :: int) = True"
  "lsb (- 1 :: int) = True"
  "lsb (- Numeral1 :: int) = True"
  "lsb (numeral (num.Bit0 w) :: int) = False"
  "lsb (numeral (num.Bit1 w) :: int) = True"
  "lsb (- numeral (num.Bit0 w) :: int) = False"
  "lsb (- numeral (num.Bit1 w) :: int) = True"
  by (simp_all add: lsb_int_def)

instantiation word :: (len) lsb
begin

definition lsb_word :: ‹'a word ⇒ bool›
  where word_lsb_def: ‹lsb a ⟷ odd (uint a)› for a :: ‹'a word›

instance
  apply standard
  apply (simp add: fun_eq_iff word_lsb_def)
  apply transfer apply simp
  done

end
  
lemma lsb_word_eq:
  ‹lsb = (odd :: 'a word ⇒ bool)› for w :: ‹'a::len word›
  by (fact lsb_odd)

lemma word_lsb_alt: "lsb w = test_bit w 0"
  for w :: "'a::len word"
  by (auto simp: word_test_bit_def word_lsb_def)

lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) ∧ ¬ lsb (0::'b::len word)"
  unfolding word_lsb_def by simp

lemma word_lsb_last:
  ‹lsb w ⟷ last (to_bl w)›
  for w :: ‹'a::len word›
  using nth_to_bl [of ‹LENGTH('a) - Suc 0› w]
  by (simp add: lsb_odd last_conv_nth)

lemma word_lsb_int: "lsb w ⟷ uint w mod 2 = 1"
  apply (simp add: lsb_odd flip: odd_iff_mod_2_eq_one)
  apply transfer
  apply simp
  done

lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]

lemma word_lsb_numeral [simp]:
  "lsb (numeral bin :: 'a::len word) ⟷ bin_last (numeral bin)"
  unfolding word_lsb_alt test_bit_numeral by simp

lemma word_lsb_neg_numeral [simp]:
  "lsb (- numeral bin :: 'a::len word) ⟷ bin_last (- numeral bin)"
  by (simp add: word_lsb_alt)

end