1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7section "32-Bit Machine Word Setup"
8
9theory Word_Setup_32
10imports Word_Enum
11begin
12
13text \<open>This theory defines standard platform-specific word size and alignment.\<close>
14
15type_synonym machine_word_len = 32
16type_synonym machine_word = "machine_word_len word"
17
18definition word_bits :: nat
19where
20  "word_bits = LENGTH(machine_word_len)"
21
22text \<open>The following two are numerals so they can be used as nats and words.\<close>
23definition word_size_bits :: "'a :: numeral"
24where
25  "word_size_bits = 2"
26
27definition word_size :: "'a :: numeral"
28where
29  "word_size = 4"
30
31lemma word_bits_conv[code]:
32  "word_bits = 32"
33  unfolding word_bits_def by simp
34
35lemma word_size_word_size_bits:
36  "(word_size::nat) = 2 ^ word_size_bits"
37  unfolding word_size_def word_size_bits_def by simp
38
39lemma word_bits_word_size_conv:
40  "word_bits = word_size * 8"
41  unfolding word_bits_def word_size_def by simp
42
43end
44