Theory FWSemantics

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

section ‹The multithreaded semantics›

theory FWSemantics
imports
  FWWellform
  FWLockingThread
  FWCondAction
  FWInterrupt
begin

inductive redT_upd :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x ⇒ 'm ⇒ ('l,'t,'x,'m,'w) state ⇒ bool"
for s t ta x' m'
where
  "redT_updWs t (wset s) ⦃ta⦄⇘w⇙ ws'
  ⟹ redT_upd s t ta x' m' (redT_updLs (locks s) t ⦃ta⦄⇘l⇙, ((redT_updTs (thr s) ⦃ta⦄⇘t⇙)(t ↦ (x', redT_updLns (locks s) t (snd (the (thr s t))) ⦃ta⦄⇘l⇙)), m'), ws', redT_updIs (interrupts s) ⦃ta⦄⇘i⇙)"

inductive_simps redT_upd_simps [simp]:
  "redT_upd s t ta x' m' s'"

definition redT_acq :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l ⇒f nat) ⇒ ('l,'t,'x,'m,'w) state"
where
  "⋀ln. redT_acq s t ln = (acquire_all (locks s) t ln, ((thr s)(t ↦ (fst (the (thr s t)), no_wait_locks)), shr s), wset s, interrupts s)"

context final_thread begin

inductive actions_ok :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l,'t,'x','m,'w,'o) thread_action ⇒ bool"
  for s :: "('l,'t,'x,'m,'w) state" and t :: 't and ta :: "('l,'t,'x','m,'w,'o) thread_action"
  where
  "⟦ lock_ok_las (locks s) t ⦃ta⦄⇘l⇙; thread_oks (thr s) ⦃ta⦄⇘t⇙; cond_action_oks s t ⦃ta⦄⇘c⇙;
     wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙; interrupt_actions_ok (interrupts s) ⦃ta⦄⇘i⇙ ⟧
  ⟹ actions_ok s t ta"

declare actions_ok.intros [intro!]
declare actions_ok.cases [elim!]

lemma actions_ok_iff [simp]:
  "actions_ok s t ta ⟷
   lock_ok_las (locks s) t ⦃ta⦄⇘l⇙ ∧ thread_oks (thr s) ⦃ta⦄⇘t⇙ ∧ cond_action_oks s t ⦃ta⦄⇘c⇙ ∧
   wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙ ∧ interrupt_actions_ok (interrupts s) ⦃ta⦄⇘i⇙"
by(auto)

lemma actions_ok_thread_oksD:
  "actions_ok s t ta ⟹ thread_oks (thr s) ⦃ta⦄⇘t⇙"
by(erule actions_ok.cases)

inductive actions_ok' :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l,'t,'x','m,'w,'o) thread_action ⇒ bool" where
  "⟦ lock_ok_las' (locks s) t ⦃ta⦄⇘l⇙; thread_oks (thr s) ⦃ta⦄⇘t⇙; cond_action_oks' s t ⦃ta⦄⇘c⇙;
     wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙; interrupt_actions_ok' (interrupts s) ⦃ta⦄⇘i⇙ ⟧
  ⟹ actions_ok' s t ta"

declare actions_ok'.intros [intro!]
declare actions_ok'.cases [elim!]

lemma actions_ok'_iff:
  "actions_ok' s t ta ⟷
   lock_ok_las' (locks s) t ⦃ta⦄⇘l⇙ ∧ thread_oks (thr s) ⦃ta⦄⇘t⇙ ∧ cond_action_oks' s t ⦃ta⦄⇘c⇙ ∧
   wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙ ∧ interrupt_actions_ok' (interrupts s) ⦃ta⦄⇘i⇙"
by auto

lemma actions_ok'_ta_upd_obs:
  "actions_ok' s t (ta_update_obs ta obs) ⟷ actions_ok' s t ta"
by(auto simp add: actions_ok'_iff lock_ok_las'_def ta_upd_simps wset_actions_ok_def)

lemma actions_ok'_empty: "actions_ok' s t ε ⟷ wset s t = None"
by(simp add: actions_ok'_iff lock_ok_las'_def)

lemma actions_ok'_convert_extTA:
  "actions_ok' s t (convert_extTA f ta) = actions_ok' s t ta"
by(simp add: actions_ok'_iff)

inductive actions_subset :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l,'t,'x','m,'w,'o) thread_action ⇒ bool"
where
 "⟦ collect_locks' ⦃ta'⦄⇘l⇙ ⊆ collect_locks ⦃ta⦄⇘l⇙; 
    collect_cond_actions ⦃ta'⦄⇘c⇙ ⊆ collect_cond_actions ⦃ta⦄⇘c⇙;
    collect_interrupts ⦃ta'⦄⇘i⇙ ⊆ collect_interrupts ⦃ta⦄⇘i⇙ ⟧
  ⟹ actions_subset ta' ta"

declare actions_subset.intros [intro!]
declare actions_subset.cases [elim!]

lemma actions_subset_iff:
  "actions_subset ta' ta ⟷ 
   collect_locks' ⦃ta'⦄⇘l⇙ ⊆ collect_locks ⦃ta⦄⇘l⇙ ∧
   collect_cond_actions ⦃ta'⦄⇘c⇙ ⊆ collect_cond_actions ⦃ta⦄⇘c⇙ ∧
   collect_interrupts ⦃ta'⦄⇘i⇙ ⊆ collect_interrupts ⦃ta⦄⇘i⇙"
by auto

lemma actions_subset_refl [intro]:
  "actions_subset ta ta"
by(auto intro: actions_subset.intros collect_locks'_subset_collect_locks del: subsetI)

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

definition final_threads :: "('l,'t,'x,'m,'w) state ⇒ 't set" 
where "final_threads s ≡ {t. final_thread s t}"

lemma [iff]: "t ∈ final_threads s = final_thread s t"
  by (simp add: final_threads_def)

lemma [pred_set_conv]: "final_thread s = (λt. t ∈ final_threads s)"
  by simp

definition mfinal :: "('l,'t,'x,'m,'w) state ⇒ bool"
where "mfinal s ⟷ (∀t x ln. thr s t = ⌊(x, ln)⌋ ⟶ final x ∧ ln = no_wait_locks ∧ wset s t = None)"

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)

lemma mfinalI:
  "(⋀t x ln. thr s t = ⌊(x, ln)⌋ ⟹ final x ∧ ln = no_wait_locks ∧ wset s t = None) ⟹ mfinal s"
unfolding mfinal_def by blast

lemma mfinalD:
  fixes ln
  assumes "mfinal s" "thr s t = ⌊(x, ln)⌋"
  shows "final x" "ln = no_wait_locks" "wset s t = None"
using assms unfolding mfinal_def by blast+

lemma mfinalE:
  fixes ln
  assumes "mfinal s" "thr s t = ⌊(x, ln)⌋"
  obtains "final x" "ln = no_wait_locks" "wset s t = None"
using mfinalD[OF assms] by(rule that)

lemma mfinal_def2: "mfinal s ⟷ dom (thr s) ⊆ final_threads s"
by(fastforce elim: mfinalE final_threadE intro: mfinalI final_threadI)

end

locale multithreaded_base = final_thread +
  constrains final :: "'x ⇒ bool" 
  fixes r :: "('l,'t,'x,'m,'w,'o) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
  and convert_RA :: "'l released_locks ⇒ 'o list"
begin

abbreviation
  r_syntax :: "'t ⇒ 'x ⇒ 'm ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x ⇒ 'm ⇒ bool"
              ("_ ⊢ ⟨_, _⟩ -_→ ⟨_, _⟩" [50,0,0,0,0,0] 80)
where
  "t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩ ≡ t ⊢ (x, m) -ta→ (x', m')"

inductive
  redT :: "('l,'t,'x,'m,'w) state ⇒ 't × ('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l,'t,'x,'m,'w) state ⇒ bool" and
  redT_syntax1 :: "('l,'t,'x,'m,'w) state ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l,'t,'x,'m,'w) state ⇒ bool" ("_ -_▹_→ _" [50,0,0,50] 80)
where
  "s -t▹ta→ s' ≡ redT s (t, ta) s'"

|  redT_normal:
  "⟦ t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩;
     thr s t = ⌊(x, no_wait_locks)⌋;
     actions_ok s t ta;
     redT_upd s t ta x' m' s' ⟧
  ⟹ s -t▹ta→ s'"

| redT_acquire:
  "⋀ln. ⟦ thr s t = ⌊(x, ln)⌋; ¬ waiting (wset s t);
     may_acquire_all (locks s) t ln; ln $ n > 0;
     s' = (acquire_all (locks s) t ln, ((thr s)(t ↦ (x, no_wait_locks)), shr s), wset s, interrupts s) ⟧
  ⟹ s -t▹((K$ []), [], [], [], [], convert_RA ln)→ s'"

abbreviation
  redT_syntax2 :: "('l,'t) locks ⇒ ('l,'t,'x) thread_info × 'm ⇒ ('w,'t) wait_sets ⇒ 't interrupts
                   ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action
                   ⇒ ('l,'t) locks ⇒ ('l,'t,'x) thread_info × 'm ⇒ ('w,'t) wait_sets ⇒ 't interrupts ⇒ bool"
                  ("⟨_, _, _, _⟩ -_▹_→ ⟨_, _, _, _⟩" [0,0,0,0,0,0,0,0,0] 80)
where
  "⟨ls, tsm, ws, is⟩ -t▹ta→ ⟨ls', tsm', ws', is'⟩ ≡ (ls, tsm, ws, is) -t▹ta→ (ls', tsm', ws', is')"


lemma redT_elims [consumes 1, case_names normal acquire]:
  assumes red: "s -t▹ta→ s'"
  and normal: "⋀x x' m' ws'.
    ⟦ t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩;
      thr s t = ⌊(x, no_wait_locks)⌋;
      lock_ok_las (locks s) t ⦃ta⦄⇘l⇙;
      thread_oks (thr s) ⦃ta⦄⇘t⇙;
      cond_action_oks s t ⦃ta⦄⇘c⇙;
      wset_actions_ok (wset s) t ⦃ta⦄⇘w⇙;
      interrupt_actions_ok (interrupts s) ⦃ta⦄⇘i⇙;
      redT_updWs t (wset s) ⦃ta⦄⇘w⇙ ws';
      s' = (redT_updLs (locks s) t ⦃ta⦄⇘l⇙, ((redT_updTs (thr s) ⦃ta⦄⇘t⇙)(t ↦ (x', redT_updLns (locks s) t no_wait_locks ⦃ta⦄⇘l⇙)), m'), ws', redT_updIs (interrupts s) ⦃ta⦄⇘i⇙) ⟧
    ⟹ thesis"
   and acquire: "⋀x ln n.
    ⟦ thr s t = ⌊(x, ln)⌋;
      ta = (K$ [], [], [], [], [], convert_RA ln);
      ¬ waiting (wset s t);
      may_acquire_all (locks s) t ln; 0 < ln $ n;
      s' = (acquire_all (locks s) t ln, ((thr s)(t ↦ (x, no_wait_locks)), shr s), wset s, interrupts s) ⟧
    ⟹ thesis"
  shows thesis
using red
proof cases
  case redT_normal
  thus ?thesis using normal by(cases s')(auto)
next
  case redT_acquire
  thus ?thesis by-(rule acquire, fastforce+)
qed

definition
  RedT :: "('l,'t,'x,'m,'w) state ⇒ ('t × ('l,'t,'x,'m,'w,'o) thread_action) list ⇒ ('l,'t,'x,'m,'w) state ⇒ bool"
          ("_ -▹_→* _" [50,0,50] 80)
where
  "RedT ≡ rtrancl3p redT"

lemma RedTI:
  "rtrancl3p redT s ttas s' ⟹ RedT s ttas s'"
by(simp add: RedT_def)

lemma RedTE:
  "⟦ RedT s ttas s'; rtrancl3p redT s ttas s' ⟹ P ⟧ ⟹ P"
by(auto simp add: RedT_def)

lemma RedTD:
  "RedT s ttas s' ⟹ rtrancl3p redT s ttas s'"
by(simp add: RedT_def)

lemma RedT_induct [consumes 1, case_names refl step]:
  "⟦ s -▹ttas→* s';
     ⋀s. P s [] s;
     ⋀s ttas s' t ta s''. ⟦ s -▹ttas→* s'; P s ttas s'; s' -t▹ta→ s'' ⟧ ⟹ P s (ttas @ [(t, ta)]) s''⟧
  ⟹ P s ttas s'"
unfolding RedT_def
by(erule rtrancl3p.induct) auto

lemma RedT_induct' [consumes 1, case_names refl step]:
  "⟦ s -▹ttas→* s';
     P s [] s;
     ⋀ttas s' t ta s''. ⟦ s -▹ttas→* s'; P s ttas s'; s' -t▹ta→ s'' ⟧ ⟹ P s (ttas @ [(t, ta)]) s''⟧
  ⟹ P s ttas s'"
  unfolding RedT_def
apply(erule rtrancl3p_induct', blast)
apply(case_tac b, blast)
done

lemma RedT_lift_preserveD:
  assumes Red: "s -▹ttas→* s'"
  and P: "P s"
  and preserve: "⋀s t tas s'. ⟦ s -t▹tas→ s'; P s ⟧ ⟹ P s'"
  shows "P s'"
  using Red P
  by(induct rule: RedT_induct)(auto intro: preserve)

lemma RedT_refl [intro, simp]:
  "s -▹[]→* s"
by(rule RedTI)(rule rtrancl3p_refl)

lemma redT_has_locks_inv:
  "⟦ ⟨ls, (ts, m), ws, is⟩ -t▹ta→ ⟨ls', (ts', m'), ws', is'⟩; t ≠ t' ⟧ ⟹
  has_locks (ls $ l) t' = has_locks (ls' $ l) t'"
by(auto elim!: redT.cases intro: redT_updLs_has_locks[THEN sym, simplified] may_acquire_all_has_locks_acquire_locks[symmetric])

lemma redT_has_lock_inv:
  "⟦ ⟨ls, (ts, m), ws, is⟩ -t▹ta→ ⟨ls', (ts', m'), ws', is'⟩; t ≠ t' ⟧
  ⟹ has_lock (ls' $ l) t' = has_lock (ls $ l) t'"
by(auto simp add: redT_has_locks_inv)

lemma redT_ts_Some_inv:
  "⟦ ⟨ls, (ts, m), ws, is⟩ -t▹ta→ ⟨ls', (ts', m'), ws', is'⟩; t ≠ t'; ts t' = ⌊x⌋ ⟧ ⟹ ts' t' = ⌊x⌋"
by(fastforce elim!: redT.cases simp: redT_updTs_upd[THEN sym] intro: redT_updTs_Some)

lemma redT_thread_not_disappear:
  "⟦ s -t▹ta→ s'; thr s' t' = None⟧ ⟹ thr s t' = None"
apply(cases "t ≠ t'")
apply(auto elim!: redT_elims simp add: redT_updTs_upd[THEN sym] intro: redT_updTs_None)
done

lemma RedT_thread_not_disappear:
  "⟦ s -▹ttas→* s'; thr s' t' = None⟧ ⟹ thr s t' = None"
apply(erule contrapos_pp[where Q="thr s' t' = None"])
apply(drule (1) RedT_lift_preserveD)
apply(erule_tac Q="thr sa t' = None" in contrapos_nn)
apply(erule redT_thread_not_disappear)
apply(auto)
done

lemma redT_preserves_wset_thread_ok:
  "⟦ s -t▹ta→ s'; wset_thread_ok (wset s) (thr s) ⟧ ⟹ wset_thread_ok (wset s') (thr s')"
by(fastforce elim!: redT.cases intro: wset_thread_ok_upd redT_updTs_preserves_wset_thread_ok redT_updWs_preserve_wset_thread_ok)

lemma RedT_preserves_wset_thread_ok:
  "⟦ s -▹ttas→* s'; wset_thread_ok (wset s) (thr s) ⟧ ⟹ wset_thread_ok (wset s') (thr s')"
by(erule (1) RedT_lift_preserveD)(erule redT_preserves_wset_thread_ok)

lemma redT_new_thread_ts_Some:
  "⟦ s -t▹ta→ s'; NewThread t' x m'' ∈ set ⦃ta⦄⇘t⇙; wset_thread_ok (wset s) (thr s) ⟧
  ⟹ thr s' t' = ⌊(x, no_wait_locks)⌋"
by(erule redT_elims)(auto dest: thread_oks_new_thread elim: redT_updTs_new_thread_ts)

lemma RedT_new_thread_ts_not_None:
  "⟦ s -▹ttas→* s'; NewThread t x m'' ∈ set (concat (map (thr_a ∘ snd) ttas)); wset_thread_ok (wset s) (thr s) ⟧
   ⟹ thr s' t ≠ None"
proof(induct rule: RedT_induct)
  case refl thus ?case by simp
next
  case (step S TTAS S' T TA S'')
  note Red = ‹S -▹TTAS→* S'›
  note IH = ‹⟦ NewThread t x m'' ∈ set (concat (map (thr_a ∘ snd) TTAS)); wset_thread_ok (wset S) (thr S) ⟧ ⟹ thr S' t ≠ None›
  note red = ‹S' -T▹TA→ S''›
  note ins = ‹NewThread t x m'' ∈ set (concat (map (thr_a ∘ snd) (TTAS @ [(T, TA)])))›
  note wto = ‹wset_thread_ok (wset S) (thr S)›
  from Red wto have wto': "wset_thread_ok (wset S') (thr S')" by(auto dest: RedT_preserves_wset_thread_ok)  
  show ?case
  proof(cases "NewThread t x m'' ∈ set ⦃TA⦄⇘t⇙")
    case True thus ?thesis using red wto'
      by(auto dest!: redT_new_thread_ts_Some)
  next
    case False
    hence "NewThread t x m'' ∈ set (concat (map (thr_a ∘ snd) TTAS))" using ins by(auto)
    hence "thr S' t ≠ None" using wto by(rule IH)
    with red show ?thesis
      by -(erule contrapos_nn, auto dest: redT_thread_not_disappear)
  qed
qed

lemma redT_preserves_lock_thread_ok:
  "⟦ s -t▹ta→ s'; lock_thread_ok (locks s) (thr s) ⟧ ⟹ lock_thread_ok (locks s') (thr s')"
by(auto elim!: redT_elims intro: redT_upds_preserves_lock_thread_ok acquire_all_preserves_lock_thread_ok)

lemma RedT_preserves_lock_thread_ok:
  "⟦ s -▹ttas→* s'; lock_thread_ok (locks s) (thr s) ⟧ ⟹ lock_thread_ok (locks s') (thr s')"
by(erule (1) RedT_lift_preserveD)(erule redT_preserves_lock_thread_ok)

lemma redT_ex_new_thread:
  assumes "s -t'▹ta→ s'" "wset_thread_ok (wset s) (thr s)" "thr s' t = ⌊(x, w)⌋" "thr s t = None"
  shows "∃m. NewThread t x m ∈ set ⦃ta⦄⇘t⇙ ∧ w = no_wait_locks"
using assms
by cases (fastforce split: if_split_asm dest: wset_thread_okD redT_updTs_new_thread)+

lemma redT_ex_new_thread':
  assumes "s -t'▹ta→ s'" "thr s' t = ⌊(x, w)⌋" "thr s t = None"
  shows "∃m x. NewThread t x m ∈ set ⦃ta⦄⇘t⇙"
using assms
by(cases)(fastforce split: if_split_asm dest!: redT_updTs_new_thread)+

definition deterministic :: "('l,'t,'x,'m,'w) state set ⇒ bool"
where
  "deterministic I ⟷ 
  (∀s t x ta' x' m' ta'' x'' m''. 
    s ∈ I
    ⟶ thr s t = ⌊(x, no_wait_locks)⌋
    ⟶ t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x', m'⟩ 
    ⟶ t ⊢ ⟨x, shr s⟩ -ta''→ ⟨x'', m''⟩ 
    ⟶ actions_ok s t ta' ⟶ actions_ok s t ta''
    ⟶ ta' = ta'' ∧ x' = x'' ∧ m' = m'') ∧ invariant3p redT I"

lemma determisticI:
  "⟦⋀s t x ta' x' m' ta'' x'' m''.
      ⟦ s ∈ I; thr s t = ⌊(x, no_wait_locks)⌋; 
        t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x', m'⟩; t ⊢ ⟨x, shr s⟩ -ta''→ ⟨x'', m''⟩; 
        actions_ok s t ta'; actions_ok s t ta'' ⟧
      ⟹ ta' = ta'' ∧ x' = x'' ∧ m' = m'';
    invariant3p redT I ⟧
  ⟹ deterministic I"
unfolding deterministic_def by blast

lemma deterministicD:
  "⟦ deterministic I;
    t ⊢ ⟨x, shr s⟩ -ta'→ ⟨x', m'⟩; t ⊢ ⟨x, shr s⟩ -ta''→ ⟨x'', m''⟩;
    thr s t = ⌊(x, no_wait_locks)⌋; actions_ok s t ta'; actions_ok s t ta''; s ∈ I ⟧
  ⟹ ta' = ta'' ∧ x' = x'' ∧ m' = m''"
unfolding deterministic_def by blast

lemma deterministic_invariant3p:
  "deterministic I ⟹ invariant3p redT I"
unfolding deterministic_def by blast

lemma deterministic_THE:
  "⟦ deterministic I; thr s t = ⌊(x, no_wait_locks)⌋; t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩; actions_ok s t ta; s ∈ I ⟧
  ⟹ (THE (ta, x', m'). t ⊢ ⟨x, shr s⟩ -ta→ ⟨x', m'⟩ ∧ actions_ok s t ta) = (ta, x', m')"
by(rule the_equality)(blast dest: deterministicD)+

end

locale multithreaded = multithreaded_base +
  constrains final :: "'x ⇒ bool"
  and r :: "('l,'t,'x,'m,'w,'o) semantics"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  assumes new_thread_memory: "⟦ t ⊢ s -ta→ s'; NewThread t' x m ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ m = snd s'"
  and final_no_red: "⟦ t ⊢ (x, m) -ta→ (x', m'); final x ⟧ ⟹ False"
begin

lemma redT_new_thread_common:
  "⟦ s -t▹ta→ s'; NewThread t' x m'' ∈ set ⦃ta⦄⇘t⇙; ⦃ta⦄⇘w⇙ = [] ⟧ ⟹ m'' = shr s'"
by(auto elim!: redT_elims rtrancl3p_cases dest: new_thread_memory)

lemma redT_new_thread:
  assumes "s -t'▹ta→ s'" "thr s' t = ⌊(x, w)⌋" "thr s t = None" "⦃ta⦄⇘w⇙ = []"
  shows "NewThread t x (shr s') ∈ set ⦃ta⦄⇘t⇙ ∧ w = no_wait_locks"
using assms
apply(cases rule: redT_elims)
apply(auto split: if_split_asm del: conjI elim!: rtrancl3p_cases)
apply(drule (2) redT_updTs_new_thread)
apply(auto dest: new_thread_memory)
done

lemma final_no_redT: 
  "⟦ s -t▹ta→ s'; thr s t = ⌊(x, no_wait_locks)⌋ ⟧ ⟹ ¬ final x"
by(auto elim!: redT_elims dest: final_no_red)

lemma mfinal_no_redT:
  assumes redT: "s -t▹ta→ s'" and mfinal: "mfinal s"
  shows False
using redT mfinalD[OF mfinal, of t]
by cases (metis final_no_red, metis neq_no_wait_locks_conv)

end

end