Theory FWSemantics

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

header {* \isaheader{The multithreaded semantics} *}

theory FWSemantics imports
  FWWellform
  FWLockingThread
  FWWait
  FWCondAction
begin

definition 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"
 where 
  "redT_upd s t ta x' m' =
   (redT_updLs (locks s) t \<lbrace>ta\<rbrace>l,
    ((redT_updTs (thr s) \<lbrace>ta\<rbrace>t)(t \<mapsto> (x', redT_updLns (locks s) t (snd (the (thr s t))) \<lbrace>ta\<rbrace>l)), m'),
    redT_updWs (wset s) t \<lbrace>ta\<rbrace>w)"

declare redT_upd_def [simp]

definition redT_acq :: "('l,'t,'x,'m,'w) state => 't => ('l =>f nat) => ('l,'t,'x,'m,'w) state"
where
  "redT_acq s t ln = (acquire_all (locks s) t ln, ((thr s)(t \<mapsto> (fst (the (thr s t)), no_wait_locks)), shr s), wset s)"

declare redT_upd_def [simp]

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 \<lbrace>ta\<rbrace>l; thread_oks (thr s) \<lbrace>ta\<rbrace>t; cond_action_oks s t \<lbrace>ta\<rbrace>c |] ==> 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 \<lbrace>ta\<rbrace>l ∧ thread_oks (thr s) \<lbrace>ta\<rbrace>t ∧ cond_action_oks s t \<lbrace>ta\<rbrace>c"
by(auto)

lemma actions_ok_upd_empty_inv:
  "thr s t = ⌊xln⌋ ==> actions_ok (redT_upd s t ε x' (shr s)) t ta = actions_ok s t ta"
by(auto simp add: redT_updLns_def redT_updLs_def cond_action_oks_upd thread_oks_upd)

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 \<lbrace>ta\<rbrace>l; thread_oks (thr s) \<lbrace>ta\<rbrace>t; cond_action_oks' s t \<lbrace>ta\<rbrace>c |] ==> 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 \<lbrace>ta\<rbrace>l ∧ thread_oks (thr s) \<lbrace>ta\<rbrace>t ∧ cond_action_oks' s t \<lbrace>ta\<rbrace>c"
by auto

inductive actions_subset :: "('l,'t,'x,'m,'w,'o) thread_action => ('l,'t,'x','m,'w,'o) thread_action => bool"
where
 "[| collect_locks' \<lbrace>ta'\<rbrace>l ⊆ collect_locks \<lbrace>ta\<rbrace>l; collect_cond_actions \<lbrace>ta'\<rbrace>c ⊆ collect_cond_actions \<lbrace>ta\<rbrace>c |] 
  ==> actions_subset ta' ta"

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

lemma actions_subset_iff:
  "actions_subset ta' ta <-> collect_locks' \<lbrace>ta'\<rbrace>l ⊆ collect_locks \<lbrace>ta\<rbrace>l ∧
                             collect_cond_actions \<lbrace>ta'\<rbrace>c ⊆ collect_cond_actions \<lbrace>ta\<rbrace>c"
by auto

lemma actions_subset_conv: 
  "actions_subset ta' ta <-> (∀l. must_acquire_lock (\<lbrace>ta'\<rbrace>lf l) --> Lock ∈ set (\<lbrace>ta\<rbrace>lf l)) ∧
                             set \<lbrace>ta'\<rbrace>c ⊆ set \<lbrace>ta\<rbrace>c"
apply(auto simp add: collect_locks_def collect_locks'_def)
apply(case_tac x)
apply(auto)
done

lemma actions_subset_intro:
  "[| ∀l. must_acquire_lock (\<lbrace>ta'\<rbrace>lf l) --> Lock ∈ set (\<lbrace>ta\<rbrace>lf l); set \<lbrace>ta'\<rbrace>c ⊆ set \<lbrace>ta\<rbrace>c |] ==> actions_subset ta' ta"
  unfolding actions_subset_conv
  by blast

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

lemma actions_ok'_empty: "actions_ok' s t ε"
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(auto simp add: actions_ok'_iff)

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 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:
  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:
  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)

end

datatype ('l,'o) observable =
    Silent
  | ReacquireLocks "'l released_locks"
  | Observable 'o

primrec observable_of :: "'o option => ('l, 'o) observable"
where 
  "observable_of None = Silent"
| "observable_of (Some obs) = Observable obs"

definition observable_ta_of :: "('l,'t,'x,'m,'w,'o option) thread_action => ('l,'t,'x,'m,'w,('l,'o) observable) thread_action"
where "observable_ta_of ta = (\<lbrace>ta\<rbrace>l, \<lbrace>ta\<rbrace>t, \<lbrace>ta\<rbrace>c, \<lbrace>ta\<rbrace>w, observable_of \<lbrace>ta\<rbrace>o)"

lemma locks_a_observable_ta_of [simp]:
  "\<lbrace>observable_ta_of ta\<rbrace>l = \<lbrace>ta\<rbrace>l"
by(simp add: observable_ta_of_def)

lemma thr_a_observable_ta_of [simp]:
  "\<lbrace>observable_ta_of ta\<rbrace>t = \<lbrace>ta\<rbrace>t"
by(simp add: observable_ta_of_def)

lemma cond_a_observable_ta_of [simp]:
  "\<lbrace>observable_ta_of ta\<rbrace>c = \<lbrace>ta\<rbrace>c"
by(simp add: observable_ta_of_def)

lemma wset_a_observable_ta_of [simp]:
  "\<lbrace>observable_ta_of ta\<rbrace>w = \<lbrace>ta\<rbrace>w"
by(simp add: observable_ta_of_def)

lemma obs_a_observable_ta_of [simp]:
  "\<lbrace>observable_ta_of ta\<rbrace>o = observable_of \<lbrace>ta\<rbrace>o"
by(simp add: observable_ta_of_def)

lemma Silent_eq_observable_of [simp]:
  "Silent = observable_of obs <-> obs = None"
by(cases obs)(simp_all)

lemma observable_of_eq_Silent [simp]:
  "observable_of obs = Silent <-> obs = None"
by(cases obs)(simp_all)

lemma ReacquireLocks_neq_observable_of [simp]:
  "ReacquireLocks ln ≠ observable_of obs"
by(cases obs) simp_all

lemmas observable_of_neq_ReacquireLocks [simp] = ReacquireLocks_neq_observable_of[symmetric]

lemma Observable_eq_observable_of [simp]:
  "Observable ob = observable_of obs <-> obs = Some ob"
by(cases obs) auto

lemma observable_of_eq_Observable [simp]:
  "observable_of obs = Observable ob <-> obs = Some ob"
by(cases obs) simp_all

lemma observable_of_inject [simp]:
  "observable_of obs = observable_of obs' <-> obs = obs'"
apply(cases obs)
 apply(cases obs', simp, simp)
apply(cases obs', simp_all)
done

lemma observable_ta_of_inject [simp]:
  "observable_ta_of ta = observable_ta_of ta' <-> ta = ta'"
by(cases ta, cases ta')(auto simp add: observable_ta_of_def)


locale multithreaded_base = final_thread +
  trsys r
  for r :: "('l,'t,'x,'m,'w,'o) semantics" ("_ -_-> _" [50,0,50] 80) +
  constrains final :: "'x => bool"
begin

abbreviation
  r_syntax :: "'x => 'm => ('l,'t,'x,'m,'w,'o option) thread_action => 'x => 'm => bool" ("⟨_, _⟩ -_-> ⟨_, _⟩" [0,0,0,0,0] 80)
where
  "⟨x, m⟩ -ta-> ⟨x', m'⟩ ≡ (x, m) -ta-> (x', m')"

inductive
  redT :: "('l,'t,'x,'m,'w) state => 't × ('l,'t,'x,'m,'w,('l,'o) observable) thread_action => ('l,'t,'x,'m,'w) state => bool" and
  redT_syntax1 :: "('l,'t,'x,'m,'w) state => 't => ('l,'t,'x,'m,'w,('l,'o) observable) thread_action => ('l,'t,'x,'m,'w) state => bool" ("_ -_\<triangleright>_-> _" [50,0,0,50] 80)
where
  "s -t\<triangleright>ta-> s' ≡ redT s (t, ta) s'"
|  redT_normal:
  "[| ⟨x, shr s⟩ -ta-> ⟨x', m'⟩;
     thr s t = ⌊(x, no_wait_locks)⌋; wset s t = None;
     actions_ok s t ta;
     s' = redT_upd s t ta x' m' |]
  ==> s -t\<triangleright>observable_ta_of ta-> s'"

| redT_acquire:
  "[| thr s t = ⌊(x, ln)⌋; wset s t = None;
     may_acquire_all (locks s) t ln; lnf n > 0;
     s' = (acquire_all (locks s) t ln, (thr s(t \<mapsto> (x, no_wait_locks)), shr s), wset s) |]
  ==> s -t\<triangleright>((λf []), [], [], [], ReacquireLocks ln)-> s'"

abbreviation
  redT_syntax2 :: "('l,'t) locks => ('l,'t,'x) thread_info × 'm => ('w,'t) wait_sets
                   => 't => ('l,'t,'x,'m,'w,('l,'o) observable) thread_action
                   => ('l,'t) locks => ('l,'t,'x) thread_info × 'm => ('w,'t) wait_sets => bool"
                  ("⟨_, _, _⟩ -_\<triangleright>_-> ⟨_, _, _⟩" [0,0,0,0,0,0,0,0] 80)
where
  "⟨ls, tsm, ws⟩ -t\<triangleright>ta-> ⟨ls', tsm', ws'⟩ ≡ (ls, tsm, ws) -t\<triangleright>ta-> (ls', tsm', ws')"

lemma redT_elims [consumes 1, case_names normal acquire]:
  assumes red: "s -t\<triangleright>ta-> s'"
  and normal: "!!x x' ta'. [| ⟨x, shr s⟩ -ta'-> ⟨x', shr s'⟩; ta = observable_ta_of ta'; thr s t = ⌊(x, no_wait_locks)⌋;
                        lock_ok_las (locks s) t \<lbrace>ta\<rbrace>l; thread_oks (thr s) \<lbrace>ta\<rbrace>t; wset s t = None;
                        cond_action_oks s t \<lbrace>ta\<rbrace>c;
                        locks s' = redT_updLs (locks s) t \<lbrace>ta\<rbrace>l;
                        thr s' = (redT_updTs (thr s) \<lbrace>ta\<rbrace>t)(t \<mapsto> (x', redT_updLns (locks s) t no_wait_locks \<lbrace>ta\<rbrace>l));
                        wset s' = redT_updWs (wset s) t \<lbrace>ta\<rbrace>w |] ==> thesis"
  and acquire: "!!x ln n. [| thr s t = ⌊(x, ln)⌋; ta = (λf [], [], [], [], ReacquireLocks ln);
                           wset s t = None; may_acquire_all (locks s) t ln; lnf n > 0;
                           locks s' = acquire_all (locks s) t ln;
                           thr s' = thr s(t \<mapsto> (x, no_wait_locks));
                           wset s' = wset s; shr s' = shr s |] ==> thesis"
  shows thesis
using red
apply -
apply(erule redT.cases)
 apply(rule normal, fastsimp+)
apply(rule acquire, fastsimp+)
done

lemma redT_elims4 [consumes 1, case_names normal acquire]:
  assumes red: "⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩"
  and normal: "!!x x' ta'. [| ⟨x, m⟩ -ta'-> ⟨x', m'⟩; ta = observable_ta_of ta'; ts t = ⌊(x, no_wait_locks)⌋;
                        lock_ok_las ls t \<lbrace>ta\<rbrace>l; thread_oks ts \<lbrace>ta\<rbrace>t; ws t = None; cond_action_oks (ls, (ts, m), ws) t \<lbrace>ta\<rbrace>c;
                        ls' = redT_updLs ls t \<lbrace>ta\<rbrace>l;
                        ts' = (redT_updTs ts \<lbrace>ta\<rbrace>t)(t \<mapsto> (x', redT_updLns ls t no_wait_locks \<lbrace>ta\<rbrace>l));
                        ws' = redT_updWs ws t \<lbrace>ta\<rbrace>w |] ==> thesis"
  and acquire: "!!x ln n. [| ts t = ⌊(x, ln)⌋; ta = (λf [], [], [], [], ReacquireLocks ln);
                           ws t = None; may_acquire_all ls t ln; lnf n > 0;
                           ls' = acquire_all ls t ln;
                           ts' = ts(t \<mapsto> (x, no_wait_locks));
                           ws' = ws; m' = m |] ==> thesis"
  shows "thesis"
using red
apply -
apply(erule redT.cases)
 apply(rule normal, fastsimp+)
apply(rule acquire, fastsimp+)
done

definition
  RedT :: "('l,'t,'x,'m,'w) state => ('t × ('l,'t,'x,'m,'w,('l,'o) observable) thread_action) list => ('l,'t,'x,'m,'w) state => bool"
          ("_ -\<triangleright>_->* _" [50,0,50] 80)
where
  "RedT ≡ rtrancl3p redT"

abbreviation
  RedT_syntax :: "('l,'t) locks => ('l,'t,'x) thread_info × 'm => ('w,'t) wait_sets
                  => ('t × ('l,'t,'x,'m,'w,('l,'o) observable) thread_action) list 
                  => ('l,'t) locks => ('l,'t,'x) thread_info × 'm => ('w,'t) wait_sets => bool"
                 ("⟨_, _, _⟩ -\<triangleright>_->* ⟨_, _, _⟩" [0,0,0,0,0,0,0] 80)
where
  "⟨ls, tsm, ws⟩ -\<triangleright>ttas->* ⟨ls', tsm', ws'⟩ ≡ (ls, tsm, ws) -\<triangleright>ttas->* (ls', tsm', ws')"

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 -\<triangleright>ttas->* s';
     !!s. P s [] s;
     !!s ttas s' t ta s''. [| s -\<triangleright>ttas->* s'; P s ttas s'; s' -t\<triangleright>ta-> s'' |] ==> P s (ttas @ [(t, ta)]) s''|]
  ==> P s ttas s'"
unfolding RedT_def
by(erule rtrancl3p.induct) auto

lemma RedT_induct4 [consumes 1, case_names refl step]:
  "[| ⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩;
     !!ls ts m ws. P ls ts m ws [] ls ts m ws;
     !!ls ts m ws ttas ls' ts' m' ws' t ta ls'' ts'' m'' ws''.
       [| ⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩; 
         P ls ts m ws ttas ls' ts' m' ws';
         ⟨ls', (ts', m'), ws'⟩ -t\<triangleright>ta-> ⟨ls'', (ts'', m''), ws''⟩ |] 
       ==> P ls ts m ws (ttas @ [(t, ta)]) ls'' ts'' m'' ws'' |]
  ==> P ls ts m ws ttas ls' ts' m' ws'"
unfolding RedT_def
by(erule rtrancl3p_induct4')(auto)

lemma RedT_induct' [consumes 1, case_names refl step]:
  "[| s -\<triangleright>ttas->* s';
     P s [] s;
     !!ttas s' t ta s''. [| s -\<triangleright>ttas->* s'; P s ttas s'; s' -t\<triangleright>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 -\<triangleright>ttas->* s'"
  and P: "P s"
  and preserve: "!!s t tas s'. [| s -t\<triangleright>tas-> s'; P s |] ==> P s'"
  shows "P s'"
  using Red P
  by(induct rule: RedT_induct)(auto intro: preserve)

lemma RedT_lift_preserveD4:
  "[| ⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩; 
     P ls ts m ws;
     !!ls ts m ws t ta ls' ts' m' ws'. [| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; P ls ts m ws |] ==> P ls' ts' m' ws' |]
  ==> P ls' ts' m' ws'"
by(drule RedT_lift_preserveD[where P="(λ(ls, (ts, m), ws). P ls ts m ws)"])(auto)

lemma RedT_refl [intro, simp]:
  "s -\<triangleright>[]->* s"
by(rule RedTI)(rule rtrancl3p_refl)

lemma redT_has_locks_inv:
  "[| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; t ≠ t' |] ==>
  has_locks (lsf l) t' = has_locks (ls'f 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⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; t ≠ t' |]
  ==> has_lock (ls'f l) t' = has_lock (lsf l) t'"
by(auto simp add: redT_has_locks_inv)

lemma redT_ts_Some_inv:
  "[| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; t ≠ t'; ts t' = ⌊x⌋ |] ==> ts' t' = ⌊x⌋"
by(auto elim!: redT.cases simp: redT_updTs_upd[THEN sym] intro: redT_updTs_Some)

lemma redT_thread_not_disappear:
  "[| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; ts' t' = None|] ==> ts t' = None"
apply(cases "t ≠ t'")
 apply(erule redT_elims4)
  apply(clarsimp)
  apply(erule redT_updTs_None)
 apply(clarsimp)
apply(auto elim!: redT_elims4 simp add: redT_updTs_upd[THEN sym])
done

lemma RedT_thread_not_disappear:
  "[| ⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩; ts' t' = None|] ==> ts t' = None"
apply(erule contrapos_pp[where Q="ts' t' = None"])
apply(drule RedT_lift_preserveD4)
 apply(assumption)
apply(erule_tac Q="tsa t' = None" in contrapos_nn)
apply(erule redT_thread_not_disappear)
apply(auto)
done

lemma redT_new_thread_ts_Some:
  "[| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; NewThread t' x m'' ∈ set \<lbrace>ta\<rbrace>t |]
  ==> ts' t' = ⌊(x, no_wait_locks)⌋"
by(erule redT_elims4)(auto dest: thread_oks_new_thread elim: redT_updTs_new_thread_ts)

lemma RedT_new_thread_ts_not_None:
  "[| ⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩;
     NewThread t x m'' ∈ set (\<down>map (thr_a o snd) ttas\<down>) |]
   ==> ts' t ≠ None"
proof(induct rule: RedT_induct4)
  case refl thus ?case by simp
next
  case (step LS TS M WS TTAS LS' TS' M' WS' T TA LS'' TS'' M'' WS'')
  note Red = `⟨LS, (TS, M), WS⟩ -\<triangleright>TTAS->* ⟨LS', (TS', M'), WS'⟩`
  note IH = `NewThread t x m'' ∈ set (\<down>map (thr_a o snd) TTAS\<down>) ==> TS' t ≠ None`
  note red = `⟨LS', (TS', M'), WS'⟩ -T\<triangleright>TA-> ⟨LS'', (TS'', M''), WS''⟩`
  note ins = `NewThread t x m'' ∈ set (\<down>map (thr_a o snd) (TTAS @ [(T, TA)])\<down>)`
  show ?case
  proof(cases "NewThread t x m'' ∈ set \<lbrace>TA\<rbrace>t")
    case True thus ?thesis using red
      by(auto dest!: redT_new_thread_ts_Some)
  next
    case False
    hence "NewThread t x m'' ∈ set (\<down>map (thr_a o snd) TTAS\<down>)" using ins by(auto)
    hence "TS' t ≠ None" by -(rule IH)
    with red show ?thesis
      by -(erule contrapos_nn, erule redT_thread_not_disappear)
  qed
qed

lemma redT_preserves_lock_thread_ok:
  "[| s -t\<triangleright>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 -\<triangleright>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)

end

locale multithreaded = multithreaded_base +
  constrains final :: "'x => bool"
  and r :: "('l,'t,'x,'m,'w,'o) semantics"
  assumes new_thread_memory: "[| s -ta-> s'; NewThread t x m ∈ set \<lbrace>ta\<rbrace>t |] ==> m = snd s'"
begin

lemma redT_new_thread_common:
  "[| ⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩; NewThread t' x m'' ∈ set \<lbrace>ta\<rbrace>t |] ==> m'' = m'"
by(auto elim!: redT_elims4 dest: new_thread_memory)

lemma redT_new_thread:
  "[| s -t'\<triangleright>ta-> s'; thr s' t = ⌊(x, w)⌋; thr s t = None |]
  ==> NewThread t x (shr s') ∈ set \<lbrace>ta\<rbrace>t ∧ w = no_wait_locks"
proof(induct rule: redT_elims)
  case (normal X X' ta')
  from `thr s t' = ⌊(X, no_wait_locks)⌋` `thr s t = None`
  have "t' ≠ t" by auto
  with `thr s' = redT_updTs (thr s) \<lbrace>ta\<rbrace>t(t' \<mapsto> (X', redT_updLns (locks s) t' no_wait_locks \<lbrace>ta\<rbrace>l))`
    `thr s' t = ⌊(x, w)⌋`
  have "redT_updTs (thr s) \<lbrace>ta\<rbrace>t t = ⌊(x, w)⌋" by(auto)
  with `thr s t = None` `thread_oks (thr s) \<lbrace>ta\<rbrace>t`
  obtain m where "NewThread t x m ∈ set \<lbrace>ta\<rbrace>t" "w = no_wait_locks"
    by(auto dest: redT_updTs_new_thread)
  with `⟨X, shr s⟩ -ta'-> ⟨X', shr s'⟩` `ta = observable_ta_of ta'`
  show ?case by(auto dest: new_thread_memory)
next
  case acquire
  thus ?thesis by(auto split: split_if_asm)
qed

lemma RedT_newThread_unique:
  assumes red: "⟨ls, (ts, m), ws⟩ -\<triangleright>ttas->* ⟨ls', (ts', m'), ws'⟩"
  and ts't: "ts' t = ⌊(x, w)⌋"
  and tst: "ts t = None"
  shows "∃!n. n < length ttas ∧ (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (ttas!n))))"
using assms
proof(induct arbitrary: x w rule: RedT_induct4)
  case refl thus ?case by auto
next
  case (step LS TS M WS TTAS LS' TS' M' WS' T TA LS'' TS'' M'' WS'' X W)
  note RedT = `⟨LS, (TS, M), WS⟩ -\<triangleright>TTAS->* ⟨LS', (TS', M'), WS'⟩`
  note IH = `!!x w. [|TS' t = ⌊(x, w)⌋; TS t = None|] 
             ==> ∃!n. n < length TTAS ∧ (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (TTAS ! n))))`
  note red = `⟨LS', (TS', M'), WS'⟩ -T\<triangleright>TA-> ⟨LS'', (TS'', M''), WS''⟩`
  note ts''t = `TS'' t = ⌊(X, W)⌋`
  note tst = `TS t = None`
  show ?case
  proof(cases "TS' t")
    case None
    note ts't = `TS' t = None`
    with ts''t red have ta: "NewThread t X M'' ∈ set \<lbrace>TA\<rbrace>t"
      by (auto dest: redT_new_thread)
    show ?thesis
    proof(rule ex1I)
      show "length TTAS < length (TTAS @ [(T, TA)]) ∧
            (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! length TTAS))))"
        using ta by auto
    next
      fix n'
      assume "n' < length (TTAS @ [(T, TA)]) ∧
              (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n'))))"
      hence n'l: "n' < length (TTAS @ [(T, TA)])" 
        and blubb: "∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n')))" 
        by auto
      from blubb obtain m' x'
        where e'x': "NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n')))"
        by blast
      { assume "n' < length TTAS"
        with e'x' have "NewThread t x' m' ∈ set (\<down>map (thr_a o snd) TTAS\<down>)"
          apply(simp add: nth_append)
          apply(erule_tac x="TTAS ! n'" in bexI)
          by auto
        hence "TS' t ≠ None" using RedT by -(erule RedT_new_thread_ts_not_None)
        with ts't have False by simp }
      thus "n' = length TTAS" using n'l by(simp, arith)
    qed
  next
    fix a
    assume "TS' t = ⌊a⌋"
    obtain x w where [simp]: "a = (x, w)" by(cases a, auto)
    with `TS' t = ⌊a⌋` have e'x': "TS' t = ⌊(x, w)⌋" by simp
    with tst have "∃!n. n < length TTAS ∧ (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (TTAS ! n))))"
      by -(rule IH)
    then obtain n
      where nl: "n < length TTAS"
      and exe'x': "∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (TTAS ! n)))"
      and unique: "∀n'. n' < length TTAS ∧ (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (TTAS ! n'))))
                        --> n' = n"
      by(blast elim: ex1E)
    show ?thesis
    proof(rule ex1I)
      show "n < length (TTAS @ [(T, TA)]) ∧
            (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n))))"
        using nl exe'x' by(simp add: nth_append)
    next
      fix n'
      assume "n' < length (TTAS @ [(T, TA)]) ∧
              (∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n'))))"
      hence n'l: "n' < length (TTAS @ [(T, TA)])"
        and ex'e'x': "∃x' m'. NewThread t x' m' ∈ set (thr_a (snd ((TTAS @ [(T, TA)]) ! n')))"
        by auto
      { assume "n' = length TTAS"
        with ex'e'x' have "∃x' m'. NewThread t x' m' ∈ set \<lbrace>TA\<rbrace>t"
          by(auto simp add: nth_append)
        then obtain m'' x''
          where "NewThread t x'' m'' ∈ set \<lbrace>TA\<rbrace>t" by blast
        with red have "TS' t = None"
          by -(erule redT.cases, auto elim: thread_oks_new_thread)
        with e'x' have False by auto }
      moreover
      { assume "n' < length TTAS"
        moreover
        with ex'e'x' have "∃x' m'. NewThread t x' m' ∈ set (thr_a (snd (TTAS ! n')))"
          by(simp add: nth_append)
        ultimately have "n' = n" using unique by(force) }
      ultimately show "n' = n" using n'l by(auto)(arith)
    qed
  qed
qed

end

end