Theory SM.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   ― ‹Word size›
  type_synonym signed = "word_size Word.word"  ― ‹Signed integer›
  
  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  ― ‹Value type›

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