header {* \isaheader{Semantics of the thread actions for purely conditional purpose such as Join} *}
theory FWCondAction imports FWState begin
locale final_thread =
fixes final :: "'x => bool"
begin
fun cond_action_ok :: "('l,'t,'x,'m,'w) state => 't => 't conditional_action => bool" where
"cond_action_ok s t (Join T) = (case thr s T of None => True | ⌊(x, ln)⌋ => t ≠ T ∧ final x ∧ ln = no_wait_locks ∧ wset s T = None)"
fun cond_action_oks :: "('l,'t,'x,'m,'w) state => 't => 't conditional_action list => bool" where
"cond_action_oks s t [] = True"
| "cond_action_oks s t (ct#cts) = (cond_action_ok s t ct ∧ cond_action_oks s t cts)"
lemma cond_action_oks_append [simp]:
"cond_action_oks s t (cts @ cts') <-> cond_action_oks s t cts ∧ cond_action_oks s t cts'"
by(induct cts, auto)
lemma cond_action_ok_Join:
"[| cond_action_ok s t (Join T); thr s T = ⌊(x, ln)⌋ |] ==> final x ∧ ln = no_wait_locks ∧ wset s T = None"
by(auto)
lemma cond_action_oks_Join:
"[| cond_action_oks s t cas; Join T ∈ set cas; thr s T = ⌊(x, ln)⌋ |] ==> final x ∧ ln = no_wait_locks ∧ wset s T = None ∧ t ≠ T"
by(induct cas)(auto)
lemma cond_action_oks_upd:
assumes tst: "thr s t = ⌊xln⌋"
shows "cond_action_oks (locks s, (thr s(t \<mapsto> xln'), shr s), wset s) t cas = cond_action_oks s t cas"
proof(induct cas)
case Nil thus ?case by simp
next
case (Cons ca cas)
from tst have eq: "cond_action_ok (locks s, (thr s(t \<mapsto> xln'), shr s), wset s) t ca = cond_action_ok s t ca"
by(cases ca) auto
with Cons show ?case by(auto simp del: fun_upd_apply)
qed
fun cond_action_ok' :: "('l,'t,'x,'m,'w) state => 't => 't conditional_action => bool" where
"cond_action_ok' _ _ _ = True"
fun cond_action_oks' :: "('l,'t,'x,'m,'w) state => 't => 't conditional_action list => bool" where
"cond_action_oks' s t [] = True"
| "cond_action_oks' s t (ct#cts) = (cond_action_ok' s t ct ∧ cond_action_oks' s t cts)"
lemma cond_action_oks'_append [simp]:
"cond_action_oks' s t (cts @ cts') <-> cond_action_oks' s t cts ∧ cond_action_oks' s t cts'"
by(induct cts, auto)
lemma cond_action_oks'_True [simp]:
"cond_action_oks' s t cts"
by(induct cts, auto)
lemma cond_action_oks'_iff:
"cond_action_oks' s t cas = True"
by(auto)
definition collect_cond_actions :: "'t conditional_action list => 't set" where
"collect_cond_actions cts = {t. Join t ∈ set cts}"
declare collect_cond_actions_def [simp]
end
end