# Theory SM_State

section ‹State for SM›
theory SM_State
imports
"HOL-Library.Word"
"HOL-Library.Multiset"
"Word_Lib.Typedef_Morphisms"
SM_Syntax
begin
section ‹Values›
text ‹The primitive values are fixed-size signed integers›
type_synonym word_size = 32
type_synonym signed = "word_size Word.word"
text ‹Currently, we only have signed integer values.
This may change if we extend the language, and allow,
i.e., channel pointers, pids or process references›
type_synonym val = signed
section ‹Configurations›
type_synonym valuation = "ident ⇀ val"
record local_state =
variables :: valuation
record global_state =
variables :: valuation
text ‹The effect of actions is on focused states›
type_synonym focused_state = "local_state × global_state"
section ‹Utilities›
abbreviation "word_len ≡ LENGTH(word_size)"
abbreviation "signeds ≡ sints (LENGTH(word_size))"
definition min_signed :: int where "min_signed ≡ -(2^(word_len - 1))"
definition max_signed :: int where "max_signed ≡ 2^(word_len - 1) - 1"
definition signed_of_int :: "int ⇒ signed"
where "signed_of_int i ≡ word_of_int i"
definition int_of_signed :: "signed ⇒ int"
where "int_of_signed i == sint i"
lemma si_inv[simp]: "signed_of_int (int_of_signed i) = i"
unfolding signed_of_int_def int_of_signed_def
by simp
lemma int_of_signed_in_range[simp]:
"int_of_signed i ≥ min_signed"
"int_of_signed i ≤ max_signed"
unfolding int_of_signed_def min_signed_def max_signed_def
apply -
apply (rule sint_ge)
using sint_lt[of i]
by simp
lemma is_inv[simp]:
"⟦ i≥min_signed; i≤max_signed ⟧ ⟹ (int_of_signed (signed_of_int i)) = i"
by (simp add: signed_take_bit_int_eq_self min_signed_def max_signed_def int_of_signed_def signed_of_int_def signed_of_int)
primrec val_of_bool :: "bool ⇒ val" where
"val_of_bool False = 0" | "val_of_bool True = 1"
definition bool_of_val :: "val ⇒ bool" where
"bool_of_val v ≡ v≠0"
lemma bool_of_val_invs[simp]:
"bool_of_val (val_of_bool b) = b"
"val_of_bool (bool_of_val v) = (if v=0 then 0 else 1)"
unfolding bool_of_val_def
by (cases b) auto
end