section \<open>Dedicated operation for the most significant bit\<close>

theory Most_significant_bit
  imports
    "HOL-Library.Word"
begin

subsection \<open>Generic abstract specification\<close>

class msb = ring_bit_operations +
  fixes msb :: \<open>'a \<Rightarrow> bool\<close>
  assumes msb_iff_bitI: \<open>possible_bit TYPE('a) n \<Longrightarrow> (\<And>q. possible_bit TYPE('a) q \<Longrightarrow> q > n \<Longrightarrow> bit a q \<longleftrightarrow> bit a n) \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
begin

lemma msb_index:
  obtains m where \<open>possible_bit TYPE('a) m\<close> \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
proof -
  from stable_index [of a] obtain m where \<open>possible_bit TYPE('a) m\<close>
    and hyp: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
    by blast
  have \<open>msb a \<longleftrightarrow> bit a n\<close> if \<open>n \<ge> m\<close> \<open>possible_bit TYPE('a) n\<close> for n
  proof -
    from \<open>possible_bit TYPE('a) m\<close> have \<open>msb a \<longleftrightarrow> bit a m\<close>
    proof (rule msb_iff_bitI)
      fix q
      assume \<open>m < q\<close>
      assume \<open>possible_bit TYPE('a) q\<close>
      show \<open>bit a q \<longleftrightarrow> bit a m\<close>
      proof (cases \<open>q = m\<close>)
        case True
        then show ?thesis
          by simp
      next
        case False
        with \<open>m < q\<close>
        have \<open>m \<le> q\<close>
          by simp
        with \<open>possible_bit TYPE('a) q\<close> show ?thesis
          by (rule hyp)
      qed
    qed
    also from that hyp [of n] have \<open>bit a m \<longleftrightarrow> bit a n\<close>
      by blast
    finally show ?thesis .
  qed
  then show thesis
    using \<open>possible_bit TYPE('a) m\<close> that by blast
qed

context
  includes bit_operations_syntax
begin

lemma not_msb_0 [iff]:
  \<open>\<not> msb 0\<close>
  using msb_index [of 0] by auto

lemma msb_minus_1 [iff]:
  \<open>msb (- 1)\<close>
  using msb_index [of \<open>- 1\<close>] by auto

lemma msb_not_iff [simp]:
  \<open>msb (NOT a) \<longleftrightarrow> \<not> msb a\<close>
proof -
  obtain r s where
    bit: \<open>possible_bit TYPE('a) r\<close> \<open>possible_bit TYPE('a) s\<close>
    and msb: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> r \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
    \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> s \<Longrightarrow> msb (NOT a) \<longleftrightarrow> bit (NOT a) n\<close>
    using that msb_index [of a thesis] msb_index [of \<open>NOT a\<close> thesis]
    by blast
  define m where \<open>m = max r s\<close>
  then have \<open>m \<in> {r, s}\<close> \<open>m \<ge> r\<close> \<open>m \<ge> s\<close>
    by auto
  with bit have m: \<open>possible_bit TYPE('a) m\<close>
    by auto
  from msb m \<open>m \<ge> r\<close> have \<open>msb a \<longleftrightarrow> bit a m\<close>
    by blast
  moreover from msb m \<open>m \<ge> s\<close> have \<open>msb (NOT a) \<longleftrightarrow> bit (NOT a) m\<close>
    by blast
  ultimately show ?thesis using m
    by (simp add: bit_simps)
qed

lemma msb_minus_iff:
  \<open>msb (- a) \<longleftrightarrow> \<not> msb (a - 1)\<close>
  by (simp add: minus_eq_not_minus_1)

lemma msb_and_iff [simp]:
  \<open>msb (a AND b) \<longleftrightarrow> msb a \<and> msb b\<close>
proof -
  obtain r s t where
    possible: \<open>possible_bit TYPE('a) r\<close> \<open>possible_bit TYPE('a) s\<close> \<open>possible_bit TYPE('a) t\<close>
    and msb: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> r \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> s \<Longrightarrow> msb b \<longleftrightarrow> bit b n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> t \<Longrightarrow> msb (a AND b) \<longleftrightarrow> bit (a AND b) n\<close>
    using that msb_index [of a thesis] msb_index [of b thesis] msb_index [of \<open>a AND b\<close> thesis] by blast
  define m where \<open>m = Max {r, s, t}\<close>
  then have \<open>m \<in> {r, s, t}\<close> \<open>m \<ge> r\<close> \<open>m \<ge> s\<close> \<open>m \<ge> t\<close>
    by auto
  with possible have m: \<open>possible_bit TYPE('a) m\<close>
    by blast
  from msb m \<open>m \<ge> r\<close> have \<open>msb a \<longleftrightarrow> bit a m\<close>
    by blast
  moreover from msb m \<open>m \<ge> s\<close> have \<open>msb b \<longleftrightarrow> bit b m\<close>
    by blast
  moreover from msb m \<open>m \<ge> t\<close> have \<open>msb (a AND b) \<longleftrightarrow> bit (a AND b) m\<close>
    by blast
  ultimately show ?thesis
    by (simp add: bit_simps)
qed

lemma msb_or_iff [simp]:
  \<open>msb (a OR b) \<longleftrightarrow> msb a \<or> msb b\<close>
proof -
  obtain r s t where
    possible: \<open>possible_bit TYPE('a) r\<close> \<open>possible_bit TYPE('a) s\<close> \<open>possible_bit TYPE('a) t\<close>
    and msb: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> r \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> s \<Longrightarrow> msb b \<longleftrightarrow> bit b n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> t \<Longrightarrow> msb (a OR b) \<longleftrightarrow> bit (a OR b) n\<close>
    using that msb_index [of a thesis] msb_index [of b thesis] msb_index [of \<open>a OR b\<close> thesis] by blast
  define m where \<open>m = Max {r, s, t}\<close>
  then have \<open>m \<in> {r, s, t}\<close> \<open>m \<ge> r\<close> \<open>m \<ge> s\<close> \<open>m \<ge> t\<close>
    by auto
  with possible have m: \<open>possible_bit TYPE('a) m\<close>
    by blast
  from msb m \<open>m \<ge> r\<close> have \<open>msb a \<longleftrightarrow> bit a m\<close>
    by blast
  moreover from msb m \<open>m \<ge> s\<close> have \<open>msb b \<longleftrightarrow> bit b m\<close>
    by blast
  moreover from msb m \<open>m \<ge> t\<close> have \<open>msb (a OR b) \<longleftrightarrow> bit (a OR b) m\<close>
    by blast
  ultimately show ?thesis
    by (simp add: bit_simps)
qed

lemma msb_xor_iff [simp]:
  \<open>msb (a XOR b) \<longleftrightarrow> msb a \<noteq> msb b\<close>
proof -
  obtain r s t where
    possible: \<open>possible_bit TYPE('a) r\<close> \<open>possible_bit TYPE('a) s\<close> \<open>possible_bit TYPE('a) t\<close>
    and msb: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> r \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> s \<Longrightarrow> msb b \<longleftrightarrow> bit b n\<close>
      \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> t \<Longrightarrow> msb (a XOR b) \<longleftrightarrow> bit (a XOR b) n\<close>
    using that msb_index [of a thesis] msb_index [of b thesis] msb_index [of \<open>a XOR b\<close> thesis] by blast
  define m where \<open>m = Max {r, s, t}\<close>
  then have \<open>m \<in> {r, s, t}\<close> \<open>m \<ge> r\<close> \<open>m \<ge> s\<close> \<open>m \<ge> t\<close>
    by auto
  with possible have m: \<open>possible_bit TYPE('a) m\<close>
    by blast
  from msb m \<open>m \<ge> r\<close> have \<open>msb a \<longleftrightarrow> bit a m\<close>
    by blast
  moreover from msb m \<open>m \<ge> s\<close> have \<open>msb b \<longleftrightarrow> bit b m\<close>
    by blast
  moreover from msb m \<open>m \<ge> t\<close> have \<open>msb (a XOR b) \<longleftrightarrow> bit (a XOR b) m\<close>
    by blast
  ultimately show ?thesis
    by (simp add: bit_simps)
qed

definition is_max_index :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
  where is_max_index_iff: \<open>is_max_index TYPE('a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> possible_bit TYPE('a) (Suc n)\<close>

lemma is_max_index_cases [case_names impossible max_index possible]:
  obtains \<open>\<not> possible_bit TYPE('a) n\<close> | \<open>is_max_index TYPE('a) n\<close> | \<open>possible_bit TYPE('a) (Suc n)\<close>
  by (auto simp add: is_max_index_iff)

lemma msb_iff_bit_if_is_max_index:
  \<open>msb a \<longleftrightarrow> bit a n\<close> if \<open>is_max_index TYPE('a) n\<close>
proof -
  obtain m where
    \<open>possible_bit TYPE('a) m\<close>
    and msb: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> msb a \<longleftrightarrow> bit a n\<close>
    using that msb_index [of a thesis] by blast
  have \<open>n \<ge> m\<close>
  proof (rule ccontr)
    assume \<open>\<not> n \<ge> m\<close>
    then have \<open>Suc n \<le> m\<close>
      by simp
    with that have \<open>\<not> possible_bit TYPE('a) m\<close>
      by (auto simp add: is_max_index_iff possible_bit_less_imp)
    with \<open>possible_bit TYPE('a) m\<close> show False
      by simp
  qed
  with that msb [of n] show ?thesis
    by (simp add: is_max_index_iff)
qed

lemma msb_exp_iff [simp]:
  \<open>msb (2 ^ n) \<longleftrightarrow> is_max_index TYPE('a) n\<close>
proof (cases n rule: is_max_index_cases)
  case impossible
  then have \<open>2 ^ n = 0\<close>
    by (simp add: fold_possible_bit)
  with impossible show ?thesis
    by (simp add: is_max_index_iff)
next
  case max_index
  then show ?thesis
    by (simp add: msb_iff_bit_if_is_max_index is_max_index_iff bit_simps)
next
  case possible
  then have \<open>msb (2 ^ n) \<longleftrightarrow> bit (2 ^ n) (Suc n)\<close>
    by (rule msb_iff_bitI) (simp add: bit_simps)
  with possible show ?thesis
    by (simp add: bit_simps is_max_index_iff)
qed

lemma msb_1_iff [simp]:
  \<open>msb 1 \<longleftrightarrow> is_max_index TYPE('a) 0\<close>
  using msb_exp_iff [of 0] by simp

lemma msb_mask_iff [simp]:
  \<open>msb (mask n) \<longleftrightarrow> \<not> possible_bit TYPE('a) n\<close>
proof (cases \<open>possible_bit TYPE('a) n\<close>)
  case True
  with msb_iff_bitI [of n \<open>mask n\<close>]
  show ?thesis
    by (simp_all add: bit_simps)
next
  case False
  with mask_eq_minus_one_if_not_possible_bit [of n]
  show ?thesis by simp
qed

lemma msb_set_bit_iff [simp]:
  \<open>msb (set_bit n a) \<longleftrightarrow> is_max_index TYPE('a) n \<or> msb a\<close>
  by (simp add: set_bit_eq_or ac_simps)

lemma msb_unset_bit_iff [simp]:
  \<open>msb (unset_bit n a) \<longleftrightarrow> \<not> is_max_index TYPE('a) n \<and> msb a\<close>
  by (simp add: unset_bit_eq_and_not ac_simps)

lemma msb_flip_bit_iff [simp]:
  \<open>msb (flip_bit n a) \<longleftrightarrow> (\<not> is_max_index TYPE('a) n \<longleftrightarrow> msb a)\<close>
  by (auto simp add: flip_bit_eq_xor)

lemma msb_take_bit_iff [simp]:
  \<open>msb (take_bit n a) \<longleftrightarrow> \<not> possible_bit TYPE('a) n \<and> msb a\<close>
  by (auto simp add: take_bit_eq_mask)

lemma msb_signed_take_bit_iff:
  \<open>msb (signed_take_bit n a) \<longleftrightarrow> (if possible_bit TYPE('a) n then bit a n else msb a)\<close>
  by (simp add: signed_take_bit_def)

end

end


subsection \<open>Special case: \<^typ>\<open>int\<close>\<close>

instantiation int :: msb
begin

definition msb_int :: \<open>int \<Rightarrow> bool\<close>
  where msb_int_iff: \<open>msb k \<longleftrightarrow> k < 0\<close> for k :: int

instance proof
  fix k :: int and n
  assume *: \<open>\<And>q. possible_bit TYPE(int) q \<Longrightarrow> q > n \<Longrightarrow> bit k q \<longleftrightarrow> bit k n\<close>
  have \<open>drop_bit n k = - of_bool (bit k n)\<close>
  proof (rule bit_eqI)
    fix q
    have \<open>bit k (n + q) = bit k n\<close>
      using * [of \<open>n + q\<close>] by (cases q) simp_all
    then show \<open>bit (drop_bit n k) q \<longleftrightarrow> bit (- of_bool (bit k n) :: int) q\<close>
      by (simp add: bit_simps)
  qed
  then have \<open>drop_bit n k < 0 \<longleftrightarrow> - of_bool (bit k n) < (0 :: int)\<close>
    by simp
  then show \<open>msb k \<longleftrightarrow> bit k n\<close>
    by (simp add: msb_int_iff)
qed

end

lemma not_is_max_index_int [iff]:
  \<open>\<not> is_max_index TYPE(int) n\<close>
  by (simp add: is_max_index_iff)

lemma not_msb_exp_int_iff [iff]:
  \<open>\<not> msb (2 ^ n :: int)\<close>
  by simp

lemma not_msb_mask_int_iff [iff]:
  \<open>\<not> msb (mask n :: int)\<close>
  by simp

lemma not_msb_numeral_int [iff]:
  \<open>\<not> msb (numeral n :: int)\<close>
  by (simp add: msb_int_iff)

lemma msb_minus_numeral_int [iff]:
  \<open>msb (- numeral n :: int)\<close>
  by (simp add: msb_int_iff)

lemma not_msb_int [iff]:
  \<open>\<not> msb (int n)\<close>
  by (simp add: msb_int_iff)

lemma msb_set_bit_int_iff [simp]:
  \<open>msb (set_bit n k) \<longleftrightarrow> msb k\<close> for k :: int
  by (simp add: set_bit_eq_or)

lemma msb_unset_bit_int_iff [simp]:
  \<open>msb (unset_bit n k) \<longleftrightarrow> msb k\<close> for k :: int
  by (simp add: unset_bit_eq_and_not)

lemma msb_flip_bit_int_iff [simp]:
  \<open>msb (flip_bit n k) \<longleftrightarrow> msb k\<close> for k :: int
  by (simp add: flip_bit_eq_xor)

lemma msb_push_bit_int_iff [simp]:
  \<open>msb (push_bit n k) \<longleftrightarrow> msb k\<close> for k :: int
  by (simp add: msb_int_iff)

lemma msb_drop_bit_int_iff [simp]:
  \<open>msb (drop_bit n k) \<longleftrightarrow> msb k\<close> for k :: int
  by (simp add: msb_int_iff)

lemma msb_half_int_iff [simp]:
  \<open>msb (k div 2) = msb k\<close> for k :: int
  by (simp add: msb_int_iff)

lemma not_msb_take_bit_int_iff [iff]:
  \<open>\<not> msb (take_bit n k)\<close> for k :: int
  by (simp add: msb_int_iff)

lemma msb_signed_take_bit_int_iff [simp]:
  \<open>msb (signed_take_bit n k) \<longleftrightarrow> bit k n\<close> for k :: int
  by (simp add: msb_int_iff)

lemma not_msb_numeral_int_iff [simp]:
  \<open>\<not> msb (numeral m :: int)\<close>
  by (simp add: msb_int_iff)

lemma msb_minus_numeral_int_iff [simp]:
  \<open>msb (- numeral m :: int)\<close>
  by (simp add: msb_int_iff)


subsection \<open>Special case: \<^typ>\<open>'a word\<close>\<close>

instantiation word :: (len) msb
begin

lift_definition msb_word :: \<open>'a word \<Rightarrow> bool\<close>
  is \<open>\<lambda>k. msb (signed_take_bit (LENGTH('a) - Suc 0) k)\<close>
  by (drule map_bit_range_eq_if_take_bit_eq) (simp add: msb_int_iff)

lemma msb_word_iff_negative:
  \<open>msb w \<longleftrightarrow> w <s 0\<close>
  by transfer (simp add: msb_int_iff)

lemma msb_word_iff_bit [code]:
  \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
  by transfer (simp add: msb_int_iff)

instance proof
  fix w :: \<open>'a word\<close> and n
  assume \<open>possible_bit TYPE('a word) n\<close>
  then have \<open>n < LENGTH('a)\<close>
    by simp
  assume *: \<open>(\<And>q. possible_bit TYPE('a word) q \<Longrightarrow> n < q \<Longrightarrow> bit w q \<longleftrightarrow> bit w n)\<close>
  have \<open>bit w (LENGTH('a) - Suc 0) \<longleftrightarrow> bit w n\<close>
  proof (cases \<open>n = LENGTH('a) - Suc 0\<close>)
    case True
    then show ?thesis
      by (simp add: msb_word_iff_bit)
  next
    case False
    with \<open>n < LENGTH('a)\<close> have \<open>n < LENGTH('a) - Suc 0\<close>
      by simp
    then show ?thesis
      by (simp add: *)
  qed
  then show \<open>msb w \<longleftrightarrow> bit w n\<close>
    by (simp add: msb_word_iff_bit)
qed

end

lemma msb_word_iff_greater:
  \<open>msb w \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> w\<close> for w :: \<open>'a::len word\<close>
proof transfer
  fix k :: int
  have \<open>bit k (LENGTH('a) - Suc 0) \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> take_bit LENGTH('a) k\<close>
    by (cases \<open>LENGTH('a)\<close>) (simp_all add: take_bit_Suc_from_most not_le)
  then show \<open>msb (signed_take_bit (LENGTH('a) - Suc 0) k) \<longleftrightarrow> take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0)) \<le> take_bit LENGTH('a) k\<close>
    by simp
qed

lemma is_max_index_word_iff [simp]:
  \<open>is_max_index TYPE('a::len word) n \<longleftrightarrow> LENGTH('a) = Suc n\<close>
  by (auto simp add: is_max_index_iff)

lemma msb_exp_word_iff [simp]:
  \<open>msb (2 ^ n :: 'a::len word) \<longleftrightarrow> LENGTH('a) = Suc n\<close>
  by simp

lemma msb_mask_word_iff [simp]:
  \<open>msb (mask n :: 'a::len word) \<longleftrightarrow> LENGTH('a) \<le> n\<close>
  by (simp add: not_less)

lemma msb_drop_bit_word_iff [simp]:
  \<open>msb (drop_bit n w) \<longleftrightarrow> n = 0 \<and> msb w\<close> for w :: \<open>'a::len word\<close>
  using bit_imp_le_length [of w \<open>n + (LENGTH('a) - Suc 0)\<close>]
  by (cases n) (auto simp add: msb_word_iff_bit bit_simps)

lemma msb_signed_drop_bit_word_iff [simp]:
  \<open>msb (signed_drop_bit n w) \<longleftrightarrow> msb w\<close> for w :: \<open>'a::len word\<close>
  by (cases n) (simp_all add: msb_word_iff_bit bit_simps)

lemma msb_numeral_word_iff [simp]:
  \<open>msb (numeral m :: 'a word) = bit (numeral m :: 'a::len word) (LENGTH('a::len) - Suc 0)\<close>
  by (fact msb_word_iff_bit)

lemma msb_minus_numeral_word_iff [simp]:
  \<open>msb (- numeral m :: 'a word) = bit (- numeral m :: 'a::len word) (LENGTH('a::len) - Suc 0)\<close>
  by (fact msb_word_iff_bit)


subsection \<open>Special case: target language numerals \<^typ>\<open>integer\<close>\<close>

instantiation integer :: msb
begin

context
  includes integer.lifting
begin

lift_definition msb_integer :: \<open>integer \<Rightarrow> bool\<close>
  is msb .

instance by (standard; transfer)
  (use msb_iff_bitI [where ?'a = int] in auto)

end

end

lemma msb_integer_code [code]:
  \<open>msb k \<longleftrightarrow> k < 0\<close> for k :: integer
  including integer.lifting by transfer (simp add: msb_int_iff)

lifting_update integer.lifting
lifting_forget integer.lifting



text\<open>\<close>

context
  includes bit_operations_syntax
begin

lemma not_msb_imp_signed_eq_unsigned:
  \<open>signed w = unsigned w\<close> if \<open>\<not> msb w\<close>
using \<open>\<not> msb w\<close> proof transfer
  fix k :: int
  assume \<open>\<not> msb (signed_take_bit (LENGTH('a) - Suc 0) k)\<close>
  then have *: \<open>\<not> bit k (LENGTH('a) - Suc 0)\<close>
    by simp
  then have \<open>signed_take_bit (LENGTH('a) - Suc 0) k = take_bit (LENGTH('a) - Suc 0) k\<close>
    by (simp add: signed_take_bit_eq_if_positive)
  also have \<open>\<dots> = take_bit LENGTH('a) k\<close>
    using take_bit_Suc_from_most [of \<open>LENGTH('a) - Suc 0\<close> k] * by simp
  finally show \<open>(of_int \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k = (of_nat \<circ> nat \<circ> take_bit LENGTH('a)) k\<close>
    by simp
qed

lemma msb_imp_signed_eq_unsigned_minus_exp:
  \<open>signed w = unsigned w - 2 ^ LENGTH('a)\<close> if \<open>msb w\<close> for w :: \<open>'a::len word\<close>
using \<open>msb w\<close> proof transfer
  fix k :: int
  assume \<open>msb (signed_take_bit (LENGTH('a) - Suc 0) k)\<close>
  then have *: \<open>bit k (LENGTH('a) - Suc 0)\<close>
    by simp
  then show \<open>(of_int \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k = (of_nat \<circ> nat \<circ> take_bit LENGTH('a)) k - 2 ^ LENGTH('a)\<close>
    by (simp add: signed_take_bit_eq_take_bit_minus)
qed

lemma signed_eq_unsigned_if_msb:
  \<open>signed w = unsigned w - of_bool (msb w) * 2 ^ LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
  by (simp add: not_msb_imp_signed_eq_unsigned msb_imp_signed_eq_unsigned_minus_exp)

lemma sless_eq_iff_less_eq:
  \<open>w \<le>s v \<longleftrightarrow> (msb v \<longrightarrow> msb w) \<and> (msb w \<and> \<not> msb v \<or> w \<le> v)\<close>
proof -
  consider \<open>msb w \<longleftrightarrow> msb v\<close> | \<open>msb w\<close> \<open>\<not> msb v\<close> | \<open>\<not> msb w\<close> \<open>msb v\<close>
    by auto
  then show ?thesis proof cases
    case 1
    then show ?thesis
      by (simp add: word_less_eq_iff_unsigned [where ?'a = int] word_sle_eq signed_eq_unsigned_if_msb)
  next
    case 2
    have \<open>uint w - 2 ^ LENGTH('a) \<le> 0\<close>
      using uint_m2p_not_non_neg [of w] by simp
    also have \<open>0 \<le> uint v\<close> using \<open>\<not> msb v\<close>
      by simp
    finally show ?thesis using \<open>msb w\<close> \<open>\<not> msb v\<close>
      by (simp add: word_less_eq_iff_unsigned [where ?'a = int] word_sle_eq signed_eq_unsigned_if_msb)
  next
    case 3
    have \<open>uint v - 2 ^ LENGTH('a) < 0\<close>
      using uint_m2p_not_non_neg [of v] by simp
    also have \<open>0 \<le> uint w\<close> using \<open>\<not> msb w\<close>
      by simp
    finally show ?thesis using \<open>\<not> msb w\<close> \<open>msb v\<close>
      by (simp add: word_less_eq_iff_unsigned [where ?'a = int] word_sle_eq signed_eq_unsigned_if_msb)
  qed
qed

lemma sless_iff_less:
  \<open>w <s v \<longleftrightarrow> (msb v \<longrightarrow> msb w) \<and> (msb w \<and> \<not> msb v \<or> w < v)\<close>
  by (auto simp add: signed.order.strict_iff_order sless_eq_iff_less_eq)

end

subsection \<open>Legacy aliasses\<close>

lemmas msb_int_def = msb_int_iff

lemmas msb_word_iff_sless_0 = msb_word_iff_negative

lemmas msb_bin_rest = msb_half_int_iff

lemmas int_msb_and = msb_and_iff [of x y for x y :: int]

lemmas int_msb_or = msb_or_iff [of x y for x y :: int]

lemmas int_msb_xor = msb_xor_iff [of x y for x y :: int]

lemmas int_msb_not = msb_not_iff [of x for x :: int]

lemma msb_0:
  \<open>msb (0 :: int) \<longleftrightarrow> False\<close>
  by simp

lemma msb_1:
  \<open>msb (1 :: int) \<longleftrightarrow> False\<close>
  by simp

lemma msb_numeral:
  \<open>msb (numeral n :: int) \<longleftrightarrow> False\<close>
  \<open>msb (- numeral n :: int) \<longleftrightarrow> True\<close>
  by simp_all

lemma msb_word_eq:
  \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
  by (simp add: msb_word_iff_bit)

lemma word_msb_sint:
  \<open>msb w \<longleftrightarrow> sint w < 0\<close>
  by (simp add: msb_word_iff_negative word_sless_alt)

lemma msb_word_of_int:
  \<open>msb (word_of_int x :: 'a::len word) \<longleftrightarrow> bit x (LENGTH('a) - 1)\<close>
  by (simp add: msb_word_iff_bit bit_simps)

lemma word_msb_numeral:
  \<open>msb (numeral w :: 'a::len word) \<longleftrightarrow> bit (numeral w :: int) (LENGTH('a) - 1)\<close>
  by simp

lemma word_msb_neg_numeral:
  "msb (- numeral w :: 'a::len word) = bit (- numeral w :: int) (LENGTH('a) - 1)"
  by simp

lemma word_msb_0:
  \<open>\<not> msb (0 :: 'a::len word)\<close>
  by (fact not_msb_0)

lemma word_msb_1:
  \<open>msb (1 :: 'a::len word) \<longleftrightarrow> LENGTH('a) = 1\<close>
  by simp

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

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

lemma word_msb_n1 [simp]:
  \<open>msb (-1 :: 'a::len word)\<close>
  by (fact msb_minus_1)

lemma word_sint_msb_eq:
  \<open>sint x = uint x - (if msb x then 2 ^ size x else 0)\<close>
  by (simp add: not_msb_imp_signed_eq_unsigned msb_imp_signed_eq_unsigned_minus_exp word_size)

lemma word_sle_msb_le:
  \<open>x \<le>s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)\<close>
  by (fact sless_eq_iff_less_eq)

lemma word_sless_msb_less:
  \<open>x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)\<close>
  by (fact sless_iff_less)

lemma not_msb_from_less:
  \<open>v < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> \<not> msb v\<close> for v :: \<open>'a::len word\<close>
  by (simp add: msb_word_iff_greater)

lemma sint_eq_uint:
  \<open>\<not> msb x \<Longrightarrow> sint x = uint x\<close>
  by (fact not_msb_imp_signed_eq_unsigned)

lemma scast_eq_ucast:
  \<open>\<not> msb x \<Longrightarrow> scast x = ucast x\<close>
  by (fact not_msb_imp_signed_eq_unsigned)

lemma msb_ucast_eq:
  \<open>LENGTH('a) = LENGTH('b) \<Longrightarrow> msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)\<close>
  by (simp add: msb_word_eq bit_simps)

lemma msb_big:
  \<open>msb a \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> a\<close>  (is "_ = ?R") for a :: \<open>'a::len word\<close>
  by (fact msb_word_iff_greater)

end