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