Theory FWWellformSem

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

header {* \isaheader{Wellformedness properties for the instantiating semantics and the multithreaded state } *}

theory FWWellformSem imports FWProgressAux begin

text {* This locale simply fixes a start state *}
locale multithreaded_start = multithreaded _ r
  for r :: "('l,'t,'x,'m,'w,'o) semantics" +
  fixes start_state :: "('l,'t,'x,'m,'w) state"
  assumes lock_thread_ok_start_state: "lock_thread_ok (locks start_state) (thr start_state)"
begin

lemma preserves_lock_thread_ok: 
  "start_state -\<triangleright>tta->* s ==> lock_thread_ok (locks s) (thr s)"
  by(erule RedT_preserves_lock_thread_ok[OF _ lock_thread_ok_start_state])

end


locale wf_red = multithreaded_start _ r start_state
  for r :: "('l,'t,'x,'m,'w,'o) semantics" and start_state :: "('l,'t,'x,'m,'w) state" +
  assumes wf_red:
    "[| start_state -\<triangleright>tta->* s; thr s t = ⌊(x, no_wait_locks)⌋;
       r (x, shr s) ta (x', m') |]
     ==> ∃ta' x' m'. r (x, shr s) ta' (x', m') ∧ final_thread.actions_ok' s t ta' ∧ final_thread.actions_subset ta' ta"
begin

lemmas wf_red_refl = wf_red[OF RedT_refl]


lemma wf_redE:
  assumes "start_state -\<triangleright>ttas->* s" "thr s t = ⌊(x, no_wait_locks)⌋" "⟨x, shr s⟩ -ta-> ⟨x'', m''⟩"
  obtains ta' x' m'
  where "⟨x, shr s⟩ -ta'-> ⟨x', m'⟩" "actions_ok' s t ta'" "actions_subset ta' ta"
using assms
by(blast dest: wf_red)

lemma wf_redE':
  assumes "start_state -\<triangleright>ttas->* s" "thr s t = ⌊(x, no_wait_locks)⌋" "⟨x, shr s⟩ -ta-> ⟨x'', m''⟩"
  obtains ta' x' m'
  where "⟨x, shr s⟩ -ta'-> ⟨x', m'⟩" "thread_oks (thr s) \<lbrace>ta'\<rbrace>t"
  and "lock_ok_las' (locks s) t \<lbrace>ta'\<rbrace>l" "collect_locks' \<lbrace>ta'\<rbrace>l ⊆ collect_locks \<lbrace>ta\<rbrace>l"
  and "cond_action_oks' s t \<lbrace>ta'\<rbrace>c"
  and "collect_cond_actions \<lbrace>ta'\<rbrace>c ⊆ collect_cond_actions \<lbrace>ta\<rbrace>c"
using assms
by(blast dest: wf_red)

end


locale preserve_lock_behav = multithreaded_start _ r
  for r :: "('l,'t,'x,'m,'w,'o) semantics" +
  assumes can_lock_preserved: 
    "[| start_state -\<triangleright>tta->* s; s -t'\<triangleright>ta'-> s';
       thr s t = ⌊(x, ln)⌋; ⟨x, shr s⟩ L \<wrong>; L ≠ {} |]
    ==> ⟨x, shr s'⟩ \<wrong>"
  and can_lock_devreserp:
    "[| RedT start_state tta s; s -t'\<triangleright>ta'-> s';
       thr s t = ⌊(x, ln)⌋; ⟨x, shr s'⟩ L \<wrong> |]
    ==> ∃L'⊆L. ⟨x, shr s⟩ L' \<wrong>"

locale wf_progress = final_thread final + multithreaded_start final r start_state 
  for final :: "'x => bool" and r :: "('l,'t,'x,'m,'w,'o) semantics" and start_state :: "('l,'t,'x,'m,'w) state" +
  assumes wf_progress: "[| start_state -\<triangleright>tta->* s; thr s t = ⌊(x, ln)⌋; ¬ final x |]
                        ==> ∃ta x' m'. ⟨x, shr s⟩ -ta-> ⟨x', m'⟩"
begin

lemmas wf_progress_refl = wf_progress[OF RedT_refl]

lemma wf_progressE:
  assumes "start_state -\<triangleright>tta->* s"
  and "thr s t = ⌊(x, ln)⌋" "¬ final x"
  obtains ta x' m' where "⟨x, shr s⟩ -ta-> ⟨x', m'⟩"
using assms
by(blast dest: wf_progress)

lemmas wf_progress_reflE = wf_progressE[OF RedT_refl]

end


end