Theory Word_Lib.Most_significant_bit

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
Proofs tidied by LCP, 2024-09
 *)

(* Author: Jeremy Dawson, NICTA *)

section ‹Dedicated operation for the most significant bit›

theory Most_significant_bit
  imports
    "HOL-Library.Word"
    Bit_Shifts_Infix_Syntax
    More_Word
    More_Arithmetic
begin

class msb =
  fixes msb :: 'a  bool

instantiation int :: msb
begin

definition msb x  x < 0 for x :: int

instance ..

end

lemma msb_bin_rest [simp]: "msb (x div 2) = msb x"
  for x :: int
  by (simp add: msb_int_def)

context
  includes bit_operations_syntax
begin

lemma int_msb_and [simp]: "msb ((x :: int) AND y)  msb x  msb y"
by(simp add: msb_int_def)

lemma int_msb_or [simp]: "msb ((x :: int) OR y)  msb x  msb y"
by(simp add: msb_int_def)

lemma int_msb_xor [simp]: "msb ((x :: int) XOR y)  msb x  msb y"
by(simp add: msb_int_def)

lemma int_msb_not [simp]: "msb (NOT (x :: int))  ¬ msb x"
by(simp add: msb_int_def not_less)

end

lemma msb_shiftl [simp]: "msb ((x :: int) << n)  msb x"
  by (simp add: msb_int_def shiftl_def)

lemma msb_shiftr [simp]: "msb ((x :: int) >> r)  msb x"
  by (simp add: msb_int_def shiftr_def)

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

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

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

instantiation word :: (len) msb
begin

definition msb_word :: 'a word  bool
  where msb_word_iff_bit: msb w  bit w (LENGTH('a) - Suc 0) for w :: 'a::len word

instance ..

end

lemma msb_word_eq:
  msb w  bit w (LENGTH('a) - 1) for w :: 'a::len word
  by (simp add: msb_word_iff_bit)

lemma word_msb_sint: "msb w  sint w < 0"
  by (simp add: msb_word_eq bit_last_iff)

lemma msb_word_iff_sless_0:
  msb w  w <s 0
  by (simp add: word_msb_sint word_sless_alt)

lemma msb_word_of_int:
  "msb (word_of_int x::'a::len word) = bit x (LENGTH('a) - 1)"
  by (simp add: msb_word_iff_bit bit_simps)

lemma word_msb_numeral [simp]:
  "msb (numeral w::'a::len word) = bit (numeral w :: int) (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) = bit (- numeral w :: int) (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: msb_word_iff_bit)

lemma word_msb_1 [simp]: "msb (1::'a::len word)  LENGTH('a) = 1"
  by (simp add: bit_last_iff msb_word_iff_bit)

lemma word_msb_nth: "msb w = bit (uint w) (LENGTH('a) - 1)"
  for w :: "'a::len word"
  by (simp add: msb_word_iff_bit bit_simps)

lemma msb_nth: "msb w = bit w (LENGTH('a) - 1)"
  for w :: "'a::len word"
  by (fact msb_word_eq)

lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  by (simp add: msb_word_eq not_le)

lemma msb_shift: "msb w  w >> LENGTH('a) - 1  0"
  for w :: "'a::len word"
  by (simp add: drop_bit_eq_zero_iff_not_bit_last msb_word_eq shiftr_def)

lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]

lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
proof (cases LENGTH('a))
  case 0
  then show ?thesis by auto
next
  case (Suc n)
  then show ?thesis
    apply (simp add: msb_word_iff_bit)
    apply transfer
    by (auto simp: signed_take_bit_eq_take_bit_minus)
qed

lemma word_sle_msb_le: "x <=s y  (msb y  msb x)  ((msb x  ¬ msb y)  x  y)"
  by (smt (verit) word_less_eq_iff_unsigned word_msb_sint word_sint_msb_eq word_sle_eq wsst_TYs(3))

lemma word_sless_msb_less: "x <s y  (msb y  msb x)  ((msb x  ¬ msb y)  x < y)"
  by (auto simp add: word_sless_eq word_sle_msb_le)

lemma not_msb_from_less:
  "(v :: 'a word) < 2 ^ (LENGTH('a :: len) - 1)  ¬ msb v"
  using bang_is_le linorder_not_le msb_word_eq by blast

lemma sint_eq_uint:
  "¬ msb x  sint x = uint x"
  by (simp add: word_sint_msb_eq)

lemma scast_eq_ucast:
  "¬ msb x  scast x = ucast x"
  by (simp add: scast_eq sint_eq_uint)

lemma msb_ucast_eq:
    "LENGTH('a) = LENGTH('b) 
         msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)"
  by (simp add: msb_word_eq bit_simps)

lemma msb_big:
  fixes a :: 'a::len word
  shows msb a  2 ^ (LENGTH('a) - Suc 0)  a  (is "_ = ?R")
proof
  show "msb a  ?R"
    by (simp add: bang_is_le msb_nth)
  show "?R  msb a"
    unfolding msb_word_iff_bit
    by (metis Suc_pred diff_Suc_less leD le_less_Suc_eq len_gt_0 less_2p_is_upper_bits_unset)
qed

instantiation integer :: msb
begin

context
  includes integer.lifting
begin

lift_definition msb_integer :: integer  bool is msb .

instance ..

end

end

end