Theory Word_Msb

(*  Title:      HOL/ex/Word_Msb.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section ‹An attempt for msb on word›


theory Word_Msb
  imports "HOL-Library.Word"
begin

class word = ring_bit_operations +
  fixes word_length :: ‹'a itself ⇒ nat›
  assumes word_length_positive [simp]: ‹0 < word_length TYPE('a)›
    and possible_bit_msb: ‹possible_bit TYPE('a) (word_length TYPE('a) - Suc 0)›
    and not_possible_bit_length: ‹¬ possible_bit TYPE('a) (word_length TYPE('a))›
begin

lemma word_length_not_0 [simp]:
  ‹word_length TYPE('a) ≠ 0›
  using word_length_positive
  by simp

lemma possible_bit_iff_less_word_length:
  ‹possible_bit TYPE('a) n ⟷ n < word_length TYPE('a)› (is ‹?P ⟷ ?Q›)
proof
  assume ‹?P›
  show ?Q
  proof (rule ccontr)
    assume ‹¬ n < word_length TYPE('a)›
    then have ‹word_length TYPE('a) ≤ n›
      by simp
    with ‹?P› have ‹possible_bit TYPE('a) (word_length TYPE('a))›
      by (rule possible_bit_less_imp)
    with not_possible_bit_length show False ..
  qed
next
  assume ‹?Q›
  then have ‹n ≤ word_length TYPE('a) - Suc 0›
    by simp
  with possible_bit_msb show ?P
    by (rule possible_bit_less_imp)
qed

end

instantiation word :: (len) word
begin

definition word_length_word :: ‹'a word itself ⇒ nat›
  where [simp, code_unfold]: ‹word_length_word _ = LENGTH('a)›

instance
  by standard simp_all

end

context word
begin

context
  includes bit_operations_syntax
begin

definition msb :: ‹'a ⇒ bool›
  where ‹msb w = bit w (word_length TYPE('a) - Suc 0)›

lemma not_msb_0 [simp]:
  ‹¬ msb 0›
  by (simp add: msb_def)

lemma msb_minus_1 [simp]:
  ‹msb (- 1)›
  by (simp add: msb_def possible_bit_iff_less_word_length)

lemma msb_1_iff [simp]:
  ‹msb 1 ⟷ word_length TYPE('a) = 1›
  by (auto simp add: msb_def bit_simps le_less)

lemma msb_minus_iff [simp]:
  ‹msb (- w) ⟷ ¬ msb (w - 1)›
  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)

lemma msb_not_iff [simp]:
  ‹msb (NOT w) ⟷ ¬ msb w›
  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)

lemma msb_and_iff [simp]:
  ‹msb (v AND w) ⟷ msb v ∧ msb w›
  by (simp add: msb_def bit_simps)

lemma msb_or_iff [simp]:
  ‹msb (v OR w) ⟷ msb v ∨ msb w›
  by (simp add: msb_def bit_simps)

lemma msb_xor_iff [simp]:
  ‹msb (v XOR w) ⟷ ¬ (msb v ⟷ msb w)›
  by (simp add: msb_def bit_simps)

lemma msb_exp_iff [simp]:
  ‹msb (2 ^ n) ⟷ n = word_length TYPE('a) - Suc 0›
  by (auto simp add: msb_def bit_simps possible_bit_iff_less_word_length)

lemma msb_mask_iff [simp]:
  ‹msb (mask n) ⟷ word_length TYPE('a) ≤ n›
  by (simp add: msb_def bit_simps less_diff_conv2 Suc_le_eq less_Suc_eq_le possible_bit_iff_less_word_length)

lemma msb_set_bit_iff [simp]:
  ‹msb (set_bit n w) ⟷ n = word_length TYPE('a) - Suc 0 ∨ msb w›
  by (simp add: set_bit_eq_or ac_simps)

lemma msb_unset_bit_iff [simp]:
  ‹msb (unset_bit n w) ⟷ n ≠ word_length TYPE('a) - Suc 0 ∧ msb w›
  by (simp add: unset_bit_eq_and_not ac_simps)

lemma msb_flip_bit_iff [simp]:
  ‹msb (flip_bit n w) ⟷ (n ≠ word_length TYPE('a) - Suc 0 ⟷ msb w)›
  by (auto simp add: flip_bit_eq_xor)

lemma msb_push_bit_iff:
  ‹msb (push_bit n w) ⟷ n < word_length TYPE('a) ∧ bit w (word_length TYPE('a) - Suc n)›
  by (simp add: msb_def bit_simps le_diff_conv2 Suc_le_eq possible_bit_iff_less_word_length)

lemma msb_drop_bit_iff [simp]:
  ‹msb (drop_bit n w) ⟷ n = 0 ∧ msb w›
  by (cases n)
    (auto simp add: msb_def bit_simps possible_bit_iff_less_word_length intro!: impossible_bit)

lemma msb_take_bit_iff [simp]:
  ‹msb (take_bit n w) ⟷ word_length TYPE('a) ≤ n ∧ msb w›
  by (simp add: take_bit_eq_mask ac_simps)

lemma msb_signed_take_bit_iff:
  ‹msb (signed_take_bit n w) ⟷ bit w (min n (word_length TYPE('a) - Suc 0))›
  by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)

definition signed_drop_bit :: ‹nat ⇒ 'a ⇒ 'a›
  where ‹signed_drop_bit n w = drop_bit n w
    OR (of_bool (bit w (word_length TYPE('a) - Suc 0)) * NOT (mask (word_length TYPE('a) - Suc n)))›

lemma msb_signed_drop_bit_iff [simp]:
  ‹msb (signed_drop_bit n w) ⟷ msb w›
  by (simp add: signed_drop_bit_def bit_simps not_le not_less)
    (simp add: msb_def)

end

end

end