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

locale final_thread =
  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)
apply(fastforce simp add: final_thread.cond_action_ok.simps)+
done

lemma cond_action_oks_final_change:
  assumes major: "final_thread.cond_action_oks final1 s1 t cas"
  and minor: "⋀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"
  shows "final_thread.cond_action_oks final2 s2 t cas"
using major
by(induct cas)(auto simp add: final_thread.cond_action_oks.simps intro: cond_action_ok_final_change[OF _ minor])

end