Theory Deadlocked (Isabelle2009-1: December 2009)

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

header{* \isaheader{Preservation of Deadlock} *}

theory Deadlocked imports ProgressThreaded begin

lemma red_Lock_hext:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); hext (hp s) h |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨e, (h, lcl s)⟩ -ta-> ⟨e', (h, lcl s')⟩"
  and reds_Lock_hext:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); hext (hp s) h |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨es, (h, lcl s)⟩ [-ta->] ⟨es', (h, lcl s')⟩"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M vs ta va h' ta' e' s')
  from `typeof_{hp s} (Addr a) = ⌊T⌋` `hext (hp s) h` have "typeof_h (Addr a) = ⌊T⌋"
    by(auto split: heapobj.splits dest: hext_objD hext_arrD)
  moreover from `P \<turnstile> ⟨a•M(vs),hp s⟩ -ta->ext ⟨va,h'⟩` `Lock ∈ set (\<lbrace>ta'\<rbrace>_l_f l)` `hext (hp s) h` `ta' = convert_extTA extNTA ta`
  have "P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h⟩" by(auto intro: red_external_Lock_hext)
  ultimately show ?case using `ta' = convert_extTA extNTA ta` `e' = extRet2J va` `s' = (h', lcl s)`
    `is_external_call P T M` by(auto intro: red_reds.RedCallExternal)
qed(fastsimp intro: red_reds.intros dest: hext_objarrD)+

lemma red_Join_hext:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; hext (hp s) h |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨e, (h, lcl s)⟩ -ta-> ⟨e', (h, lcl s')⟩"

  and reds_Join_hext:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; hext (hp s) h |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨es, (h, lcl s)⟩ [-ta->] ⟨es', (h, lcl s')⟩"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M vs ta va h' ta' e' s')
  from `typeof_{hp s} (Addr a) = ⌊T⌋` `hext (hp s) h` have "typeof_h (Addr a) = ⌊T⌋"
    by(auto split: heapobj.splits dest: hext_objD hext_arrD)
  moreover from `P \<turnstile> ⟨a•M(vs),hp s⟩ -ta->ext ⟨va,h'⟩` `Join t ∈ set \<lbrace>ta'\<rbrace>_c` `hext (hp s) h`
    `ta' = convert_extTA extNTA ta` `typeof_{hp s} (Addr a) = ⌊T⌋`
  have "P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h⟩" by(auto intro: red_external_Join_hext)
  ultimately show ?case using `ta' = convert_extTA extNTA ta` `e' = extRet2J va` `s' = (h', lcl s)`
    `is_external_call P T M` by(auto intro: red_reds.RedCallExternal)
qed(fastsimp intro: red_reds.intros)+


lemma red_Lock_wth:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); P,E,h \<turnstile> e : T; hext h (hp s) |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨e, (h, lcl s)⟩ -ta-> ⟨e', (h, lcl s')⟩"

  and reds_Lock_wth:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); P,E,h \<turnstile> es [:] Ts; hext h (hp s) |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨es, (h, lcl s)⟩ [-ta->] ⟨es', (h, lcl s')⟩"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
  case (RedCallExternal s a U M vs ta va h' ta' e' s')
  from `typeof_{hp s} (Addr a) = ⌊U⌋` `P,E,h \<turnstile> addr a•M(map Val vs) : T` `hext h (hp s)`
  have "typeof_h (Addr a) = ⌊U⌋" by(fastsimp split: heapobj.split_asm dest: hext_objD hext_arrD)
  moreover with `P \<turnstile> ⟨a•M(vs),hp s⟩ -ta->ext ⟨va,h'⟩` `P,E,h \<turnstile> addr a•M(map Val vs) : T` 
    `Lock ∈ set (\<lbrace>ta'\<rbrace>_l_f l)` `hext h (hp s)` `ta' = convert_extTA extNTA ta` `is_external_call P U M`
  have "P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h⟩"
    by(auto intro: red_external_Lock_wth intro!: external_WT'.intros split: heapobj.split_asm)
  ultimately show ?case using `is_external_call P U M` `ta' = convert_extTA extNTA ta`
    `e' = extRet2J va` `s' = (h', lcl s)` by(auto intro: red_reds.RedCallExternal)
next
  case (LockSynchronized s a arrobj e E T)
  from `P,E,h \<turnstile> sync(addr a) e : T`
  have "∃arrobj. h a = ⌊arrobj⌋"
    by(auto elim: WTrt_elim_cases)
  thus ?case by(fastsimp intro: red_reds.LockSynchronized)
qed(fastsimp intro: red_reds.intros split: split_if_asm simp: finfun_upd_apply)+

lemma red_Join_wth:
  "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; P,E,h \<turnstile> e : T; hext h (hp s) |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨e, (h, lcl s)⟩ -ta-> ⟨e', (h, lcl s')⟩"
  and reds_Join_wth:
  "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; P,E,h \<turnstile> es [:] Ts; hext h (hp s) |]
  ==> convert_extTA extNTA,P \<turnstile> ⟨es, (h, lcl s)⟩ [-ta->] ⟨es', (h, lcl s')⟩"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
  case (RedCallExternal s a U M vs ta va h' ta' e' s')
  from `typeof_{hp s} (Addr a) = ⌊U⌋` `P,E,h \<turnstile> addr a•M(map Val vs) : T` `hext h (hp s)`
  have "typeof_h (Addr a) = ⌊U⌋" by(fastsimp split: heapobj.split_asm dest: hext_objD hext_arrD)
  moreover with `P \<turnstile> ⟨a•M(vs),hp s⟩ -ta->ext ⟨va,h'⟩` `P,E,h \<turnstile> addr a•M(map Val vs) : T` 
    `Join t ∈ set \<lbrace>ta'\<rbrace>_c` `hext h (hp s)` `ta' = convert_extTA extNTA ta` `is_external_call P U M`
  have "P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h⟩"
    by(auto intro: red_external_Join_wth intro!: external_WT'.intros split: heapobj.split_asm)
  ultimately show ?case using `is_external_call P U M` `ta' = convert_extTA extNTA ta`
    `e' = extRet2J va` `s' = (h', lcl s)` by(auto intro: red_reds.RedCallExternal)
qed(fastsimp intro: red_reds.intros split: split_if_asm)+

lemma red_wt_hconf_hext:
  assumes wf: "wf_J_prog P"
  and hconf: "P \<turnstile> H \<surd>"
  shows "[| convert_extTA extNTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; P,E,H \<turnstile> e : T; hext H (hp s) |]
        ==> ∃ta' e' s'. convert_extTA extNTA,P \<turnstile> ⟨e, (H, lcl s)⟩ -ta'-> ⟨e', s'⟩ ∧ locks_a ta' = locks_a ta ∧ wset_a ta' = wset_a ta ∧ cond_a ta' = cond_a ta"
  and "[| convert_extTA extNTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; P,E,H \<turnstile> es [:] Ts; hext H (hp s) |]
        ==> ∃ta' es' s'. convert_extTA extNTA,P \<turnstile> ⟨es, (H, lcl s)⟩ [-ta'->] ⟨es', s'⟩ ∧ locks_a ta' = locks_a ta ∧ wset_a ta' = wset_a ta ∧ cond_a ta' = cond_a ta"
proof(induct arbitrary: E T and E Ts rule: red_reds.inducts)
  case (RedNew h a C FDTs h' l E T)
  show ?case
  proof(cases "new_Addr H")
    case None thus ?thesis
      by(fastsimp intro: RedNewFail)
  next
    case (Some a)
    with `P \<turnstile> C has_fields FDTs` show ?thesis
      by(fastsimp intro: red_reds.RedNew)
  qed
next
  case (RedNewFail s C E T)
  show ?case
  proof(cases "new_Addr H")
    case None thus ?thesis
      by(fastsimp intro: red_reds.RedNewFail)
  next
    case (Some a)
    with `P,E,H \<turnstile> new C : T` wf show ?thesis
      by(fastsimp del:exE intro!:RedNew simp add:new_Addr_def elim!:wf_Fields_Ex[THEN exE])
  qed
next 
  case NewArrayRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedNewArray h a i h' T l E T')
  show ?case
  proof(cases "new_Addr H")
    case None thus ?thesis using `0 ≤ i`
      by(fastsimp intro: red_reds.RedNewArrayFail)
  next
    case (Some a)
    with `0 ≤ i` show ?thesis
      by(fastsimp intro: red_reds.RedNewArray)
  qed
next 
  case (RedNewArrayFail h i T l E T')
  show ?case
  proof(cases "new_Addr H")
    case None thus ?thesis using `0 ≤ i`
      by(fastsimp intro: red_reds.RedNewArrayFail)
  next
    case (Some a)
    with `0 ≤ i` show ?thesis
      by(fastsimp intro: red_reds.RedNewArray)
  qed
next
  case RedNewArrayNegative thus ?case by(fastsimp intro: red_reds.intros)
next
  case CastRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedCast s v U T E T')
  from `P,E,H \<turnstile> Cast T (Val v) : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix T''
    assume wt: "P,E,H \<turnstile> Val v : T''" "T = T'"
    show ?thesis
    proof(cases "P \<turnstile> T'' ≤ T")
      case True
      with wt show ?thesis
        by(fastsimp intro: red_reds.RedCast)
    next
      case False
      with wt show ?thesis
        by(fastsimp intro: red_reds.RedCastFail)
    qed
  qed
next 
  case (RedCastFail s v U T E T')
  from `P,E,H \<turnstile> Cast T (Val v) : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix T''
    assume wt: "P,E,H \<turnstile> Val v : T''" "T = T'"
    show ?thesis
    proof(cases "P \<turnstile> T'' ≤ T")
      case True
      with wt show ?thesis
        by(fastsimp intro: red_reds.RedCast)
    next
      case False
      with wt show ?thesis
        by(fastsimp intro: red_reds.RedCastFail)
    qed
  qed
next
  case BinOpRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case BinOpRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedBinOp thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedVar thus ?case by(fastsimp intro: red_reds.intros)
next
  case LAssRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedLAss thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAccRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAccRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedAAccNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedAAccBounds s a T el i E T')
  from `P,E,H \<turnstile> addr a⌊Val (Intg i)⌉ : T'` show ?case
  proof(rule WTrt_elim_cases)
    assume wt: "P,E,H \<turnstile> addr a : T'⌊⌉"
    then obtain el' where Ha: "H a = ⌊Arr T' el'⌋" by(auto split: heapobj.split_asm)
    with `hext H (hp s)` `hp s a = ⌊Arr T el⌋` have si': "length el' = length el"
      by(auto dest!: hext_arrD)
    with Ha `i < 0 ∨ int (length el) ≤ i` show ?thesis
      by(fastsimp intro: red_reds.RedAAccBounds)
  next
    assume wt: "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next 
  case (RedAAcc s a T el i E T')
  from `P,E,H \<turnstile> addr a⌊Val (Intg i)⌉ : T'` show ?case
  proof(rule WTrt_elim_cases)
    assume wt: "P,E,H \<turnstile> addr a : T'⌊⌉"
    then obtain el' where Ha: "H a = ⌊Arr T' el'⌋" by(auto split: heapobj.split_asm)
    with `hext H (hp s)` `hp s a = ⌊Arr T el⌋` have si': "length el' = length el"
      by(auto dest!: hext_arrD)
    with Ha `0 ≤ i` `i < int (length el)` show ?thesis
      by(fastsimp intro: red_reds.RedAAcc)
  next
    assume wt: "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case AAssRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAssRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAssRed3 thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedAAssNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedAAssBounds s a T el i e E T')
  from `P,E,H \<turnstile> addr a⌊Val (Intg i)⌉ := Val e : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix T'' T'''
    assume wt: "P,E,H \<turnstile> addr a : T''⌊⌉"
    then obtain el' where Ha: "H a = ⌊Arr T'' el'⌋" by(auto split: heapobj.split_asm)
    with `hext H (hp s)` `hp s a = ⌊Arr T el⌋` have si': "length el' = length el" and T'': "T'' = T"
      by(auto dest!: hext_arrD)
    with Ha `i < 0 ∨ int (length el) ≤ i` show ?thesis
      by(fastsimp intro: red_reds.RedAAssBounds)
  next
    fix T''
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case (RedAAssStore s a T el i w U E T')
  from `P,E,H \<turnstile> addr a⌊Val (Intg i)⌉ := Val w : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix T'' T'''
    assume wt: "P,E,H \<turnstile> addr a : T''⌊⌉"
      and wtw: "P,E,H \<turnstile> Val w : T'''"
    then obtain el' where Ha: "H a = ⌊Arr T'' el'⌋" by(auto split: heapobj.split_asm)
    with `hext H (hp s)` `hp s a = ⌊Arr T el⌋` have si': "length el' = length el" and T'': "T'' = T"
      by(auto dest!: hext_arrD)
    from `typeof_{hp s} w = ⌊U⌋` wtw `hext H (hp s)` have "typeof_H w = ⌊U⌋" 
      by(auto dest: type_of_hext_type_of)
    with Ha `0 ≤ i` `i < int (length el)` `¬ P \<turnstile> U ≤ T` T'' si' show ?thesis
      by(fastsimp intro: red_reds.RedAAssStore)
  next
    fix T''
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case (RedAAss h a T el i w U h' l E T')
  from `P,E,H \<turnstile> addr a⌊Val (Intg i)⌉ := Val w : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix T'' T'''
    assume wt: "P,E,H \<turnstile> addr a : T''⌊⌉"
      and wtw: "P,E,H \<turnstile> Val w : T'''"
    then obtain el' where Ha: "H a = ⌊Arr T'' el'⌋" by(auto split: heapobj.split_asm)
    with `hext H (hp (h, l))` `h a = ⌊Arr T el⌋` have si': "length el' = length el" and T'': "T'' = T"
      by(auto dest!: hext_arrD)
    from `typeof_h w = ⌊U⌋` wtw `hext H (hp (h, l))` have "typeof_H w = ⌊U⌋" 
      by(auto dest: type_of_hext_type_of)
    with Ha `0 ≤ i` `i < int (length el)` `P \<turnstile> U ≤ T` T'' si' show ?thesis
      by(fastsimp intro: red_reds.RedAAss)
  next
    fix T''
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case ALengthRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedALength s a T elem E T')
  from `P,E,H \<turnstile> addr a•length : T'`
  show ?case
  proof(rule WTrt_elim_cases)
    fix T''
    assume [simp]: "T' = Integer"
      and wta: "P,E,H \<turnstile> addr a : T''⌊⌉"
    then obtain len' elem' where "H a = ⌊Arr T'' elem'⌋" by(auto split: heapobj.split_asm)
    thus ?thesis by(fastsimp intro: red_reds.RedALength)
  next
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case (RedALengthNull s E T)
  show ?case by(fastsimp intro: red_reds.RedALengthNull)
next
  case FAccRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedFAcc s a C fs F D v E T)
  from `P,E,H \<turnstile> addr a•F{D} : T` show ?case
  proof(rule WTrt_elim_cases)
    fix C'
    assume wt: "P,E,H \<turnstile> addr a : Class C'"
      and has: "P \<turnstile> C' has F:T in D"
    then obtain fs' where fs': "H a = ⌊Obj C' fs'⌋" by(auto split: heapobj.split_asm)
    with hconf have "P,H \<turnstile> Obj C' fs' \<surd>" by(auto simp: hconf_def)
    with has have "∃v. fs' (F, D) = ⌊v⌋"
      by(fastsimp simp: oconf_def)
    with has fs' show ?thesis
      by(fastsimp intro: red_reds.RedFAcc)
  next
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case RedFAccNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case FAssRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case FAssRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedFAssNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedFAss h a C fs F D v l E T)
  from `P,E,H \<turnstile> addr a•F{D} := Val v : T` show ?case
  proof(rule WTrt_elim_cases)
    fix C' T' T2
    assume wt: "P,E,H \<turnstile> addr a : Class C'"
      and has: "P \<turnstile> C' has F:T' in D"
      and wtv: "P,E,H \<turnstile> Val v : T2"
      and T2T: "P \<turnstile> T2 ≤ T'"
    moreover from wt obtain fs' where "H a = ⌊Obj C' fs'⌋" by(auto split: heapobj.split_asm)
    ultimately show ?thesis
      by(fastsimp intro: red_reds.RedFAss)
  next
    fix T2
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case CallObj thus ?case by(fastsimp intro: red_reds.intros)
next
  case CallParams thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedCall s a C fs M Ts T pns body D vs E T')
  from `P,E,H \<turnstile> addr a•M(map Val vs) : T'` show ?case
  proof(rule WTrt_elim_cases)
    fix C' Ts' pns' body' D' Ts''
    assume wta: "P,E,H \<turnstile> addr a : Class C'"
      and sees: "P \<turnstile> C' sees M: Ts'->T' = (pns', body') in D'"
      and wtes: "P,E,H \<turnstile> map Val vs [:] Ts''"
      and widens: "P \<turnstile> Ts'' [≤] Ts'"
      and nexc: "¬ is_external_call P (Class C') M"
    from wta obtain fs' where fs': "H a = ⌊Obj C' fs'⌋" by(auto split: heapobj.split_asm)
    moreover from wtes have "length vs = length Ts''"
      by(auto intro: map_eq_imp_length_eq')
    moreover from widens have "length Ts'' = length Ts'"
      by(auto dest: widens_lengthD)
    moreover from sees wf have "wf_mdecl wf_J_mdecl P D' (M, Ts', T', pns', body')"
      by(auto intro: sees_wf_mdecl)
    hence "length pns' = length Ts'"
      by(simp add: wf_mdecl_def)
    moreover from `hp s a = ⌊Obj C fs⌋` `hext H (hp s)` fs' have "C = C'"
      by(auto dest: hext_objD)
    ultimately show ?thesis using sees nexc
      by(fastsimp intro: red_reds.RedCall)
  next
    fix Ts
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(auto split: heapobj.split_asm)
    thus ?thesis ..
  next
    fix T Ts'
    assume "P \<turnstile> T•M(Ts') :: T'" "P,E,H \<turnstile> addr a : T" "P,E,H \<turnstile> map Val vs [:] Ts'"
    with `hp s a = ⌊Obj C fs⌋` `hext H (hp s)` have "is_external_call P (Class C) M"
      by(fastsimp split: heapobj.split_asm intro: external_WT_is_external_call dest: hext_objD hext_arrD)
    then  show ?case using `¬ is_external_call P (Class C) M` by simp
  qed
next
  case (RedCallExternal s a U M vs ta va h' ta' e' s')
  from `P,E,H \<turnstile> addr a•M(map Val vs) : T` show ?case
  proof(rule WTrt_elim_cases)
    fix C ts pns body D Ts'
    assume "P,E,H \<turnstile> addr a : Class C" "¬ is_external_call P (Class C) M"
    with `is_external_call P U M` `typeof_{hp s} (Addr a) = ⌊U⌋` `hext H (hp s)` have False
      by(auto split: heapobj.split_asm dest: hext_objD hext_arrD)
    thus ?thesis ..
  next
    fix Ts
    assume "P,E,H \<turnstile> addr a : NT" thus ?thesis by(auto split: heapobj.split_asm)
  next
    fix T' Ts
    assume wta: "P,E,H \<turnstile> addr a : T'" and wtvs: "P,E,H \<turnstile> map Val vs [:] Ts"
      and wtext: "P \<turnstile> T'•M(Ts) :: T"
    from wta `typeof_{hp s} (Addr a) = ⌊U⌋` `hext H (hp s)` have [simp]: "T' = U"
      by(auto split: heapobj.split_asm dest: hext_objD hext_arrD)
    with wta have "typeof_H (Addr a) = ⌊U⌋" by simp
    hence "P,H \<turnstile> a•M(vs) : T" using wtext `P,E,H \<turnstile> map Val vs [:] Ts` by(auto intro: external_WT'.intros)
    from red_external_wt_hconf_hext[OF `P \<turnstile> ⟨a•M(vs),hp s⟩ -ta->ext ⟨va,h'⟩` this `hext H (hp s)`] wta
      `is_external_call P U M` `ta' = convert_extTA extNTA ta` `e' = extRet2J va` `s' = (h', lcl s)`
    show ?thesis by(fastsimp intro: red_reds.RedCallExternal simp del: split_paired_Ex)
  qed
next
  case RedCallNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case (BlockRed e h l V vo ta e' h' l' T E T')
  note IH = `!!E T. [|P,E,H \<turnstile> e : T; hext H (hp (h, l(V := vo)))|]
              ==> ∃ta' e' s'. convert_extTA extNTA,P \<turnstile> ⟨e,(H, lcl (h, l(V := vo)))⟩ -ta'-> ⟨e',s'⟩ ∧ \<lbrace>ta'\<rbrace>_l = \<lbrace>ta\<rbrace>_l ∧ \<lbrace>ta'\<rbrace>_w = \<lbrace>ta\<rbrace>_w ∧ \<lbrace>ta'\<rbrace>_c = \<lbrace>ta\<rbrace>_c`
  from IH[of "E(V \<mapsto> T)" T'] `P,E,H \<turnstile> {V:T=vo; e} : T'` `hext H (hp (h, l))`
  obtain ta' e' s' where "convert_extTA extNTA,P \<turnstile> ⟨e,(H, lcl (h, l(V := vo)))⟩ -ta'-> ⟨e',s'⟩" "\<lbrace>ta'\<rbrace>_l = \<lbrace>ta\<rbrace>_l" "\<lbrace>ta'\<rbrace>_w = \<lbrace>ta\<rbrace>_w" "\<lbrace>ta'\<rbrace>_c = \<lbrace>ta\<rbrace>_c"
    by auto
  thus ?case by(cases s', cases ta', fastsimp dest: red_reds.BlockRed)
next
  case RedBlock thus ?case by(fastsimp intro: red_reds.intros)
next
  case SynchronizedRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case SynchronizedNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case (LockSynchronized s a arrobj e E T)
  from `P,E,H \<turnstile> sync(addr a) e : T` show ?case
  proof(rule WTrt_elim_cases)
    fix T
    assume "P,E,H \<turnstile> addr a : T" "is_refT T" "T ≠ NT"
    then obtain arrobj where "H a = ⌊arrobj⌋"
      by(auto)
    thus ?thesis by(fastsimp intro: red_reds.LockSynchronized)
  next
    fix T
    assume "P,E,H \<turnstile> addr a : NT"
    hence False by(clarsimp split: heapobj.split_asm)
    thus ?thesis ..
  qed
next
  case SynchronizedRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case UnlockSynchronized thus ?case by(fastsimp intro: red_reds.intros)
next
  case SeqRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedSeq thus ?case by(fastsimp intro: red_reds.intros)
next
  case CondRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedCondT thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedCondF thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedWhile thus ?case by(fastsimp intro: red_reds.intros)
next
  case ThrowRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedThrowNull thus ?case by(fastsimp intro: red_reds.intros)
next
  case TryRed thus ?case by(fastsimp intro: red_reds.intros)
next
  case RedTry thus ?case by(fastsimp intro: red_reds.intros)
next
  case (RedTryCatch s a D fs C V e2 E T)
  from `P,E,H \<turnstile> try Throw a catch(C V) e2 : T`
  show ?case
  proof(rule WTrt_elim_cases)
    fix T1
    assume "P,E,H \<turnstile> Throw a : T1"
    thus ?thesis
    proof(rule WTrt_elim_cases)
      fix T'
      assume "P,E,H \<turnstile> addr a : T'"
      with `hp s a = ⌊Obj D fs⌋` `hext H (hp s)`
      obtain fs' where Ha: "H a = ⌊Obj D fs'⌋"
        by(auto dest: hext_objD hext_arrD split: split:heapobj.split_asm)
      with `P \<turnstile> D \<preceq>^* C` show ?thesis
        by(fastsimp intro: red_reds.RedTryCatch)
    qed
  qed
next
  case (RedTryFail s a D fs C V e2 E T)
  from `P,E,H \<turnstile> try Throw a catch(C V) e2 : T`
  show ?case
  proof(rule WTrt_elim_cases)
    fix T1
    assume "P,E,H \<turnstile> Throw a : T1"
    thus ?thesis
    proof(rule WTrt_elim_cases)
      fix T'
      assume "P,E,H \<turnstile> addr a : T'"
      with `hp s a = ⌊Obj D fs⌋` `hext H (hp s)`
      obtain fs' where Ha: "H a = ⌊Obj D fs'⌋" 
        by(clarsimp, case_tac aa, auto dest: hext_objD hext_arrD)
      with `¬ P \<turnstile> D \<preceq>^* C` show ?thesis
        apply -
        apply(rule exI)+
        apply(rule conjI)
        apply(rule red_reds.RedTryFail)
        by(fastsimp)+
    qed
  qed
next
  case ListRed1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case ListRed2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case NewArrayThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case CastThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case BinOpThrow1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case BinOpThrow2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case LAssThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAccThrow1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAccThrow2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAssThrow1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAssThrow2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case AAssThrow3 thus ?case by(fastsimp intro: red_reds.intros)
next
  case ALengthThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case FAccThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case FAssThrow1 thus ?case by(fastsimp intro: red_reds.intros)
next 
  case FAssThrow2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case CallThrowObj thus ?case by(fastsimp intro: red_reds.intros)
next
  case CallThrowParams thus ?case by(fastsimp intro: red_reds.intros)
next
  case BlockThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case SynchronizedThrow1 thus ?case by(fastsimp intro: red_reds.intros)
next
  case SynchronizedThrow2 thus ?case by(fastsimp intro: red_reds.intros)
next
  case SeqThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case CondThrow thus ?case by(fastsimp intro: red_reds.intros)
next
  case ThrowThrow thus ?case by(fastsimp intro: red_reds.intros)
qed

lemma can_lock_devreserp:
  "[| wf_J_prog P; P \<turnstile> ⟨e, (h', l)⟩ L \<wrong>; P,E,h \<turnstile> e : T; P \<turnstile> h \<surd>; hext h h' |] ==> P \<turnstile> ⟨e, (h, l)⟩ L \<wrong>"
apply(cases "L = {}")
 apply(clarsimp)
 apply(erule multithreaded_base.can_syncE)
 apply(clarsimp)
 apply(drule sym)
 apply(clarsimp)
 apply(drule red_wt_hconf_hext, assumption+)
  apply(simp)
 apply(clarsimp)
 apply(rule multithreaded_base.can_syncI)
 apply(fastsimp)
 apply(rule sym)
 apply(simp)
apply(erule multithreaded_base.can_syncE)
apply(case_tac x', auto elim!: collect_locksE)
 apply(drule red_Lock_wth)
 apply(auto intro: multithreaded_base.can_syncI)
apply(drule red_Join_wth)
apply(auto intro: multithreaded_base.can_syncI)
done


lemma can_sync_preserved:
  assumes "P \<turnstile> ⟨e, (h, l)⟩ LT \<wrong>"
  and "hext h h'"
  and "LT ≠ {}"
  shows "P \<turnstile> ⟨e, (h', l)⟩ \<wrong>"
using assms
apply -
apply(rule multithreaded_base.must_syncI)
apply(erule multithreaded_base.can_syncE)
apply(clarsimp)
apply(auto simp add: collect_locks_def)
apply(drule red_Lock_hext)
   apply(simp)
  apply(simp)
 apply(simp)
apply(drule red_Join_hext)
  apply(simp)
 apply(simp)
apply fastsimp
done

lemma preserve_deadlocked:
  assumes wf: "wf_J_prog P"
  and st: "sconf_type_ts_ok P Es (thr S) (shr S)"
  and da: "def_ass_ts_ok (thr S) (shr S)"
  and lto: "lock_thread_ok (locks S) (thr S)"
  shows "preserve_deadlocked final_expr (mred P) S"
proof -
  { fix tta s t' ta' s' t x ln
    assume Red: "P \<turnstile> S -\<triangleright>tta->* s"
      and red: "P \<turnstile> s -t'\<triangleright>ta'-> s'"
      and tst: "thr s t = ⌊(x, ln)⌋"
    obtain e l where x [simp]: "x = (e, l)" by(cases x, auto)
    let ?Es' = "upd_invs Es (λET (e, x) m. sconf_type_ok P ET e m x) (\<down>map (thr_a o snd) tta\<down>)"
    from st Red have st': "sconf_type_ts_ok P ?Es' (thr s) (shr s)"
      by(auto dest: RedT_invariant_sconf_type[OF wf])
    with tst obtain E T where Est: "?Es' t = ⌊(E, T)⌋" 
      and stt: "sconf_type_ok P (E, T) e (shr s) l" by(auto dest!: ts_invD)
    from stt have hconf: "P \<turnstile> shr s \<surd>"
      by(simp add: sconf_type_ok_def sconf_def)
    from stt obtain T' where wte: "P,E,shr s \<turnstile> e : T'"
      by(auto simp add: sconf_type_ok_def type_ok_def)
    from red have hext: "hext (shr s) (shr s')"
      by(cases s, cases s')(auto dest: redT_hext_incr)

    { fix LT
      assume "multithreaded_base.can_sync (mred P) x (shr s) LT"
        and LT: "LT ≠ {}"
      hence cl: "P \<turnstile> ⟨e, (shr s, l)⟩ LT \<wrong>" by auto
      with hext hconf LT have "P \<turnstile> ⟨e, (shr s', l)⟩ \<wrong>"
        by-(rule can_sync_preserved)
      hence "multithreaded_base.must_sync (mred P) x (shr s')" by simp }
    note ml = this
    { fix LT
      assume "multithreaded_base.can_sync (mred P) x (shr s') LT"
      hence cl: "P \<turnstile> ⟨e, (shr s', l)⟩ LT \<wrong>" by auto
      with wf wte hext hconf have "P \<turnstile> ⟨e, (shr s, l)⟩ LT \<wrong>"
        by -(rule can_lock_devreserp)
      hence "∃LT'⊆LT. multithreaded_base.can_sync (mred P) x (shr s) LT'"
        by(auto) }
    note this ml }
  with lto show ?thesis by(unfold_locales)
qed

end