Theory FWLockingThread

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

section ‹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"

primrec 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 "⋀ln. redT_updLns ls t ln las = (λ(l, n, la). upd_threadRs n l t la) ∘$ ($ls, ($ln, las$)$)"

lemma redT_updLns_iff [simp]:
  "⋀ln. redT_updLns ls t ln las $ l = upd_threadRs (ln $ l) (ls $ l) t (las $ l)"
by(simp add: redT_updLns_def)

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

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

end