Theory JMM_Typesafe

(*  Title:      JinjaThreads/MM/JMM_Typesafe.thy
    Author:     Andreas Lochbihler
*)

section ‹Type-safety proof for the Java memory model›

theory JMM_Typesafe 
imports
  JMM_Framework
begin

text ‹
  Create a dynamic list heap_independent› of theorems for replacing 
  heap-dependent constants by heap-independent ones. 
›
ML structure Heap_Independent_Rules = Named_Thms
(
  val name = @{binding heap_independent}
  val description = "Simplification rules for heap-independent constants"
)
setup Heap_Independent_Rules.setup

locale heap_base' = 
  h: heap_base 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write
  for addr2thread_id :: "('addr :: addr)  'thread_id"
  and thread_id2addr :: "'thread_id  'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap  htype  ('heap × 'addr) set"
  and typeof_addr :: "'addr  htype"
  and heap_read :: "'heap  'addr  addr_loc  'addr val  bool"
  and heap_write :: "'heap  'addr  addr_loc  'addr val  'heap  bool"
begin

definition typeof_h :: "'addr val  ty option"
where "typeof_h = h.typeof_h undefined"
lemma typeof_h_conv_typeof_h [heap_independent, iff]: "h.typeof_h h = typeof_h"
by(rule ext)(case_tac x, simp_all add: typeof_h_def)
lemmas typeof_h_simps [simp] = h.typeof_h.simps [unfolded heap_independent]

definition cname_of :: "'addr  cname"
where "cname_of = h.cname_of undefined"
lemma cname_of_conv_cname_of [heap_independent, iff]: "h.cname_of h = cname_of"
by(simp add: cname_of_def h.cname_of_def[abs_def])

definition addr_loc_type :: "'m prog  'addr  addr_loc  ty  bool"
where "addr_loc_type P = h.addr_loc_type P undefined"
notation addr_loc_type ("_  _@_ : _" [50, 50, 50, 50] 51)
lemma addr_loc_type_conv_addr_loc_type [heap_independent, iff]: 
  "h.addr_loc_type P h = addr_loc_type P"
by(simp add: addr_loc_type_def h.addr_loc_type_def)
lemmas addr_loc_type_cases [cases pred: addr_loc_type] = 
  h.addr_loc_type.cases[unfolded heap_independent]
lemmas addr_loc_type_intros = h.addr_loc_type.intros[unfolded heap_independent]

definition typeof_addr_loc :: "'m prog  'addr  addr_loc  ty"
where "typeof_addr_loc P = h.typeof_addr_loc P undefined"
lemma typeof_addr_loc_conv_typeof_addr_loc [heap_independent, iff]:
  "h.typeof_addr_loc P h = typeof_addr_loc P"
by(simp add: typeof_addr_loc_def h.typeof_addr_loc_def[abs_def])

definition conf :: "'a prog  'addr val  ty  bool"
where "conf P  h.conf P undefined"
notation conf ("_  _ :≤ _"  [51,51,51] 50)
lemma conf_conv_conf [heap_independent, iff]: "h.conf P h = conf P"
by(simp add: conf_def heap_base.conf_def[abs_def])
lemmas defval_conf [simp] = h.defval_conf[unfolded heap_independent]

definition lconf :: "'m prog  (vname  'addr val)  (vname  ty)  bool" 
where "lconf P = h.lconf P undefined"
notation lconf ("_  _ '(:≤') _" [51,51,51] 50)
lemma lconf_conv_lconf [heap_independent, iff]: "h.lconf P h = lconf P"
by(simp add: lconf_def h.lconf_def[abs_def])

definition confs :: "'m prog  'addr val list  ty list  bool"
where "confs P = h.confs P undefined"
notation confs ("_  _ [:≤] _" [51,51,51] 50)
lemma confs_conv_confs [heap_independent, iff]: "h.confs P h = confs P"
by(simp add: confs_def)

definition tconf :: "'m prog  'thread_id  bool" 
where "tconf P = h.tconf P undefined"
notation tconf ("_  _ √t" [51,51] 50)
lemma tconf_conv_tconf [heap_independent, iff]: "h.tconf P h = tconf P"
by(simp add: tconf_def h.tconf_def[abs_def])

definition vs_conf :: "'m prog  ('addr × addr_loc  'addr val set)  bool"
where "vs_conf P = h.vs_conf P undefined"
lemma vs_conf_conv_vs_conf [heap_independent, iff]: "h.vs_conf P h = vs_conf P"
by(simp add: vs_conf_def h.vs_conf_def[abs_def])

lemmas vs_confI = h.vs_confI[unfolded heap_independent]
lemmas vs_confD = h.vs_confD[unfolded heap_independent]

text ‹
  use non-speculativity to express that only type-correct values are read
›

primrec vs_type_all :: "'m prog  'addr × addr_loc  'addr val set"
where "vs_type_all P (ad, al) = {v. T. P  ad@al : T  P  v :≤ T}"

lemma vs_conf_vs_type_all [simp]: "vs_conf P (vs_type_all P)"
by(rule h.vs_confI[unfolded heap_independent])(simp)

lemma w_addrs_vs_type_all: "w_addrs (vs_type_all P)  dom typeof_addr"
by(auto simp add: w_addrs_def h.conf_def[unfolded heap_independent])

lemma w_addrs_vs_type_all_in_vs_type_all:
  "(ad  w_addrs (vs_type_all P). {(ad, al)|al. T. P  ad@al : T})  {adal. vs_type_all P adal  {}}"
by(auto simp add: w_addrs_def vs_type_all_def intro: defval_conf)

declare vs_type_all.simps [simp del]

lemmas vs_conf_insert_iff = h.vs_conf_insert_iff[unfolded heap_independent]

end


locale heap' =
  h: heap
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write
    P
  for addr2thread_id :: "('addr :: addr)  'thread_id"
  and thread_id2addr :: "'thread_id  'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap  htype  ('heap × 'addr) set"
  and typeof_addr :: "'addr  htype"
  and heap_read :: "'heap  'addr  addr_loc  'addr val  bool"
  and heap_write :: "'heap  'addr  addr_loc  'addr val  'heap  bool"
  and P :: "'m prog"

sublocale heap' < heap_base' .

context heap' begin

lemma vs_conf_w_value_WriteMemD: 
  " vs_conf P (w_value P vs ob); ob = NormalAction (WriteMem ad al v) 
   T. P  ad@al : T  P  v :≤ T"
by(auto elim: vs_confD)

lemma vs_conf_w_values_WriteMemD:
  " vs_conf P (w_values P vs obs); NormalAction (WriteMem ad al v)  set obs 
   T. P  ad@al : T  P  v :≤ T"
apply(induct obs arbitrary: vs)
apply(auto 4 3 elim: vs_confD intro: w_values_mono[THEN subsetD])
done

lemma w_values_vs_type_all_start_heap_obs:
  assumes wf: "wf_syscls P"
  shows "w_values P (vs_type_all P) (map snd (lift_start_obs h.start_tid h.start_heap_obs)) = vs_type_all P"
  (is "?lhs = ?rhs")
proof(rule antisym, rule le_funI, rule subsetI)
  fix adal v
  assume v: "v  ?lhs adal"
  obtain ad al where adal: "adal = (ad, al)" by(cases adal)
  show "v  ?rhs adal"
  proof(rule ccontr)
    assume v': "¬ ?thesis"
    from in_w_valuesD[OF v[unfolded adal] this[unfolded adal]]
    obtain obs' wa obs''
      where eq: "map snd (lift_start_obs h.start_tid h.start_heap_obs) = obs' @ wa # obs''"
      and "write": "is_write_action wa"
      and loc: "(ad, al)  action_loc_aux P wa"
      and vwa: "value_written_aux P wa al = v"
      by blast+
    from "write" show False
    proof cases
      case (WriteMem ad' al' v')
      with vwa loc eq have "WriteMem ad al v  set h.start_heap_obs"
        by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
      from h.start_heap_write_typeable[OF this] v' adal
      show ?thesis by(auto simp add: vs_type_all_def)
    next
      case (NewHeapElem ad' hT)
      with vwa loc eq have "NewHeapElem ad hT  set h.start_heap_obs"
        by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
      hence "typeof_addr ad = hT"
        by(rule h.NewHeapElem_start_heap_obsD[OF wf])
      with v' adal loc vwa NewHeapElem show ?thesis
        by(auto  simp add: vs_type_all_def intro: addr_loc_type_intros h.addr_loc_default_conf[unfolded heap_independent])
    qed
  qed
qed(rule w_values_greater)

end


lemma lprefix_lappend2I: "lprefix xs ys  lprefix xs (lappend ys zs)"
by(auto simp add: lappend_assoc lprefix_conv_lappend)

locale known_addrs_typing' =
  h: known_addrs_typing
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate "λ_. typeof_addr" heap_read heap_write 
    allocated known_addrs 
    final r wfx
    P
  for addr2thread_id :: "('addr :: addr)  'thread_id"
  and thread_id2addr :: "'thread_id  'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap  htype  ('heap × 'addr) set"
  and typeof_addr :: "'addr  htype"
  and heap_read :: "'heap  'addr  addr_loc  'addr val  bool"
  and heap_write :: "'heap  'addr  addr_loc  'addr val  'heap  bool" 
  and allocated :: "'heap  'addr set"
  and known_addrs :: "'thread_id  'x  'addr set"
  and final :: "'x  bool"
  and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_  _ -_ _" [50,0,0,50] 80) 
  and wfx :: "'thread_id  'x  'heap  bool"
  and P :: "'md prog"
  +
  assumes NewHeapElem_typed: ― ‹Should this be moved to known\_addrs\_typing?›
  " t  (x, h) -ta (x', h'); NewHeapElem ad CTn  set tao; typeof_addr ad  None 
   typeof_addr ad = CTn"

sublocale known_addrs_typing' < heap' by unfold_locales

context known_addrs_typing' begin

lemma known_addrs_typeable_in_vs_type_all:
  "h.if.known_addrs_state s  dom typeof_addr 
   (a  h.if.known_addrs_state s. {(a, al)|al. T. P  a@al : T})  {adal. vs_type_all P adal  {}}"
by(auto 4 4 dest: subsetD simp add: vs_type_all.simps intro: defval_conf)

lemma if_NewHeapElem_typed: 
  " t  xh -ta→i x'h'; NormalAction (NewHeapElem ad CTn)  set tao; typeof_addr ad  None 
   typeof_addr ad = CTn"
by(cases rule: h.mthr.init_fin.cases)(auto dest: NewHeapElem_typed)

lemma if_redT_NewHeapElem_typed:
  " h.mthr.if.redT s (t, ta) s'; NormalAction (NewHeapElem ad CTn)  set tao; typeof_addr ad  None 
   typeof_addr ad = CTn"
by(cases rule: h.mthr.if.redT.cases)(auto dest: if_NewHeapElem_typed)

lemma non_speculative_written_value_typeable:
  assumes wfx_start: "ts_ok wfx (thr (h.start_state f P C M vs)) h.start_heap" 
  and wfP: "wf_syscls P"
  and E: "E  h.ℰ_start f P C M vs status"
  and "write": "w  write_actions E"
  and adal: "(ad, al)  action_loc P E w"
  and ns: "non_speculative P (vs_type_all P) (lmap snd (ltake (enat w) E))"
  shows "T. P  ad@al : T  P  value_written P E w (ad, al) :≤ T"
proof -
  let ?start_state = "init_fin_lift_state status (h.start_state f P C M vs)"
    and ?start_obs = "lift_start_obs h.start_tid h.start_heap_obs"
    and ?v = "value_written P E w (ad, al)"

  from "write" have iwa: "is_write_action (action_obs E w)" by cases

  from E obtain E' where E': "E = lappend (llist_of ?start_obs) E'"
    and : "E'  h.mthr.if.ℰ ?start_state" by blast
  from  obtain E'' where E'': "E' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E'')"
    and Runs: "h.mthr.if.mthr.Runs ?start_state E''"
    by-(rule h.mthr.if.ℰ.cases[OF ])
  
  have wfx': "ts_ok (init_fin_lift wfx) (thr ?start_state) (shr ?start_state)"
    using wfx_start by(simp add: h.shr_start_state)

  from ns E'
  have ns: "non_speculative P (vs_type_all P) (lmap snd (ldropn (length (lift_start_obs h.start_tid h.start_heap_obs)) (ltake (enat w) E)))"
    by(subst (asm) lappend_ltake_ldrop[where n="enat (length (lift_start_obs h.start_tid h.start_heap_obs))", symmetric])(simp add: non_speculative_lappend min_def ltake_lappend1 w_values_vs_type_all_start_heap_obs[OF wfP] ldrop_enat split: if_split_asm)

  show ?thesis
  proof(cases "w < length ?start_obs")
    case True
    hence in_start: "action_obs E w  set (map snd ?start_obs)"
      unfolding in_set_conv_nth E' by(simp add: lnth_lappend action_obs_def map_nth exI[where x="w"])
    
    from iwa show ?thesis
    proof(cases)
      case (WriteMem ad' al' v')
      with adal have "ad' = ad" "al' = al" "?v = v'" by(simp_all add: value_written.simps)
      with WriteMem in_start have "WriteMem ad al ?v  set h.start_heap_obs" by auto
      thus ?thesis by(rule h.start_heap_write_typeable[unfolded heap_independent])
    next
      case (NewHeapElem ad' CTn)
      with adal have [simp]: "ad' = ad" by auto
      with NewHeapElem in_start have "NewHeapElem ad CTn  set h.start_heap_obs" by auto
      with wfP have "typeof_addr ad = CTn" by(rule h.NewHeapElem_start_heap_obsD)
      with adal NewHeapElem show ?thesis
        by(cases al)(auto simp add: value_written.simps intro: addr_loc_type_intros h.addr_loc_default_conf[unfolded heap_independent])
    qed
  next
    case False
    define w' where "w' = w - length ?start_obs"
    with "write" False have w'_len: "enat w' < llength E'"
      by(cases "llength E'")(auto simp add: actions_def E' elim: write_actions.cases)
    with Runs obtain m_w n_w t_w ta_w 
      where E'_w: "lnth E' w' = (t_w, ta_wo ! n_w)"
      and n_w: "n_w < length ta_wo"
      and m_w: "enat m_w < llength E''"
      and w_sum: "w' = (i<m_w. length snd (lnth E'' i)o) + n_w"
      and E''_m_w: "lnth E'' m_w = (t_w, ta_w)"
      unfolding E'' by(rule h.mthr.if.actions_ℰE_aux)

    from E'_w have obs_w: "action_obs E w = ta_wo ! n_w"
      using False E' w'_def by(simp add: action_obs_def lnth_lappend)
    
    let ?E'' = "ldropn (Suc m_w) E''"
    let ?m_E'' = "ltake (enat m_w) E''"
    have E'_unfold: "E'' = lappend ?m_E'' (LCons (lnth E'' m_w) ?E'')"
      unfolding ldropn_Suc_conv_ldropn[OF m_w] by simp
    hence "h.mthr.if.mthr.Runs ?start_state (lappend ?m_E'' (LCons (lnth E'' m_w) ?E''))"
      using Runs by simp
    then obtain σ' where σ_σ': "h.mthr.if.mthr.Trsys ?start_state (list_of ?m_E'') σ'"
      and Runs': "h.mthr.if.mthr.Runs σ' (LCons (lnth E'' m_w) ?E'')"
      by(rule h.mthr.if.mthr.Runs_lappendE) simp
    from Runs' obtain σ''' where red_w: "h.mthr.if.redT σ' (t_w, ta_w) σ'''"
      and Runs'': "h.mthr.if.mthr.Runs σ''' ?E''"
      unfolding E''_m_w by cases

    let ?EE'' = "lmap snd (lappend (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E'')) (llist_of (map (Pair t_w) (take (n_w + 1) ta_wo))))"
    have len_EE'': "llength ?EE'' = enat (w' + 1)" using n_w m_w
      apply(simp add: w_sum)
      apply(subst llength_lconcat_lfinite_conv_sum)
      apply(simp_all add: split_beta plus_enat_simps(1)[symmetric] add_Suc_right[symmetric] del: plus_enat_simps(1) add_Suc_right)
      apply(subst sum_comp_morphism[symmetric, where h=enat])
      apply(simp_all add: zero_enat_def min_def le_Suc_eq)
      apply(rule sum.cong)
      apply(auto simp add: lnth_ltake less_trans[where y="enat m_w"])
      done
    have prefix: "lprefix ?EE'' (lmap snd E')" unfolding E''
      by(subst (2) E'_unfold)(rule lmap_lprefix, clarsimp simp add: lmap_lappend_distrib E''_m_w lprefix_lappend2I[OF lprefix_llist_ofI[OF exI[where x="map (Pair t_w) (drop (n_w + 1) ta_wo)"]]] map_append[symmetric])

    from iwa False have iwa': "is_write_action (action_obs E' w')" by(simp add: E' action_obs_def lnth_lappend w'_def)
    from ns False
    have "non_speculative P (vs_type_all P) (lmap snd (ltake (enat w') E'))"
      by(simp add: E' ltake_lappend lmap_lappend_distrib non_speculative_lappend ldropn_lappend2 w'_def)
    with iwa'
    have "non_speculative P (vs_type_all P) (lappend (lmap snd (ltake (enat w') E')) (LCons (action_obs E' w') LNil))"
      by cases(simp_all add: non_speculative_lappend)
    also have "lappend (lmap snd (ltake (enat w') E')) (LCons (action_obs E' w') LNil) = lmap snd (ltake (enat (w' + 1)) E')"
      using w'_len by(simp add: ltake_Suc_conv_snoc_lnth lmap_lappend_distrib action_obs_def)
    also {
      have "lprefix (lmap snd (ltake (enat (w' + 1)) E')) (lmap snd E')" by(rule lmap_lprefix) simp
      with prefix have "lprefix ?EE'' (lmap snd (ltake (enat (w' + 1)) E'))  
        lprefix (lmap snd (ltake (enat (w' + 1)) E')) ?EE''"
        by(rule lprefix_down_linear)
      moreover have "llength (lmap snd (ltake (enat (w' + 1)) E')) = enat (w' + 1)"
        using w'_len by(cases "llength E'") simp_all
      ultimately have "lmap snd (ltake (enat (w' + 1)) E') = ?EE''"
        using len_EE'' by(auto dest: lprefix_llength_eq_imp_eq) }
    finally
    have ns1: "non_speculative P (vs_type_all P) (llist_of (concat (map (λ(t, ta). tao) (list_of ?m_E''))))"
      and ns2: "non_speculative P (w_values P (vs_type_all P) (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E''))))) (llist_of (take (Suc n_w) ta_wo))"
      by(simp_all add: lmap_lappend_distrib non_speculative_lappend split_beta lconcat_llist_of[symmetric] lmap_lconcat llist.map_comp o_def split_def list_of_lmap[symmetric] del: list_of_lmap)

    have "vs_conf P (vs_type_all P)" by simp
    with σ_σ' wfx' ns1
    have wfx': "ts_ok (init_fin_lift wfx) (thr σ') (shr σ')"
      and vs_conf: "vs_conf P (w_values P (vs_type_all P) (concat (map (λ(t, ta). tao) (list_of ?m_E''))))"
      by(rule h.if_RedT_non_speculative_invar[unfolded h.mthr.if.RedT_def heap_independent])+
    
    have "concat (map (λ(t, ta). tao) (list_of ?m_E'')) = map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E'')))"
      by(simp add: split_def lmap_lconcat llist.map_comp o_def list_of_lconcat map_concat)
    with vs_conf have "vs_conf P (w_values P (vs_type_all P) )" by simp
    with red_w wfx' ns2
    have vs_conf': "vs_conf P (w_values P (w_values P (vs_type_all P) (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E''))))) (take (Suc n_w) ta_wo))"
      (is "vs_conf _ ?vs'")
      by(rule h.if_redT_non_speculative_vs_conf[unfolded heap_independent])

    from len_EE'' have "enat w' < llength ?EE''" by simp
    from w'_len have "lnth ?EE'' w' = action_obs E' w'"
      using lprefix_lnthD[OF prefix enat w' < llength ?EE''] by(simp add: action_obs_def)
    hence "  lset ?EE''" using enat w' < llength ?EE'' unfolding lset_conv_lnth by(auto intro!: exI)
    also have "  set (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E''))) @ take (Suc n_w) ta_wo)"
      by(auto 4 4 intro: rev_image_eqI rev_bexI simp add: split_beta lset_lconcat_lfinite dest: lset_lappend[THEN subsetD])
    also have "action_obs E' w' = action_obs E w"
      using False by(simp add: E' w'_def lnth_lappend action_obs_def)
    also note obs_w_in_set = calculation and calculation = nothing

    from iwa have "?v  w_values P (vs_type_all P) (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) ?m_E''))) @ take (Suc n_w) ta_wo) (ad, al)"
    proof(cases)
      case (WriteMem ad' al' v')
      with adal have "ad' = ad" "al' = al" "?v = v'" by(simp_all add: value_written.simps)
      with obs_w_in_set WriteMem show ?thesis
        by -(rule w_values_WriteMemD, simp)
    next
      case (NewHeapElem ad' CTn)
      with adal have [simp]: "ad' = ad" and v: "?v = addr_loc_default P CTn al" 
        by(auto simp add: value_written.simps)
      with obs_w_in_set NewHeapElem adal show ?thesis
        by(unfold v)(rule w_values_new_actionD, simp_all)
    qed
    hence "?v  ?vs' (ad, al)" by simp
    with vs_conf' show "T. P  ad@al : T  P  ?v :≤ T"
      by(rule h.vs_confD[unfolded heap_independent])
  qed
qed

lemma hb_read_value_typeable:
  assumes wfx_start: "ts_ok wfx (thr (h.start_state f P C M vs)) h.start_heap" 
    (is "ts_ok wfx (thr ?start_state) _")
  and wfP: "wf_syscls P"
  and E: "E  h.ℰ_start f P C M vs status"
  and wf: "P  (E, ws) "
  and races: "a ad al v.  enat a < llength E; action_obs E a = NormalAction (ReadMem ad al v); ¬ P,E  ws a ≤hb a 
               T. P  ad@al : T  P  v :≤ T"
  and r: "enat a < llength E"
  and read: "action_obs E a = NormalAction (ReadMem ad al v)"
  shows "T. P  ad@al : T  P  v :≤ T"
using r read
proof(induction a arbitrary: ad al v rule: less_induct)
  case (less a)
  note r = enat a < llength E
    and read = action_obs E a = NormalAction (ReadMem ad al v)
  show ?case
  proof(cases "P,E  ws a ≤hb a")
    case False with r read show ?thesis by(rule races)
  next
    case True
    note hb = this
    hence ao: "E  ws a ≤a a" by(rule happens_before_into_action_order)

    from wf have ws: "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
    from r have "a  actions E" by(simp add: actions_def)
    hence "a  read_actions E" using read ..
    from is_write_seenD[OF ws this read]
    have "write": "ws a  write_actions E" 
      and adal_w: "(ad, al)  action_loc P E (ws a)"
      and written: "value_written P E (ws a) (ad, al) = v" by simp_all
    from "write" have iwa: "is_write_action (action_obs E (ws a))" by cases

    let ?start_state = "init_fin_lift_state status (h.start_state f P C M vs)"
      and ?start_obs = "lift_start_obs h.start_tid h.start_heap_obs"

    show ?thesis
    proof(cases "ws a < a")
      case True
      let ?EE'' = "lmap snd (ltake (enat (ws a)) E)"

      have "non_speculative P (vs_type_all P) ?EE''"
      proof(rule non_speculative_nthI)
        fix i ad' al' v'
        assume i: "enat i < llength ?EE''"
          and nth_i: "lnth ?EE'' i = NormalAction (ReadMem ad' al' v')"
        
        from i have "i < ws a" by simp
        hence i': "i < a" using True by(simp)
        moreover
        with r have "enat i < llength E" by(metis enat_ord_code(2) order_less_trans) 
        moreover
        with nth_i i i < ws a
        have "action_obs E i = NormalAction (ReadMem ad' al' v')"
          by(simp add: action_obs_def lnth_ltake ac_simps)
        ultimately have "T. P  ad'@al' : T  P  v' :≤ T" by(rule less.IH)
        hence "v'  vs_type_all P (ad', al')" by(simp add: vs_type_all.simps)
        thus "v'  w_values P (vs_type_all P) (list_of (ltake (enat i) ?EE'')) (ad', al')"
          by(rule w_values_mono[THEN subsetD])
      qed
      with wfx_start wfP E "write" adal_w
      show ?thesis unfolding written[symmetric] by(rule non_speculative_written_value_typeable)
    next
      case False
      
      from E obtain E' where E': "E = lappend (llist_of ?start_obs) E'"
        and : "E'  h.mthr.if.ℰ ?start_state" by blast
      from  obtain E'' where E'': "E' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E'')"
        and Runs: "h.mthr.if.mthr.Runs ?start_state E''"
        by-(rule h.mthr.if.ℰ.cases[OF ])

      have wfx': "ts_ok (init_fin_lift wfx) (thr ?start_state) (shr ?start_state)"
        using wfx_start by(simp add: h.shr_start_state)

      have a_start: "¬ a < length ?start_obs"
      proof
        assume "a < length ?start_obs"
        with read have "NormalAction (ReadMem ad al v)  snd ` set ?start_obs"
          unfolding set_map[symmetric] in_set_conv_nth
          by(auto simp add: E' lnth_lappend action_obs_def)
        hence "ReadMem ad al v  set h.start_heap_obs" by auto
        thus False by(simp add: h.start_heap_obs_not_Read)
      qed
      hence ws_a_not_le: "¬ ws a < length ?start_obs" using False by simp

      define w where "w = ws a - length ?start_obs"
      from "write" ws_a_not_le w_def
      have "enat w < llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E''))"
        by(cases "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E''))")(auto simp add: actions_def E' E'' elim: write_actions.cases)
      with Runs obtain m_w n_w t_w ta_w 
        where E'_w: "lnth E' w = (t_w, ta_wo ! n_w)"
        and n_w: "n_w < length ta_wo"
        and m_w: "enat m_w < llength E''"
        and w_sum: "w = (i<m_w. length snd (lnth E'' i)o) + n_w"
        and E''_m_w: "lnth E'' m_w = (t_w, ta_w)"
        unfolding E'' by(rule h.mthr.if.actions_ℰE_aux)

      from E'_w have obs_w: "action_obs E (ws a) = ta_wo ! n_w"
        using ws_a_not_le E' w_def by(simp add: action_obs_def lnth_lappend)

      let ?E'' = "ldropn (Suc m_w) E''"
      let ?m_E'' = "ltake (enat m_w) E''"
      have E'_unfold: "E'' = lappend ?m_E'' (LCons (lnth E'' m_w) ?E'')"
        unfolding ldropn_Suc_conv_ldropn[OF m_w] by simp
      hence "h.mthr.if.mthr.Runs ?start_state (lappend ?m_E'' (LCons (lnth E'' m_w) ?E''))"
        using Runs by simp
      then obtain σ' where σ_σ': "h.mthr.if.mthr.Trsys ?start_state (list_of ?m_E'') σ'"
        and Runs': "h.mthr.if.mthr.Runs σ' (LCons (lnth E'' m_w) ?E'')"
        by(rule h.mthr.if.mthr.Runs_lappendE) simp
      from Runs' obtain σ''' where red_w: "h.mthr.if.redT σ' (t_w, ta_w) σ'''"
        and Runs'': "h.mthr.if.mthr.Runs σ''' ?E''"
        unfolding E''_m_w by cases

      from "write" a  read_actions E have "ws a  a" by(auto dest: read_actions_not_write_actions)
      with False have "ws a > a" by simp
      with ao have new: "is_new_action (action_obs E (ws a))"
        by(simp add: action_order_def split: if_split_asm)
      then obtain CTn where obs_w': "action_obs E (ws a) = NormalAction (NewHeapElem ad CTn)" 
        using adal_w by cases auto

      define a' where "a' = a - length ?start_obs"
      with False w_def
      have "enat a' < llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E''))"
        by(simp add: le_less_trans[OF _ enat w < llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E''))])
      with Runs obtain m_a n_a t_a ta_a 
        where E'_a: "lnth E' a' = (t_a, ta_ao ! n_a)"
        and n_a: "n_a < length ta_ao"
        and m_a: "enat m_a < llength E''"
        and a_sum: "a' = (i<m_a. length snd (lnth E'' i)o) + n_a"
        and E''_m_a: "lnth E'' m_a = (t_a, ta_a)"
        unfolding E'' by(rule h.mthr.if.actions_ℰE_aux)
        
      from a_start E'_a read have obs_a: "ta_ao ! n_a = NormalAction (ReadMem ad al v)"
        using E' w_def by(simp add: action_obs_def lnth_lappend a'_def)
      
      let ?E'' = "ldropn (Suc m_a) E''"
      let ?m_E'' = "ltake (enat m_a) E''"
      have E'_unfold: "E'' = lappend ?m_E'' (LCons (lnth E'' m_a) ?E'')"
        unfolding ldropn_Suc_conv_ldropn[OF m_a] by simp
      hence "h.mthr.if.mthr.Runs ?start_state (lappend ?m_E'' (LCons (lnth E'' m_a) ?E''))"
        using Runs by simp
      then obtain σ'' where σ_σ'': "h.mthr.if.mthr.Trsys ?start_state (list_of ?m_E'') σ''"
        and Runs'': "h.mthr.if.mthr.Runs σ'' (LCons (lnth E'' m_a) ?E'')"
        by(rule h.mthr.if.mthr.Runs_lappendE) simp
      from Runs'' obtain σ''' where red_a: "h.mthr.if.redT σ'' (t_a, ta_a) σ'''"
        and Runs'': "h.mthr.if.mthr.Runs σ''' ?E''"
        unfolding E''_m_a by cases

      let ?EE'' = "llist_of (concat (map (λ(t, ta). tao) (list_of ?m_E'')))"
      from m_a have "enat m_a  llength E''" by simp
      hence len_EE'': "llength ?EE'' = enat (a' - n_a)"
        by(simp add: a_sum length_concat sum_list_sum_nth atLeast0LessThan length_list_of_conv_the_enat min_def split_beta lnth_ltake)
      have prefix: "lprefix ?EE'' (lmap snd E')" unfolding E''
        by(subst (2) E'_unfold)(simp add: lmap_lappend_distrib  lmap_lconcat llist.map_comp o_def split_def lconcat_llist_of[symmetric] lmap_llist_of[symmetric] lprefix_lappend2I del: lmap_llist_of)
      
      have ns: "non_speculative P (vs_type_all P) ?EE''"
      proof(rule non_speculative_nthI)
        fix i ad' al' v'
        assume i: "enat i < llength ?EE''"
          and lnth_i: "lnth ?EE'' i = NormalAction (ReadMem ad' al' v')"
          and "non_speculative P (vs_type_all P) (ltake (enat i) ?EE'')"
        
        let ?i = "i + length ?start_obs"
        
        from i len_EE'' have "i < a'" by simp
        hence i': "?i < a" by(simp add: a'_def)
        moreover
        hence "enat ?i < llength E" using enat a < llength E by(simp add: less_trans[where y="enat a"])
        moreover have "enat i < llength E'" using i
          by -(rule less_le_trans[OF _ lprefix_llength_le[OF prefix], simplified], simp)          
        from lprefix_lnthD[OF prefix i] lnth_i
        have "lnth (lmap snd E') i = NormalAction (ReadMem ad' al' v')" by simp
        hence "action_obs E ?i = NormalAction (ReadMem ad' al' v')" using enat i < llength E'
          by(simp add: E' action_obs_def lnth_lappend E'')
        ultimately have "T. P  ad'@al' : T  P  v' :≤ T" by(rule less.IH)
        hence "v'  vs_type_all P (ad', al')" by(simp add: vs_type_all.simps)
        thus "v'  w_values P (vs_type_all P) (list_of (ltake (enat i) ?EE'')) (ad', al')"
          by(rule w_values_mono[THEN subsetD])
      qed
        
      have "vs_conf P (vs_type_all P)" by simp
      with σ_σ'' wfx' ns
      have wfx'': "ts_ok (init_fin_lift wfx) (thr σ'') (shr σ'')" 
        and vs'': "vs_conf P (w_values P (vs_type_all P) (concat (map (λ(t, ta). tao) (list_of ?m_E''))))"
        by(rule h.if_RedT_non_speculative_invar[unfolded heap_independent h.mthr.if.RedT_def])+

      note red_w moreover
      from n_w obs_w obs_w' have "NormalAction (NewHeapElem ad CTn)  set ta_wo"
        unfolding in_set_conv_nth by auto
      moreover
      have ta_a_read: "NormalAction (ReadMem ad al v)  set ta_ao"
        using n_a obs_a unfolding in_set_conv_nth by blast
      from red_a have "T. P  ad@al : T"
      proof(cases)
        case (redT_normal x x' h')
        from wfx'' thr σ'' t_a = (x, no_wait_locks)
        have "init_fin_lift wfx t_a x (shr σ'')" by(rule ts_okD)
        with t_a  (x, shr σ'') -ta_a→i (x', h')
        show ?thesis using ta_a_read
          by(rule h.init_fin_red_read_typeable[unfolded heap_independent])
      next
        case redT_acquire thus ?thesis using n_a obs_a ta_a_read by auto
      qed
      hence "typeof_addr ad  None" by(auto elim: addr_loc_type_cases)
      ultimately have "typeof_addr ad = CTn" by(rule if_redT_NewHeapElem_typed)
      with written adal_w obs_w' show ?thesis
        by(cases al)(auto simp add: value_written.simps intro: addr_loc_type_intros h.addr_loc_default_conf[unfolded heap_independent])
    qed
  qed
qed

theorem 
  assumes wfx_start: "ts_ok wfx (thr (h.start_state f P C M vs)) h.start_heap" 
  and wfP: "wf_syscls P"
  and justified: "P  (E, ws) weakly_justified_by J"
  and J: "range (justifying_exec  J)  h.ℰ_start f P C M vs status"
  shows read_value_typeable_justifying:
    " 0 < n; enat a < llength (justifying_exec (J n));
      action_obs (justifying_exec (J n)) a = NormalAction (ReadMem ad al v) 
     T. P  ad@al : T  P  v :≤ T" 
  and read_value_typeable_justifed:
    " E  h.ℰ_start f P C M vs status; P  (E, ws) ;
       enat a < llength E; action_obs E a = NormalAction (ReadMem ad al v) 
     T. P  ad@al : T  P  v :≤ T"
proof -
  let ?E = "λn. justifying_exec (J n)"
    and  = "λn. action_translation (J n)"
    and ?C = "λn. committed (J n)"
    and ?ws = "λn. justifying_ws (J n)"
  let ?ℰ = "h.ℰ_start f P C M vs status"
    and ?start_obs = "lift_start_obs h.start_tid h.start_heap_obs"
  { fix a n
    assume "enat a < llength (justifying_exec (J n))"
      and "action_obs (justifying_exec (J n)) a = NormalAction (ReadMem ad al v)"
      and "n > 0"
    thus "T. P  ad@al : T  P  v :≤ T"
    proof(induction n arbitrary: a ad al v)
      case 0 thus ?case by simp
    next
      case (Suc n')
      define n where "n = Suc n'"
      with Suc have n: "0 < n" and a: "enat a < llength (?E n)"
        and a_obs: "action_obs (?E n) a = NormalAction (ReadMem ad al v)"
        by simp_all
      have wf_n: "P  (?E n, ?ws n) "
        using justified by(simp add: justification_well_formed_def)
      from J have E: "?E n  ?ℰ" 
        and E': "?E n'  ?ℰ" by auto
      from a a_obs wfx_start wfP E wf_n show ?case
      proof(rule hb_read_value_typeable[rotated -2])
        fix a' ad' al' v'
        assume a': "enat a' < llength (?E n)"
          and a'_obs: "action_obs (?E n) a' = NormalAction (ReadMem ad' al' v')"
          and nhb: "¬ P,?E n  ?ws n a' ≤hb a'"
        from a' have "a'  actions (?E n)" by(simp add: actions_def)
        hence read_a': "a'  read_actions (?E n)" using a'_obs ..
        with justified nhb have committed': " n a'   n' ` ?C n'"
          unfolding is_weakly_justified_by.simps n_def uncommitted_reads_see_hb_def by blast

        from justified have wfa_n: "wf_action_translation E (J n)"
          and wfa_n': "wf_action_translation E (J n')" by(simp_all add: wf_action_translations_def)
        hence inj_n: "inj_on ( n) (actions (?E n))"
          and inj_n': "inj_on ( n') (actions (?E n'))"
          by(blast dest: wf_action_translation_on_inj_onD)+
        from justified have C_n: "?C n  actions (?E n)"
          and C_n': "?C n'  actions (?E n')"
          and wf_n': "P  (?E n', ?ws n') "
          by(simp_all add: committed_subset_actions_def justification_well_formed_def)

        from justified have " n' ` ?C n'   n ` ?C n"
          unfolding n_def by(simp add: is_commit_sequence_def)
        with n_def committed' have " n a'   n ` ?C n" by auto
        with inj_n C_n have committed: "a'  ?C n"
          using a'  actions (?E n) by(auto dest: inj_onD)
        with justified read_a' have ws_committed: "ws ( n a')   n ` ?C n"
          by(rule weakly_justified_write_seen_hb_read_committed)

        from wf_n have ws_n: "is_write_seen P (?E n) (?ws n)" by(rule wf_exec_is_write_seenD)
        from is_write_seenD[OF this read_a' a'_obs]
        have ws_write: "?ws n a'  write_actions (?E n)"
          and adal: "(ad', al')  action_loc P (?E n) (?ws n a')"
          and written: "value_written P (?E n) (?ws n a') (ad', al') = v'" by simp_all

        define a'' where "a'' = inv_into (actions (?E n')) ( n') ( n a')"
        from C_n' n committed' have " n a'   n' ` actions (?E n')" by auto
        hence a'': " n' a'' =  n a'"
          and a''_action: "a''  actions (?E n')" using inj_n' committed' n
          by(simp_all add: a''_def f_inv_into_f inv_into_into)
        hence committed'': "a''  ?C n'" using committed' n inj_n' C_n' by(fastforce dest: inj_onD)

        from committed committed'' wfa_n wfa_n' a'' have "action_obs (?E n') a''  action_obs (?E n) a'"
          by(auto dest!: wf_action_translation_on_actionD intro: sim_action_trans sim_action_sym)
        with a'_obs committed'' C_n' have read_a'': "a''  read_actions (?E n')"
          by(auto intro: read_actions.intros)

        then obtain ad'' al'' v'' 
          where a''_obs: "action_obs (?E n') a'' = NormalAction (ReadMem ad'' al'' v'')" by cases

        from committed'' have "n' > 0" using justified 
          by(cases n')(simp_all add: is_commit_sequence_def)
        then obtain n'' where n'': "n' = Suc n''" by(cases n') simp_all

        from justified have wfa_n'': "wf_action_translation E (J n'')" by(simp add: wf_action_translations_def)
        hence inj_n'': "inj_on ( n'') (actions (?E n''))" by(blast dest: wf_action_translation_on_inj_onD)+
        from justified have C_n'': "?C n''  actions (?E n'')" by(simp add: committed_subset_actions_def)

        from justified committed' committed'' n_def read_a' read_a'' n
        have " n (?ws n (inv_into (actions (?E n)) ( n) ( n' a''))) = ws ( n' a'')"
          by(simp add: write_seen_committed_def)
        hence " n (?ws n a') = ws ( n a')" using inj_n a'  actions (?E n) by(simp add: a'')

        from ws_committed obtain w where w: "ws ( n a') =  n w" 
          and committed_w: "w  ?C n" by blast
        from committed_w C_n have "w  actions (?E n)" by blast
        hence w_def: "w = ?ws n a'" using  n (?ws n a') = ws ( n a') inj_n ws_write
          unfolding w by(auto dest: inj_onD)
        have committed_ws: "?ws n a'  ?C n" using committed_w by(simp add: w_def)

        with wfa_n have sim_ws: "action_obs (?E n) (?ws n a')  action_obs E ( n (?ws n a'))"
          by(blast dest: wf_action_translation_on_actionD)

        from wfa_n committed_ws have sim_ws: "action_obs (?E n) (?ws n a')  action_obs E ( n (?ws n a'))"
          by(blast dest: wf_action_translation_on_actionD)
        with adal have adal_E: "(ad', al')  action_loc P E ( n (?ws n a'))"
          by(simp add: action_loc_aux_sim_action)

        have "w  write_actions (?E n'). (ad', al')  action_loc P (?E n') w  value_written P (?E n') w (ad', al') = v'"
        proof(cases " n' a''   n'' ` ?C n''")
          case True
          then obtain a''' where a''': " n'' a''' =  n' a''" 
            and committed''': "a'''  ?C n''" by auto
          from committed''' C_n'' have a'''_action: "a'''  actions (?E n'')" by auto
          
          from committed'' committed''' wfa_n' wfa_n'' a''' have "action_obs (?E n'') a'''  action_obs (?E n') a''"
            by(auto dest!: wf_action_translation_on_actionD intro: sim_action_trans sim_action_sym)
          with read_a'' committed''' C_n'' have read_a''': "a'''  read_actions (?E n'')"
            by cases(auto intro: read_actions.intros)
          
          hence " n' (?ws n' (inv_into (actions (?E n')) ( n') ( n'' a'''))) = ws ( n'' a''')"
            using justified committed'''
            unfolding is_weakly_justified_by.simps n'' Let_def write_seen_committed_def by blast
          also have "inv_into (actions (?E n')) ( n') ( n'' a''') = a''"
            using a''' inj_n' a''_action by(simp)
          also note a''' also note a''
          finally have φ_n': " n' (?ws n' a'') = ws ( n a')" .
          then have "ws ( n a') =  n' (?ws n' a'')" ..
          with  n (?ws n a') = ws ( n a')[symmetric]
          have eq_ws: " n' (?ws n' a'') =  n (?ws n a')" by simp

          from wf_n'[THEN wf_exec_is_write_seenD, THEN is_write_seenD, OF read_a'' a''_obs]
          have ws_write': "?ws n' a''  write_actions (?E n')" by simp

          from justified read_a'' committed''
          have "ws ( n' a'')   n' ` ?C n'" by(rule weakly_justified_write_seen_hb_read_committed)
          then obtain w' where w': "ws ( n' a'') =  n' w'"
            and committed_w': "w'  ?C n'" by blast
          from committed_w' C_n' have "w'  actions (?E n')" by blast
          hence w'_def: "w' = ?ws n' a''" using φ_n' inj_n' ws_write'
            unfolding w' a''[symmetric] by(auto dest: inj_onD)
          with committed_w' have committed_ws'': "?ws n' a''  committed (J n')" by simp
          with committed_ws wfa_n wfa_n' eq_ws
          have "action_obs (?E n') (?ws n' a'')  action_obs (?E n) (?ws n a')"
            by(auto dest!: wf_action_translation_on_actionD intro: sim_action_trans sim_action_sym)
          hence adal_eq: "action_loc P (?E n') (?ws n' a'') = action_loc P (?E n) (?ws n a')"
            by(simp add: action_loc_aux_sim_action)
          with adal have adal': "(ad', al')  action_loc P (?E n') (?ws n' a'')" by(simp add: action_loc_aux_sim_action)
          
          from committed_ws'' have "?ws n' a''  actions (?E n')" using C_n' by blast
          with ws_write action_obs (?E n') (?ws n' a'')  action_obs (?E n) (?ws n a') 
          have ws_write'': "?ws n' a''  write_actions (?E n')" 
            by(cases)(auto intro: write_actions.intros simp add: sim_action_is_write_action_eq)
          from wfa_n' committed_ws''
          have sim_ws': "action_obs (?E n') (?ws n' a'')  action_obs E ( n' (?ws n' a''))"
            by(blast dest: wf_action_translation_on_actionD)
          with adal' have adal'_E: "(ad', al')  action_loc P E ( n' (?ws n' a''))"
            by(simp add: action_loc_aux_sim_action)
          
          from justified committed_ws ws_write adal_E
          have "value_written P (?E n) (?ws n a') (ad', al') = value_written P E ( n (?ws n a')) (ad', al')"
            unfolding is_weakly_justified_by.simps Let_def value_written_committed_def by blast
          also note eq_ws[symmetric]
          also from justified committed_ws'' ws_write'' adal'_E
          have "value_written P E ( n' (?ws n' a'')) (ad', al') = value_written P (?E n') (?ws n' a'') (ad', al')"
            unfolding is_weakly_justified_by.simps Let_def value_written_committed_def by(blast dest: sym)
          finally show ?thesis using written ws_write'' adal' by auto
        next
          case False
          with justified read_a'' committed''
          have "ws ( n' a'')   n'' ` ?C n''"
            unfolding is_weakly_justified_by.simps Let_def n'' committed_reads_see_committed_writes_weak_def by blast
          with a'' obtain w where w: " n'' w = ws ( n a')"
            and committed_w: "w  ?C n''" by auto
          from justified have " n'' ` ?C n''   n' ` ?C n'" by(simp add: is_commit_sequence_def n'')
          with committed_w w[symmetric] have "ws ( n a')   n' ` ?C n'" by(auto)
          then obtain w' where w': "ws ( n a') =  n' w'" and committed_w': "w'  ?C n'" by blast
          from wfa_n' committed_w' have "action_obs (?E n') w'  action_obs E ( n' w')"
            by(blast dest: wf_action_translation_on_actionD)
          from this[folded w', folded  n (?ws n a') = ws ( n a')] sim_ws[symmetric]
          have sim_w': "action_obs (?E n') w'  action_obs (?E n) (?ws n a')" by(rule sim_action_trans)
          with ws_write committed_w' C_n' have write_w': "w'  write_actions (?E n')"
            by(cases)(auto intro!: write_actions.intros simp add: sim_action_is_write_action_eq)
          hence "value_written P (?E n') w' (ad', al') = value_written P E ( n' w') (ad', al')"
            using adal_E committed_w' justified
            unfolding  n (?ws n a') = ws ( n a') w' is_weakly_justified_by.simps Let_def value_written_committed_def by blast
          also note w'[symmetric] 
          also note  n (?ws n a') = ws ( n a')[symmetric]
          also have "value_written P E ( n (?ws n a')) (ad', al') = value_written P (?E n) (?ws n a') (ad', al')"
            using justified committed_ws ws_write adal_E 
            unfolding is_weakly_justified_by.simps Let_def value_written_committed_def by(blast dest: sym)
          also have "(ad', al')  action_loc P (?E n') w'" using sim_w' adal by(simp add: action_loc_aux_sim_action)
          ultimately show ?thesis using written write_w' by auto
        qed
        then obtain w where w: "w  write_actions (?E n')"
          and adal: "(ad', al')  action_loc P (?E n') w"
          and written: "value_written P (?E n') w (ad', al') = v'" by blast
        from w have w_len: "enat w < llength (?E n')"
          by(cases)(simp add: actions_def)

        let ?EE'' = "lmap snd (ltake (enat w) (?E n'))"
        have "non_speculative P (vs_type_all P) ?EE''"
        proof(rule non_speculative_nthI)
          fix i ad al v
          assume i: "enat i < llength ?EE''"
            and i_nth: "lnth ?EE'' i = NormalAction (ReadMem ad al v)"
            and ns: "non_speculative P (vs_type_all P) (ltake (enat i) ?EE'')"

          from i w_len have "i < w" by(simp add: min_def not_le split: if_split_asm)
          with w_len have "enat i < llength (?E n')" by(simp add: less_trans[where y="enat w"])
          moreover
          from i_nth i i < w w_len
          have "action_obs (?E n') i = NormalAction (ReadMem ad al v)"
            by(simp add: action_obs_def ac_simps less_trans[where y="enat w"] lnth_ltake)
          moreover from n'' have "0 < n'" by simp
          ultimately have "T. P  ad@al : T  P  v :≤ T" by(rule Suc.IH)
          hence "v  vs_type_all P (ad, al)" by(simp add: vs_type_all.simps)
          thus "v  w_values P (vs_type_all P) (list_of (ltake (enat i) ?EE'')) (ad, al)"
            by(rule w_values_mono[THEN subsetD])
        qed
        with wfx_start wfP E' w adal
        show "T. P  ad'@al' : T  P  v' :≤ T"
          unfolding written[symmetric] by(rule non_speculative_written_value_typeable)
      qed
    qed
  }
  note justifying = this

  assume a: "enat a < llength E"
    and read: "action_obs E a = NormalAction (ReadMem ad al v)"
    and E: "E  h.ℰ_start f P C M vs status"
    and wf: "P  (E, ws) "
  from a have action: "a  actions E" by(auto simp add: actions_def action_obs_def)
  with justified obtain n a' where a': "a =  n a'"
    and committed': "a'  ?C n" by(auto simp add: is_commit_sequence_def)
  from justified have C_n: "?C n  actions (?E n)"
    and C_Sn: "?C (Suc n)  actions (?E (Suc n))"
    and wf_tr: "wf_action_translation E (J n)" 
    and wf_tr': "wf_action_translation E (J (Suc n))"
    by(auto simp add: committed_subset_actions_def wf_action_translations_def)
  from C_n committed' have action': "a'  actions (?E n)" by blast
  from wf_tr committed' a'
  have "action_tid E a = action_tid (?E n) a'" "action_obs E a  action_obs (?E n) a'"
    by(auto simp add: wf_action_translation_on_def intro: sim_action_sym)
  with read obtain v'
    where "action_obs (?E n) a' = NormalAction (ReadMem ad al v')"
    by(clarsimp simp add: action_obs_def)
  with action' have read': "a'  read_actions (?E n)" ..

  from justified have " n ` ?C n   (Suc n) ` ?C (Suc n)"
    by(simp add: is_commit_sequence_def)
  with committed' a' have "a  " by auto
  then obtain a'' where a'': "a =  (Suc n) a''"
    and committed'': "a''  ?C (Suc n)" by auto
  from committed'' C_Sn have action'': "a''  actions (?E (Suc n))" by blast
  
  with wf_tr' have "a'' = inv_into (actions (?E (Suc n))) ( (Suc n)) a"
    by(simp add: a'' wf_action_translation_on_def)
  with justified read' committed' a' have ws_a: "ws a =  (Suc n) (?ws (Suc n) a'')"
    by(simp add: write_seen_committed_def)

  from wf_tr' committed'' a''
  have "action_tid E a = action_tid (?E (Suc n)) a''"
    and "action_obs E a  action_obs (?E (Suc n)) a''"
    by(auto simp add: wf_action_translation_on_def intro: sim_action_sym)
  with read obtain v''
    where a_obs'': "action_obs (?E (Suc n)) a'' = NormalAction (ReadMem ad al v'')"
    by(clarsimp simp add: action_obs_def)
  with action'' have read'': "a''  read_actions (?E (Suc n))"
    by(auto intro: read_actions.intros simp add: action_obs_def)

  have "a  read_actions E" "action_obs E a = NormalAction (ReadMem ad al v)"
    using action read by(auto intro: read_actions.intros simp add: action_obs_def read)
  from is_write_seenD[OF wf_exec_is_write_seenD[OF wf] this]
  have v_eq: "v = value_written P E (ws a) (ad, al)" 
    and adal: "(ad, al)  action_loc P E (ws a)" by simp_all

  from justified have "P  (?E (Suc n), ?ws (Suc n)) " by(simp add: justification_well_formed_def)
  from is_write_seenD[OF wf_exec_is_write_seenD[OF this] read'' a_obs'']
  have write'': "?ws (Suc n) a''  write_actions (?E (Suc n))" 
    and written'': "value_written P (?E (Suc n)) (?ws (Suc n) a'') (ad, al) = v''" 
    by simp_all

  from justified read'' committed'' 
  have "ws ( (Suc n) a'')   (Suc n) ` ?C (Suc n)"
    by(rule weakly_justified_write_seen_hb_read_committed)
  then obtain w where w: "ws ( (Suc n) a'') =  (Suc n) w"
    and committed_w: "w  ?C (Suc n)" by blast
  with C_Sn have "w  actions (?E (Suc n))" by blast
  moreover have "ws ( (Suc n) a'') =  (Suc n) (?ws (Suc n) a'')"
    using ws_a a'' by simp
  ultimately have w_def: "w = ?ws (Suc n) a''"
    using wf_action_translation_on_inj_onD[OF wf_tr'] write''
    unfolding w by(auto dest: inj_onD)
  with committed_w have "?ws (Suc n) a''  ?C (Suc n)" by simp
  hence "value_written P E (ws a) (ad, al) = value_written P (?E (Suc n)) (?ws (Suc n) a'') (ad, al)"
    using adal justified write'' by(simp add: value_written_committed_def ws_a)
  with v_eq written'' have "v = v''" by simp

  from read'' have "enat a'' < llength (?E (Suc n))" by(cases)(simp add: actions_def)
  thus "T. P  ad@al : T  P  v :≤ T"
    by(rule justifying)(simp_all add: a_obs'' v = v'')
qed

corollary weakly_legal_read_value_typeable:
  assumes wfx_start: "ts_ok wfx (thr (h.start_state f P C M vs)) h.start_heap" 
  and wfP: "wf_syscls P"
  and legal: "weakly_legal_execution P (h.ℰ_start f P C M vs status) (E, ws)"
  and a: "enat a < llength E"
  and read: "action_obs E a = NormalAction (ReadMem ad al v)"
  shows "T. P  ad@al : T  P  v :≤ T"
proof -
  from legal obtain J 
    where "P  (E, ws) weakly_justified_by J"
    and "range (justifying_exec  J)  h.ℰ_start f P C M vs status"
    and "E  h.ℰ_start f P C M vs status"
    and "P  (E, ws) " by(rule legal_executionE)
  with wfx_start wfP show ?thesis using a read by(rule read_value_typeable_justifed)
qed

corollary legal_read_value_typeable:
  " ts_ok wfx (thr (h.start_state f P C M vs)) h.start_heap; wf_syscls P;
     legal_execution P (h.ℰ_start f P C M vs status) (E, ws);
     enat a < llength E; action_obs E a = NormalAction (ReadMem ad al v) 
   T. P  ad@al : T  P  v :≤ T"
by(erule (1) weakly_legal_read_value_typeable)(rule legal_imp_weakly_legal_execution)

end

end