Theory Machine_Word_32

(*
 * Copyright 2014, NICTA
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "32-Bit Machine Word Setup"

theory Machine_Word_32
  imports Machine_Word_32_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit
begin

context
  includes bit_operations_syntax
begin

type_synonym machine_word = ‹machine_word_len word›

lemma word_bits_len_of:
  ‹LENGTH(machine_word_len) = word_bits›
  by (simp add: word_bits_conv)

lemma word_bits_size:
  "size (w :: machine_word) = word_bits"
  by (simp add: word_bits_def word_size)

lemma word_bits_word_size_conv:
  ‹word_bits = word_size * 8›
  by (simp add: word_bits_def word_size_def)

lemma word_size_word_size_bits:
  ‹word_size = (2 :: 'a :: semiring_1) ^ word_size_bits›
  by (simp add: word_size_def word_size_bits_def)

lemma lt_word_bits_lt_pow:
  "sz < word_bits ⟹ sz < 2 ^ word_bits"
  by (simp add: word_bits_conv)

lemma bool_mask [simp]:
  ‹0 < x AND 1 ⟷ x AND 1 = 1› for x :: machine_word
  by (rule bool_mask') auto

lemma in_16_range:
  "0 ∈ S ⟹ r ∈ (λx. r + x * (16 :: machine_word)) ` S"
  "n - 1 ∈ S ⟹ (r + (16 * n - 16)) ∈ (λx :: machine_word. r + x * 16) ` S"
  by (clarsimp simp: image_def elim!: bexI[rotated])+

lemma le_step_down_word_3:
  fixes x :: machine_word
  shows "⟦x ≤ y; x ≠ y⟧ ⟹ x ≤ y - 1"
  by (fact le_step_down_word_2)

lemma shiftr_1:
  "(x::machine_word) >> 1 = 0 ⟹ x < 2"
  apply transfer
  apply (simp add: take_bit_drop_bit)
  apply (simp add: drop_bit_Suc)
  done

lemma Suc_unat_mask_div:
  "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)"
  by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
    flip: drop_bit_eq_div word_bits_conv)

lemma ucast_not_helper:
  fixes a::"8 word"
  assumes a: "a ≠ 0xFF"
  shows "ucast a ≠ (0xFF::machine_word)"
proof
  assume "ucast a = (0xFF::machine_word)"
  also
  have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp
  finally
  show False using a
    apply -
    apply (drule up_ucast_inj, simp)
    apply simp
    done
qed

lemma unat_less_2p_word_bits:
  "unat (x :: machine_word) < 2 ^ word_bits"
  apply (simp only: word_bits_def)
  apply (rule unat_lt2p)
  done

lemma unat_less_word_bits:
  fixes y :: machine_word
  shows "x < unat y ⟹ x < 2 ^ word_bits"
  unfolding word_bits_def
  by (rule order_less_trans [OF _ unat_lt2p])

lemma unat_mask_2_less_4:
  "unat (p AND mask 2 :: machine_word) < 4"
  by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)

lemma unat_mult_simple:
  ‹unat (x * y) = unat x * unat y›
    if ‹unat x * unat y < 2 ^ LENGTH(machine_word_len)›
    for x y :: machine_word
  using that by (simp flip: unat_mult_lem)

lemma upto_2_helper:
  "{0..<2 :: machine_word} = {0, 1}"
  by (safe; simp) unat_arith

lemma word_ge_min:
  ‹- (2 ^ (word_bits - 1)) ≤ sint x› for x :: machine_word
  using sint_ge [of x] by (simp add: word_bits_def)

(* We want the rhs unfolded here for later matching *)
lemma word_rsplit_0:
  "word_rsplit (0::machine_word) = [0, 0, 0, (0::8 word)]"
  by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)

lemma x_less_2_0_1:
  fixes x :: machine_word
  shows "x < 2 ⟹ x = 0 ∨ x = 1"
  by (rule x_less_2_0_1') auto

lemma less_4_cases:
  "(x::machine_word) < 4 ⟹ x=0 ∨ x=1 ∨ x=2 ∨ x=3"
  apply clarsimp
  apply (drule word_less_cases, erule disjE, simp, simp)+
  done

end

end