Theory Least_significant_bit

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* Author: Jeremy Dawson, NICTA *)

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