Theory FWLockingThread

(*  Title:      JinjaThreads/Framework/FWLockingThread.thy
    Author:     Andreas Lochbihler
*)

header {* \isaheader{Semantics of the thread action ReleaseAcquire for the thread state} *}

theory FWLockingThread imports FWLocking begin

fun upd_threadR :: "nat => 't lock => 't => lock_action => nat"
where
  "upd_threadR n l t ReleaseAcquire = n + has_locks l t"
| "upd_threadR n l t _ = n"

fun upd_threadRs :: "nat => 't lock => 't => lock_action list => nat"
where
  "upd_threadRs n l t [] = n"
| "upd_threadRs n l t (la # las) = upd_threadRs (upd_threadR n l t la) (upd_lock l t la) t las"

lemma upd_threadRs_append [simp]:
  "upd_threadRs n l t (las @ las') = upd_threadRs (upd_threadRs n l t las) (upd_locks l t las) t las'"
by(induct las arbitrary: n l, auto)

definition redT_updLns :: "('l,'t) locks => 't => ('l =>f nat) => 'l lock_actions => ('l =>f nat)"
where "redT_updLns ls t ln las = (λ(l, n, la). upd_threadRs n l t la) of (ls, (ln, las)f)f"

lemma redT_updLns_iff [simp]:
  "(redT_updLns ls t ln las)f l = upd_threadRs (lnf l) (lsf l) t (lasf l)"
by(simp add: redT_updLns_def)

lemma upd_threadRs_comp_empty [simp]: "(λ(l, n, las). upd_threadRs n l t las) of (ls, (lns, λf [])f)f = lns"
by(auto intro!: finfun_ext)

lemma redT_updLs_empty [simp]: "redT_updLs ls t (λf []) = ls"
by(simp add: redT_updLs_def)

end