Theory Threaded

(*  Title:      JinjaThreads/J/Threaded.thy
    Author:     Andreas Lochbihler
*)

header{* \isaheader{The source language as an instance of the framework} *}

theory Threaded imports
  SmallStep
  "../Framework/FWLiftingSem"
  JWellForm
  "../Common/ConformThreaded" 
  "../Framework/FWProgressAux"
begin


abbreviation final_expr :: "expr × locals => bool"where
  "final_expr ≡ λ(e, x). final e"

abbreviation
  mred :: "J_prog => (addr, thread_id, expr × locals, heap, addr, obs_event) semantics"
where
  "mred P ≡ (λ((e, l), h)  ta ((e', l'), h'). P \<turnstile> ⟨e, (h, l)⟩ -ta-> ⟨e', (h', l')⟩)"

lemma red_new_thread_heap:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t'' ex'' h'' ∈ set \<lbrace>ta\<rbrace>t |] ==> h'' = hp s'"
  and reds_new_thread_heap:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t'' ex'' h'' ∈ set \<lbrace>ta\<rbrace>t |] ==> h'' = hp s'"
apply(induct rule: red_reds.inducts)
apply(fastsimp dest: red_ext_new_thread_heap)+
done

lemma red_mthr: "multithreaded (mred P)"
by(unfold_locales)(auto dest: red_new_thread_heap)

interpretation red_mthr: multithreaded "final_expr" "mred P"
by(rule red_mthr)

lemmas red_mthr_redT_elims4 = red_mthr.redT_elims4[consumes 1, case_names normal acquire]

abbreviation
  mredT :: "J_prog => (addr,thread_id,expr × locals,heap,addr) state => (thread_id × (addr,thread_id,expr × locals,heap,addr,(addr, obs_event) observable) thread_action) => (addr,thread_id,expr × locals,heap,addr) state => bool"
where
  "mredT P ≡ multithreaded_base.redT final_expr (mred P)"

abbreviation
  mredT_syntax1 :: "J_prog => (addr,thread_id,expr × locals,heap,addr) state
                  => thread_id => (addr,thread_id,expr × locals,heap,addr,(addr, obs_event) observable) thread_action
                  => (addr,thread_id,expr × locals,heap,addr) state => bool"
                    ("_ \<turnstile> _ -_\<triangleright>_-> _" [50,0,0,0,50] 80)
where
  "mredT_syntax1 P s t ta s' ≡ mredT P s (t, ta) s'"

abbreviation
  mredT_syntax2 :: "J_prog => (addr,thread_id) locks => (addr,thread_id,expr × locals) thread_info × heap => (addr,thread_id) wait_sets
                  => thread_id => (addr,thread_id,expr × locals,heap,addr,(addr,obs_event) observable) thread_action
                  => (addr,thread_id) locks => (addr,thread_id,expr × locals) thread_info × heap => (addr,thread_id) wait_sets => bool"
                    ("_ \<turnstile> ⟨_, _, _⟩ -_\<triangleright>_-> ⟨_, _, _⟩" [50,0,0,0,0,0,0,0,0] 80)
where
  "P \<turnstile> ⟨ls, tsm, ws⟩ -t\<triangleright>ta-> ⟨ls', tsm', ws'⟩ ≡ P \<turnstile> (ls, tsm, ws) -t\<triangleright>ta-> (ls', tsm', ws')"


abbreviation
  mRedT_syntax1 :: "J_prog => (addr,thread_id,expr × locals,heap,addr) state
                  => (thread_id × (addr,thread_id,expr × locals,heap,addr,(addr, obs_event) observable) thread_action) list
                  => (addr,thread_id,expr × locals,heap,addr) state => bool"
                    ("_ \<turnstile> _ -\<triangleright>_->* _" [50,0,0,50] 80)
where
  "P \<turnstile> s -\<triangleright>ttas->* s' ≡ multithreaded_base.RedT final_expr (mred P) s ttas s'"

abbreviation
  mRedT_syntax2 :: "J_prog => (addr,thread_id) locks => (addr,thread_id,expr × locals) thread_info × heap => (addr,thread_id) wait_sets
                  => (thread_id × (addr,thread_id,expr × locals,heap,addr,(addr, obs_event) observable) thread_action) list
                  => (addr,thread_id) locks => (addr,thread_id,expr × locals) thread_info × heap => (addr,thread_id) wait_sets => bool"
                    ("_ \<turnstile> ⟨_, _, _⟩ -\<triangleright>_->* ⟨_, _, _⟩" [50,0,0,0,0,0,0,0] 80)
where
  "P \<turnstile> ⟨ls, tsm, ws⟩ -\<triangleright>ttas->* ⟨ls', tsm', ws'⟩ ≡ P \<turnstile> (ls, tsm, ws) -\<triangleright>ttas->* (ls', tsm', ws')"



lemma redT_hext_incr:
  "P \<turnstile> s -t\<triangleright>ta-> s' ==> hext (shr s) (shr s')"
by(erule red_mthr.redT.cases, auto dest: red_hext_incr)

section {* Towards agreement between the framework semantics' lock state and the locks stored in the expressions *}

consts
  sync_ok :: "('a,'b) exp => bool"
  sync_oks :: "('a,'b) exp list => bool"

primrec
  "sync_ok (new C) = True"
  "sync_ok (newA T⌊i⌉) = sync_ok i"
  "sync_ok (Cast T e) = sync_ok e"
  "sync_ok (Val v) = True"
  "sync_ok (Var v) = True"
  "sync_ok (e «bop» e') = (sync_ok e ∧ sync_ok e' ∧ (contains_insync e' --> is_val e))"
  "sync_ok (V := e) = sync_ok e"
  "sync_ok (a⌊i⌉) = (sync_ok a ∧ sync_ok i ∧ (contains_insync i --> is_val a))"
  "sync_ok (AAss a i e) = (sync_ok a ∧ sync_ok i ∧ sync_ok e ∧ (contains_insync i --> is_val a) ∧ (contains_insync e --> is_val a ∧ is_val i))"
  "sync_ok (a•length) = sync_ok a"
  "sync_ok (e•F{D}) = sync_ok e"
  "sync_ok (FAss e F D e') = (sync_ok e ∧ sync_ok e' ∧ (contains_insync e' --> is_val e))"
  "sync_ok (e•m(pns)) = (sync_ok e ∧ sync_oks pns ∧ (contains_insyncs pns --> is_val e))"
  "sync_ok ({V : T=vo; e}) = sync_ok e"
  "sync_ok (syncV (o') e) = (sync_ok o' ∧ ¬ contains_insync e)"
  "sync_ok (insyncV (a) e) = sync_ok e"
  "sync_ok (e;;e') = (sync_ok e ∧ sync_ok e' ∧ (contains_insync e' --> is_val e))"
  "sync_ok (if (b) e else e') = (sync_ok b ∧ ¬ contains_insync e ∧ ¬ contains_insync e')"
  "sync_ok (while (b) e) = (¬ contains_insync b ∧ ¬ contains_insync e)"
  "sync_ok (throw e) = sync_ok e"
  "sync_ok (try e catch(C v) e') = (sync_ok e ∧ ¬ contains_insync e')"
  "sync_oks [] = True"
  "sync_oks (x # xs) = (sync_ok x ∧ sync_oks xs ∧ (contains_insyncs xs --> is_val x))"

lemma sync_oks_append [simp]:
  "sync_oks (xs @ ys) <-> sync_oks xs ∧ sync_oks ys ∧ (contains_insyncs ys --> (∃vs. xs = map Val vs))"
by(induct xs)(auto simp add: Cons_eq_map_conv)

lemma fixes e :: "('a,'b) exp" and es :: "('a,'b) exp list"
  shows not_contains_insync_sync_ok: "¬ contains_insync e ==> sync_ok e"
  and not_contains_insyncs_sync_oks: "¬ contains_insyncs es ==> sync_oks es"
by(induct e and es)(auto)

lemma expr_locks_sync_ok: "(!!ad. expr_locks e ad = 0) ==> sync_ok e"
  and expr_lockss_sync_oks: "(!!ad. expr_lockss es ad = 0) ==> sync_oks es"
by(auto intro!: not_contains_insync_sync_ok not_contains_insyncs_sync_oks
        simp add: contains_insync_conv contains_insyncs_conv)

lemma sync_ok_extRet2J [simp]: "sync_ok (extRet2J va)"
by(cases va) auto

lemma 
  assumes wf: "wf_J_prog P"
  shows red_preserve_sync_ok: "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; sync_ok e |] ==> sync_ok e'"
  and reds_preserve_sync_oks: "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; sync_oks es |] ==> sync_oks es'"
proof(induct rule: red_reds.inducts)
  case (RedCall s a C fs M Ts T pns body D vs)
  from wf `P \<turnstile> C sees M: Ts->T = (pns, body) in D`
  have "wf_mdecl wf_J_mdecl P D (M,Ts,T,pns,body)"
    by(rule sees_wf_mdecl)
  then obtain T where "P,[this\<mapsto>Class D,pns[\<mapsto>]Ts] \<turnstile> body :: T"
    by(auto simp add: wf_mdecl_def)
  hence "expr_locks body = (λad. 0)" by(rule WT_expr_locks)
  with `length vs = length pns` `length Ts = length pns` 
  have "expr_locks (blocks (pns, Ts, vs, body)) = (λad. 0)"
    by(simp add: expr_locks_blocks)
  thus ?case by(auto intro: expr_locks_sync_ok)
qed(fastsimp intro: not_contains_insync_sync_ok)+

lemma assumes wf: "wf_J_prog P"
  shows expr_locks_new_thread:
  "[| P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t (e'', x'') h ∈ set \<lbrace>ta\<rbrace>t |] ==> expr_locks e'' = (λad. 0)"

  and expr_locks_new_thread':
  "[| P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t (e'', x'') h ∈ set \<lbrace>ta\<rbrace>t |] ==> expr_locks e'' = (λad. 0)"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M vs ta va h' ta' e' s')
  then obtain C fs where subThread: "P \<turnstile> C \<preceq>* Thread" and ext: "extNTA2J P (C, run, t) = (e'', x'')"
    by(fastsimp elim!: red_external.cases split: heapobj.split_asm dest: Array_widen)
  from sub_Thread_sees_run[OF wf subThread] obtain D pns body
    where sees: "P \<turnstile> C sees run: []->Void = (pns, body) in D" by auto
  from sees_wf_mdecl[OF wf this] obtain T where "P,[this \<mapsto> Class D] \<turnstile> body :: T"
    by(auto simp add: wf_mdecl_def)
  hence "expr_locks body = (λad. 0)" by(rule WT_expr_locks)
  with sees ext show ?case by(auto simp add: extNTA2J_def)
qed(auto)

lemma assumes wf: "wf_J_prog P"
  shows red_new_thread_sync_ok: "[| P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t'' (e'', x'') h'' ∈ set \<lbrace>ta\<rbrace>t |] ==> sync_ok e''"
  and reds_new_thread_sync_ok: "[| P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t'' (e'', x'') h'' ∈ set \<lbrace>ta\<rbrace>t |] ==> sync_ok e''"
by(auto dest!: expr_locks_new_thread[OF wf] expr_locks_new_thread'[OF wf] intro: expr_locks_sync_ok expr_lockss_sync_oks)

abbreviation
  sync_es_ok :: "(addr,thread_id,('a,'b) exp×'c) thread_info => heap => bool"
where
  "sync_es_ok ≡ ts_ok (λ(e, x) m. sync_ok e)"

lemma lifting_wf_sync_ok: "wf_J_prog P ==> lifting_wf (mred P) (λ(e, x) m. sync_ok e)"
by(unfold_locales)(auto intro: red_preserve_sync_ok red_new_thread_sync_ok)

lemma redT_preserve_sync_ok:
  assumes red: "P \<turnstile> s -t\<triangleright>ta-> s'"
  shows "[| wf_J_prog P; sync_es_ok (thr s) (shr s) |] ==> sync_es_ok (thr s') (shr s')"
by(rule lifting_wf.redT_preserves[OF lifting_wf_sync_ok red])

lemmas RedT_preserves_sync_ok = lifting_wf.RedT_preserves[OF lifting_wf_sync_ok]

text {* Framework lock state agrees with locks stored in the expression *}

definition lock_ok :: "(addr,thread_id) locks => (addr,thread_id,expr × locals) thread_info => bool" where
  "lock_ok ls ts ≡ ∀t. (case (ts t) of None    => (∀l. has_locks (lsf l) t = 0)
                                     | ⌊((e, x), ln)⌋ => (∀l. has_locks (lsf l) t + lnf l = expr_locks e l))"

lemma lock_okI:
  "[| !!t l. ts t = None ==> has_locks (lsf l) t = 0; !!t e x ln l. ts t = ⌊((e, x), ln)⌋ ==> has_locks (lsf l) t + lnf l= expr_locks e l |] ==> lock_ok ls ts"
apply(fastsimp simp add: lock_ok_def)
done

lemma lock_okE:
  "[| lock_ok ls ts;
     ∀t. ts t = None --> (∀l. has_locks (lsf l) t = 0) ==> Q;
     ∀t e x ln. ts t = ⌊((e, x), ln)⌋ --> (∀l. has_locks (lsf l) t + lnf l = expr_locks e l) ==> Q |]
  ==> Q"
by(fastsimp simp add: lock_ok_def)

lemma lock_okD1:
  "[| lock_ok ls ts; ts t = None |] ==> ∀l. has_locks (lsf l) t = 0"
apply(simp add: lock_ok_def)
apply(erule_tac x="t" in allE)
apply(auto)
done

lemma lock_okD2:
  "[| lock_ok ls ts; ts t = ⌊((e, x), ln)⌋ |] ==> ∀l. has_locks (lsf l) t + lnf l = expr_locks e l"
apply(fastsimp simp add: lock_ok_def)
done

lemma lock_ok_lock_thread_ok:
  assumes lock: "lock_ok ls ts"
  shows "lock_thread_ok ls ts"
proof(rule lock_thread_okI)
  fix l t
  assume lsl: "has_lock (lsf l) t"
  show "∃xw. ts t = ⌊xw⌋"
  proof(cases "ts t")
    case None
    with lock have "has_locks (lsf l) t = 0"
      by(auto dest: lock_okD1)
    with lsl show ?thesis by simp
  next
    case (Some a) thus ?thesis by blast
  qed
qed

section {* Preservation of lock state agreement *}

fun upd_expr_lock_action :: "int => lock_action => int"
where
  "upd_expr_lock_action i Lock = i + 1"
| "upd_expr_lock_action i Unlock = i - 1"
| "upd_expr_lock_action i UnlockFail = i"
| "upd_expr_lock_action i ReleaseAcquire = i"

fun upd_expr_lock_actions :: "int => lock_action list => int" where
  "upd_expr_lock_actions n [] = n"
| "upd_expr_lock_actions n (L # Ls) = upd_expr_lock_actions (upd_expr_lock_action n L) Ls"

lemma upd_expr_lock_actions_append [simp]:
  "upd_expr_lock_actions n (Ls @ Ls') = upd_expr_lock_actions (upd_expr_lock_actions n Ls) Ls'"
by(induct Ls arbitrary: n, auto)

definition upd_expr_locks :: "('l => int) => 'l lock_actions => 'l => int"
where "upd_expr_locks els las ≡ λl. upd_expr_lock_actions (els l) (lasf l)"

lemma upd_expr_locks_iff [simp]:
  "upd_expr_locks els las l = upd_expr_lock_actions (els l) (lasf l)"
by(simp add: upd_expr_locks_def)

lemma upd_expr_lock_action_add [simp]:
  "upd_expr_lock_action (l + l') L = upd_expr_lock_action l L + l'"
by(cases L, auto)

lemma upd_expr_lock_actions_add [simp]:
  "upd_expr_lock_actions (l + l') Ls = upd_expr_lock_actions l Ls + l'"
by(induct Ls arbitrary: l, auto)

lemma upd_expr_locks_add [simp]:
  "upd_expr_locks (λa. x a + y a) las = (λa. upd_expr_locks x las a + y a)"
by(auto intro: ext)

lemma expr_locks_extRet2J [simp]: "expr_locks (extRet2J va) = (λad. 0)"
by(cases va) auto

lemma assumes wf: "wf_J_prog P"
  shows red_update_expr_locks:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; sync_ok e |] ==> upd_expr_locks (int o expr_locks e) \<lbrace>ta\<rbrace>l = int o expr_locks e'"
  and reds_update_expr_lockss:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; sync_oks es |] ==> upd_expr_locks (int o expr_lockss es) \<lbrace>ta\<rbrace>l = int o expr_lockss es'"
proof -
  have "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; sync_ok e |] ==> upd_expr_locks (λad. 0) \<lbrace>ta\<rbrace>l = (λad. (int o expr_locks e') ad - (int o expr_locks e) ad)"
    and "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; sync_oks es |] ==> upd_expr_locks (λad. 0) \<lbrace>ta\<rbrace>l = (λad. (int o expr_lockss es') ad - (int o expr_lockss es) ad)"
  proof(induct rule: red_reds.inducts)
    case (RedCall s a C fs M Ts T pns body D vs)
    from wf `P \<turnstile> C sees M: Ts->T = (pns, body) in D`
    have "wf_mdecl wf_J_mdecl P D (M,Ts,T,pns,body)"
      by(rule sees_wf_mdecl)
    then obtain T where "P,[this\<mapsto>Class D,pns[\<mapsto>]Ts] \<turnstile> body :: T"
      by(auto simp add: wf_mdecl_def)
    hence "expr_locks body = (λad. 0)" by(rule WT_expr_locks)
    with `length vs = length pns` `length Ts = length pns` 
    have "expr_locks (blocks (pns, Ts, vs, body)) = (λad. 0)"
      by(simp add: expr_locks_blocks)
    thus ?case by(auto intro: expr_locks_sync_ok)
  next
    case RedCallExternal thus ?case
      by(auto simp add: expand_fun_eq contains_insync_conv contains_insyncs_conv finfun_upd_apply elim!: red_external.cases)
  qed(fastsimp simp add: expand_fun_eq contains_insync_conv contains_insyncs_conv finfun_upd_apply)+
  hence "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; sync_ok e |] ==> upd_expr_locks (λad. 0 + (int o expr_locks e) ad) \<lbrace>ta\<rbrace>l = int o expr_locks e'"
    and "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; sync_oks es |] ==> upd_expr_locks (λad. 0 + (int o expr_lockss es) ad) \<lbrace>ta\<rbrace>l = int o expr_lockss es'"
    by(auto intro: ext simp only: upd_expr_locks_add)
  thus "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; sync_ok e |] ==> upd_expr_locks (int o expr_locks e) \<lbrace>ta\<rbrace>l = int o expr_locks e'"
    and "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; sync_oks es |] ==> upd_expr_locks (int o expr_lockss es) \<lbrace>ta\<rbrace>l = int o expr_lockss es'"
    by(auto simp add: o_def)
qed

definition lock_expr_locks_ok :: "'t FWState.lock => 't => nat => int => bool" where
  "lock_expr_locks_ok l t n i ≡ (i = int (has_locks l t) + int n) ∧ i ≥ 0"

lemma upd_lock_upd_expr_lock_action_preserve_lock_expr_locks_ok:
  assumes lao: "lock_action_ok l t L"
  and lelo: "lock_expr_locks_ok l t n i"
  shows "lock_expr_locks_ok (upd_lock l t L) t (upd_threadR n l t L) (upd_expr_lock_action i L)"
proof -
  from lelo have i: "i ≥ 0"
    and hl: "i = int (has_locks l t) + int n"
    by(auto simp add: lock_expr_locks_ok_def)
  from lelo
  show ?thesis
  proof(cases L)
    case Lock
    with lao have "may_lock l t" by(simp)
    with hl have "has_locks (lock_lock l t) t = (Suc (has_locks l t))" by(auto)
    with Lock i hl show ?thesis
      by(simp add: lock_expr_locks_ok_def)
  next
    case Unlock
    with lao have "has_lock l t" by simp
    then obtain n' 
      where hl': "has_locks l t = Suc n'"
      by(auto dest: has_lock_has_locks_Suc)
    hence "has_locks (unlock_lock l) t = n'" by simp
    with Unlock i hl hl' show ?thesis
      by(simp add: lock_expr_locks_ok_def)
  qed(auto simp add: lock_expr_locks_ok_def)
qed

lemma upd_locks_upd_expr_lock_preserve_lock_expr_locks_ok:
  "[| lock_actions_ok l t Ls; lock_expr_locks_ok l t n i |]
  ==> lock_expr_locks_ok (upd_locks l t Ls) t (upd_threadRs n l t Ls) (upd_expr_lock_actions i Ls)"
by(induct Ls arbitrary: l i n)(auto intro: upd_lock_upd_expr_lock_action_preserve_lock_expr_locks_ok)


definition ls_els_ok :: "(addr,thread_id) locks => thread_id => (addr =>f nat) => (addr => int) => bool" where
  "ls_els_ok ls t ln els ≡ ∀l. lock_expr_locks_ok (lsf l) t (lnf l) (els l)"

lemma ls_els_okI:
  "(!!l. lock_expr_locks_ok (lsf l) t (lnf l) (els l)) ==> ls_els_ok ls t ln els"
by(auto simp add: ls_els_ok_def)

lemma ls_els_okE:
  "[| ls_els_ok ls t ln els; ∀l. lock_expr_locks_ok (lsf l) t (lnf l) (els l) ==> P |] ==> P"
by(auto simp add: ls_els_ok_def)

lemma ls_els_okD:
  "ls_els_ok ls t ln els ==> lock_expr_locks_ok (lsf l) t (lnf l) (els l)"
by(auto simp add: ls_els_ok_def)

lemma redT_updLs_upd_expr_locks_preserves_ls_els_ok:  
 "[| ls_els_ok ls t ln els; lock_ok_las ls t las |] ==> ls_els_ok (redT_updLs ls t las) t (redT_updLns ls t ln las) (upd_expr_locks els las)"
by(auto intro!: ls_els_okI upd_locks_upd_expr_lock_preserve_lock_expr_locks_ok elim!: ls_els_okE simp add: redT_updLs_def lock_ok_las_def)

lemma sync_ok_redT_updT: 
  assumes "sync_es_ok ts h"
  and nt: "!!t e x h''. ta = NewThread t (e, x) h'' ==> sync_ok e"
  shows "sync_es_ok (redT_updT ts ta) h'"
using assms
proof(cases ta)
  case (NewThread T x m)
  obtain E X where [simp]: "x = (E, X)" by (cases x, auto)
  with NewThread have "sync_ok E" by(simp)(rule nt)
  with NewThread `sync_es_ok ts h` show ?thesis
    apply -
    apply(rule ts_okI)
    apply(case_tac "t=T")
    by(auto dest: ts_okD)
qed(auto intro: ts_okI dest: ts_okD)


lemma sync_ok_redT_updTs: 
  "[| sync_es_ok ts h; !!t e x h. NewThread t (e, x) h ∈ set tas ==> sync_ok e |]
  ==> sync_es_ok (redT_updTs ts tas) h'"
proof(induct tas arbitrary: ts)
  case Nil thus ?case by(auto intro: ts_okI dest: ts_okD)
next
  case (Cons TA TAS TS)
  note IH = `!!ts. [|sync_es_ok ts h; !!t e x h''. NewThread t (e, x) h'' ∈ set TAS ==> sync_ok e|] ==> sync_es_ok (redT_updTs ts TAS) h'`
  note nt = `!!t e x h. NewThread t (e, x) h ∈ set (TA # TAS) ==> sync_ok e`
  from `sync_es_ok TS h` nt
  have "sync_es_ok (redT_updT TS TA) h"
    by(auto elim!: sync_ok_redT_updT)
  hence "sync_es_ok (redT_updTs (redT_updT TS TA) TAS) h'"
    by(rule IH)(auto intro: nt)
  thus ?case by simp
qed

lemma redT_preserves_lock_ok:
  assumes wf: "wf_J_prog P"
  and "P \<turnstile> s -t\<triangleright>ta-> s'"
  and "lock_ok (locks s) (thr s)"
  and "sync_es_ok (thr s) (shr s)"
  shows "lock_ok (locks s') (thr s')"
proof -
  obtain ls ts h ws where s [simp]: "s = (ls, (ts, h), ws)" by(cases s, auto)
  obtain ls' ts' h' ws' where s' [simp]: "s' = (ls', (ts', h'), ws')" by(cases s', auto)
  from assms have redT: "P \<turnstile> ⟨ls, (ts, h), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', h'), ws'⟩"
    and loes: "lock_ok ls ts"
    and aoes: "sync_es_ok ts h" by auto
  from redT have "lock_ok ls' ts'"
  proof(induct rule: red_mthr_redT_elims4)
    case (normal a a' ta')
    moreover obtain e x where "a = (e, x)" by (cases a, auto)
    moreover obtain e' x' where "a' = (e', x')" by (cases a', auto)
    ultimately have P: "P \<turnstile> ⟨e,(h, x)⟩ -ta'-> ⟨e',(h', x')⟩"
      and est: "ts t = ⌊((e, x), no_wait_locks)⌋"
      and lota: "lock_ok_las ls t \<lbrace>ta'\<rbrace>l"
      and cctta: "thread_oks ts \<lbrace>ta'\<rbrace>t"
      and ls': "ls' = redT_updLs ls t \<lbrace>ta'\<rbrace>l"
      and es': "ts' = redT_updTs ts \<lbrace>ta'\<rbrace>t(t \<mapsto> ((e', x'), redT_updLns ls t no_wait_locks \<lbrace>ta'\<rbrace>l))"
      and ws': "ws' = redT_updWs ws t \<lbrace>ta'\<rbrace>w"
      and ta [simp]: "ta = observable_ta_of ta'"
      by auto
    from est aoes have aoe: "sync_ok e" by(auto dest: ts_okD)
    from aoe P have aoe': "sync_ok e'" by(auto dest: red_preserve_sync_ok[OF wf])
    from aoes red_new_thread_sync_ok[OF wf P]
    have "sync_es_ok (redT_updTs ts \<lbrace>ta'\<rbrace>t) h'"
      by(rule sync_ok_redT_updTs)
    with aoe' have aoes': "sync_es_ok (redT_updTs ts \<lbrace>ta\<rbrace>t(t \<mapsto> ((e', x'), redT_updLns ls t no_wait_locks \<lbrace>ta\<rbrace>l))) h"
      by(auto intro!: ts_okI dest: ts_okD split: split_if_asm)
    show ?thesis
    proof(rule lock_okI)
      fix t'' l
      assume "ts' t'' = None"
      with es' have "ts t'' = None"
        by(auto split: split_if_asm intro: redT_updTs_None)
      with loes have "has_locks (lsf l) t'' = 0"
        by(auto dest: lock_okD1)
      moreover from `ts' t'' = None` es'
      have "t ≠ t''" by(simp split: split_if_asm)
      ultimately show "has_locks (ls'f l) t'' = 0"
        by(simp add: red_mthr.redT_has_locks_inv[OF redT])
    next
      fix t'' e'' x'' l ln''
      assume ts't'': "ts' t'' = ⌊((e'', x''), ln'')⌋"
      with aoes' es' have aoe'': "sync_ok e''" by(auto dest: ts_okD)
      show "has_locks (ls'f l) t'' + ln''f l = expr_locks e'' l"
      proof(cases "t = t''")
        case True
        note tt'' = `t = t''`
        with ts't'' es' have  e'': "e'' = e'" and x'': "x'' = x'"
          and ln'': "ln'' = redT_updLns ls t no_wait_locks \<lbrace>ta\<rbrace>l" by auto
        have "ls_els_ok ls t no_wait_locks (int o expr_locks e)"
        proof(rule ls_els_okI)
          fix l
          note lock_okD2[OF loes, OF est]
          thus "lock_expr_locks_ok (lsf l) t (no_wait_locksf l) ((int o expr_locks e) l)"
            by(simp add: lock_expr_locks_ok_def)
        qed
        hence "ls_els_ok (redT_updLs ls t \<lbrace>ta'\<rbrace>l) t (redT_updLns ls t no_wait_locks \<lbrace>ta'\<rbrace>l) (upd_expr_locks (int o expr_locks e) \<lbrace>ta'\<rbrace>l)"
          by(rule redT_updLs_upd_expr_locks_preserves_ls_els_ok[OF _ lota])
        hence "ls_els_ok (redT_updLs ls t \<lbrace>ta'\<rbrace>l) t (redT_updLns ls t no_wait_locks \<lbrace>ta'\<rbrace>l) (int o expr_locks e')"
          by(simp only: red_update_expr_locks[OF wf P aoe])
        thus ?thesis using ls' e'' tt'' ln''
          by(auto dest: ls_els_okD[where l = l] simp: lock_expr_locks_ok_def)
      next
        case False
        note tt'' = `t ≠ t''`
        from lota have lao: "lock_actions_ok (lsf l) t (\<lbrace>ta\<rbrace>lf l)"
          by(simp add: lock_ok_las_def)
        show ?thesis
        proof(cases "ts t''")
          case None
          with est ts't'' es' tt'' cctta
          obtain m' where "NewThread t'' (e'', x'') m' ∈ set \<lbrace>ta\<rbrace>t" and ln'': "ln'' = no_wait_locks"
            by(auto dest: redT_updTs_new_thread)
          moreover with P have "m' = h'" by(auto dest: red_new_thread_heap)
          ultimately have "NewThread t'' (e'', x'') h' ∈ set \<lbrace>ta'\<rbrace>t" by simp
          with wf P ln'' have "expr_locks e'' = (λad. 0)"
            by -(rule expr_locks_new_thread)
          hence elel: "expr_locks e'' l = 0" by simp
          from loes None  have "has_locks (lsf l) t'' = 0"
            by(auto dest: lock_okD1)
          moreover note lock_actions_ok_has_locks_upd_locks_eq_has_locks[OF lao tt''[symmetric]]
          ultimately have "has_locks ((redT_updLs ls t \<lbrace>ta\<rbrace>l)f l) t'' = 0"
            by(auto simp add: expand_fun_eq)
          with elel ls' ln'' show ?thesis by(auto)
        next
          case (Some a)
          then obtain E X LN where est'': "ts t'' = ⌊((E, X), LN)⌋" by(cases a, auto)
          with loes have IH: "has_locks (lsf l) t'' + LNf l = expr_locks E l"
            by(auto dest: lock_okD2)
          from est est'' es' tt'' cctta have "ts' t'' = ⌊((E, X), LN)⌋"
            apply(simp)
            apply(rule redT_updTs_Some)
            by(simp_all)
          with ts't'' es' have e'': "E = e''" and x'': "X = x''"
            and ln'': "ln'' = LN" by(simp_all)
          with lock_actions_ok_has_locks_upd_locks_eq_has_locks[OF lao tt''[symmetric]] IH ls'
          show ?thesis by(clarsimp simp add: redT_updLs_def expand_fun_eq)
        qed
      qed
    qed
  next
    case (acquire a ln n)
    note [simp] = `ta = (λf [], [], [], [], ReacquireLocks ln)` `ws' = ws` `h' = h`
    obtain e x where [simp]: "a = (e, x)" by (cases a, auto)
    note ls' = `ls' = acquire_all ls t ln`
    from `ts' = ts(t \<mapsto> (a, no_wait_locks))`
    have ts': "ts' = ts(t \<mapsto> ((e, x), no_wait_locks))" by simp
    from `ts t = ⌊(a, ln)⌋` have tst: "ts t = ⌊((e, x), ln)⌋" by simp
    show ?thesis
    proof(rule lock_okI)
      fix t'' l
      assume rtutes: "ts' t'' = None"
      with ts' have tst'': "ts t'' = None"
        by(simp split: split_if_asm)
      with tst have tt'': "t ≠ t''" by auto
      from tst'' loes have "has_locks (lsf l) t'' = 0"
        by(auto dest: lock_okD1)
      thus "has_locks (ls'f l) t'' = 0"
        by(simp add: red_mthr.redT_has_locks_inv[OF redT tt''])
    next
      fix t'' e'' x'' ln'' l
      assume ts't'': "ts' t'' = ⌊((e'', x''), ln'')⌋"
      show "has_locks (ls'f l) t'' + ln''f l = expr_locks e'' l"
      proof(cases "t = t''")
        case True
        note [simp] = this
        with ts't'' ts' tst
        have [simp]: "ln'' = no_wait_locks" "e = e''" by auto
        from tst loes have "has_locks (lsf l) t + lnf l = expr_locks e l"
          by(auto dest: lock_okD2)
        show ?thesis
        proof(cases "lnf l > 0")
          case True
          with `may_acquire_all ls t ln` ls' have "may_lock (lsf l) t"
            by(auto elim: may_acquire_allE)
          with ls'
          have "has_locks (ls'f l) t = has_locks (lsf l) t + lnf l"
            by(simp add: has_locks_acquire_locks_conv)
          with `has_locks (lsf l) t + lnf l = expr_locks e l`
          show ?thesis by(simp)
        next
          case False
          hence "lnf l = 0" by simp
          with ls' have "has_locks (ls'f l) t = has_locks (lsf l) t"
            by(simp)
          with `has_locks (lsf l) t + lnf l = expr_locks e l` `lnf l = 0`
          show ?thesis by(simp)
        qed
      next
        case False
        with ts' ts't'' have tst'': "ts t'' = ⌊((e'', x''), ln'')⌋" by(simp)
        with loes have "has_locks (lsf l) t'' + ln''f l = expr_locks e'' l"
          by(auto dest: lock_okD2)
        show ?thesis
        proof(cases "lnf l > 0")
          case False
          with `t ≠ t''` ls'
          have "has_locks (ls'f l) t'' = has_locks (lsf l) t''" by(simp)
          with `has_locks (lsf l) t'' + ln''f l = expr_locks e'' l`
          show ?thesis by(simp)
        next
          case True
          with `may_acquire_all ls t ln` have "may_lock (lsf l) t"
            by(auto elim: may_acquire_allE)
          with ls' `t ≠ t''` have "has_locks (ls'f l) t'' = has_locks (lsf l) t''"
            by(simp add: has_locks_acquire_locks_conv')
          with ls' `has_locks (lsf l) t'' + ln''f l = expr_locks e'' l`
          show ?thesis by(simp)
        qed
      qed
    qed
  qed
  thus ?thesis by simp
qed


lemma RedT_preserves_lock_ok:
  assumes wf: "wf_J_prog P"
  and Red: "P \<turnstile> s -\<triangleright>ttas->* s'"
  and ae: "sync_es_ok (thr s) (shr s)"
  and loes: "lock_ok (locks s) (thr s)"
  shows "lock_ok (locks s') (thr s')"
using Red ae loes
proof(induct rule: red_mthr.RedT_induct[consumes 1, case_names refl step])
  case refl thus ?case by blast
next
  case step thus ?case
    apply -
    apply(erule redT_preserves_lock_ok[OF wf], assumption)
    by(auto dest: RedT_preserves_sync_ok[OF wf])
qed

lemma red_NewThread_Thread_Object:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t x m ∈ set \<lbrace>ta\<rbrace>t |] ==> ∃C fs. hp s' t = ⌊Obj C fs⌋ ∧ P \<turnstile> C \<preceq>* Thread"
  and reds_NewThread_Thread_Object:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t x m ∈ set \<lbrace>ta\<rbrace>t |] ==> ∃C fs. hp s' t = ⌊Obj C fs⌋ ∧ P \<turnstile> C \<preceq>* Thread"
apply(induct rule: red_reds.inducts)
apply(fastsimp dest: red_external_new_thread_exists_thread_object)+
done

lemma redT_NewThread_Thread_Object:
  "[| P \<turnstile> s -t'\<triangleright>ta-> s'; NewThread t x m ∈ set \<lbrace>ta\<rbrace>t |] ==> ∃C fs. shr s' t = ⌊Obj C fs⌋ ∧ P \<turnstile> C \<preceq>* Thread"
by(auto elim!: red_mthr.redT.cases dest:red_NewThread_Thread_Object)

lemma redT_preserves_thread_conf:
  assumes red: "P \<turnstile> s -t'\<triangleright>ta-> s'"
  and tc: "thread_conf P (thr s) (shr s)"
  shows "thread_conf P (thr s') (shr s')"
proof(rule thread_confI)
  fix t xln
  assume tst': "thr s' t = ⌊xln⌋"
  obtain e x ln where xln [simp]: "xln = ((e, x), ln)" by(cases xln, auto)
  show "∃T. typeofshr s' (Addr t) = ⌊T⌋ ∧ P \<turnstile> T ≤ Class Thread"
  proof(cases "thr s t")
    case None
    with red tst' have nt: "NewThread t (e, x) (shr s') ∈ set \<lbrace>ta\<rbrace>t" 
      and [simp]: "ln = no_wait_locks" by(auto dest: red_mthr.redT_new_thread)
    from red nt obtain C fs where "shr s' t = ⌊Obj C fs⌋" "P \<turnstile> Class C ≤ Class Thread"
      by(auto dest!: redT_NewThread_Thread_Object)
    thus ?thesis by(clarsimp)
  next
    case (Some Xln)
    with tc obtain T where "typeofshr s (Addr t) = ⌊T⌋" "P \<turnstile> T ≤ Class Thread"
      by(rule thread_confDE)
    moreover from red have "hext (shr s) (shr s')"
      by(cases s, cases s')(auto intro: redT_hext_incr)
    ultimately have "typeofshr s' (Addr t) = ⌊T⌋"
      by(blast dest: type_of_hext_type_of hext_objarrD)
    with `P \<turnstile> T ≤ Class Thread` show ?thesis by blast
  qed
qed
    
lemma RedT_preserves_thread_conf:
  "[| P \<turnstile> s -\<triangleright>tta->* s'; thread_conf P (thr s) (shr s) |] ==> thread_conf P (thr s') (shr s')"
by(rule red_mthr.RedT_lift_preserveD[OF _ _ redT_preserves_thread_conf])

section {* Interpreting final\_thread\_wf with final *}

lemma final_no_red [elim]:
  "final e ==> ¬ P \<turnstile> ⟨e, (h, l)⟩ -ta-> ⟨e', (h', l')⟩"
apply(auto elim: red.cases finalE)
done

lemma final_locks: "final e ==> expr_locks e l = 0"
by(auto elim: finalE)

lemma final_thread_wf_interp: "final_thread_wf final_expr (mred P)"
proof(unfold_locales)
  fix x m ta x' m'
  assume "final_expr x" "mred P (x, m) ta (x', m')"
  moreover obtain e l where e: "x = (e, l)" by (cases x, auto)
  ultimately have "final e" by simp
  moreover obtain e' :: expr and l' :: locals where e': "x' = (e', l')" by (cases x', auto)
  ultimately show "False" using e `mred P (x, m) ta (x', m')` by(auto)
qed

interpretation red_mthr: final_thread_wf "final_expr" "mred P" for P
by(rule final_thread_wf_interp)

end