header {* \isaheader{Semantics of the thread actions for wait and notify} *}
theory FWWait imports FWState begin
text {* Update functions for the wait sets in the multithreaded state *}
fun redT_updW :: "('w,'t) wait_sets => 't => 'w wait_set_action => ('w,'t) wait_sets"
where
"redT_updW ws t (Notify w) = (if (∃t. ws t = ⌊w⌋) then ws((SOME t. ws t = ⌊w⌋) := None) else ws)"
| "redT_updW ws t (NotifyAll w) = (λt. if ws t = ⌊w⌋ then None else ws t)"
| "redT_updW ws t (Suspend w) = ws(t \<mapsto> w)"
fun redT_updWs :: "('w,'t) wait_sets => 't => 'w wait_set_action list => ('w,'t) wait_sets"
where
"redT_updWs ws t [] = ws"
| "redT_updWs ws t (wa#was) = redT_updWs (redT_updW ws t wa) t was"
lemma redT_updWs_append [simp]:
"redT_updWs ws t (was @ was') = redT_updWs (redT_updWs ws t was) t was'"
by(induct was arbitrary: ws, auto)
lemma redT_updW_None_implies_None:
"[| t ≠ t'; ws t = None |] ==> redT_updW ws t' wa t = None"
by(cases wa, auto)
lemma redT_updWs_None_implies_None:
assumes "t ≠ t'"
shows "ws t = None ==> redT_updWs ws t' was t = None"
proof(induct was arbitrary: ws)
case Nil thus ?case by simp
next
case (Cons WA WAS WS)
from `t ≠ t'` `WS t = None`
have "redT_updW WS t' WA t = None"
by(rule redT_updW_None_implies_None)
with `!!ws. ws t = None ==> redT_updWs ws t' WAS t = None`
show ?case by(auto)
qed
lemma redT_updW_Some_Some_eq:
"[| t ≠ t'; ws t = ⌊w⌋; redT_updW ws t' wa t = ⌊w'⌋ |] ==> w = w'"
by(cases wa, auto split: split_if_asm)
lemma redT_updWs_Some_Some_eq:
assumes "t ≠ t'"
shows "[| ws t = ⌊w⌋; redT_updWs ws t' was t = ⌊w'⌋ |] ==> w = w'"
proof(induct was arbitrary: ws)
case Nil thus ?case using `t ≠ t'` by auto
next
case (Cons WA WAS WS)
from `redT_updWs WS t' (WA # WAS) t = ⌊w'⌋`
have "redT_updWs (redT_updW WS t' WA) t' WAS t = ⌊w'⌋" by simp
moreover from `t ≠ t'` `WS t = ⌊w⌋`
show ?case
proof(cases "redT_updW WS t' WA t")
case None
with `t ≠ t'` have "redT_updWs (redT_updW WS t' WA) t' WAS t = None"
by(rule redT_updWs_None_implies_None)
with `redT_updWs (redT_updW WS t' WA) t' WAS t = ⌊w'⌋` have False by simp
thus ?thesis ..
next
case (Some W)
with `t ≠ t'` `WS t = ⌊w⌋` have "W = w"
by(rule redT_updW_Some_Some_eq[THEN sym])
with `!!ws. [|ws t = ⌊w⌋; redT_updWs ws t' WAS t = ⌊w'⌋|] ==> w = w'`
`redT_updWs (redT_updW WS t' WA) t' WAS t = ⌊w'⌋` Some
show ?thesis by(simp)
qed
qed
lemma redT_updW_neq_Some_SomeD:
"[| redT_updW ws t' wa t = ⌊w⌋; ws t ≠ ⌊w⌋ |] ==> t = t' ∧ wa = Suspend w"
by(cases wa, auto split: split_if_asm)
lemma redT_updWs_neq_Some_SomeD:
"[| redT_updWs ws t' was t = ⌊w⌋; ws t ≠ ⌊w⌋ |] ==> t = t' ∧ Suspend w ∈ set was"
proof(induct was arbitrary: ws)
case Nil thus ?case by simp
next
case (Cons WA WAS WS)
show ?case
proof(cases "redT_updW WS t' WA t = ⌊w⌋")
case False
with `[| redT_updWs (redT_updW WS t' WA) t' WAS t = ⌊w⌋; redT_updW WS t' WA t ≠ ⌊w⌋ |]
==> t = t' ∧ Suspend w ∈ set WAS` `redT_updWs WS t' (WA # WAS) t = ⌊w⌋`
show ?thesis by(auto)
next
case True
with `WS t ≠ ⌊w⌋` show ?thesis
by(auto dest: redT_updW_neq_Some_SomeD)
qed
qed
end