Theory BoolProgs_Philosophers

theory BoolProgs_Philosophers
imports "../BoolProgs_Extras"

context begin interpretation BoolProg_Syntax .

definition "eat m i = i"
definition "one m i = m + i"
definition "free m i = (2*m) + (i mod m)"
definition "Eat m i = V(eat m i)"
definition Free where "Free m i = V(free m i)"
definition One where "One m i = V(one m i)"

definition phil_const :: "nat  const_map" where
  "phil_const n  Mapping.empty"

definition phil_fun :: "nat  fun_map" where
  "phil_fun n  mapping_from_list [
              (STR ''eat'', Eat n),
              (STR ''one'', One n),
              (STR ''free'', Free n) ]"

definition phil_init :: "nat  state" where
  "phil_init n = foldl (λxs i. bs_insert (free n i) xs) (bs_empty ()) [0..<n]"

(*definition phil_init :: "nat ⇒ state" where
  "phil_init n = replicate (2 * n) False @ replicate n True"

fun dining :: "nat  nat  (bexp × com) list" where
"dining m 0 = []" |
"dining m (Suc i) = [
   And (Not (Eat m i)) (Free m i),
   [one m i, free m i] ::= [TT, FF]
  ), (
   And (One m i) (Free m (i + 1)),
   [one m i, free m (i+1), eat m i] ::= [FF, FF, TT]
  ), (
   Eat m i,
   [free m i, free m (i+1), eat m i] ::= [TT, TT, FF]
  )] @ dining m i"

definition philosophers :: " nat  bprog × config" where
  "philosophers n = (optcomp (WHILE TT DO IF dining n n FI), (0, phil_init n))"


hide_const eat one free Eat Free One