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]: 
    " imin_signed; imax_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  v0"

  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