Theory Word_Setup_32

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

section "32-Bit Machine Word Setup"

theory Word_Setup_32
imports Word_Enum
begin

text ‹This theory defines standard platform-specific word size and alignment.›

type_synonym machine_word_len = 32
type_synonym machine_word = "machine_word_len word"

definition word_bits :: nat
where
  "word_bits = LENGTH(machine_word_len)"

text ‹The following two are numerals so they can be used as nats and words.›
definition word_size_bits :: "'a :: numeral"
where
  "word_size_bits = 2"

definition word_size :: "'a :: numeral"
where
  "word_size = 4"

lemma word_bits_conv[code]:
  "word_bits = 32"
  unfolding word_bits_def by simp

lemma word_size_word_size_bits:
  "(word_size::nat) = 2 ^ word_size_bits"
  unfolding word_size_def word_size_bits_def by simp

lemma word_bits_word_size_conv:
  "word_bits = word_size * 8"
  unfolding word_bits_def word_size_def by simp

end