# Theory FWCondAction

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

section ‹Semantics of the thread actions for purely conditional purpose such as Join›

theory FWCondAction
imports
FWState
begin

fixes final :: "'x ⇒ bool"
begin

primrec cond_action_ok :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action ⇒ bool" where
"⋀ln. 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)"
| "cond_action_ok s t Yield = True"

primrec 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_conv_set:
"cond_action_oks s t cts ⟷ (∀ct ∈ set cts. cond_action_ok s t ct)"
by(induct cts) simp_all

lemma cond_action_ok_Join:
"⋀ln. ⟦ 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:
"⋀ln. ⟦ 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 ↦ xln'), shr s), wset s, interrupts 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 ↦ xln'), shr s), wset s, interrupts 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

lemma cond_action_ok_shr_change:
"cond_action_ok (ls, (ts, m), ws, is) t ct ⟹ cond_action_ok (ls, (ts, m'), ws, is) t ct"
by(cases ct) auto

lemma cond_action_oks_shr_change:
"cond_action_oks (ls, (ts, m), ws, is) t cts ⟹ cond_action_oks (ls, (ts, m'), ws, is) t cts"
by(auto simp add: cond_action_oks_conv_set intro: cond_action_ok_shr_change)

primrec cond_action_ok' :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ 't conditional_action ⇒ bool"
where
"cond_action_ok' _ _ (Join t) = True"
| "cond_action_ok' _ _ Yield = True"

primrec 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'_subset_Join:
"set cts ⊆ insert Yield (range Join) ⟹ cond_action_oks' s t cts"
apply(induct cts)
apply(auto)
done

end

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]

lemma cond_action_ok_final_change:
"⟦ final_thread.cond_action_ok final1 s1 t ca;
⋀t. thr s1 t = None ⟷ thr s2 t = None;
⋀t x1. ⟦ thr s1 t = ⌊(x1, no_wait_locks)⌋; final1 x1; wset s1 t = None ⟧
⟹ ∃x2. thr s2 t = ⌊(x2, no_wait_locks)⌋ ∧ final2 x2 ∧ ln2 = no_wait_locks ∧ wset s2 t = None ⟧
⟹ final_thread.cond_action_ok final2 s2 t ca"
apply(cases ca)