Theory ProgressThreaded

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

section ‹Progress and type safety theorem for the multithreaded system›

theory ProgressThreaded 
imports 
  Threaded
  TypeSafe
  "../Framework/FWProgress"
begin

lemma lock_ok_ls_Some_ex_ts_not_final:
  assumes lock: "lock_ok ls ts"
  and hl: "has_lock (ls $ l) t"
  shows "e x ln. ts t = ((e, x), ln)  ¬ final e"
proof -
  from lock have "lock_thread_ok ls ts"
    by(rule lock_ok_lock_thread_ok)
  with hl obtain e x ln
    where tst: "ts t = ((e, x), ln)"
    by(auto dest!: lock_thread_okD)
  { assume "final e"
    hence "expr_locks e l = 0" by(rule final_locks)
    with lock tst have "has_locks (ls $ l) t = 0"
      by(auto dest: lock_okD2[rule_format, where l=l])
    with hl have False by simp }
  with tst show ?thesis by auto
qed

subsection ‹Preservation lemmata›

subsection ‹Definite assignment›

abbreviation
  def_ass_ts_ok :: "('addr,'thread_id,'addr expr × 'addr locals) thread_info  'heap  bool"
where
  "def_ass_ts_ok  ts_ok (λt (e, x) h. 𝒟 e dom x)"

context J_heap_base begin

lemma assumes wf: "wf_J_prog P"
  shows red_def_ass_new_thread:
  " P,t  e, s -ta e', s'; NewThread t'' (e'', x'') c''  set tat   𝒟 e'' dom x''"
  
  and reds_def_ass_new_thread:
  " P,t  es, s [-ta→] es', s'; NewThread t'' (e'', x'') c''  set tat   𝒟 e'' dom x''"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M vs ta va h' ta' e' s')
  then obtain C fs a where subThread: "P  C * Thread" and ext: "extNTA2J P (C, run, a) = (e'', x'')"
    by(fastforce dest: red_external_new_thread_sub_thread)
  from sub_Thread_sees_run[OF wf subThread] obtain D pns body
    where sees: "P  C sees run: []Void = (pns, body) in D" by auto
  from sees_wf_mdecl[OF wf this] have "𝒟 body {this}"
    by(auto simp add: wf_mdecl_def)
  with sees ext show ?case by(clarsimp simp del: fun_upd_apply)
qed(auto simp add: ta_upd_simps)

lemma lifting_wf_def_ass: "wf_J_prog P  lifting_wf final_expr (mred P) (λt (e, x) m. 𝒟 e dom x)"
apply(unfold_locales)
apply(auto dest: red_preserves_defass red_def_ass_new_thread)
done

lemma def_ass_ts_ok_J_start_state:
  " wf_J_prog P; P  C sees M:TsT = (pns, body) in D; length vs = length Ts  
  def_ass_ts_ok (thr (J_start_state P C M vs)) h"
apply(rule ts_okI)
apply(drule (1) sees_wf_mdecl)
apply(clarsimp simp add: wf_mdecl_def start_state_def split: if_split_asm)
done

end

subsection ‹typeability›

context J_heap_base begin

definition type_ok :: "'addr J_prog  env × ty  'addr expr  'heap  bool"
where "type_ok P  (λ(E, T) e c. (T'. (P,E,c  e : T'  P  T'  T)))"

definition J_sconf_type_ET_start :: "'m prog  cname  mname  ('thread_id  (env × ty))"
where
  "J_sconf_type_ET_start P C M 
   let (_, _, T, _) = method P C M
   in ([start_tid  (Map.empty, T)])"

lemma fixes E :: env
  assumes wf: "wf_J_prog P"
  shows red_type_newthread:
  " P,t  e, s -ta e', s'; P,E,hp s  e : T; NewThread t'' (e'', x'') (hp s')  set tat 
   E T. P,E,hp s'  e'' : T  P,hp s'  x'' (:≤) E"
  and reds_type_newthread:
  " P,t  es, s [-ta→] es', s'; NewThread t'' (e'', x'') (hp s')  set tat; P,E,hp s  es [:] Ts 
   E T. P,E,hp s'  e'' : T  P,hp s'  x'' (:≤) E"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
  case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s')
  from NewThread t'' (e'', x'') (hp s')  set ta't ta' = extTA2J P ta
  obtain C' M' a' where nt: "NewThread t'' (C', M', a') (hp s')  set tat"
    and "extNTA2J P (C', M', a') = (e'', x'')" by fastforce
  from red_external_new_thread_sees[OF wf P,t  aM(vs),hp s -ta→ext va,h' nt] typeof_addr (hp s) a = U
  obtain T pns body D where h'a': "typeof_addr h' a' = Class_type C'"
    and sees: " P  C' sees M': []T = (pns, body) in D" by auto
  from sees_wf_mdecl[OF wf sees] obtain T where "P,[this  Class D]  body :: T"
    by(auto simp add: wf_mdecl_def)
  hence "WTrt P (hp s') [this  Class D] body T" by(rule WT_implies_WTrt)
  moreover from sees have "P  C' * D" by(rule sees_method_decl_above)
  with h'a' have "P,h'  [this  Addr a'] (:≤) [this  Class D]" by(auto simp add: lconf_def conf_def)
  ultimately show ?case using h'a' sees s' = (h', lcl s)
    extNTA2J P (C', M', a') = (e'', x'') by(fastforce intro: sees_method_decl_above)
qed(fastforce simp add: ta_upd_simps)+

end

context J_heap_conf_base begin

definition sconf_type_ok :: "(env × ty)  'thread_id  'addr expr × 'addr locals  'heap  bool" 
where
  "sconf_type_ok ET t ex h  fst ET  (h, snd ex)   type_ok P ET (fst ex) h  P,h  t √t"

abbreviation sconf_type_ts_ok ::
  "('thread_id  (env × ty))  ('addr,'thread_id,'addr expr × 'addr locals) thread_info  'heap  bool"
where
  "sconf_type_ts_ok  ts_inv sconf_type_ok"

lemma ts_inv_ok_J_sconf_type_ET_start:
  "ts_inv_ok (thr (J_start_state P C M vs)) (J_sconf_type_ET_start P C M)"
by(rule ts_inv_okI)(simp add: start_state_def J_sconf_type_ET_start_def split_beta)

end

lemma (in J_heap) red_preserve_welltype:
  " extTA,P,t  e, (h, x) -ta e', (h', x'); P,E,h  e'' : T   P,E,h'  e'' : T"
by(auto elim: WTrt_hext_mono dest!: red_hext_incr)

context J_heap_conf begin

lemma sconf_type_ts_ok_J_start_state:
  " wf_J_prog P; wf_start_state P C M vs 
   sconf_type_ts_ok (J_sconf_type_ET_start P C M) (thr (J_start_state P C M vs)) (shr (J_start_state P C M vs))"
apply(erule wf_start_state.cases)
apply(rule ts_invI)
apply(simp add: start_state_def split: if_split_asm)
apply(frule (1) sees_wf_mdecl)
apply(auto simp add: wf_mdecl_def J_sconf_type_ET_start_def sconf_type_ok_def sconf_def type_ok_def)
   apply(erule hconf_start_heap)
  apply(erule preallocated_start_heap)
  apply(erule wf_prog_wf_syscls)
 apply(frule list_all2_lengthD)
 apply(auto simp add: wt_blocks confs_conv_map intro: WT_implies_WTrt)[1]
apply(erule tconf_start_heap_start_tid)
apply(erule wf_prog_wf_syscls)
done

lemma J_start_state_sconf_type_ok:
  assumes wf: "wf_J_prog P"
  and ok: "wf_start_state P C M vs"
  shows "ts_ok (λt x h. ET. sconf_type_ok ET t x h) (thr (J_start_state P C M vs)) start_heap"
using sconf_type_ts_ok_J_start_state[OF assms]
unfolding shr_start_state by(rule ts_inv_into_ts_ok_Ex)

end

context J_conf_read begin

lemma red_preserves_type_ok: 
  " extTA,P,t  e,s -ta e',s'; wf_J_prog P; E  s ; type_ok P (E, T) e (hp s); P,hp s  t √t   type_ok P (E, T) e' (hp s')"
apply(clarsimp simp add: type_ok_def)
apply(subgoal_tac "T''. P,E,hp s'  e' : T''  P  T''  T'")
 apply(fast elim: widen_trans)
by(rule subject_reduction)

lemma lifting_inv_sconf_subject_ok:
  assumes wf: "wf_J_prog P"
  shows "lifting_inv final_expr (mred P) sconf_type_ok"
proof(unfold_locales)
  fix t x m ta x' m' i
  assume mred: "mred P t (x, m) ta (x', m')"
    and "sconf_type_ok i t x m"
  moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
  moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
  moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
  ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
    and red: "P,t  e, (m, l) -ta e', (m', l')" by auto
  from sconf_type have sconf: "E  (m, l) " and "type_ok P (E, T) e m" and tconf: "P,m  t √t"
    by(auto simp add: sconf_type_ok_def)
  then obtain T' where "P,E,m  e : T'" "P  T'  T" by(auto simp add: type_ok_def)
  from E  (m, l)  P,E,m  e : T' red tconf
  have "E  (m', l') " by(auto elim: red_preserves_sconf)
  moreover
  from red P,E,m  e : T' wf E  (m, l)  tconf
  obtain T'' where "P,E,m'  e' : T''" "P  T''  T'"
    by(auto dest: subject_reduction)
  note P,E,m'  e' : T''
  moreover
  from P  T''  T' P  T'  T
  have "P  T''  T" by(rule widen_trans)
  moreover from mred tconf have "P,m'  t √t" by(rule red_tconf.preserves_red)  
  ultimately have "sconf_type_ok (E, T) t (e', l') m'"
    by(auto simp add: sconf_type_ok_def type_ok_def)
  thus "sconf_type_ok i t x' m'" by simp
next
  fix t x m ta x' m' i t'' x''
  assume mred: "mred P t (x, m) ta (x', m')"
    and "sconf_type_ok i t x m"
    and "NewThread t'' x'' m'  set tat"
  moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
  moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
  moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
  moreover obtain e'' l'' where x'' [simp]: "x'' = (e'', l'')" by(cases x'', auto) 
  ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
    and red: "P,t  e, (m, l) -ta e', (m', l')"
    and nt: "NewThread t'' (e'', l'') m'  set tat" by auto
  from sconf_type have sconf: "E  (m, l) " and "type_ok P (E, T) e m" and tconf: "P,m  t √t"
    by(auto simp add: sconf_type_ok_def)
  then obtain T' where "P,E,m  e : T'" "P  T'  T" by(auto simp add: type_ok_def)
  from nt P,E,m  e : T' red have "E T. P,E,m'  e'' : T  P,m'  l'' (:≤) E"
    by(fastforce dest: red_type_newthread[OF wf])
  then obtain E'' T'' where "P,E'',m'  e'' : T''" "P,m'  l'' (:≤) E''" by blast
  moreover
  from sconf red P,E,m  e : T' tconf have "E  (m', l') "
    by(auto intro: red_preserves_sconf)
  moreover from mred tconf NewThread t'' x'' m'  set tat have "P,m'  t'' √t"
    by(rule red_tconf.preserves_NewThread)
  ultimately show "i''. sconf_type_ok i'' t'' x'' m'"
    by(auto simp add: sconf_type_ok_def type_ok_def sconf_def)
next
  fix t x m ta x' m' i i'' t'' x''
  assume mred: "mred P t (x, m) ta (x', m')" 
    and "sconf_type_ok i t x m" 
    and "sconf_type_ok i'' t'' x'' m" 
  moreover obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
  moreover obtain e' l' where x' [simp]: "x' = (e', l')" by(cases x', auto)
  moreover obtain E T where i [simp]: "i = (E, T)" by(cases i, auto)
  moreover obtain e'' l'' where x'' [simp]: "x'' = (e'', l'')" by(cases x'', auto)
  moreover obtain E'' T'' where i'' [simp]: "i'' = (E'', T'')" by(cases i'', auto)
  ultimately have sconf_type: "sconf_type_ok (E, T) t (e, l) m"
    and red: "P,t  e, (m, l) -ta e', (m', l')"
    and sc: "sconf_type_ok (E'', T'') t'' (e'', l'') m" by auto
  from sconf_type obtain T' where "P,E,m  e : T'" and "P,m  t √t"
    by(auto simp add: sconf_type_ok_def type_ok_def)
  from sc have sconf: "E''  (m, l'') " and "type_ok P (E'', T'') e'' m" and "P,m  t'' √t"
    by(auto simp add: sconf_type_ok_def)
  then obtain T''' where "P,E'',m  e'' : T'''" "P  T'''  T''" by(auto simp add: type_ok_def)
  moreover from red P,E'',m  e'' : T''' have "P,E'',m'  e'' : T'''"
    by(rule red_preserve_welltype)
  moreover from sconf red P,E,m  e : T' have "hconf m'"
    unfolding sconf_def by(auto dest: red_preserves_hconf)
  moreover {
    from red have "hext m m'" by(auto dest: red_hext_incr)
    moreover from sconf have "P,m  l'' (:≤) E''" "preallocated m"
      by(simp_all add: sconf_def)
    ultimately have "P,m'  l'' (:≤) E''" "preallocated m'"
      by(blast intro: lconf_hext preallocated_hext)+ }
  moreover from mred P,m  t √t P,m  t'' √t
  have "P,m'  t'' √t" by(rule red_tconf.preserves_other)
  ultimately have "sconf_type_ok (E'', T'') t'' (e'', l'') m'"
    by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
  thus "sconf_type_ok i'' t'' x'' m'" by simp
qed

end

subsection @{term "wf_red"}

context J_progress begin

context begin

declare red_mthr.actions_ok_iff [simp del]
declare red_mthr.actions_ok.cases [rule del]
declare red_mthr.actions_ok.intros [rule del]

lemma assumes wf: "wf_prog wf_md P"
  shows red_wf_red_aux:
  " P,t  e, s -ta e',s'; ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta; 
    sync_ok e; hconf (hp s); P,hp s  t √t;
     l. has_locks (ls $ l) t  expr_locks e l;
     ws t = None  
     (a vs w T Ts Tr D. call e = (a, wait, vs)  typeof_addr (hp s) a = T  P  class_type_of T sees wait: TsTr = Native in D  ws t = PostWS w) 
     e'' s'' ta'. P,t  e, s -ta' e'',s''  
        (red_mthr.actions_ok (ls, (ts, m), ws, is) t ta'  
         red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta'  red_mthr.actions_subset ta' ta)"
  (is " _; _; _; _; _; _; ?wakeup e s   ?concl e s ta")
    and reds_wf_red_aux:
  " P,t  es, s [-ta→] es',s'; ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta;
     sync_oks es; hconf (hp s); P,hp s  t √t;
     l. has_locks (ls $ l) t  expr_lockss es l;
     ws t = None  
     (a vs w T Ts T Tr D. calls es = (a, wait, vs)  typeof_addr (hp s) a = T  P  class_type_of T sees wait: TsTr = Native in D  ws t = PostWS w) 
     es'' s'' ta'. P,t  es, s [-ta'→] es'',s''  
        (red_mthr.actions_ok (ls, (ts, m), ws, is) t ta'  
         red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta'  red_mthr.actions_subset ta' ta)"
proof(induct rule: red_reds.inducts)
  case (SynchronizedRed2 e s ta e' s' a)
  note IH = ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta; sync_ok e; hconf (hp s); P,hp s  t √t;
            l. expr_locks e l  has_locks (ls $ l) t; ?wakeup e s
             ?concl e s ta
  note ¬ red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta
  moreover from sync_ok (insync(a) e) have "sync_ok e" by simp
  moreover note hconf (hp s) P,hp s  t √t
  moreover from l. expr_locks (insync(a) e) l  has_locks (ls $ l) t
  have "l. expr_locks e l  has_locks (ls $ l) t" by(force split: if_split_asm)
  moreover from ?wakeup (insync(a) e) s have "?wakeup e s" by auto
  ultimately have "?concl e s ta" by(rule IH)
  thus ?case by(fastforce intro: red_reds.SynchronizedRed2)
next
  case RedCall thus ?case
    by(auto simp add: is_val_iff contains_insync_conv contains_insyncs_conv red_mthr.actions_ok'_empty red_mthr.actions_ok'_ta_upd_obs dest: sees_method_fun)
next
  case (RedCallExternal s a U M Ts T D vs ta va h' ta' e' s')
  from ?wakeup (addr aM(map Val vs)) s
  have "wset (ls, (ts, m), ws, is) t = None  (M = wait  (w. wset (ls, (ts, m), ws, is) t = PostWS w))" by auto
  with wf  P,t  aM(vs),hp s -ta→ext va, h' P,hp s  t √t hconf (hp s)
  obtain ta'' va' h'' where red': "P,t  aM(vs),hp s -ta''→ext va',h''"
    and aok: "red_mthr.actions_ok (ls, (ts, m), ws, is) t ta'' 
              red_mthr.actions_ok' (ls, (ts, m), ws, is) t ta''  final_thread.actions_subset ta'' ta"
    by(rule red_external_wf_red)
  from aok ta' = extTA2J P ta
  have "red_mthr.actions_ok (ls, (ts, m), ws, is) t (extTA2J P ta'') 
        red_mthr.actions_ok' (ls, (ts, m), ws, is) t (extTA2J P ta'')  red_mthr.actions_subset (extTA2J P ta'') ta'"
    by(auto simp add: red_mthr.actions_ok'_convert_extTA red_mthr.actions_ok_iff elim: final_thread.actions_subset.cases del: subsetI)
  moreover from red' typeof_addr (hp s) a = U P  class_type_of U sees M: TsT = Native in D
  obtain s'' e'' where "P,t  addr aM(map Val vs),s -extTA2J P ta'' e'',s''"
    by(fastforce intro: red_reds.RedCallExternal)
  ultimately show ?case by blast
next
  case LockSynchronized
  hence False by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
  thus ?case ..
next
  case (UnlockSynchronized a v s)
  from l. expr_locks (insync(a) Val v) l  has_locks (ls $ l) t
  have "has_lock (ls $ a) t" by(force split: if_split_asm)
  with UnlockSynchronized have False by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
  thus ?case ..
next
  case (SynchronizedThrow2 a ad s)
  from l. expr_locks (insync(a) Throw ad) l  has_locks (ls $ l) t
  have "has_lock (ls $ a) t" by(force split: if_split_asm)
  with SynchronizedThrow2 have False
    by(auto simp add: lock_ok_las'_def finfun_upd_apply ta_upd_simps)
  thus ?case ..
next
  case BlockRed thus ?case by(simp)(blast intro: red_reds.intros)
qed
 (simp_all add: is_val_iff contains_insync_conv contains_insyncs_conv red_mthr.actions_ok'_empty
   red_mthr.actions_ok'_ta_upd_obs thread_action'_to_thread_action.simps red_mthr.actions_ok_iff
  split: if_split_asm del: split_paired_Ex,
  (blast intro: red_reds.intros elim: add_leE)+)

end

end

context J_heap_base begin

lemma shows red_ta_satisfiable:
  "P,t  e, s -ta e', s'  s. red_mthr.actions_ok s t ta"
  and reds_ta_satisfiable:
  "P,t  es, s [-ta→] es', s'  s. red_mthr.actions_ok s t ta"
apply(induct rule: red_reds.inducts)
apply(fastforce simp add: lock_ok_las_def finfun_upd_apply intro: exI[where x="K$ None"] exI[where x="K$ (t, 0)"] may_lock.intros dest: red_external_ta_satisfiable[where final="final_expr :: ('addr expr × 'addr locals)  bool"])+
done

end

context J_typesafe begin

lemma wf_progress: 
  assumes wf: "wf_J_prog P"
  shows "progress final_expr (mred P)
            (red_mthr.wset_Suspend_ok P ({s. sync_es_ok (thr s) (shr s)  lock_ok (locks s) (thr s)}  {s. Es. sconf_type_ts_ok Es (thr s) (shr s)}  {s. def_ass_ts_ok (thr s) (shr s)}))"
  (is "progress _ _ ?wf_state")
proof
  {
    fix s t x ta x' m' w
    assume "mred P t (x, shr s) ta (x', m')"
      and Suspend: "Suspend w  set taw"
    moreover obtain e xs where x: "x = (e, xs)" by(cases x)
    moreover obtain e' xs' where x': "x' = (e', xs')" by(cases x')
    ultimately have red: "P,t  e, (shr s, xs) -ta e', (m', xs')" by simp
    from red_Suspend_is_call[OF red Suspend]
    show "¬ final_expr x'" by(auto simp add: x')
  }
  note Suspend_final = this
  {
    fix s
    assume s: "s  ?wf_state"
    hence "lock_thread_ok (locks s) (thr s)"
      by(auto dest: red_mthr.wset_Suspend_okD1 intro: lock_ok_lock_thread_ok)
    moreover
    have "red_mthr.wset_final_ok (wset s) (thr s)"
    proof(rule red_mthr.wset_final_okI)
      fix t w
      assume "wset s t = w"
      from red_mthr.wset_Suspend_okD2[OF s this]
      obtain x0 ta x m1 w' ln'' and s0 :: "('addr, 'thread_id, 'heap) J_state"
        where mred: "mred P t (x0, shr s0) ta (x, m1)"
        and Suspend: "Suspend w'  set taw" 
        and tst: "thr s t = (x, ln'')" by blast
      from Suspend_final[OF mred Suspend] tst
      show " x ln. thr s t = (x, ln)  ¬ final_expr x" by blast
    qed
    ultimately show "lock_thread_ok (locks s) (thr s)  red_mthr.wset_final_ok (wset s) (thr s)" ..
  }
next
  fix s t ex ta e'x' m'
  assume wfs: "s  ?wf_state"
    and "thr s t = (ex, no_wait_locks)"
    and "mred P t (ex, shr s) ta (e'x', m')"
    and wait: "¬ waiting (wset s t)"
  moreover obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
  moreover obtain e x where ex: "ex = (e, x)" by(cases ex)
  moreover obtain e' x' where e'x': "e'x' = (e', x')" by(cases e'x')
  ultimately have tst: "ts t = (ex, no_wait_locks)" 
    and red: "P,t  e, (m, x) -ta e', (m', x')" by auto
  from wf have wwf: "wwf_J_prog P" by(rule wf_prog_wwf_prog)
  from wfs s obtain Es where aeos: "sync_es_ok ts m"
    and lockok: "lock_ok ls ts"
    and "sconf_type_ts_ok Es ts m"
    by(auto dest: red_mthr.wset_Suspend_okD1)
  with tst ex obtain E T where sconf: "sconf_type_ok (E, T) t (e, x) m"
    and aoe: "sync_ok e" by(fastforce dest: ts_okD ts_invD)
  then obtain T' where "hconf m" "P,E,m  e : T'" "preallocated m"
    by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
  from sconf_type_ts_ok Es ts m s have "thread_conf P (thr s) (shr s)"
    by(auto dest: ts_invD intro!: ts_okI simp add: sconf_type_ok_def)
  with thr s t = (ex, no_wait_locks) have "P,shr s  t √t" by(auto dest: ts_okD)

  show "ta' x' m'. mred P t (ex, shr s) ta' (x', m')  
        (red_mthr.actions_ok s t ta'  red_mthr.actions_ok' s t ta'  red_mthr.actions_subset ta' ta)"
  proof(cases "red_mthr.actions_ok' s t ta")
    case True
    have "red_mthr.actions_subset ta ta" ..
    with True mred P t (ex, shr s) ta (e'x', m') show ?thesis by blast
  next
    case False
    from lock_okD2[OF lockok, OF tst[unfolded ex]]
    have locks: "l. has_locks (ls $ l) t  expr_locks e l" by simp
    have "ws t = None  (a vs w T Ts Tr D. call e = (a, wait, vs)  typeof_addr (hp (m, x)) a = T  P  class_type_of T sees wait: TsTr = Native in D  ws t = PostWS w)"
    proof(cases "ws t")
      case None thus ?thesis ..
    next
      case (Some w)
      with red_mthr.wset_Suspend_okD2[OF wfs, of t w] tst ex s
      obtain e0 x0 m0 ta0 w' s1 tta1 
        where red0: "P,t  e0, (m0, x0) -ta0 e, (shr s1, x)"
        and Suspend: "Suspend w'  set ta0w"
        and s1: "P  s1 -▹tta1→* s" by auto 
      from red_Suspend_is_call[OF red0 Suspend] obtain a vs T Ts Tr D
        where call: "call e = (a, wait, vs)"
        and type: "typeof_addr m0 a = T" 
        and iec: "P  class_type_of T sees wait: TsTr = Native in D" by fastforce
      from red0 have "m0  shr s1" by(auto dest: red_hext_incr)
      also from s1 have "shr s1  shr s" by(rule RedT_hext_incr)
      finally have "typeof_addr (shr s) a = T" using type
        by(rule typeof_addr_hext_mono)
      moreover from Some wait s obtain w' where "ws t = PostWS w'"
        by(auto simp add: not_waiting_iff)
      ultimately show ?thesis using call iec s by auto
    qed
    from red_wf_red_aux[OF wf red False[unfolded s] aoe _ _ locks, OF _ _ this] hconf m P,shr s  t √t ex s
    show ?thesis by fastforce
  qed
next
  fix s t x
  assume wfs: "s  ?wf_state"
    and tst: "thr s t = (x, no_wait_locks)" 
    and nfin: "¬ final_expr x"
  obtain e xs where x: "x = (e, xs)" by(cases x)
  from wfs have "def_ass_ts_ok (thr s) (shr s)" by(auto dest: red_mthr.wset_Suspend_okD1)
  with tst x have DA: "𝒟 e dom xs" by(auto dest: ts_okD)
  from wfs obtain Es where "sconf_type_ts_ok Es (thr s) (shr s)"
    by(auto dest: red_mthr.wset_Suspend_okD1)
  with tst x obtain E T where "sconf_type_ok (E, T) t (e, xs) (shr s)" by(auto dest: ts_invD)
  then obtain T' where "hconf (shr s)" "P,E,shr s  e : T'"
    by(auto simp add: sconf_type_ok_def sconf_def type_ok_def)
  from red_progress(1)[OF wf_prog_wwf_prog[OF wf] this DA, where extTA="extTA2J P" and t=t] nfin x
  show "ta x' m'. mred P t (x, shr s) ta (x', m')" by fastforce
next
  fix s t x xm ta xm'
  assume "s  ?wf_state"
    and "thr s t = (x, no_wait_locks)"
    and "mred P t xm ta xm'"
    and "Notified  set taw  WokenUp  set taw"
  thus "collect_waits ta = {}"
    by(auto dest: red_ta_Wakeup_no_Join_no_Lock_no_Interrupt simp: split_beta)
next
  fix s t x ta x' m'
  assume "s  ?wf_state"
    and "thr s t = (x, no_wait_locks)"
    and "mred P t (x, shr s) ta (x', m')"
  thus "s'. red_mthr.actions_ok s' t ta"
    by(fastforce simp add: split_beta dest!: red_ta_satisfiable)
qed

lemma redT_progress_deadlock:
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  and Red: "P  J_start_state P C M vs -▹ttas→* s"
  and ndead: "¬ red_mthr.deadlock P s"
  shows "t' ta' s'. P  s -t'ta' s'"
proof -
  let ?wf_state = "red_mthr.wset_Suspend_ok P ({s. sync_es_ok (thr s) (shr s)  lock_ok (locks s) (thr s)}  {s. Es. sconf_type_ts_ok Es (thr s) (shr s)}  {s. def_ass_ts_ok (thr s) (shr s)})"
  interpret red_mthr: progress
    final_expr "mred P" convert_RA ?wf_state
    using wf by(rule wf_progress)
  from wf_start obtain Ts T pns body D 
    where start: "start_heap_ok" "P  C sees M:TsT = (pns, body) in D" "P,start_heap  vs [:≤] Ts"
    by(cases) auto
  from start have len: "length Ts = length vs" by(auto dest: list_all2_lengthD)

  have "invariant3p (mredT P) ?wf_state"
    by(rule red_mthr.invariant3p_wset_Suspend_ok) (intro invariant3p_IntI invariant3p_sync_es_ok_lock_ok[OF wf] lifting_inv.invariant3p_ts_inv[OF lifting_inv_sconf_subject_ok[OF wf]] lifting_wf.invariant3p_ts_ok[OF lifting_wf_def_ass[OF wf]])
  moreover note Red moreover
  have start': "J_start_state P C M vs  ?wf_state"
    apply(rule red_mthr.wset_Suspend_okI)
     apply(blast intro: sconf_type_ts_ok_J_start_state sync_es_ok_J_start_state lock_ok_J_start_state def_ass_ts_ok_J_start_state start wf len len[symmetric] wf_start)
    apply(simp add: start_state_def split_beta)
    done
  ultimately have "s  ?wf_state" unfolding red_mthr.RedT_def
    by(rule invariant3p_rtrancl3p)
  thus ?thesis using ndead by(rule red_mthr.redT_progress)
qed

lemma redT_progress_deadlocked:
  assumes wf: "wf_J_prog P" 
  and wf_start: "wf_start_state P C M vs"
  and Red: "P  J_start_state P C M vs -▹ttas→* s"
  and ndead:  "red_mthr.not_final_thread s t" "¬ t  red_mthr.deadlocked P s"
  shows "t' ta' s'. P  s -t'ta' s'"
using wf wf_start Red
proof(rule redT_progress_deadlock)
  from ndead show "¬ red_mthr.deadlock P s"
    unfolding red_mthr.deadlock_eq_deadlocked'
    by(auto simp add: red_mthr.deadlocked'_def)
qed

subsection ‹Type safety proof›

theorem TypeSafetyT:
  fixes C and M and ttas and Es
  defines "Es  == J_sconf_type_ET_start P C M"
  and     "Es' == upd_invs Es sconf_type_ok (concat (map (thr_a  snd) ttas))"
  assumes wf: "wf_J_prog P"
  and start_wf: "wf_start_state P C M vs"
  and RedT: "P  J_start_state P C M vs -▹ttas→* s'"
  and nored: "¬ (t ta s''. P  s' -tta s'')"
  shows "thread_conf P (thr s') (shr s')"
  and "thr s' t = ((e', x'), ln') 
       (v. e' = Val v  (E T. Es' t = (E, T)  P,shr s'  v :≤ T)  ln' = no_wait_locks)
        (a C. e' = Throw a  typeof_addr (shr s') a = Class_type C  P  C * Throwable  ln' = no_wait_locks)
        (t  red_mthr.deadlocked P s'  (E T. Es' t = (E, T)  (T'. P,E,shr s'  e' : T'  P  T'  T)))"
     (is "_  ?thesis2")
  and "Es m Es'"
proof -
  from start_wf obtain Ts T pns body D
    where start_heap: "start_heap_ok"
    and sees: "P  C sees M:TsT = (pns, body) in D"
    and conf: "P,start_heap  vs [:≤] Ts"
    by cases auto

  from RedT show "thread_conf P (thr s') (shr s')"
    by(rule red_tconf.RedT_preserves)(rule thread_conf_start_state[OF start_heap wf_prog_wf_syscls[OF wf]])

  show "Es m Es'" using RedT ts_inv_ok_J_sconf_type_ET_start
    unfolding Es'_def Es_def by(rule red_mthr.RedT_upd_inv_ext)

  assume "thr s' t = ((e', x'), ln')"
  moreover obtain ls' ts' m' ws' is' where s' [simp]: "s' = (ls', (ts', m'), ws', is')" by(cases s') fastforce
  ultimately have es't: "ts' t = ((e', x'), ln')" by simp
  from wf have wwf: "wwf_J_prog P" by(rule wf_prog_wwf_prog)
  from conf have len: "length vs = length Ts" by(rule list_all2_lengthD)
  from RedT def_ass_ts_ok_J_start_state[OF wf sees len] have defass': "def_ass_ts_ok ts' m'"
    by(fastforce dest: lifting_wf.RedT_preserves[OF lifting_wf_def_ass, OF wf])
  from RedT sync_es_ok_J_start_state[OF wf sees len[symmetric]] lock_ok_J_start_state[OF wf sees len[symmetric]]
  have lock': "lock_ok ls' ts'" by (fastforce dest: RedT_preserves_lock_ok[OF wf])
  from RedT sync_es_ok_J_start_state[OF wf sees len[symmetric]] have addr': "sync_es_ok ts' m'"
    by(fastforce dest: RedT_preserves_sync_ok[OF wf])
  from RedT sconf_type_ts_ok_J_start_state[OF wf start_wf]
  have sconf_subject': "sconf_type_ts_ok Es' ts' m'" unfolding Es'_def Es_def
    by(fastforce dest: lifting_inv.RedT_invariant[OF lifting_inv_sconf_subject_ok, OF wf] intro: thread_conf_start_state[OF _ wf_prog_wf_syscls[OF wf]])
  with es't obtain E T where ET: "Es' t = (E, T)" 
    and "sconf_type_ok (E, T) t (e', x') m'" by(auto dest!: ts_invD)
  { assume "final e'"
    have "ln' = no_wait_locks"
    proof(rule ccontr)
      assume "ln'  no_wait_locks"
      then obtain l where "ln' $ l > 0"
        by(auto simp add: neq_no_wait_locks_conv)
      from lock' es't have "has_locks (ls' $ l) t + ln' $ l = expr_locks e' l"
        by(auto dest: lock_okD2)
      with ln' $ l > 0 have "expr_locks e' l > 0" by simp
      moreover from final e' have "expr_locks e' l = 0" by(rule final_locks)
      ultimately show False by simp
    qed }
  note ln' = this
  { assume "v. e' = Val v"
    then obtain v where v: "e' = Val v" by blast
    with sconf_subject' ET es't have "P,m'  v :≤ T"
      by(auto dest: ts_invD simp add: type_ok_def sconf_type_ok_def conf_def)
    moreover from v ln' have "ln' = no_wait_locks" by(auto)
    ultimately have "v. e' = Val v  (E T. Es' t = (E, T)  P,m'  v :≤ T  ln' = no_wait_locks)"
      using ET v by blast }
  moreover
  { assume "a. e' = Throw a"
    then obtain a where a: "e' = Throw a" by blast
    with sconf_subject' ET es't have "T'. P,E,m'  e' : T'  P  T'  T"
      apply -
      apply(drule ts_invD, assumption)
      by(clarsimp simp add: type_ok_def sconf_type_ok_def)
    then obtain T' where "P,E,m'  e' : T'" and "P  T'  T" by blast
    with a have "C. typeof_addr m' a = Class_type C  P  C * Throwable"
      by(auto simp add: widen_Class)
    moreover from a ln' have "ln' = no_wait_locks" by(auto)
    ultimately have "a C. e' = Throw a  typeof_addr m' a = Class_type C  P  C * Throwable  ln' = no_wait_locks"
      using a by blast }
  moreover
  { assume nfine': "¬ final e'"
    with es't have "red_mthr.not_final_thread s' t"
      by(auto intro: red_mthr.not_final_thread.intros)
    with nored have "t  red_mthr.deadlocked P s'"
      by -(erule contrapos_np, rule redT_progress_deadlocked[OF wf start_wf RedT])
    moreover 
    from sconf_type_ok (E, T) t (e', x') m'
    obtain T'' where "P,E,m'  e' : T''" "P  T''  T"
      by(auto simp add: sconf_type_ok_def type_ok_def)
    with ET have "E T. Es' t = (E, T)  (T'. P,E,m'  e' : T'  P  T'  T)"
      by blast
    ultimately have "t  red_mthr.deadlocked P s'  (E T. Es' t = (E, T)  (T'. P,E,m'  e' : T'  P  T'  T))" .. }
  ultimately show ?thesis2 by simp(blast)
qed

end

end