Theory Word_Lib.Least_significant_bit
section ‹Operation variant for the least significant bit›
theory Least_significant_bit
imports
"HOL-Library.Word"
More_Word
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 = bit i 0› for i :: int
instance
by standard (simp add: fun_eq_iff lsb_int_def bit_0)
end
lemma bin_last_conv_lsb: "odd = (lsb :: int ⇒ bool)"
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 bit_0)
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 = bit w 0"
for w :: "'a::len word"
by (simp add: lsb_word_eq bit_0)
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_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) ⟷ odd (numeral bin :: int)"
by (simp only: lsb_odd, transfer) rule
lemma word_lsb_neg_numeral [simp]:
"lsb (- numeral bin :: 'a::len word) ⟷ odd (- numeral bin :: int)"
by (simp only: lsb_odd, transfer) rule
lemma word_lsb_nat:"lsb w = (unat w mod 2 = 1)"
apply (simp add: word_lsb_def Groebner_Basis.algebra(31))
apply transfer
apply (simp add: even_nat_iff)
done
instantiation integer :: lsb
begin
context
includes integer.lifting
begin
lift_definition lsb_integer :: ‹integer ⇒ bool› is lsb .
instance
by (standard; transfer) (fact lsb_odd)
end
end
end