Theory FWProgressAux

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

header {* \isaheader{Auxiliary definitions for the progress theorem for the multithreaded semantics} *}

theory FWProgressAux imports FWSemantics begin

context multithreaded_base begin

definition must_sync :: "'x => 'm => bool" ("⟨_,/ _⟩/ \<wrong>" [0,0] 81) where
  "must_sync x m = (∃ta x' m'. ⟨x, m⟩ -ta-> ⟨x', m'⟩)"

lemma must_syncI:
  "∃ta x' m'. ⟨x, m⟩ -ta-> ⟨x', m'⟩ ==> ⟨x, m⟩ \<wrong>"
by(fastsimp simp add: must_sync_def)

lemma must_syncE:
  "[| ⟨x, m⟩ \<wrong>; !!ta x' m'. ⟨x, m⟩ -ta-> ⟨x', m'⟩ ==> thesis |] ==> thesis"
by(auto simp only: must_sync_def)


definition can_sync :: "'x => 'm => ('l + 't) set => bool" ("⟨_,/ _⟩/ _/ \<wrong>" [0,0,0] 81) where
  "⟨x, m⟩ LT \<wrong> ≡ ∃ta x' m'. ⟨x, m⟩ -ta-> ⟨x', m'⟩ ∧ (LT = collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c})"

lemma can_syncI:
  "[| ⟨x, m⟩ -ta-> ⟨x', m'⟩; LT = collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c} |] ==> ⟨x, m⟩ LT \<wrong>"
by(cases ta)(fastsimp simp add: can_sync_def)

lemma can_syncE:
  assumes "⟨x, m⟩ LT \<wrong>"
  obtains ta x' m'
  where "⟨x, m⟩ -ta-> ⟨x', m'⟩" "LT = collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
  using assms
by(clarsimp simp add: can_sync_def)

lemma must_sync_ex_can_sync:
  "⟨x, m⟩ \<wrong> ==> ∃LT. ⟨x, m⟩ LT \<wrong>"
by(auto intro: can_syncI elim!: must_syncE)

lemma can_sync_must_sync:
  "⟨x, m⟩ LT \<wrong> ==> ⟨x, m⟩ \<wrong>"
by(auto intro: must_syncI elim!: can_syncE)

lemma must_sync_can_sync_conv:
  "⟨x, m⟩ \<wrong> <-> (∃LT. ⟨x, m⟩ LT \<wrong>)"
by(auto intro: must_sync_ex_can_sync can_sync_must_sync)


end

text {* Well-formedness conditions for final *}

context final_thread begin

definition final_thread :: "('l,'t,'x,'m,'w) state => 't => bool" where
  "final_thread s t ≡ (case thr s t of None => False | ⌊(x, ln)⌋ => final x ∧ ln = no_wait_locks ∧ wset s t = None)"

inductive not_final_thread :: "('l,'t,'x,'m,'w) state => 't => bool"
for s :: "('l,'t,'x,'m,'w) state" and t :: "'t" where
  not_final_thread_final: "[| thr s t = ⌊(x, ln)⌋; ¬ final x |] ==> not_final_thread s t"
| not_final_thread_wait_locks: "[| thr s t = ⌊(x, ln)⌋; ln ≠ no_wait_locks |] ==> not_final_thread s t"
| not_final_thread_wait_set: "[| thr s t = ⌊(x, ln)⌋; wset s t = ⌊w⌋ |] ==> not_final_thread s t"

lemma final_threadI:
  "[| thr s t = ⌊(x, no_wait_locks)⌋; final x; wset s t = None |] ==> final_thread s t"
by(simp add: final_thread_def)

lemma final_threadE:
  assumes "final_thread s t"
  obtains x where "thr s t = ⌊(x, no_wait_locks)⌋" "final x" "wset s t = None"
using assms by(auto simp add: final_thread_def)

declare not_final_thread.cases [elim]

lemmas not_final_thread_cases = not_final_thread.cases [consumes 1, case_names final wait_locks wait_set]

lemma not_final_thread_cases2 [consumes 2, case_names final wait_locks wait_set]:
  "[| not_final_thread s t; thr s t = ⌊(x, ln)⌋;
     ¬ final x ==> thesis; ln ≠ no_wait_locks ==> thesis; !!w. wset s t = ⌊w⌋ ==> thesis |]
  ==> thesis"
by(auto)

lemma not_final_thread_iff:
  "not_final_thread s t <-> (∃x ln. thr s t = ⌊(x, ln)⌋ ∧ (¬ final x ∨ ln ≠ no_wait_locks ∨ (∃w. wset s t = ⌊w⌋)))"
by(auto intro: not_final_thread.intros)

lemma not_final_thread_conv:
  "not_final_thread s t <-> thr s t ≠ None ∧ ¬ final_thread s t"
by(auto simp add: final_thread_def intro: not_final_thread.intros)

lemma not_final_thread_existsE:
  assumes "not_final_thread s t"
  obtains x ln where "thr s t = ⌊(x, ln)⌋"
using assms by blast

lemma not_final_thread_final_thread_conv:
  "thr s t ≠ None ==> ¬ final_thread s t <-> not_final_thread s t"
by(simp add: not_final_thread_iff final_thread_def)

lemma may_join_cond_action_oks:
  assumes "!!t'. Join t' ∈ set cas ==> ¬ not_final_thread s t' ∧ t ≠ t'"
  shows "cond_action_oks s t cas"
using assms
proof (induct cas)
  case Nil thus ?case by clarsimp
next
  case (Cons ca cas)
  note IH = `(!!t'. Join t' ∈ set cas ==> ¬ not_final_thread s t' ∧ t ≠ t') ==> cond_action_oks s t cas`
  note ass = `!!t'. Join t' ∈ set (ca # cas) ==> ¬ not_final_thread s t' ∧ t ≠ t'`
  hence "!!t'. Join t' ∈ set cas ==> ¬ not_final_thread s t' ∧ t ≠ t'" by simp
  hence "cond_action_oks s t cas" by(rule IH)
  moreover have "cond_action_ok s t ca"
  proof(cases ca)
    case (Join t')
    with ass have "¬ not_final_thread s t'" "t ≠ t'" by auto
    thus ?thesis using Join by(auto simp add: not_final_thread_iff)
  qed
  ultimately show ?case by simp
qed

end

locale final_thread_wf = multithreaded _ r
  for r :: "('l,'t,'x,'m,'w,'o) semantics" +
  assumes final_no_red [dest]: "[| final x; r (x, m) ta (x', m') |] ==> False" begin

lemma final_no_redT: 
  "[| s -t\<triangleright>ta-> s'; thr s t = ⌊(x, no_wait_locks)⌋ |] ==> ¬ final x"
by(auto elim!: redT_elims dest: final_no_red)

lemma red_not_final_thread:
  "s -t\<triangleright>ta-> s' ==> not_final_thread s t"
by(fastsimp elim: redT.cases intro: not_final_thread.intros)

lemma redT_preserves_final_thread:
  "[| s -t'\<triangleright>ta-> s'; final_thread s t |] ==> final_thread s' t"
apply(erule redT.cases)
apply(auto simp add: final_thread_def dest: redT_updTs_None redT_updTs_Some intro: redT_updWs_None_implies_None)
done

end

end