Theory JMM_Framework

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

section ‹Combination of locales for heap operations and interleaving›

theory JMM_Framework
imports
  JMM_Heap
  "../Framework/FWInitFinLift"
  "../Common/WellForm"
begin

lemma enat_plus_eq_enat_conv: ― ‹Move to Extended\_Nat›
  "enat m + n = enat k ⟷ k ≥ m ∧ n = enat (k - m)"
by(cases n) auto

declare convert_new_thread_action_id [simp]

context heap begin

lemma init_fin_lift_state_start_state:
  "init_fin_lift_state s (start_state f P C M vs) = start_state (λC M Ts T meth vs. (s, f C M Ts T meth vs)) P C M vs"
by(simp add: start_state_def init_fin_lift_state_def split_beta fun_eq_iff)

lemma non_speculative_start_heap_obs:
  "non_speculative P vs  (llist_of (map snd (lift_start_obs start_tid start_heap_obs)))"
apply(rule non_speculative_nthI)
using start_heap_obs_not_Read
by(clarsimp simp add: lift_start_obs_def lnth_LCons o_def eSuc_enat[symmetric] in_set_conv_nth split: nat.split_asm)

lemma ta_seq_consist_start_heap_obs:
  "ta_seq_consist P Map.empty (llist_of (map snd (lift_start_obs start_tid start_heap_obs)))"
using start_heap_obs_not_Read
by(auto intro: ta_seq_consist_nthI simp add: lift_start_obs_def o_def lnth_LCons in_set_conv_nth split: nat.split_asm)

end

context allocated_heap begin

lemma w_addrs_lift_start_heap_obs:
  "w_addrs (w_values P vs (map snd (lift_start_obs start_tid start_heap_obs))) ⊆ w_addrs vs"
by(simp add: lift_start_obs_def o_def w_addrs_start_heap_obs)

end

context heap begin

lemma w_values_start_heap_obs_typeable:
  assumes wf: "wf_syscls P"
  and mrws: "v ∈ w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)) (ad, al)"
  shows "∃T. P,start_heap ⊢ ad@al : T ∧ P,start_heap ⊢ v :≤ T"
proof -
  from in_w_valuesD[OF mrws]
  obtain obs' wa obs'' 
    where eq: "map snd (lift_start_obs start_tid start_heap_obs) = obs' @ wa # obs''"
    and "is_write_action wa"
    and adal: "(ad, al) ∈ action_loc_aux P wa"
    and vwa: "value_written_aux P wa al = v"
    by blast
  from ‹is_write_action wa› show ?thesis
  proof cases
    case (WriteMem ad' al' v')
    with vwa adal eq have "WriteMem ad al v ∈ set start_heap_obs"
      by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
    thus ?thesis by(rule start_heap_write_typeable)
  next
    case (NewHeapElem ad' hT)
    with vwa adal eq have "NewHeapElem ad hT ∈ set start_heap_obs"
      by(auto simp add: map_eq_append_conv Cons_eq_append_conv lift_start_obs_def)
    hence "typeof_addr start_heap ad = ⌊hT⌋"
      by(rule NewHeapElem_start_heap_obsD[OF wf])
    thus ?thesis using adal vwa NewHeapElem
      apply(cases hT)
      apply(auto intro!: addr_loc_type.intros dest: has_field_decl_above)
      apply(frule has_field_decl_above)
      apply(auto intro!: addr_loc_type.intros dest: has_field_decl_above)
      done
  qed
qed

lemma start_state_vs_conf:
  "wf_syscls P ⟹ vs_conf P start_heap (w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs)))"
by(rule vs_confI)(rule w_values_start_heap_obs_typeable)

end


subsection ‹JMM traces for Jinja semantics›

context multithreaded_base begin

inductive_set ℰ :: "('l,'t,'x,'m,'w) state ⇒ ('t × 'o) llist set"
  for σ :: "('l,'t,'x,'m,'w) state"
where
  "mthr.Runs σ E'
  ⟹ lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') ∈ ℰ σ"

lemma actions_ℰE_aux:
  fixes σ E'
  defines "E == lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
  assumes mthr: "mthr.Runs σ E'"
  and a: "enat a < llength E"
  obtains m n t ta
  where "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
  and "n < length ⦃ta⦄⇘o⇙" and "enat m < llength E'"
  and "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
  and "lnth E' m = (t, ta)"
proof -
  from lnth_lconcat_conv[OF a[unfolded E_def], folded E_def]
  obtain m n
    where "lnth E a = lnth (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') m) n"
    and "enat n < llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') m)"
    and "enat m < llength (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
    and "enat a = (∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat n"
    by blast
  moreover
  obtain t ta where "lnth E' m = (t, ta)" by(cases "lnth E' m")
  ultimately have E_a: "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
    and n: "n < length ⦃ta⦄⇘o⇙"
    and m: "enat m < llength E'"
    and a: "enat a = (∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat n"
    by(simp_all)
  note a
  also have "(∑i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) = 
            sum (enat ∘ (λi. length ⦃snd (lnth E' i)⦄⇘o⇙)) {..<m}"
    using m by(simp add: less_trans[where y="enat m"] split_beta)
  also have "… = enat (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
    by(subst sum_comp_morphism)(simp_all add: zero_enat_def)
  finally have a: "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n" by simp
  with E_a n m show thesis using ‹lnth E' m = (t, ta)› by(rule that)
qed

lemma actions_ℰE:
  assumes E: "E ∈ ℰ σ"
  and a: "enat a < llength E"
  obtains E' m n t ta
  where "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
  and "mthr.Runs σ E'"
  and "lnth E a = (t, ⦃ta⦄⇘o⇙ ! n)"
  and "n < length ⦃ta⦄⇘o⇙" and "enat m < llength E'"
  and "a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
  and "lnth E' m = (t, ta)"
proof -
  from E obtain E' ws
    where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
    and "mthr.Runs σ E'" by(rule ℰ.cases) blast
  from ‹mthr.Runs σ E'› a[unfolded E]
  show ?thesis
    by(rule actions_ℰE_aux)(fold E, rule that[OF E ‹mthr.Runs σ E'›])
qed

end

context τmultithreaded_wf begin

text ‹Alternative characterisation for @{term "ℰ"}›
lemma ℰ_conv_Runs:
  "ℰ σ = lconcat ` lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ` llist_of_tllist ` {E. mthr.τRuns σ E}"
  (is "?lhs = ?rhs")
proof(intro equalityI subsetI)
  fix E
  assume "E ∈ ?rhs"
  then obtain E' where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of_tllist E'))"
    and τRuns: "mthr.τRuns σ E'" by(blast)
  obtain E'' where E': "E' = tmap (λ(tls, s', tl, s''). tl) (case_sum (λ(tls, s'). ⌊s'⌋) Map.empty) E''"
    and τRuns': "mthr.τRuns_table2 σ E''"
    using τRuns by(rule mthr.τRuns_into_τRuns_table2)
  have "mthr.Runs σ (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) 
                                      (LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil)))"
    (is "mthr.Runs _ ?E'''")
    using τRuns' by(rule mthr.τRuns_table2_into_Runs)
  moreover 
  let ?tail = "λE''. case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls"
  {
    have "E = lconcat (lfilter (λxs. ¬ lnull xs) (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of_tllist E')))"
      unfolding E by(simp add: lconcat_lfilter_neq_LNil)
    also have "… = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E''))))"
      by(simp add: E' lfilter_lmap llist.map_comp o_def split_def)
    also
    from ‹mthr.τRuns_table2 σ E''›
    have "lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')) = 
          lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (?tail E'') LNil)))"
      (is "?lhs σ E'' = ?rhs σ E''")
    proof(coinduction arbitrary: σ E'' rule: llist.coinduct_strong)
      case (Eq_llist σ E'')
      have ?lnull
        by(cases "lfinite (llist_of_tllist E'')")(fastforce split: sum.split_asm simp add: split_beta lset_lconcat_lfinite lappend_inf mthr.silent_move2_def dest: mthr.τRuns_table2_silentsD[OF Eq_llist] mthr.τRuns_table2_terminal_silentsD[OF Eq_llist] mthr.τRuns_table2_terminal_inf_stepD[OF Eq_llist] mτmove_silentD inf_step_silentD silent_moves2_silentD split: sum.split_asm)+
      moreover
      have ?LCons
      proof(intro impI conjI)
        assume lhs': "¬ lnull (lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')))"
          (is "¬ lnull ?lhs'")
          and "¬ lnull (lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil))))"
          (is "¬ lnull ?rhs'")

        note τRuns' = ‹mthr.τRuns_table2 σ E''›
        from lhs' obtain tl tls' where "?lhs σ E'' = LCons tl tls'"
          by(auto simp only: not_lnull_conv)
        then obtain tls s' s'' tlsstlss'
          where tls': "tls' = lmap (λ(tls, s', tta, s''). tta) tlsstlss'"
          and filter: "lfilter (λ(tls, s', (t, ta), s''). obs_a ta ≠ []) (llist_of_tllist E'') = LCons (tls, s', tl, s'') tlsstlss'"
          using lhs' by(fastforce simp add: lmap_eq_LCons_conv)
        from lfilter_eq_LConsD[OF filter]
        obtain us vs where eq: "llist_of_tllist E'' = lappend us (LCons (tls, s', tl, s'') vs)"
          and fin: "lfinite us"
          and empty: "∀(tls, s', (t, ta), s'')∈lset us. obs_a ta = []"
          and neq_empty: "obs_a (snd tl) ≠ []"
          and tlsstlss': "tlsstlss' = lfilter (λ(tls, s', (t, ta), s''). obs_a ta ≠ []) vs"
          by(auto simp add: split_beta)
        from eq obtain E''' where E'': "E'' = lappendt us E'''" 
          and eq': "llist_of_tllist E''' = LCons (tls, s', tl, s'') vs"
          and terminal: "terminal E''' = terminal E''"
          unfolding llist_of_tllist_eq_lappend_conv by auto
        from τRuns' fin E'' obtain σ' where τRuns'': "mthr.τRuns_table2 σ' E'''"
          by(auto dest: mthr.τRuns_table2_lappendtD)
        then obtain σ'' E'''' where "mthr.τRuns_table2 σ'' E''''" "E''' = TCons (tls, s', tl, s'') E''''"
          using eq' by cases auto
        moreover from τRuns' E'' fin
        have "∀(tls, s, tl, s')∈lset us. ∀(t, ta)∈set tls. ta = ε"
          by(fastforce dest: mthr.τRuns_table2_silentsD mτmove_silentD simp add: mthr.silent_move2_def)
        hence "lfilter (λ(t, ta). obs_a ta ≠ []) (lconcat (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) us)) = LNil"
          using empty by(auto simp add: lfilter_empty_conv lset_lconcat_lfinite split_beta)
        moreover from τRuns'' eq' have "snd ` set tls ⊆ {ε}"
          by(cases)(fastforce dest: silent_moves2_silentD)+
        hence "[(t, ta)←tls . obs_a ta ≠ []] = []"
          by(auto simp add: filter_empty_conv split_beta)
        ultimately 
        show "lhd ?lhs' = lhd ?rhs'"
          and "(∃σ E''. ltl ?lhs' = lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). ⦃ta⦄⇘o⇙ ≠ []) (llist_of_tllist E'')) ∧
           ltl ?rhs' = lfilter (λ(t, ta). ⦃ta⦄⇘o⇙ ≠ []) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (case terminal E'' of Inl (tls, s') ⇒ llist_of tls | Inr tls ⇒ tls) LNil))) ∧
           τtrsys.τRuns_table2 redT mτmove σ E'') ∨
          ltl ?lhs' = ltl ?rhs'"
          using lhs' E'' fin tls' tlsstlss' filter eq' neq_empty
          by(auto simp add: lmap_lappend_distrib lappend_assoc split_beta filter_empty_conv simp del: split_paired_Ex)
      qed
      ultimately show ?case ..
    qed
    also have "lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) … = lfilter (λobs. ¬ lnull obs) (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) (lconcat (lappend (lmap (λ(tls, s, tl, s'). llist_of (tls @ [tl])) (llist_of_tllist E'')) (LCons (?tail E'') LNil))))"
      unfolding lfilter_lmap by(simp add: o_def split_def llist_of_eq_LNil_conv)
    finally have "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?E''')"
      by(simp add: lconcat_lfilter_neq_LNil) }
  ultimately show "E ∈ ?lhs" by(blast intro: ℰ.intros)
next
  fix E
  assume "E ∈ ?lhs"
  then obtain E' where E: "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) E')"
    and Runs: "mthr.Runs σ E'" by(blast elim: ℰ.cases)
  from Runs obtain E'' where E': "E' = lmap (λ(s, tl, s'). tl) E''"
    and Runs': "mthr.Runs_table σ E''" by(rule mthr.Runs_into_Runs_table)
  have "mthr.τRuns σ (tmap (λ(s, tl, s'). tl) id (tfilter None (λ(s, tl, s'). ¬ mτmove s tl s') (tllist_of_llist (Some (llast (LCons σ (lmap (λ(s, tl, s'). s') E'')))) E'')))"
    (is "mthr.τRuns _ ?E'''")
    using Runs' by(rule mthr.Runs_table_into_τRuns)
  moreover
  have "(λ(s, (t, ta), s'). obs_a ta ≠ []) = (λ(s, (t, ta), s'). obs_a ta ≠ [] ∧ ¬ mτmove s (t, ta) s')"
    by(rule ext)(auto dest: mτmove_silentD)
  hence "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) (obs_a ta))) (llist_of_tllist ?E'''))"
    unfolding E E'
    by(subst (1 2) lconcat_lfilter_neq_LNil[symmetric])(simp add: lfilter_lmap lfilter_lfilter o_def split_def)
  ultimately show "E ∈ ?rhs" by(blast)
qed

end

text ‹Running threads have been started before›

definition Status_no_wait_locks :: "('l,'t,status × 'x) thread_info ⇒ bool"
where
  "Status_no_wait_locks ts ⟷ 
  (∀t status x ln. ts t = ⌊((status, x), ln)⌋ ⟶ status ≠ Running ⟶ ln = no_wait_locks)"

lemma Status_no_wait_locks_PreStartD:
  "⋀ln. ⟦ Status_no_wait_locks ts; ts t = ⌊((PreStart, x), ln)⌋ ⟧ ⟹ ln = no_wait_locks"
unfolding Status_no_wait_locks_def by blast

lemma Status_no_wait_locks_FinishedD:
  "⋀ln. ⟦ Status_no_wait_locks ts; ts t = ⌊((Finished, x), ln)⌋ ⟧ ⟹ ln = no_wait_locks"
unfolding Status_no_wait_locks_def by blast

lemma Status_no_wait_locksI:
  "(⋀t status x ln. ⟦ ts t = ⌊((status, x), ln)⌋; status = PreStart ∨ status = Finished ⟧ ⟹ ln = no_wait_locks)
  ⟹ Status_no_wait_locks ts"
unfolding Status_no_wait_locks_def 
apply clarify
apply(case_tac status)
apply auto
done

context heap_base begin

lemma Status_no_wait_locks_start_state:
  "Status_no_wait_locks (thr (init_fin_lift_state status (start_state f P C M vs)))"
by(clarsimp simp add: Status_no_wait_locks_def init_fin_lift_state_def start_state_def split_beta)

end

context multithreaded_base begin

lemma init_fin_preserve_Status_no_wait_locks:
  assumes ok: "Status_no_wait_locks (thr s)"
  and redT: "multithreaded_base.redT init_fin_final init_fin (map NormalAction ∘ convert_RA) s tta s'"
  shows "Status_no_wait_locks (thr s')"
using redT
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names redT_normal redT_acquire])
  case redT_acquire
  with ok show ?thesis
    by(auto intro!: Status_no_wait_locksI dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD split: if_split_asm)
next
  case redT_normal
  show ?thesis
  proof(rule Status_no_wait_locksI)
    fix t' status' x' ln'
    assume tst': "thr s' t' = ⌊((status', x'), ln')⌋"
      and status: "status' = PreStart ∨ status' = Finished"
    show "ln' = no_wait_locks"
    proof(cases "thr s t'")
      case None
      with redT_normal tst' show ?thesis
        by(fastforce elim!: init_fin.cases dest: redT_updTs_new_thread simp add: final_thread.actions_ok_iff split: if_split_asm)
    next
      case (Some sxln)
      obtain status'' x'' ln'' 
        where [simp]: "sxln = ((status'', x''), ln'')" by(cases sxln) auto
      show ?thesis
      proof(cases "fst tta = t'")
        case True
        with redT_normal tst' status show ?thesis by(auto simp add: expand_finfun_eq fun_eq_iff)
      next
        case False
        with tst' redT_normal Some status have "status'' = status'" "ln'' = ln'" 
          by(force dest: redT_updTs_Some simp add: final_thread.actions_ok_iff)+
        with ok Some status show ?thesis
          by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
      qed
    qed
  qed
qed

lemma init_fin_Running_InitialThreadAction:
  assumes redT: "multithreaded_base.redT init_fin_final init_fin (map NormalAction ∘ convert_RA) s tta s'"
  and not_running: "⋀x ln. thr s t ≠ ⌊((Running, x), ln)⌋"
  and running: "thr s' t = ⌊((Running, x'), ln')⌋"
  shows "tta = (t, ⦃InitialThreadAction⦄)"
using redT
proof(cases rule: multithreaded_base.redT.cases[consumes 1, case_names redT_normal redT_acquire])
  case redT_acquire
  with running not_running show ?thesis by(auto split: if_split_asm)
next
  case redT_normal
  show ?thesis
  proof(cases "thr s t")
    case None
    with redT_normal running not_running show ?thesis
      by(fastforce simp add: final_thread.actions_ok_iff elim: init_fin.cases dest: redT_updTs_new_thread split: if_split_asm)
  next
    case (Some a)
    with redT_normal running not_running show ?thesis
      apply(cases a)
      apply(auto simp add: final_thread.actions_ok_iff split: if_split_asm elim: init_fin.cases)
      apply((drule (1) redT_updTs_Some)?, fastforce)+
      done
  qed
qed

end

context if_multithreaded begin

lemma init_fin_Trsys_preserve_Status_no_wait_locks:
  assumes ok: "Status_no_wait_locks (thr s)"
  and Trsys: "if.mthr.Trsys s ttas s'"
  shows "Status_no_wait_locks (thr s')"
using Trsys ok
by(induct)(blast dest: init_fin_preserve_Status_no_wait_locks)+

lemma init_fin_Trsys_Running_InitialThreadAction:
  assumes redT: "if.mthr.Trsys s ttas s'"
  and not_running: "⋀x ln. thr s t ≠ ⌊((Running, x), ln)⌋"
  and running: "thr s' t = ⌊((Running, x'), ln')⌋"
  shows "(t, ⦃InitialThreadAction⦄) ∈ set ttas"
using redT not_running running
proof(induct arbitrary: x' ln')
  case rtrancl3p_refl thus ?case by(fastforce)
next
  case (rtrancl3p_step s ttas s' tta s'') thus ?case
    by(cases "∃x ln. thr s' t = ⌊((Running, x), ln)⌋")(fastforce dest: init_fin_Running_InitialThreadAction)+
qed

end

locale heap_multithreaded_base =
  heap_base
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write 
  +
  mthr: multithreaded_base final r convert_RA
  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 :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool" 
  and final :: "'x ⇒ bool"
  and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80) 
  and convert_RA :: "'addr released_locks ⇒ ('addr, 'thread_id) obs_event list"

sublocale heap_multithreaded_base < mthr: if_multithreaded_base final r convert_RA
.

context heap_multithreaded_base begin

abbreviation ℰ_start ::
  "(cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'md ⇒ 'addr val list ⇒ 'x) 
  ⇒ 'md prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ status 
  ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) llist set"
where
  "ℰ_start f P C M vs status ≡ 
  lappend (llist_of (lift_start_obs start_tid start_heap_obs)) ` 
  mthr.if.ℰ (init_fin_lift_state status (start_state f P C M vs))"

end

locale heap_multithreaded =
  heap_multithreaded_base 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    final r convert_RA
  +
  heap
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write 
    P 
  + 
  mthr: multithreaded final r convert_RA

  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 :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool" 
  and final :: "'x ⇒ bool"
  and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80) 
  and convert_RA :: "'addr released_locks ⇒ ('addr, 'thread_id) obs_event list" 
  and P :: "'md prog"

sublocale heap_multithreaded < mthr: if_multithreaded final r convert_RA
by(unfold_locales)

sublocale heap_multithreaded < "if": jmm_multithreaded
  mthr.init_fin_final mthr.init_fin "map NormalAction ∘ convert_RA" P
.

context heap_multithreaded begin

lemma thread_start_actions_ok_init_fin_RedT:
  assumes Red: "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas s'"
           (is "mthr.if.RedT ?start_state _ _")
  shows "thread_start_actions_ok (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas)))"
   (is "thread_start_actions_ok (llist_of (?obs_prefix @ ?E'))")
proof(rule thread_start_actions_okI)
  let ?E = "llist_of (?obs_prefix @ ?E')"
  fix a
  assume a: "a ∈ actions ?E"
    and new: "¬ is_new_action (action_obs ?E a)"
  show "∃i ≤ a. action_obs ?E i = InitialThreadAction ∧ action_tid ?E i = action_tid ?E a"
  proof(cases "action_tid ?E a = start_tid")
    case True thus ?thesis
      by(auto simp add: lift_start_obs_def action_tid_def action_obs_def)
  next
    case False
    let ?a = "a - length ?obs_prefix"

    from False have a_len: "a ≥ length ?obs_prefix"
      by(rule contrapos_np)(auto simp add: lift_start_obs_def action_tid_def lnth_LCons nth_append split: nat.split)
    hence [simp]: "action_tid ?E a = action_tid (llist_of ?E') ?a" "action_obs ?E a = action_obs (llist_of ?E') ?a"
      by(simp_all add: action_tid_def nth_append action_obs_def)

    from False have not_running: "⋀x ln. thr ?start_state (action_tid (llist_of ?E') ?a) ≠ ⌊((Running, x), ln)⌋"
      by(auto simp add: start_state_def split_beta init_fin_lift_state_def split: if_split_asm)
    
    from a a_len have "?a < length ?E'" by(simp add: actions_def)
    from nth_concat_conv[OF this]
    obtain m n where E'_a: "?E' ! ?a = (λ(t, ta). (t, ⦃ta⦄⇘o⇙ ! n)) (ttas ! m)"
      and n: "n < length ⦃snd (ttas ! m)⦄⇘o⇙"
      and m: "m < length ttas"
      and a_conv: "?a = (∑i<m. length (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas ! i)) + n"
      by(clarsimp simp add: split_def)

    from Red obtain s'' s''' where Red1: "mthr.if.RedT ?start_state (take m ttas) s''"
      and red: "mthr.if.redT s'' (ttas ! m) s'''"
      and Red2: "mthr.if.RedT s''' (drop (Suc m) ttas) s'"
      unfolding mthr.if.RedT_def
      by(subst (asm) (4) id_take_nth_drop[OF m])(blast elim: rtrancl3p_appendE rtrancl3p_converseE)

    from E'_a m n have [simp]: "action_tid (llist_of ?E') ?a = fst (ttas ! m)"
      by(simp add: action_tid_def split_def)
    
    from red obtain status x ln where tst: "thr s'' (fst (ttas ! m)) = ⌊((status, x), ln)⌋" by cases auto
    show ?thesis
    proof(cases "status = PreStart ∨ status = Finished")
      case True
      from Red1 have "Status_no_wait_locks (thr s'')"
        unfolding mthr.if.RedT_def
        by(rule mthr.init_fin_Trsys_preserve_Status_no_wait_locks[OF Status_no_wait_locks_start_state])
      with True tst have "ln = no_wait_locks"
        by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
      with red tst True have "⦃snd (ttas ! m)⦄⇘o⇙ = [InitialThreadAction]" by(cases) auto
      hence "action_obs ?E a = InitialThreadAction" using a_conv n a_len E'_a
        by(simp add: action_obs_def nth_append split_beta)
      thus ?thesis by(auto)
    next
      case False
      hence "status = Running" by(cases status) auto
      with tst mthr.init_fin_Trsys_Running_InitialThreadAction[OF Red1[unfolded mthr.if.RedT_def] not_running]
      have "(fst (ttas ! m), ⦃InitialThreadAction⦄) ∈ set (take m ttas)"
        using E'_a by(auto simp add: action_tid_def split_beta)
      then obtain i where i: "i < m" 
        and nth_i: "ttas ! i = (fst (ttas ! m), ⦃InitialThreadAction⦄)"
        unfolding in_set_conv_nth by auto

      let ?i' = "length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (take i ttas)))"
      let ?i = "length ?obs_prefix + ?i'"

      from i m nth_i
      have "?i' < length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (take m ttas)))"
        apply(simp add: length_concat o_def split_beta)
        apply(subst (6) id_take_nth_drop[where i=i])
        apply(simp_all add: take_map[symmetric] min_def)
        done
      also from m have "… ≤ ?a" unfolding a_conv
        by(simp add: length_concat sum_list_sum_nth min_def split_def atLeast0LessThan)
      finally have "?i < a" using a_len by simp
      moreover
      from i m nth_i have "?i' < length ?E'"
        apply(simp add: length_concat o_def split_def)
        apply(subst (7) id_take_nth_drop[where i=i])
        apply(simp_all add: take_map[symmetric])
        done
      from nth_i i E'_a a_conv m
      have "lnth ?E ?i = (fst (ttas ! m), InitialThreadAction)"
        by(simp add: lift_start_obs_def nth_append length_concat o_def split_def)(rule nth_concat_eqI[where k=0 and i=i], simp_all add: take_map o_def split_def)
      ultimately show ?thesis using E'_a
        by(cases "ttas ! m")(auto simp add: action_obs_def action_tid_def nth_append intro!: exI[where x="?i"])
    qed
  qed
qed

(* TODO: use previous lemma for proof *)

lemma thread_start_actions_ok_init_fin:
  assumes E: "E ∈ mthr.if.ℰ (init_fin_lift_state status (start_state f P C M vs))"
  shows "thread_start_actions_ok (lappend (llist_of (lift_start_obs start_tid start_heap_obs)) E)"
  (is "thread_start_actions_ok ?E")
proof(rule thread_start_actions_okI)
  let ?start_heap_obs = "lift_start_obs start_tid start_heap_obs"
  let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
  fix a
  assume a: "a ∈ actions ?E"
    and a_new: "¬ is_new_action (action_obs ?E a)"
  show "∃i. i ≤ a ∧ action_obs ?E i = InitialThreadAction ∧ action_tid ?E i = action_tid ?E a"
  proof(cases "action_tid ?E a = start_tid")
    case True thus ?thesis
      by(auto simp add: lift_start_obs_def action_tid_def action_obs_def)
  next
    case False

    let ?a = "a - length ?start_heap_obs"

    from False have "a ≥ length ?start_heap_obs"
      by(rule contrapos_np)(auto simp add: lift_start_obs_def action_tid_def lnth_LCons lnth_lappend1 split: nat.split)
    hence [simp]: "action_tid ?E a = action_tid E ?a" "action_obs ?E a = action_obs E ?a"
      by(simp_all add: action_tid_def lnth_lappend2 action_obs_def)

    from False have not_running: "⋀x ln. thr ?start_state (action_tid E ?a) ≠ ⌊((Running, x), ln)⌋"
      by(auto simp add: start_state_def split_beta init_fin_lift_state_def split: if_split_asm)
    
    from E obtain E' where E': "E = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
      and τRuns: "mthr.if.mthr.Runs ?start_state E'" by(rule mthr.if.ℰ.cases)
    from a E' ‹a ≥ length ?start_heap_obs›
    have enat_a: "enat ?a < llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))"
      by(cases "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))")(auto simp add: actions_def)
    with τRuns obtain m n t ta
    where a_obs: "lnth (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')) (a - length ?start_heap_obs) = (t, ⦃ta⦄⇘o⇙ ! n)"
      and n: "n < length ⦃ta⦄⇘o⇙" 
      and m: "enat m < llength E'"
      and a_conv: "?a = (∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) + n"
      and E'_m: "lnth E' m = (t, ta)"
      by(rule mthr.if.actions_ℰE_aux)
    from a_obs have [simp]: "action_tid E ?a = t" "action_obs E ?a = ⦃ta⦄⇘o⇙ ! n"
      by(simp_all add: E' action_tid_def action_obs_def)

    let ?E' = "ldropn (Suc m) E'"
    let ?m_E' = "ltake (enat m) E'"
    have E'_unfold: "E' = lappend (ltake (enat m) E') (LCons (lnth E' m) ?E')"
      unfolding ldropn_Suc_conv_ldropn[OF m] by simp
    hence "mthr.if.mthr.Runs ?start_state (lappend ?m_E' (LCons (lnth E' m) ?E'))"
      using τRuns by simp
    then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?m_E') σ'"
      and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' m) ?E')"
      by(rule mthr.if.mthr.Runs_lappendE) simp
    from τRuns' obtain σ''' where red_a: "mthr.if.redT σ' (t, ta) σ'''"
      and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
      unfolding E'_m by cases
    from red_a obtain status x ln where tst: "thr σ' t = ⌊((status, x), ln)⌋" by cases auto
    show ?thesis
    proof(cases "status = PreStart ∨ status = Finished")
      case True
      have "Status_no_wait_locks (thr σ')"
        by(rule mthr.init_fin_Trsys_preserve_Status_no_wait_locks[OF _ σ_σ'])(rule Status_no_wait_locks_start_state)
      with True tst have "ln = no_wait_locks"
        by(auto dest: Status_no_wait_locks_PreStartD Status_no_wait_locks_FinishedD)
      with red_a tst True have "⦃ta⦄⇘o⇙ = [InitialThreadAction]" by(cases) auto
      hence "action_obs E ?a = InitialThreadAction" using a_obs n unfolding E'
        by(simp add: action_obs_def)
      thus ?thesis by(auto)
    next
      case False
      hence "status = Running" by(cases status) auto
      with tst mthr.init_fin_Trsys_Running_InitialThreadAction[OF σ_σ' not_running]
      have "(action_tid E ?a, ⦃InitialThreadAction⦄) ∈ set (list_of (ltake (enat m) E'))"
        using a_obs E' by(auto simp add: action_tid_def)
      then obtain i where "i < m" "enat i < llength E'" 
        and nth_i: "lnth E' i = (action_tid E ?a, ⦃InitialThreadAction⦄)"
        unfolding in_set_conv_nth 
        by(cases "llength E'")(auto simp add: length_list_of_conv_the_enat lnth_ltake)

      let ?i' = "∑i<i. length ⦃snd (lnth E' i)⦄⇘o⇙"
      let ?i = "length ?start_heap_obs + ?i'"

      from ‹i < m› have "(∑i<m. length ⦃snd (lnth E' i)⦄⇘o⇙) = ?i' + (∑i=i..<m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
        unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
      hence "?i' ≤ ?a" unfolding a_conv by simp
      hence "?i ≤ a" using ‹a ≥ length ?start_heap_obs› by arith


      from ‹?i' ≤ ?a› have "enat ?i' < llength E" using enat_a E'
        by(simp add: le_less_trans[where y="enat ?a"])
      from lnth_lconcat_conv[OF this[unfolded E'], folded E']
      obtain k l 
        where nth_i': "lnth E ?i' = lnth (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') k) l"
        and l: "l < length ⦃snd (lnth E' k)⦄⇘o⇙"
        and k: "enat k < llength E'"
        and i_conv: "enat ?i' = (∑i<k. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) + enat l"
        by(fastforce simp add: split_beta)

      have "(∑i<k. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) =
            (∑i<k. (enat ∘ (λi. length ⦃snd (lnth E' i)⦄⇘o⇙)) i)"
        by(rule sum.cong)(simp_all add: less_trans[where y="enat k"] split_beta k)
      also have "… = enat (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙)"
        by(rule sum_comp_morphism)(simp_all add: zero_enat_def)
      finally have i_conv: "?i' = (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) + l" using i_conv by simp

      have [simp]: "i = k"
      proof(rule ccontr)
        assume "i ≠ k"
        thus False unfolding neq_iff
        proof
          assume "i < k"
          hence "(∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) = 
                 (∑i<i. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙)"
            unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
          with i_conv have "(∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙) = l" "l = 0" by simp_all
          moreover have "(∑i=i..<k. length ⦃snd (lnth E' i)⦄⇘o⇙) ≥ length ⦃snd (lnth E' i)⦄⇘o⇙"
            by(subst sum.atLeast_Suc_lessThan[OF ‹i < k›]) simp
          ultimately show False using nth_i by simp
        next
          assume "k < i"
          hence "?i' = (∑i<k. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙)"
            unfolding atLeast0LessThan[symmetric] by(subst sum.atLeastLessThan_concat) simp_all
          with i_conv have "(∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙) = l" by simp
          moreover have "(∑i=k..<i. length ⦃snd (lnth E' i)⦄⇘o⇙) ≥ length ⦃snd (lnth E' k)⦄⇘o⇙"
            by(subst sum.atLeast_Suc_lessThan[OF ‹k < i›]) simp
          ultimately show False using l by simp
        qed
      qed
      with l nth_i have [simp]: "l = 0" by simp
      
      hence "lnth E ?i' = (action_tid E ?a, InitialThreadAction)"
        using nth_i nth_i' k by simp
      with ‹?i ≤ a› show ?thesis
        by(auto simp add: action_tid_def action_obs_def lnth_lappend2)
    qed
  qed
qed



end

text ‹In the subsequent locales, ‹convert_RA› refers to @{term "convert_RA"} and is no longer a parameter!›

lemma convert_RA_not_write:
  "⋀ln. ob ∈ set (convert_RA ln) ⟹ ¬ is_write_action (NormalAction ob)"
by(auto simp add: convert_RA_def)

lemma ta_seq_consist_convert_RA:
  fixes ln shows
  "ta_seq_consist P vs (llist_of ((map NormalAction ∘ convert_RA) ln))"
proof(rule ta_seq_consist_nthI)
  fix i ad al v
  assume "enat i < llength (llist_of ((map NormalAction ∘ convert_RA) ln :: ('b, 'c) obs_event action list))"
    and "lnth (llist_of ((map NormalAction ∘ convert_RA) ln :: ('b, 'c) obs_event action list)) i = NormalAction (ReadMem ad al v)"
  hence "ReadMem ad al v ∈ set (convert_RA ln :: ('b, 'c) obs_event list)"
    by(auto simp add: in_set_conv_nth)
  hence False by(auto simp add: convert_RA_def)
  thus "∃b. mrw_values P vs (list_of (ltake (enat i) (llist_of ((map NormalAction ∘ convert_RA) ln)))) (ad, al) = ⌊(v, b)⌋" ..
qed

lemma ta_hb_consistent_convert_RA:
  "⋀ln. ta_hb_consistent P E (llist_of (map (Pair t) ((map NormalAction ∘ convert_RA) ln)))"
by(rule ta_hb_consistent_not_ReadI)(auto simp add: convert_RA_def)

locale allocated_multithreaded =
  allocated_heap
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write 
    allocated
    P 
  + 
  mthr: multithreaded final r convert_RA

  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 :: "'heap ⇒ '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 final :: "'x ⇒ bool"
  and r :: "('addr, 'thread_id, 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80) 
  and P :: "'md prog"
  +
  assumes red_allocated_mono: "t ⊢ (x, m) -ta→ (x', m') ⟹ allocated m ⊆ allocated m'"
  and red_New_allocatedD:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙ ⟧
  ⟹ ad ∈ allocated m' ∧ ad ∉ allocated m"
  and red_allocated_NewD:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); ad ∈ allocated m'; ad ∉ allocated m ⟧
  ⟹ ∃CTn. NewHeapElem ad CTn ∈ set ⦃ta⦄⇘o⇙"
  and red_New_same_addr_same:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); 
     ⦃ta⦄⇘o⇙ ! i = NewHeapElem a CTn; i < length ⦃ta⦄⇘o⇙;
     ⦃ta⦄⇘o⇙ ! j = NewHeapElem a CTn'; j < length ⦃ta⦄⇘o⇙ ⟧
  ⟹ i = j"


sublocale allocated_multithreaded < heap_multithreaded
  addr2thread_id thread_id2addr
  spurious_wakeups
  empty_heap allocate typeof_addr heap_read heap_write
  final r convert_RA P
by(unfold_locales)

context allocated_multithreaded begin

lemma redT_allocated_mono:
  assumes "mthr.redT σ (t, ta) σ'"
  shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms
by cases(auto dest: red_allocated_mono del: subsetI)

lemma RedT_allocated_mono:
  assumes "mthr.RedT σ ttas σ'"
  shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms unfolding mthr.RedT_def
by induct(auto dest!: redT_allocated_mono intro: subset_trans del: subsetI)

lemma init_fin_allocated_mono:
  "t ⊢ (x, m) -ta→i (x', m') ⟹ allocated m ⊆ allocated m'"
by(cases rule: mthr.init_fin.cases)(auto dest: red_allocated_mono)

lemma init_fin_redT_allocated_mono:
  assumes "mthr.if.redT σ (t, ta) σ'"
  shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms
by cases(auto dest: init_fin_allocated_mono del: subsetI)

lemma init_fin_RedT_allocated_mono:
  assumes "mthr.if.RedT σ ttas σ'"
  shows "allocated (shr σ) ⊆ allocated (shr σ')"
using assms unfolding mthr.if.RedT_def
by induct(auto dest!: init_fin_redT_allocated_mono intro: subset_trans del: subsetI)

lemma init_fin_red_New_allocatedD:
  assumes "t ⊢ (x, m) -ta→i (x', m')" "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
  shows "ad ∈ allocated m' ∧ ad ∉ allocated m"
using assms
by cases(auto dest: red_New_allocatedD)

lemma init_fin_red_allocated_NewD:
  assumes "t ⊢ (x, m) -ta→i (x', m')" "ad ∈ allocated m'" "ad ∉ allocated m"
  shows "∃CTn. NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
by(cases)(auto dest!: red_allocated_NewD)

lemma init_fin_red_New_same_addr_same:
  assumes "t ⊢ (x, m) -ta→i (x', m')"
  and "⦃ta⦄⇘o⇙ ! i = NormalAction (NewHeapElem a CTn)" "i < length ⦃ta⦄⇘o⇙"
  and "⦃ta⦄⇘o⇙ ! j = NormalAction (NewHeapElem a CTn')" "j < length ⦃ta⦄⇘o⇙"
  shows "i = j"
using assms
by cases(auto dest: red_New_same_addr_same)

lemma init_fin_redT_allocated_NewHeapElemD:
  assumes  "mthr.if.redT s (t, ta) s'"
  and "ad ∈ allocated (shr s')"
  and "ad ∉ allocated (shr s)"
  shows "∃CTn. NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
by(cases)(auto dest: init_fin_red_allocated_NewD)

lemma init_fin_RedT_allocated_NewHeapElemD:
  assumes "mthr.if.RedT s ttas s'"
  and "ad ∈ allocated (shr s')"
  and "ad ∉ allocated (shr s)"
  shows "∃t ta CTn. (t, ta) ∈ set ttas ∧ NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta⦄⇘o⇙"
using assms
proof(induct rule: mthr.if.RedT_induct')
  case refl thus ?case by simp
next
  case (step ttas s' t ta s'') thus ?case
    by(cases "ad ∈ allocated (shr s')")(fastforce simp del: split_paired_Ex dest: init_fin_redT_allocated_NewHeapElemD)+
qed

lemma ℰ_new_actions_for_unique:
  assumes E: "E ∈ ℰ_start f P C M vs status"
  and a: "a ∈ new_actions_for P E adal"
  and a': "a' ∈ new_actions_for P E adal"
  shows "a = a'"
using a a'
proof(induct a a' rule: wlog_linorder_le)
  case symmetry thus ?case by simp
next
  case (le a a')
  note a = ‹a ∈ new_actions_for P E adal›
    and a' = ‹a' ∈ new_actions_for P E adal›
    and a_a' = ‹a ≤ a'›
  obtain ad al where adal: "adal = (ad, al)" by(cases adal)
  
  let ?init_obs = "lift_start_obs start_tid start_heap_obs"
  let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"

  have distinct: "distinct (filter (λobs. ∃a CTn. obs = NormalAction (NewHeapElem a CTn)) (map snd ?init_obs))"
    unfolding start_heap_obs_def
    by(fastforce intro: inj_onI intro!: distinct_filter simp add: distinct_map distinct_zipI1 distinct_initialization_list)

  from start_addrs_allocated
  have dom_start_state: "{a. ∃CTn. NormalAction (NewHeapElem a CTn) ∈ snd ` set ?init_obs} ⊆ allocated (shr ?start_state)"
    by(fastforce simp add: init_fin_lift_state_conv_simps shr_start_state dest: NewHeapElem_start_heap_obs_start_addrsD subsetD)
  
  show ?case
  proof(cases "a' < length ?init_obs")
    case True
    with a' adal E obtain t_a' CTn_a'
      where CTn_a': "?init_obs ! a' = (t_a', NormalAction (NewHeapElem ad CTn_a'))"
      by(cases "?init_obs ! a'")(fastforce elim!: is_new_action.cases action_loc_aux_cases simp add: action_obs_def lnth_lappend1 new_actions_for_def )+
    from True a_a' have len_a: "a < length ?init_obs" by simp
    with a adal E obtain t_a CTn_a
      where CTn_a: "?init_obs ! a = (t_a, NormalAction (NewHeapElem ad CTn_a))"
      by(cases "?init_obs ! a")(fastforce elim!: is_new_action.cases action_loc_aux_cases simp add: action_obs_def lnth_lappend1 new_actions_for_def )+
    from CTn_a CTn_a' True len_a
    have "NormalAction (NewHeapElem ad CTn_a') ∈ snd ` set ?init_obs"
      and "NormalAction (NewHeapElem ad CTn_a) ∈ snd ` set ?init_obs" unfolding set_conv_nth
      by(fastforce intro: rev_image_eqI)+
    hence [simp]: "CTn_a' = CTn_a" using distinct_start_addrs'
      by(auto simp add: in_set_conv_nth distinct_conv_nth start_heap_obs_def start_addrs_def) blast
    from distinct_filterD[OF distinct, of a' a "NormalAction (NewHeapElem ad CTn_a)"] len_a True CTn_a CTn_a'
    show "a = a'" by simp
  next
    case False
    obtain n where n: "length ?init_obs = n" by blast
    with False have "n ≤ a'" by simp
    
    from E obtain E'' where E: "E = lappend (llist_of ?init_obs) E''"
      and E'': "E'' ∈ mthr.if.ℰ ?start_state" by auto
    from E'' obtain E' where E': "E'' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
      and τRuns: "mthr.if.mthr.Runs ?start_state E'" by(rule mthr.if.ℰ.cases)
    
    from E E'' a' n ‹n ≤ a'› adal have a': "a' - n ∈ new_actions_for P E'' adal"
      by(auto simp add: new_actions_for_def lnth_lappend2 action_obs_def actions_lappend elim: actionsE)
    
    from a' have "a' - n ∈ actions E''" by(auto elim: new_actionsE)
    hence "enat (a' - n) < llength E''" by(rule actionsE)
    with τRuns obtain a'_m a'_n t_a' ta_a'
      where E_a': "lnth E'' (a' - n) = (t_a', ⦃ta_a'⦄⇘o⇙ ! a'_n)"
      and a'_n: "a'_n < length ⦃ta_a'⦄⇘o⇙" and a'_m: "enat a'_m < llength E'"
      and a'_conv: "a' - n = (∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + a'_n"
      and E'_a'_m: "lnth E' a'_m = (t_a', ta_a')"
      unfolding E' by(rule mthr.if.actions_ℰE_aux)
    
    from a' have "is_new_action (action_obs E'' (a' - n))"
      and "(ad, al) ∈ action_loc P E'' (a' - n)"
      unfolding adal by(auto elim: new_actionsE)
    then obtain CTn'
      where "action_obs E'' (a' - n) = NormalAction (NewHeapElem ad CTn')"
      by cases(fastforce)+
    hence New_ta_a': "⦃ta_a'⦄⇘o⇙ ! a'_n = NormalAction (NewHeapElem ad CTn')"
      using E_a' a'_n unfolding action_obs_def by simp

    show ?thesis
    proof(cases "a < n")
      case True
      with a adal E n obtain t_a CTn_a where "?init_obs ! a = (t_a, NormalAction (NewHeapElem ad CTn_a))"
        by(cases "?init_obs ! a")(fastforce elim!: is_new_action.cases simp add: action_obs_def lnth_lappend1 new_actions_for_def)+

      with subsetD[OF dom_start_state, of ad] n True
      have a_shr_σ: "ad ∈ allocated (shr ?start_state)"
        by(fastforce simp add: set_conv_nth intro: rev_image_eqI)
      
      have E'_unfold': "E' = lappend (ltake (enat a'_m) E') (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E'))"
        unfolding ldropn_Suc_conv_ldropn[OF a'_m] by simp
      hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat a'_m) E') (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E')))"
        using τRuns by simp

      then obtain σ'
        where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat a'_m) E')) σ'"
        and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' a'_m) (ldropn (Suc a'_m) E'))"
        by(rule mthr.if.mthr.Runs_lappendE) simp
      from τRuns' obtain σ''
        where red_a': "mthr.if.redT σ' (t_a', ta_a') σ''"
        and τRuns'': "mthr.if.mthr.Runs σ'' (ldropn (Suc a'_m) E')"
        unfolding E'_a'_m by cases
      from New_ta_a' a'_n have "NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙"
        unfolding in_set_conv_nth by blast
      with red_a' obtain x_a' x'_a' m'_a' 
        where red'_a': "mthr.init_fin t_a' (x_a', shr σ') ta_a' (x'_a', m'_a')"
        and σ''': "redT_upd σ' t_a' ta_a' x'_a' m'_a' σ''"
        and ts_t_a': "thr σ' t_a' = ⌊(x_a', no_wait_locks)⌋"
        by cases auto
      from red'_a' ‹NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙›
      obtain ta'_a' X_a' X'_a'
        where x_a': "x_a' = (Running, X_a')"
        and x'_a': "x'_a' = (Running, X'_a')"
        and ta_a': "ta_a' = convert_TA_initial (convert_obs_initial ta'_a')"
        and red''_a': "t_a' ⊢ ⟨X_a', shr σ'⟩ -ta'_a'→ ⟨X'_a', m'_a'⟩"
        by cases fastforce+
      
      from ta_a' New_ta_a' a'_n have New_ta'_a': "⦃ta'_a'⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'"
        and a'_n': "a'_n < length ⦃ta'_a'⦄⇘o⇙" by auto
      hence "NewHeapElem ad CTn' ∈ set ⦃ta'_a'⦄⇘o⇙" unfolding in_set_conv_nth by blast
      with red''_a' have allocated_ad': "ad ∉ allocated (shr σ')"
        by(auto dest: red_New_allocatedD)
      
      have "allocated (shr ?start_state) ⊆ allocated (shr σ')"
        using σ_σ' unfolding mthr.if.RedT_def[symmetric] by(rule init_fin_RedT_allocated_mono)
      hence False using allocated_ad' a_shr_σ by blast
      thus ?thesis ..
    next
      case False
      hence "n ≤ a" by simp

      from E E'' a n ‹n ≤ a› adal have a: "a - n ∈ new_actions_for P E'' adal"
        by(auto simp add: new_actions_for_def lnth_lappend2 action_obs_def actions_lappend elim: actionsE)

      from a have "a - n ∈ actions E''" by(auto elim: new_actionsE)
      hence "enat (a - n) < llength E''" by(rule actionsE)

      with τRuns obtain a_m a_n t_a ta_a 
        where E_a: "lnth E'' (a - n) = (t_a, ⦃ta_a⦄⇘o⇙ ! a_n)"
        and a_n: "a_n < length ⦃ta_a⦄⇘o⇙" and a_m: "enat a_m < llength E'"
        and a_conv: "a - n = (∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + a_n"
        and E'_a_m: "lnth E' a_m = (t_a, ta_a)"
        unfolding E' by(rule mthr.if.actions_ℰE_aux)
  
      from a have "is_new_action (action_obs E'' (a - n))" 
        and "(ad, al) ∈ action_loc P E'' (a - n)" 
        unfolding adal by(auto elim: new_actionsE)
      then obtain CTn where "action_obs E'' (a - n) = NormalAction (NewHeapElem ad CTn)"
        by cases(fastforce)+
      hence New_ta_a: " ⦃ta_a⦄⇘o⇙ ! a_n = NormalAction (NewHeapElem ad CTn)"
        using E_a a_n unfolding action_obs_def by simp
      
      let ?E' = "ldropn (Suc a_m) E'"
  
      have E'_unfold: "E' = lappend (ltake (enat a_m) E') (LCons (lnth E' a_m) ?E')"
        unfolding ldropn_Suc_conv_ldropn[OF a_m] by simp
      hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat a_m) E') (LCons (lnth E' a_m) ?E'))"
        using τRuns by simp
      then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat a_m) E')) σ'"
        and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' a_m) ?E')"
        by(rule mthr.if.mthr.Runs_lappendE) simp
      from τRuns' obtain σ''
        where red_a: "mthr.if.redT σ' (t_a, ta_a) σ''"
        and τRuns'': "mthr.if.mthr.Runs σ'' ?E'"
        unfolding E'_a_m by cases
      from New_ta_a a_n have "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta_a⦄⇘o⇙"
        unfolding in_set_conv_nth by blast
      with red_a obtain x_a x'_a m'_a 
        where red'_a: "mthr.init_fin t_a (x_a, shr σ') ta_a (x'_a, m'_a)"
        and σ''': "redT_upd σ' t_a ta_a x'_a m'_a σ''"
        and ts_t_a: "thr σ' t_a = ⌊(x_a, no_wait_locks)⌋"
        by cases auto
      from red'_a ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta_a⦄⇘o⇙›
      obtain ta'_a X_a X'_a
        where x_a: "x_a = (Running, X_a)"
        and x'_a: "x'_a = (Running, X'_a)"
        and ta_a: "ta_a = convert_TA_initial (convert_obs_initial ta'_a)"
        and red''_a: "t_a ⊢ (X_a, shr σ') -ta'_a→ (X'_a, m'_a)"
        by cases fastforce+
      from ta_a New_ta_a a_n have New_ta'_a: "⦃ta'_a⦄⇘o⇙ ! a_n = NewHeapElem ad CTn"
        and a_n': "a_n < length ⦃ta'_a⦄⇘o⇙" by auto
      hence "NewHeapElem ad CTn ∈ set ⦃ta'_a⦄⇘o⇙" unfolding in_set_conv_nth by blast
      with red''_a have allocated_m'_a_ad: "ad ∈ allocated m'_a"
        by(auto dest: red_New_allocatedD)
      
      have "a_m ≤ a'_m"
      proof(rule ccontr)
        assume "¬ ?thesis"
        hence "a'_m < a_m" by simp
        hence "(∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i = a'_m..<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
          by(simp add: sum_upto_add_nat)
        hence "a' - n < a - n" using ‹a'_m < a_m› a'_n E'_a'_m unfolding a_conv a'_conv
          by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
        with a_a' show False by simp
      qed
  
      have a'_less: "a' - n < (a - n) - a_n + length ⦃ta_a⦄⇘o⇙"
      proof(rule ccontr)
        assume "¬ ?thesis"
        hence a'_greater: "(a - n) - a_n + length ⦃ta_a⦄⇘o⇙ ≤ a' - n" by simp
        
        have "a_m < a'_m"
        proof(rule ccontr)
          assume "¬ ?thesis"
          with ‹a_m ≤ a'_m› have "a_m = a'_m" by simp
          with a'_greater a_n a'_n E'_a'_m E'_a_m show False
            unfolding a_conv a'_conv by simp
        qed
        hence a'_m_a_m: "enat (a'_m - Suc a_m) < llength ?E'" using a'_m
          by(cases "llength E'") simp_all
        from ‹a_m < a'_m› a'_m E'_a'_m
        have E'_a'_m': "lnth ?E' (a'_m - Suc a_m) = (t_a', ta_a')" by simp
    
        have E'_unfold': "?E' = lappend (ltake (enat (a'_m - Suc a_m)) ?E') (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E'))"
          unfolding ldropn_Suc_conv_ldropn[OF a'_m_a_m] lappend_ltake_enat_ldropn ..
        hence "mthr.if.mthr.Runs σ'' (lappend (ltake (enat (a'_m - Suc a_m)) ?E') (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E')))"
          using τRuns'' by simp
        then obtain σ'''
          where σ''_σ''': "mthr.if.mthr.Trsys σ'' (list_of (ltake (enat (a'_m - Suc a_m)) ?E')) σ'''"
          and τRuns''': "mthr.if.mthr.Runs σ''' (LCons (lnth ?E' (a'_m - Suc a_m)) (ldropn (Suc (a'_m - Suc a_m)) ?E'))"
          by(rule mthr.if.mthr.Runs_lappendE) simp
        from τRuns''' obtain σ''''
          where red_a': "mthr.if.redT σ''' (t_a', ta_a') σ''''"
          and τRuns'''': "mthr.if.mthr.Runs σ'''' (ldropn (Suc (a'_m - Suc a_m)) ?E')"
          unfolding E'_a'_m' by cases
        from New_ta_a' a'_n have "NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙"
          unfolding in_set_conv_nth by blast
        with red_a' obtain x_a' x'_a' m'_a' 
          where red'_a': "mthr.init_fin t_a' (x_a', shr σ''') ta_a' (x'_a', m'_a')"
          and σ'''''': "redT_upd σ''' t_a' ta_a' x'_a' m'_a' σ''''"
          and ts_t_a': "thr σ''' t_a' = ⌊(x_a', no_wait_locks)⌋"
          by cases auto
        from red'_a' ‹NormalAction (NewHeapElem ad CTn') ∈ set ⦃ta_a'⦄⇘o⇙›
        obtain ta'_a' X_a' X'_a' 
          where x_a': "x_a' = (Running, X_a')"
          and x'_a': "x'_a' = (Running, X'_a')"
          and ta_a': "ta_a' = convert_TA_initial (convert_obs_initial ta'_a')"
          and red''_a': "t_a' ⊢ (X_a', shr σ''') -ta'_a'→ (X'_a', m'_a')"
          by cases fastforce+
        from ta_a' New_ta_a' a'_n have New_ta'_a': "⦃ta'_a'⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'"
          and a'_n': "a'_n < length ⦃ta'_a'⦄⇘o⇙" by auto
        hence "NewHeapElem ad CTn' ∈ set ⦃ta'_a'⦄⇘o⇙" unfolding in_set_conv_nth by blast
        with red''_a' have allocated_ad': "ad ∉ allocated (shr σ''')"
          by(auto dest: red_New_allocatedD)
    
        have "allocated m'_a = allocated (shr σ'')" using σ''' by auto
        also have "… ⊆ allocated (shr σ''')"
          using σ''_σ''' unfolding mthr.if.RedT_def[symmetric] by(rule init_fin_RedT_allocated_mono)
        finally have "ad ∈ allocated (shr σ''')" using allocated_m'_a_ad by blast
        with allocated_ad' show False by contradiction
      qed
      
      from ‹a_m ≤ a'_m› have [simp]: "a_m = a'_m"
      proof(rule le_antisym)
        show "a'_m ≤ a_m"
        proof(rule ccontr)
          assume "¬ ?thesis"
          hence "a_m < a'_m" by simp
          hence "(∑i<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<a_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + (∑i = a_m..<a'_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
            by(simp add: sum_upto_add_nat)
          with a'_less ‹a_m < a'_m› E'_a_m a_n a'_n show False
            unfolding a'_conv a_conv by(subst (asm) sum.atLeast_Suc_lessThan) simp_all
        qed
      qed
      with E'_a_m E'_a'_m have [simp]: "t_a' = t_a" "ta_a' = ta_a" by simp_all
      from New_ta_a' a'_n ta_a have a'_n': "a'_n < length ⦃ta'_a⦄⇘o⇙"
        and New_ta'_a': "⦃ta'_a⦄⇘o⇙ ! a'_n = NewHeapElem ad CTn'" by auto
      with red''_a New_ta'_a a_n' have "a'_n = a_n"
        by(auto dest: red_New_same_addr_same)
      with ‹a_m = a'_m› have "a - n = a' - n" unfolding a_conv a'_conv by simp
      thus ?thesis using ‹n ≤ a› ‹n ≤ a'› by simp
    qed
  qed
qed

end


text ‹Knowledge of addresses of a multithreaded state›

fun ka_Val :: "'addr val ⇒ 'addr set"
where
  "ka_Val (Addr a) = {a}"
| "ka_Val _ = {}"

fun new_obs_addr :: "('addr, 'thread_id) obs_event ⇒ 'addr set"
where
  "new_obs_addr (ReadMem ad al (Addr ad')) = {ad'}"
| "new_obs_addr (NewHeapElem ad hT) = {ad}"
| "new_obs_addr _ = {}"

lemma new_obs_addr_cases[consumes 1, case_names ReadMem NewHeapElem, cases set]:
  assumes "ad ∈ new_obs_addr ob"
  obtains ad' al where "ob = ReadMem ad' al (Addr ad)"
  | CTn where "ob = NewHeapElem ad CTn"
using assms
by(cases ob rule: new_obs_addr.cases) auto

definition new_obs_addrs :: "('addr, 'thread_id) obs_event list ⇒ 'addr set"
where
  "new_obs_addrs obs = ⋃(new_obs_addr ` set obs)"

fun new_obs_addr_if :: "('addr, 'thread_id) obs_event action ⇒ 'addr set"
where
  "new_obs_addr_if (NormalAction a) = new_obs_addr a"
| "new_obs_addr_if _ = {}"

definition new_obs_addrs_if :: "('addr, 'thread_id) obs_event action list ⇒ 'addr set"
where 
  "new_obs_addrs_if obs = ⋃(new_obs_addr_if ` set obs)"

lemma ka_Val_subset_new_obs_Addr_ReadMem:
  "ka_Val v ⊆ new_obs_addr (ReadMem ad al v)"
by(cases v) simp_all

lemma typeof_ka: "typeof v ≠ None ⟹ ka_Val v = {}"
by(cases v) simp_all

lemma ka_Val_undefined_value [simp]:
  "ka_Val undefined_value = {}"
apply(cases "undefined_value :: 'a val")
apply(bestsimp simp add: undefined_value_not_Addr dest: subst)+
done

locale known_addrs_base =
  fixes known_addrs :: "'t ⇒ 'x ⇒ 'addr set"
begin

definition known_addrs_thr :: "('l, 't, 'x) thread_info ⇒ 'addr set"
where "known_addrs_thr ts = (⋃t ∈ dom ts. known_addrs t (fst (the (ts t))))"

definition known_addrs_state :: "('l,'t,'x,'m,'w) state ⇒ 'addr set"
where "known_addrs_state s = known_addrs_thr (thr s)"

lemma known_addrs_state_simps [simp]:
  "known_addrs_state (ls, (ts, m), ws) = known_addrs_thr ts"
by(simp add: known_addrs_state_def)

lemma known_addrs_thr_cases[consumes 1, case_names known_addrs, cases set: known_addrs_thr]:
  assumes "ad ∈ known_addrs_thr ts"
  and "⋀t x ln. ⟦ ts t = ⌊(x, ln)⌋; ad ∈ known_addrs t x ⟧ ⟹ thesis"
  shows thesis
using assms
by(auto simp add: known_addrs_thr_def ran_def)

lemma known_addrs_stateI:
  "⋀ln. ⟦ ad ∈ known_addrs t x; thr s t = ⌊(x, ln)⌋ ⟧ ⟹ ad ∈ known_addrs_state s"
by(fastforce simp add: known_addrs_state_def known_addrs_thr_def intro: rev_bexI)

fun known_addrs_if :: "'t ⇒ status × 'x ⇒ 'addr set"
where "known_addrs_if t (s, x) = known_addrs t x"

end

locale if_known_addrs_base = 
  known_addrs_base known_addrs 
  +
  multithreaded_base final r convert_RA
  for known_addrs :: "'t ⇒ 'x ⇒ 'addr set"
  and final :: "'x ⇒ bool"
  and r :: "('addr, 't, 'x, 'heap, 'addr, 'obs) semantics" ("_ ⊢ _ -_→ _" [50,0,0,50] 80)
  and convert_RA :: "'addr released_locks ⇒ 'obs list"

sublocale if_known_addrs_base < "if": known_addrs_base known_addrs_if .

locale known_addrs =
  allocated_multithreaded (* Check why all the heap operations are necessary in this locale! *)
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    allocated
    final r
    P 
  +
  if_known_addrs_base known_addrs final r convert_RA

  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 :: "'heap ⇒ '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 P :: "'md prog"
  +
  assumes red_known_addrs_new:
  "t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩
  ⟹ known_addrs t x' ⊆ known_addrs t x ∪ new_obs_addrs ⦃ta⦄⇘o⇙"
  and red_known_addrs_new_thread:
  "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙ ⟧
  ⟹ known_addrs t' x'' ⊆ known_addrs t x"
  and red_read_knows_addr:
  "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧
  ⟹ ad ∈ known_addrs t x"
  and red_write_knows_addr:
  "⟦ t ⊢ ⟨x, m⟩ -ta→ ⟨x', m'⟩; ⦃ta⦄⇘o⇙ ! n = WriteMem ad al (Addr ad'); n < length ⦃ta⦄⇘o⇙ ⟧
  ⟹ ad' ∈ known_addrs t x ∨ ad' ∈ new_obs_addrs (take n ⦃ta⦄⇘o⇙)"
  ― ‹second possibility necessary for @{term heap_clone}›
begin

notation mthr.redT_syntax1 ("_ -_▹_→ _" [50,0,0,50] 80)

lemma if_red_known_addrs_new: 
  assumes "t ⊢ (x, m) -ta→i (x', m')"
  shows "known_addrs_if t x' ⊆ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
using assms
by cases(auto dest!: red_known_addrs_new simp add: new_obs_addrs_if_def new_obs_addrs_def)

lemma if_red_known_addrs_new_thread:
  assumes "t ⊢ (x, m) -ta→i (x', m')" "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
  shows "known_addrs_if t' x'' ⊆ known_addrs_if t x"
using assms
by cases(fastforce dest: red_known_addrs_new_thread)+

lemma if_red_read_knows_addr:
  assumes "t ⊢ (x, m) -ta→i (x', m')" "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
  shows "ad ∈ known_addrs_if t x"
using assms
by cases(fastforce dest: red_read_knows_addr)+

lemma if_red_write_knows_addr:
  assumes "t ⊢ (x, m) -ta→i (x', m')"
  and "⦃ta⦄⇘o⇙ ! n = NormalAction (WriteMem ad al (Addr ad'))" "n < length ⦃ta⦄⇘o⇙"
  shows "ad' ∈ known_addrs_if t x ∨ ad' ∈ new_obs_addrs_if (take n ⦃ta⦄⇘o⇙)"
using assms
by cases(auto dest: red_write_knows_addr simp add: new_obs_addrs_if_def new_obs_addrs_def take_map)

lemma if_redT_known_addrs_new:
  assumes redT: "mthr.if.redT s (t, ta) s'"
  shows "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
using redT
proof(cases)
  case redT_acquire thus ?thesis
    by(cases s)(fastforce simp add: if.known_addrs_thr_def split: if_split_asm intro: rev_bexI)
next
  case (redT_normal x x' m)
  note red = ‹t ⊢ (x, shr s) -ta→i (x', m)›
  show ?thesis
  proof
    fix ad
    assume "ad ∈ if.known_addrs_state s'"
    hence "ad ∈ if.known_addrs_thr (thr s')" by(simp add: if.known_addrs_state_def)
    then obtain t' x'' ln'' where ts't': "thr s' t' = ⌊(x'', ln'')⌋" 
      and ad: "ad ∈ known_addrs_if t' x''"
      by(rule if.known_addrs_thr_cases)
    show "ad ∈ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
    proof(cases "thr s t'")
      case None
      with redT_normal ‹thr s' t' = ⌊(x'', ln'')⌋›
      obtain m'' where "NewThread t' x'' m'' ∈ set ⦃ta⦄⇘t⇙"
        by(fastforce dest: redT_updTs_new_thread split: if_split_asm)
      with red have "known_addrs_if t' x'' ⊆ known_addrs_if t x" by(rule if_red_known_addrs_new_thread)
      also have "… ⊆ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" by simp
      finally have "ad ∈ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" using ad by blast
      thus ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋› by(blast intro: if.known_addrs_stateI)
    next
      case (Some xln)
      show ?thesis
      proof(cases "t = t'")
        case True
        with redT_normal ts't' if_red_known_addrs_new[OF red] ad
        have "ad ∈ known_addrs_if t x ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙" by auto
        thus ?thesis using ‹thr s t = ⌊(x, no_wait_locks)⌋› by(blast intro: if.known_addrs_stateI)
      next
        case False
        with ts't' redT_normal ad Some show ?thesis
          by(fastforce dest: redT_updTs_Some[where ts="thr s" and t=t'] intro: if.known_addrs_stateI)
      qed
    qed
  qed
qed

lemma if_redT_read_knows_addr:
  assumes redT: "mthr.if.redT s (t, ta) s'"
  and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
  shows "ad ∈ if.known_addrs_state s"
using redT
proof(cases)
  case redT_acquire thus ?thesis using read by auto
next
  case (redT_normal x x' m')
  with if_red_read_knows_addr[OF ‹t ⊢ (x, shr s) -ta→i (x', m')› read]
  show ?thesis
    by(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def intro: bexI[where x=t])
qed

lemma init_fin_redT_known_addrs_subset:
  assumes "mthr.if.redT s (t, ta) s'"
  shows "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ known_addrs_if t (fst (the (thr s' t)))"
using assms
apply(cases)
 apply(rule subsetI)
 apply(clarsimp simp add: if.known_addrs_thr_def split: if_split_asm)
 apply(rename_tac status x status' x' m' a ws' t'' status'' x'' ln'')
 apply(case_tac "thr s t''")
  apply(drule (2) redT_updTs_new_thread)
  apply clarsimp
  apply(drule (1) if_red_known_addrs_new_thread)
  apply simp
  apply(drule (1) subsetD)
  apply(rule_tac x="(status, x)" in if.known_addrs_stateI)
   apply(simp)
  apply simp
 apply(frule_tac t="t''" in redT_updTs_Some, assumption)
 apply clarsimp
 apply(rule_tac x="(status'', x'')" in if.known_addrs_stateI)
  apply simp
 apply simp
apply(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def split: if_split_asm)
done

lemma w_values_no_write_unchanged:
  assumes no_write: "⋀w. ⟦ w ∈ set obs; is_write_action w; adal ∈ action_loc_aux P w ⟧ ⟹ False"
  shows "w_values P vs obs adal = vs adal"
using assms
proof(induct obs arbitrary: vs)
  case Nil show ?case by simp
next
  case (Cons ob obs)
  from Cons.prems[of ob]
  have "w_value P vs ob adal = vs adal"
    by(cases adal)(cases ob rule: w_value_cases, auto simp add: addr_locs_def split: htype.split_asm, blast+)
  moreover
  have "w_values P (w_value P vs ob) obs adal = w_value P vs ob adal"
  proof(rule Cons.hyps)
    fix w
    assume "w ∈ set obs" "is_write_action w" "adal ∈ action_loc_aux P w"
    with Cons.prems[of w] ‹w_value P vs ob adal = vs adal›
    show "False" by simp
  qed
  ultimately show ?case by simp
qed

lemma redT_non_speculative_known_addrs_allocated:
  assumes red: "mthr.if.redT s (t, ta) s'"
  and tasc: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
  and ka: "if.known_addrs_state s ⊆ allocated (shr s)"
  and vs: "w_addrs vs ⊆ allocated (shr s)"
  shows "if.known_addrs_state s' ⊆ allocated (shr s')" (is "?thesis1")
  and "w_addrs (w_values P vs ⦃ta⦄⇘o⇙) ⊆ allocated (shr s')" (is "?thesis2")
proof -
  have "?thesis1 ∧ ?thesis2" using red
  proof(cases)
    case (redT_acquire x ln n)
    hence "if.known_addrs_state s' = if.known_addrs_state s"
      by(auto 4 4 simp add: if.known_addrs_state_def if.known_addrs_thr_def split: if_split_asm dest: bspec)
    also note ka 
    also from redT_acquire have "shr s = shr s'" by simp
    finally have "if.known_addrs_state s' ⊆ allocated (shr s')" .
    moreover have "w_values P vs ⦃ta⦄⇘o⇙ = vs" using redT_acquire
      by(fastforce intro!: w_values_no_write_unchanged del: equalityI dest: convert_RA_not_write)
    ultimately show ?thesis using vs by(simp add: ‹shr s = shr s'›)
  next
    case (redT_normal x x' m')
    note red = ‹t ⊢ (x, shr s) -ta→i (x', m')›
      and tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
    have allocated_subset: "allocated (shr s) ⊆ allocated (shr s')"
      using ‹mthr.if.redT s (t, ta) s'› by(rule init_fin_redT_allocated_mono)
    with vs have vs': "w_addrs vs ⊆ allocated (shr s')" by blast
    { fix obs obs'
      assume "⦃ta⦄⇘o⇙ = obs @ obs'"
      moreover with tasc have "non_speculative P vs (llist_of obs)"
        by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
      ultimately have "w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs ⊆ allocated (shr s')" 
        (is "?concl obs")
      proof(induct obs arbitrary: obs' rule: rev_induct)
        case Nil thus ?case using vs' by(simp add: new_obs_addrs_if_def)
      next
        case (snoc ob obs)
        note ta = ‹⦃ta⦄⇘o⇙ = (obs @ [ob]) @ obs'›
        note tasc = ‹non_speculative P vs (llist_of (obs @ [ob]))›
        from snoc have IH: "?concl obs"
          by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
        hence "?concl (obs @ [ob])"
        proof(cases "ob" rule: mrw_value_cases)
          case (1 ad' al v)
          note ob = ‹ob = NormalAction (WriteMem ad' al v)›
          with ta have Write: "⦃ta⦄⇘o⇙ ! length obs = NormalAction (WriteMem ad' al v)" by simp
          show ?thesis
          proof
            fix ad''
            assume "ad'' ∈ w_addrs (w_values P vs (obs @ [ob])) ∪ new_obs_addrs_if (obs @ [ob])"
            hence "ad'' ∈ w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs ∨ v = Addr ad''"
              by(auto simp add: ob w_addrs_def ran_def new_obs_addrs_if_def split: if_split_asm)
            thus "ad'' ∈ allocated (shr s')"
            proof
              assume "ad'' ∈ w_addrs (w_values P vs obs) ∪ new_obs_addrs_if obs"
              also note IH finally show ?thesis .
            next
              assume v: "v = Addr ad''"
              with Write have "⦃ta⦄⇘o⇙ ! length obs = NormalAction (WriteMem ad' al (Addr ad''))" by simp
              with red have "ad'' ∈ known_addrs_if t x ∨ ad'' ∈ new_obs_addrs_if (take (length obs) ⦃ta⦄⇘o⇙)"
                by(rule if_red_write_knows_addr)(simp add: ta)
              thus ?thesis
              proof
                assume "ad'' ∈ known_addrs_if t x"
                hence "ad'' ∈ if.known_addrs_state s" using tst by(rule if.known_addrs_stateI)
                with ka allocated_subset show ?thesis by blast
              next
                assume "ad'' ∈ new_obs_addrs_if (take (length obs) ⦃ta⦄⇘o⇙)"
                with ta have "ad'' ∈ new_obs_addrs_if obs" by simp
                with IH show ?thesis by blast
              qed
            qed
          qed
        next
          case (2 ad hT)

          hence ob: "ob = NormalAction (NewHeapElem ad hT)" by simp
          hence "w_addrs (w_values P vs (obs @ [ob])) ⊆ w_addrs (w_values P vs obs)"
            by(cases hT)(auto simp add: w_addrs_def default_val_not_Addr Addr_not_default_val)
          moreover from ob ta have "NormalAction (NewHeapElem ad hT) ∈ set ⦃ta⦄⇘o⇙" by simp
          from init_fin_red_New_allocatedD[OF red this] have "ad ∈ allocated m'" ..
          with redT_normal have "ad ∈ allocated (shr s')" by auto
          ultimately show ?thesis using IH ob by(auto simp add: new_obs_addrs_if_def)
        next
          case (4 ad al v)
          note ob = ‹ob = NormalAction (ReadMem ad al v)›
          { fix ad'
            assume v: "v = Addr ad'"
            with tasc ob have mrw: "Addr ad' ∈ w_values P vs obs (ad, al)"
              by(auto simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend simp del: lappend_llist_of_llist_of)
            hence "ad' ∈ w_addrs (w_values P vs obs)"
              by(auto simp add: w_addrs_def)
            with IH have "ad' ∈ allocated (shr s')" by blast }
          with ob IH show ?thesis by(cases v)(simp_all add: new_obs_addrs_if_def)
        qed(simp_all add: new_obs_addrs_if_def)
        thus ?case by simp
      qed }
    note this[of "⦃ta⦄⇘o⇙" "[]"]
    moreover have "if.known_addrs_state s' ⊆ if.known_addrs_state s ∪ new_obs_addrs_if ⦃ta⦄⇘o⇙"
      using ‹mthr.if.redT s (t, ta) s'› by(rule if_redT_known_addrs_new)
    ultimately show ?thesis using ka allocated_subset by blast
  qed
  thus ?thesis1 ?thesis2 by simp_all
qed


lemma RedT_non_speculative_known_addrs_allocated:
  assumes red: "mthr.if.RedT s ttas s'"
  and tasc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
  and ka: "if.known_addrs_state s ⊆ allocated (shr s)"
  and vs: "w_addrs vs ⊆ allocated (shr s)"
  shows "if.known_addrs_state s' ⊆ allocated (shr s')" (is "?thesis1 s'")
  and "w_addrs (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) ⊆ allocated (shr s')" (is "?thesis2 s' ttas")
proof -
  from red tasc have "?thesis1 s' ∧ ?thesis2 s' ttas"
  proof(induct rule: mthr.if.RedT_induct')
    case refl thus ?case using ka vs by simp
  next
    case (step ttas s' t ta s'')
    hence "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta⦄⇘o⇙)"
      and "?thesis1 s'" "?thesis2 s' ttas"
      by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
    from redT_non_speculative_known_addrs_allocated[OF ‹mthr.if.redT s' (t, ta) s''› this]
    show ?case by simp
  qed
  thus "?thesis1 s'" "?thesis2 s' ttas" by simp_all
qed

lemma read_ex_NewHeapElem [consumes 5, case_names start Red]:
  assumes RedT: "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas s"
  and red: "mthr.if.redT s (t, ta) s'"
  and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
  and sc: "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
  and known: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  obtains (start) CTn where "NewHeapElem ad CTn ∈ set start_heap_obs"
  | (Red) ttas' s'' t' ta' s''' ttas'' CTn
  where "mthr.if.RedT (init_fin_lift_state status (start_state f P C M vs)) ttas' s''"
  and "mthr.if.redT s'' (t', ta') s'''"
  and "mthr.if.RedT s''' ttas'' s"
  and "ttas = ttas' @ (t', ta') # ttas''"
  and "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙"
proof -
  let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"
  let ?obs_prefix = "lift_start_obs start_tid start_heap_obs"
  let ?vs_start = "w_values P (λ_. {}) (map snd ?obs_prefix)"

  from sc have "non_speculative P (w_values P (λ_. {}) (map snd (lift_start_obs start_tid start_heap_obs))) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    by(simp add: non_speculative_lappend lappend_llist_of_llist_of[symmetric] del: lappend_llist_of_llist_of)
  with RedT have "if.known_addrs_state s ⊆ allocated (shr s)"
  proof(rule RedT_non_speculative_known_addrs_allocated)
    show "if.known_addrs_state ?start_state ⊆ allocated (shr ?start_state)"
      using known
      by(auto simp add: if.known_addrs_state_def if.known_addrs_thr_def start_state_def init_fin_lift_state_def split_beta split: if_split_asm)
    
    have "w_addrs ?vs_start ⊆ w_addrs (λ_. {})" by(rule w_addrs_lift_start_heap_obs)
    thus "w_addrs ?vs_start ⊆ allocated (shr ?start_state)" by simp
  qed
  also from red read obtain x_ra x'_ra m'_ra 
    where red'_ra: "t ⊢ (x_ra, shr s) -ta→i (x'_ra, m'_ra)"
    and s': "redT_upd s t ta x'_ra m'_ra s'"
    and ts_t: "thr s t = ⌊(x_ra, no_wait_locks)⌋"
    by cases auto
  from red'_ra read
  have "ad ∈ known_addrs_if t x_ra" by(rule if_red_read_knows_addr)
  hence "ad ∈ if.known_addrs_state s" using ts_t by(rule if.known_addrs_stateI)
  finally have "ad ∈ allocated (shr s)" .

  show ?thesis
  proof(cases "ad ∈ allocated start_heap")
    case True
    then obtain CTn where "NewHeapElem ad CTn ∈ set start_heap_obs"
      unfolding start_addrs_allocated by(blast dest: start_addrs_NewHeapElem_start_heap_obsD)
    thus ?thesis by(rule start)
  next
    case False
    hence "ad ∉ allocated (shr ?start_state)" by(simp add: start_state_def split_beta shr_init_fin_lift_state)
    with RedT ‹ad ∈ allocated (shr s)› obtain t' ta' CTn
      where tta: "(t', ta') ∈ set ttas"
      and new: "NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙"
      by(blast dest: init_fin_RedT_allocated_NewHeapElemD)
    from tta obtain ttas' ttas'' where ttas: "ttas = ttas' @ (t', ta') # ttas''" by(auto dest: split_list)
    with RedT obtain s'' s''' 
      where "mthr.if.RedT ?start_state ttas' s''"
      and "mthr.if.redT s'' (t', ta') s'''"
      and "mthr.if.RedT s''' ttas'' s"
      unfolding mthr.if.RedT_def by(auto elim!: rtrancl3p_appendE dest!: converse_rtrancl3p_step)
    thus thesis using ttas new by(rule Red)
  qed
qed

end

locale known_addrs_typing =
  known_addrs
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    allocated known_addrs
    final r 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 :: "'heap ⇒ '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 wfs_non_speculative_invar:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
     vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)) ⟧
  ⟹ wfx t x' m'"
  and wfs_non_speculative_spawn:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
     vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙));
     NewThread t'' x'' m'' ∈ set ⦃ta⦄⇘t⇙ ⟧
  ⟹ wfx t'' x'' m''"
  and wfs_non_speculative_other:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
     vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙));
     wfx t'' x'' m ⟧
  ⟹ wfx t'' x'' m'"
  and wfs_non_speculative_vs_conf:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m;
     vs_conf P m vs; non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙))) ⟧
  ⟹ vs_conf P m' (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
  and red_read_typeable:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m; ReadMem ad al v ∈ set ⦃ta⦄⇘o⇙ ⟧ 
  ⟹ ∃T. P,m ⊢ ad@al : T"
  and red_NewHeapElemD:
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m; NewHeapElem ad hT ∈ set ⦃ta⦄⇘o⇙ ⟧
  ⟹ typeof_addr m' ad = ⌊hT⌋"
  and red_hext_incr: 
  "⟦ t ⊢ (x, m) -ta→ (x', m'); wfx t x m; 
     vs_conf P m vs; non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙)) ⟧
  ⟹ m ⊴ m'"
begin

lemma redT_wfs_non_speculative_invar:
  assumes redT: "mthr.redT s (t, ta) s'"
  and wfx: "ts_ok wfx (thr s) (shr s)"
  and vs: "vs_conf P (shr s) vs"
  and ns: "non_speculative P vs (llist_of (map NormalAction ⦃ta⦄⇘o⇙))"
  shows "ts_ok wfx (thr s') (shr s')"
using redT
proof(cases)
  case (redT_normal x x' m')
  with vs wfx ns show ?thesis
    apply(clarsimp intro!: ts_okI split: if_split_asm)
     apply(erule wfs_non_speculative_invar, auto dest: ts_okD)
    apply(rename_tac t' x' ln ws')
    apply(case_tac "thr s t'")
    apply(frule (2) redT_updTs_new_thread, clarify)
    apply(frule (1) mthr.new_thread_memory)
    apply(auto intro: wfs_non_speculative_other wfs_non_speculative_spawn dest: ts_okD simp add: redT_updTs_Some)
    done
next
  case (redT_acquire x ln n)
  thus ?thesis using wfx by(auto intro!: ts_okI dest: ts_okD split: if_split_asm)
qed

lemma redT_wfs_non_speculative_vs_conf:
  assumes redT: "mthr.redT s (t, ta) s'"
  and wfx: "ts_ok wfx (thr s) (shr s)"
  and conf: "vs_conf P (shr s) vs"
  and ns: "non_speculative P vs (llist_of (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
  shows "vs_conf P (shr s') (w_values P vs (take n (map NormalAction ⦃ta⦄⇘o⇙)))"
using redT
proof(cases)
  case (redT_normal x x' m')
  thus ?thesis using ns conf wfx by(auto dest: wfs_non_speculative_vs_conf ts_okD)
next
  case (redT_acquire x l ln)
  have "w_values P vs (take n (map NormalAction (convert_RA ln :: ('addr, 'thread_id) obs_event list))) = vs"
    by(fastforce dest: in_set_takeD simp add: convert_RA_not_write intro!: w_values_no_write_unchanged del: equalityI)
  thus ?thesis using conf redT_acquire by(auto)
qed

lemma if_redT_non_speculative_invar:
  assumes red: "mthr.if.redT s (t, ta) s'"
  and ts_ok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and sc: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)" 
  and vs: "vs_conf P (shr s) vs"
  shows "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
proof -
  let ?s = "λs. (locks s, (λt. map_option (λ((status, x), ln). (x, ln)) (thr s t), shr s), wset s, interrupts s)"
  
  from ts_ok have ts_ok': "ts_ok wfx (thr (?s s)) (shr (?s s))" by(auto intro!: ts_okI dest: ts_okD)
  from vs have vs': "vs_conf P (shr (?s s)) vs" by simp

  from red show ?thesis
  proof(cases)
    case (redT_normal x x' m)
    note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
    from ‹t ⊢ (x, shr s) -ta→i (x', m)›
    show ?thesis 
    proof(cases)
      case (NormalAction X TA X')
      from ‹ta = convert_TA_initial (convert_obs_initial TA)› ‹mthr.if.actions_ok s t ta›
      have "mthr.actions_ok (?s s) t TA"
        by(auto elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)

      with tst NormalAction ‹redT_upd s t ta x' m s'› have "mthr.redT (?s s) (t, TA) (?s s')"
        using map_redT_updTs[of snd "thr s" "⦃ta⦄⇘t⇙"]
        by(auto intro!: mthr.redT.intros simp add: split_def map_prod_def o_def fun_eq_iff)
      moreover note ts_ok' vs'
      moreover from ‹ta = convert_TA_initial (convert_obs_initial TA)› have "⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙" by(auto)
      with sc have "non_speculative P vs (llist_of (map NormalAction ⦃TA⦄⇘o⇙))" by simp
      ultimately have "ts_ok wfx (thr (?s s')) (shr (?s s'))"
        by(auto dest: redT_wfs_non_speculative_invar)
      thus ?thesis using ‹⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙› by(auto intro!: ts_okI dest: ts_okD)
    next
      case InitialThreadAction
      with redT_normal ts_ok' vs show ?thesis
        by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
    next
      case ThreadFinishAction
      with redT_normal ts_ok' vs show ?thesis
        by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
    qed
  next
    case (redT_acquire x ln l)
    thus ?thesis using vs ts_ok by(auto 4 3 intro!: ts_okI dest: ts_okD split: if_split_asm)
  qed
qed

lemma if_redT_non_speculative_vs_conf:
  assumes red: "mthr.if.redT s (t, ta) s'"
  and ts_ok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and sc: "non_speculative P vs (llist_of (take n ⦃ta⦄⇘o⇙))"
  and vs: "vs_conf P (shr s) vs"
  shows "vs_conf P (shr s') (w_values P vs (take n ⦃ta⦄⇘o⇙))"
proof -
  let ?s = "λs. (locks s, (λt. map_option (λ((status, x), ln). (x, ln)) (thr s t), shr s), wset s, interrupts s)"
  
  from ts_ok have ts_ok': "ts_ok wfx (thr (?s s)) (shr (?s s))" by(auto intro!: ts_okI dest: ts_okD)
  from vs have vs': "vs_conf P (shr (?s s)) vs" by simp

  from red show ?thesis
  proof(cases)
    case (redT_normal x x' m)
    note tst = ‹thr s t = ⌊(x, no_wait_locks)⌋›
    from ‹t ⊢ (x, shr s) -ta→i (x', m)›
    show ?thesis 
    proof(cases)
      case (NormalAction X TA X')
      from ‹ta = convert_TA_initial (convert_obs_initial TA)› ‹mthr.if.actions_ok s t ta›
      have "mthr.actions_ok (?s s) t TA"
        by(auto elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)

      with tst NormalAction ‹redT_upd s t ta x' m s'› have "mthr.redT (?s s) (t, TA) (?s s')"
        using map_redT_updTs[of snd "thr s" "⦃ta⦄⇘t⇙"]
        by(auto intro!: mthr.redT.intros simp add: split_def map_prod_def o_def fun_eq_iff)
      moreover note ts_ok' vs'
      moreover from ‹ta = convert_TA_initial (convert_obs_initial TA)› have "⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙" by(auto)
      with sc have "non_speculative P vs (llist_of (take n (map NormalAction ⦃TA⦄⇘o⇙)))" by simp
      ultimately have "vs_conf P (shr (?s s')) (w_values P vs (take n (map NormalAction ⦃TA⦄⇘o⇙)))"
        by(auto dest: redT_wfs_non_speculative_vs_conf)
      thus ?thesis using ‹⦃ta⦄⇘o⇙ = map NormalAction ⦃TA⦄⇘o⇙› by(auto)
    next
      case InitialThreadAction
      with redT_normal vs show ?thesis by(auto simp add: take_Cons')
    next
      case ThreadFinishAction
      with redT_normal vs show ?thesis by(auto simp add: take_Cons')
    qed
  next
    case (redT_acquire x l ln)
    have "w_values P vs (take n (map NormalAction (convert_RA ln :: ('addr, 'thread_id) obs_event list))) = vs"
      by(fastforce simp add: convert_RA_not_write take_Cons' dest: in_set_takeD intro!: w_values_no_write_unchanged del: equalityI)
    thus ?thesis using vs redT_acquire by auto 
  qed
qed

lemma if_RedT_non_speculative_invar:
  assumes red: "mthr.if.RedT s ttas s'"
  and tsok: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and sc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
  and vs: "vs_conf P (shr s) vs"
  shows "ts_ok (init_fin_lift wfx) (thr s') (shr s')" (is ?thesis1)
  and "vs_conf P (shr s') (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))" (is ?thesis2)
using red tsok sc vs unfolding mthr.if.RedT_def
proof(induct arbitrary: vs rule: rtrancl3p_converse_induct')
  case refl
  case 1 thus ?case by -
  case 2 thus ?case by simp
next
  case (step s tta s' ttas)
  obtain t ta where tta: "tta = (t, ta)" by(cases tta)

  case 1
  hence sc1: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
    and sc2: "non_speculative P (w_values P vs ⦃ta⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    unfolding lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def llist_of.simps llist.map(2) lconcat_LCons tta
    by(simp_all add: non_speculative_lappend list_of_lconcat o_def)
  from if_redT_non_speculative_invar[OF step(2)[unfolded tta] _ sc1] if_redT_non_speculative_vs_conf[OF step(2)[unfolded tta], where vs = vs and n="length ⦃ta⦄⇘o⇙"] 1 step.hyps(3)[of "w_values P vs ⦃ta⦄⇘o⇙"] sc2 sc1
  show ?case by simp

  case 2
  hence sc1: "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
    and sc2: "non_speculative P (w_values P vs ⦃ta⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    unfolding lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def llist_of.simps llist.map(2) lconcat_LCons tta
    by(simp_all add: non_speculative_lappend list_of_lconcat o_def)
  from if_redT_non_speculative_invar[OF step(2)[unfolded tta] _ sc1] if_redT_non_speculative_vs_conf[OF step(2)[unfolded tta], where vs = vs and n="length ⦃ta⦄⇘o⇙"] 2 step.hyps(4)[of "w_values P vs ⦃ta⦄⇘o⇙"] sc2 sc1
  show ?case by(simp add: tta o_def)
qed

lemma init_fin_hext_incr:
  assumes "t ⊢ (x, m) -ta→i (x', m')"
  and "init_fin_lift wfx t x m"
  and "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
  and "vs_conf P m vs"
  shows "m ⊴ m'"
using assms
by(cases)(auto intro: red_hext_incr)

lemma init_fin_redT_hext_incr:
  assumes "mthr.if.redT s (t, ta) s'"
  and "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and "non_speculative P vs (llist_of ⦃ta⦄⇘o⇙)"
  and "vs_conf P (shr s) vs"
  shows "shr s ⊴ shr s'"
using assms
by(cases)(auto dest: init_fin_hext_incr ts_okD)

lemma init_fin_RedT_hext_incr:
  assumes "mthr.if.RedT s ttas s'"
  and "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and sc: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
  and vs: "vs_conf P (shr s) vs"
  shows "shr s ⊴ shr s'"
using assms
proof(induction rule: mthr.if.RedT_induct')
  case refl thus ?case by simp
next
  case (step ttas s' t ta s'')
  note ts_ok = ‹ts_ok (init_fin_lift wfx) (thr s) (shr s)›
  from ‹non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas @ [(t, ta)]))))›
  have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    and ns': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of ⦃ta⦄⇘o⇙)"
    by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
  from ts_ok ns have "shr s ⊴ shr s'" 
    using ‹vs_conf P (shr s) vs› by(rule step.IH)
  also have "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
    using ‹mthr.if.RedT s ttas s'› ts_ok ns ‹vs_conf P (shr s) vs›
    by(rule if_RedT_non_speculative_invar)
  with ‹mthr.if.redT s' (t, ta) s''› 
  have "… ⊴ shr s''" using ns'
  proof(rule init_fin_redT_hext_incr)
    from ‹mthr.if.RedT s ttas s'› ts_ok ns ‹vs_conf P (shr s) vs›
    show "vs_conf P (shr s') (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
      by(rule if_RedT_non_speculative_invar)
  qed
  finally show ?case .
qed

lemma init_fin_red_read_typeable:
  assumes "t ⊢ (x, m) -ta→i (x', m')"
  and "init_fin_lift wfx t x m" "NormalAction (ReadMem ad al v) ∈ set ⦃ta⦄⇘o⇙"
  shows "∃T. P,m ⊢ ad@al : T"
using assms
by cases(auto dest: red_read_typeable)

lemma Ex_new_action_for:
  assumes wf: "wf_syscls P"
  and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  and E: "E ∈ ℰ_start f P C M vs status"
  and read: "ra ∈ read_actions E"
  and aloc: "adal ∈ action_loc P E ra"
  and sc: "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))"
  shows "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
proof -
  let ?obs_prefix = "lift_start_obs start_tid start_heap_obs"
  let ?start_state = "init_fin_lift_state status (start_state f P C M vs)"

  from start_state_vs_conf[OF wf]
  have vs_conf_start: "vs_conf P start_heap (w_values P (λ_. {}) (map NormalAction start_heap_obs))" 
    by(simp add: lift_start_obs_def o_def)

  obtain ad al where adal: "adal = (ad, al)" by(cases adal)
  with read aloc obtain v where ra: "action_obs E ra = NormalAction (ReadMem ad al v)"
    and ra_len: "enat ra < llength E"
    by(cases "lnth E ra")(auto elim!: read_actions.cases actionsE)

  from E obtain E'' where E: "E = lappend (llist_of ?obs_prefix) E''"
    and E'': "E'' ∈ mthr.if.ℰ ?start_state" by(auto)
  from E'' obtain E' where E': "E'' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
    and τRuns: "mthr.if.mthr.Runs ?start_state E'" by(rule mthr.if.ℰ.cases)

  have ra_len': "length ?obs_prefix ≤ ra"
  proof(rule ccontr)
    assume "¬ ?thesis"
    hence "ra < length ?obs_prefix" by simp
    moreover with ra ra_len E obtain ra' ad al v 
      where "start_heap_obs ! ra' = ReadMem ad al v" "ra' < length start_heap_obs"
      by(cases ra)(auto simp add: lnth_LCons lnth_lappend1 action_obs_def lift_start_obs_def)
    ultimately have "ReadMem ad al v ∈ set start_heap_obs" unfolding in_set_conv_nth by blast
    thus False by(simp add: start_heap_obs_not_Read)
  qed
  let ?n = "length ?obs_prefix"
  from ra ra_len ra_len' E have "enat (ra - ?n) < llength E''"
    and ra_obs: "action_obs E'' (ra - ?n) = NormalAction (ReadMem ad al v)"
    by(cases "llength E''", auto simp add: action_obs_def lnth_lappend2)
  
  from τRuns ‹enat (ra - ?n) < llength E''› obtain ra_m ra_n t_ra ta_ra 
    where E_ra: "lnth E'' (ra - ?n) = (t_ra, ⦃ta_ra⦄⇘o⇙ ! ra_n)"
    and ra_n: "ra_n < length ⦃ta_ra⦄⇘o⇙" and ra_m: "enat ra_m < llength E'"
    and ra_conv: "ra - ?n = (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + ra_n"
    and E'_ra_m: "lnth E' ra_m = (t_ra, ta_ra)"
    unfolding E' by(rule mthr.if.actions_ℰE_aux)
    
  let ?E' = "ldropn (Suc ra_m) E'"
    
  have E'_unfold: "E' = lappend (ltake (enat ra_m) E') (LCons (lnth E' ra_m) ?E')"
    unfolding ldropn_Suc_conv_ldropn[OF ra_m] by simp
  hence "mthr.if.mthr.Runs ?start_state (lappend (ltake (enat ra_m) E') (LCons (lnth E' ra_m) ?E'))"
    using τRuns by simp
  then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of (ltake (enat ra_m) E')) σ'"
    and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' ra_m) ?E')"
    by(rule mthr.if.mthr.Runs_lappendE) simp
  from τRuns' obtain σ'' where red_ra: "mthr.if.redT σ' (t_ra, ta_ra) σ''"
    and τRuns'': "mthr.if.mthr.Runs σ'' ?E'"
    unfolding E'_ra_m by cases

  from E_ra ra_n ra_obs have "NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙"
    by(auto simp add: action_obs_def in_set_conv_nth)
  with red_ra obtain x_ra x'_ra m'_ra 
    where red'_ra: "mthr.init_fin t_ra (x_ra, shr σ') ta_ra (x'_ra, m'_ra)"
    and σ'': "redT_upd σ' t_ra ta_ra x'_ra m'_ra σ''"
    and ts_t_a: "thr σ' t_ra = ⌊(x_ra, no_wait_locks)⌋"
    by cases auto
  from red'_ra ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙›
  obtain ta'_ra X_ra X'_ra
    where x_ra: "x_ra = (Running, X_ra)"
    and x'_ra: "x'_ra = (Running, X'_ra)"
    and ta_ra: "ta_ra = convert_TA_initial (convert_obs_initial ta'_ra)"
    and red''_ra: "t_ra ⊢ (X_ra, shr σ') -ta'_ra→ (X'_ra, m'_ra)"
    by cases fastforce+

  from ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙› ta_ra 
  have "ReadMem ad al v ∈ set ⦃ta'_ra⦄⇘o⇙" by auto

  from wfx_start have wfx_start: "ts_ok (init_fin_lift wfx) (thr ?start_state) (shr ?start_state)"
    by(simp add: start_state_def split_beta)

  from sc ra_len'
  have "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix))
    (lmap snd (ltake (enat (ra - ?n)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E'))))"
    unfolding E E' by(simp add: ltake_lappend2 lmap_lappend_distrib non_speculative_lappend)
  also note ra_conv also note plus_enat_simps(1)[symmetric]
  also have "enat (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = (∑i<ra_m. enat (length ⦃snd (lnth E' i)⦄⇘o⇙))"
    by(subst sum_comp_morphism[symmetric])(simp_all add: zero_enat_def)
  also have "… = (∑i<ra_m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i))"
    using ra_m by-(rule sum.cong[OF refl], simp add: le_less_trans[where y="enat ra_m"] split_beta)
  also note ltake_plus_conv_lappend also note lconcat_ltake[symmetric]
  also note lmap_lappend_distrib
  also note non_speculative_lappend
  finally have "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (llist_of (list_of (ltake (enat ra_m) E'))))))"
    by(simp add: split_def)
  hence sc': "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat ra_m) E')))))"
    unfolding lmap_lconcat llist.map_comp o_def lconcat_llist_of[symmetric] lmap_llist_of[symmetric]
    by(simp add: split_beta o_def)

  from vs_conf_start have vs_conf_start: "vs_conf P (shr ?start_state) (w_values P (λ_. {}) (map snd ?obs_prefix))"
    by(simp add:init_fin_lift_state_conv_simps start_state_def split_beta lift_start_obs_def o_def)
  with σ_σ' wfx_start sc' have "ts_ok (init_fin_lift wfx) (thr σ') (shr σ')"
    unfolding mthr.if.RedT_def[symmetric] by(rule if_RedT_non_speculative_invar)
  with ts_t_a have "wfx t_ra X_ra (shr σ')" unfolding x_ra by(auto dest: ts_okD)

  with red''_ra ‹ReadMem ad al v ∈ set ⦃ta'_ra⦄⇘o⇙›
  obtain T' where type_adal: "P,shr σ' ⊢ ad@al : T'" by(auto dest: red_read_typeable)

  from sc ra_len' have "non_speculative P (λ_. {}) (llist_of (map snd ?obs_prefix))"
    unfolding E by(simp add: ltake_lappend2 lmap_lappend_distrib non_speculative_lappend)
  with sc' have sc'': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat ra_m) E')))))"
    by(simp add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)

  from σ_σ' red_ra ‹NormalAction (ReadMem ad al v) ∈ set ⦃ta_ra⦄⇘o⇙› sc'' ka
  show "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
    unfolding mthr.if.RedT_def[symmetric]
  proof(cases rule: read_ex_NewHeapElem)
    case (start CTn)
    then obtain n where n: "start_heap_obs ! n = NewHeapElem ad CTn" 
      and len: "n < length start_heap_obs"
      unfolding in_set_conv_nth by blast
    from len have "Suc n ∈ actions E" unfolding E by(simp add: actions_def enat_less_enat_plusI)
    moreover
    from σ_σ' have hext: "start_heap ⊴ shr σ'" unfolding mthr.if.RedT_def[symmetric]
      using wfx_start sc' vs_conf_start
      by(auto dest!: init_fin_RedT_hext_incr simp add: start_state_def split_beta init_fin_lift_state_conv_simps)
    
    from start have "typeof_addr start_heap ad = ⌊CTn⌋"
      by(auto dest: NewHeapElem_start_heap_obsD[OF wf])
    with hext have "typeof_addr (shr σ') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
    with type_adal have "adal ∈ action_loc P E (Suc n)" using n len unfolding E adal
      by cases(auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
    moreover have "is_new_action (action_obs E (Suc n))" using n len unfolding E
      by(simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
    ultimately have "Suc n ∈ new_actions_for P E adal" by(rule new_actionsI)
    moreover have "Suc n < ra" using ra_len' len by(simp)
    ultimately show ?thesis by blast
  next
    case (Red ttas' s'' t' ta' s''' ttas'' CTn)
    
    from ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
    obtain obs obs' where obs: "⦃ta'⦄⇘o⇙ = obs @ NormalAction (NewHeapElem ad CTn) # obs'"
      by(auto dest: split_list)
    
    let ?wa = "?n + length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs"
    have "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas' @ [(t', ta')]))))"
      using obs by simp
    also have "… = llength (lconcat (lmap llist_of (lmap (λ(t, ta). ⦃ta⦄⇘o⇙) (llist_of (ttas' @ [(t', ta')])))))"
      by(simp del: map_map map_append add: lconcat_llist_of)
    also have "… ≤ llength (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (llist_of (ttas' @ (t', ta') # ttas''))))"
      by(auto simp add: o_def split_def intro: lprefix_llist_ofI intro!: lprefix_lconcatI lprefix_llength_le)
    also note len_less = calculation
    have "… ≤ (∑i<ra_m. llength (lnth (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E') i))"
      unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›[symmetric]
      by(simp add: ltake_lmap[symmetric] lconcat_ltake del: ltake_lmap)
    also have "… = enat (∑i<ra_m. length ⦃snd (lnth E' i)⦄⇘o⇙)" using ra_m
      by(subst sum_comp_morphism[symmetric, where h="enat"])(auto intro: sum.cong simp add: zero_enat_def less_trans[where y="enat ra_m"] split_beta)
    also have "… ≤ enat (ra - ?n)" unfolding ra_conv by simp
    finally have enat_length: "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < enat (ra - length (lift_start_obs start_tid start_heap_obs))" .
    then have wa_ra: "?wa < ra" by simp
    with ra_len have "?wa ∈ actions E" by(cases "llength E")(simp_all add: actions_def)
    moreover
    from ‹mthr.if.redT s'' (t', ta') s'''› ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
    obtain x_wa x_wa' where ts''t': "thr s'' t' = ⌊(x_wa, no_wait_locks)⌋"
      and red_wa: "mthr.init_fin t' (x_wa, shr s'') ta' (x_wa', shr s''')"
      by(cases) fastforce+

    from sc'
    have ns: "non_speculative P (w_values P (λ_. {}) (map snd ?obs_prefix)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
      and ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of ⦃ta'⦄⇘o⇙)"
      and ns'': "non_speculative P (w_values P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'')))"
      unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›
      by(simp_all add: lappend_llist_of_llist_of[symmetric] lmap_lappend_distrib non_speculative_lappend del: lappend_llist_of_llist_of)
    from ‹mthr.if.RedT ?start_state ttas' s''› wfx_start ns
    have ts_ok'': "ts_ok (init_fin_lift wfx) (thr s'') (shr s'')"
      using vs_conf_start by(rule if_RedT_non_speculative_invar)
    with ts''t' have wfxt': "wfx t' (snd x_wa) (shr s'')" by(cases x_wa)(auto dest: ts_okD)

    {
      have "action_obs E ?wa = 
        snd (lnth (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')) (length (concat (map (λ(t, y). ⦃y⦄⇘o⇙) ttas')) + length obs))"
        unfolding E E' by(simp add: action_obs_def lnth_lappend2)
      also from enat_length ‹enat (ra - ?n) < llength E''›
      have "… = lnth (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E')) (length (concat (map (λ(t, y). ⦃y⦄⇘o⇙) ttas')) + length obs)"
        unfolding E'
        by(subst lnth_lmap[symmetric, where f=snd])(erule (1) less_trans, simp add: lmap_lconcat llist.map_comp split_def o_def)
      also from len_less
      have "enat (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) < llength (lconcat (ltake (enat ra_m) (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) E')))"
        unfolding ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›[symmetric]
        by(simp add: ltake_lmap[symmetric] del: ltake_lmap)
      note lnth_lconcat_ltake[OF this, symmetric]
      also note ltake_lmap
      also have "ltake (enat ra_m) E' = llist_of (list_of (ltake (enat ra_m) E'))" by(simp)
      also note ‹list_of (ltake (enat ra_m) E') = ttas' @ (t', ta') # ttas''›
      also note lmap_llist_of also have "(λ(t, ta). llist_of ⦃ta⦄⇘o⇙) = llist_of ∘ (λ(t, ta). ⦃ta⦄⇘o⇙)"
        by(simp add: o_def split_def)
      also note map_map[symmetric] also note lconcat_llist_of
      also note lnth_llist_of 
      also have "concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (ttas' @ (t', ta') # ttas'')) ! (length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs) = NormalAction (NewHeapElem ad CTn)"
        by(simp add: nth_append obs)
      finally have "action_obs E ?wa = NormalAction (NewHeapElem ad CTn)" .
    }
    note wa_obs = this
    
    from ‹mthr.if.RedT ?start_state ttas' s''› wfx_start ns vs_conf_start
    have vs'': "vs_conf P (shr s'') (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
      by(rule if_RedT_non_speculative_invar)
    from if_redT_non_speculative_vs_conf[OF ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' _ vs'', of "length ⦃ta'⦄⇘o⇙"] ns'
    have vs''': "vs_conf P (shr s''') (w_values P (w_values P (w_values P (λ_. {}) (map snd ?obs_prefix)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙)"
      by simp
    
    from ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' ns' vs''
    have "ts_ok (init_fin_lift wfx) (thr s''') (shr s''')"
      by(rule if_redT_non_speculative_invar)
    with ‹mthr.if.RedT s''' ttas'' σ'›
    have hext: "shr s''' ⊴ shr σ'" using ns'' vs'''
      by(rule init_fin_RedT_hext_incr)

    from red_wa have "typeof_addr (shr s''') ad = ⌊CTn⌋"
      using wfxt' ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙› by cases(auto dest: red_NewHeapElemD)
    with hext have "typeof_addr (shr σ') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
    with type_adal have "adal ∈ action_loc P E ?wa" using wa_obs unfolding E adal
      by cases (auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
    moreover have "is_new_action (action_obs E ?wa)" using wa_obs by simp
    ultimately have "?wa ∈ new_actions_for P E adal" by(rule new_actionsI)
    thus ?thesis using wa_ra by blast
  qed
qed

lemma executions_sc_hb:
  assumes "wf_syscls P"
  and "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
  and "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  shows
  "executions_sc_hb (ℰ_start f P C M vs status) P"
  (is "executions_sc_hb ?E P")
proof
  fix E a adal a'
  assume "E ∈ ?E" "a ∈ new_actions_for P E adal" "a' ∈ new_actions_for P E adal"
  thus "a = a'" by(rule ℰ_new_actions_for_unique)
next
  fix E ra adal
  assume "E ∈ ?E" "ra ∈ read_actions E" "adal ∈ action_loc P E ra" 
    and "non_speculative P (λ_. {}) (ltake (enat ra) (lmap snd E))"
  with assms show "∃wa. wa ∈ new_actions_for P E adal ∧ wa < ra"
    by(rule Ex_new_action_for)
qed

lemma executions_aux:
  assumes wf: "wf_syscls P"
  and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap" (is "ts_ok wfx (thr ?start_state) _")
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  shows "executions_aux (ℰ_start f P C M vs status) P"
  (is "executions_aux ?ℰ P")
proof
  fix E a adal a'
  assume "E ∈ ?ℰ" "a ∈ new_actions_for P E adal" "a' ∈ new_actions_for P E adal"
  thus "a = a'" by(rule ℰ_new_actions_for_unique)
next
  fix E ws r adal
  assume E: "E ∈ ?ℰ"
    and wf_exec: "P ⊢ (E, ws) √" 
    and read: "r ∈ read_actions E" "adal ∈ action_loc P E r"
    and sc: "⋀a. ⟦a < r; a ∈ read_actions E⟧ ⟹ P,E ⊢ a ↝mrw ws a"

  interpret jmm: executions_sc_hb ?ℰ P
    using wf wfx_start ka by(rule executions_sc_hb)

  from E wf_exec sc
  have "ta_seq_consist P Map.empty (ltake (enat r) (lmap snd E))"
    unfolding ltake_lmap by(rule jmm.ta_seq_consist_mrwI) simp
  hence "non_speculative P (λ_. {}) (ltake (enat r) (lmap snd E))"
    by(rule ta_seq_consist_into_non_speculative) simp
  with wf wfx_start ka E read
  have "∃i. i ∈ new_actions_for P E adal ∧ i < r"
    by(rule Ex_new_action_for)
  thus "∃i<r. i ∈ new_actions_for P E adal" by blast
qed

lemma drf:
  assumes cut_and_update:
    "if.cut_and_update
       (init_fin_lift_state status (start_state f P C M vs))
       (mrw_values P Map.empty (map snd (lift_start_obs start_tid start_heap_obs)))"
    (is "if.cut_and_update ?start_state (mrw_values _ _ (map _ ?start_heap_obs))")
  and wf: "wf_syscls P"
  and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  shows "drf (ℰ_start f P C M vs status) P" (is "drf ?ℰ _")
proof -
  interpret jmm: executions_sc_hb "?ℰ" P
    using wf wfx_start ka by(rule executions_sc_hb)

  let ?n = "length ?start_heap_obs"
  let ?ℰ' = "lappend (llist_of ?start_heap_obs) ` mthr.if.ℰ ?start_state"

  show ?thesis 
  proof
    fix E ws r
    assume E: "E ∈ ?ℰ'"
      and wf: "P ⊢ (E, ws) √"
      and mrw: "⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
    show "∃E'∈?ℰ'. ∃ws'. P ⊢ (E', ws') √ ∧ ltake (enat r) E = ltake (enat r) E' ∧
                           sequentially_consistent P (E', ws') ∧
                           action_tid E r = action_tid E' r ∧ action_obs E r ≈ action_obs E' r ∧
                           (r ∈ actions E ⟶ r ∈ actions E')"
    proof(cases "∃r'. r' ∈ read_actions E ∧ r ≤ r'")
      case False
      have "sequentially_consistent P (E, ws)"
      proof(rule sequentially_consistentI)
        fix a
        assume "a ∈ read_actions E"
        with False have "a < r" by auto
        thus "P,E ⊢ a ↝mrw ws a" using ‹a ∈ read_actions E› by(rule mrw)
      qed
      moreover have "action_obs E r ≈ action_obs E r" by(rule sim_action_refl)
      ultimately show ?thesis using wf E by blast
    next
      case True
      let ?P = "λr'. r' ∈ read_actions E ∧ r ≤ r'"
      let ?r = "Least ?P"
      from True obtain r' where r': "?P r'" by blast
      hence r: "?P ?r" by(rule LeastI)
      {
        fix a
        assume "a < ?r" "a ∈ read_actions E"
        have "P,E ⊢ a ↝mrw ws a"
        proof(cases "a < r")
          case True
          thus ?thesis using ‹a ∈ read_actions E› by(rule mrw)
        next
          case False
          with ‹a ∈ read_actions E› have "?P a" by simp
          hence "?r ≤ a" by(rule Least_le)
          with ‹a < ?r› have False by simp
          thus ?thesis ..
        qed }
      note mrw' = this

      from E obtain E'' where E: "E = lappend (llist_of ?start_heap_obs) E''"
        and E'': "E'' ∈ mthr.if.ℰ ?start_state" by auto

      from E'' obtain E' where E': "E'' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
        and τRuns: "mthr.if.mthr.Runs ?start_state E'"
        by(rule mthr.if.ℰ.cases)

      have r_len: "length ?start_heap_obs ≤ ?r"
      proof(rule ccontr)
        assume "¬ ?thesis"
        hence "?r < length ?start_heap_obs" by simp
        moreover with r E obtain t ad al v where "?start_heap_obs ! ?r = (t, NormalAction (ReadMem ad al v))"
          by(cases "?start_heap_obs ! ?r")(fastforce elim!: read_actions.cases simp add: actions_def action_obs_def lnth_lappend1)
        ultimately have "(t, NormalAction (ReadMem ad al v)) ∈ set ?start_heap_obs" unfolding in_set_conv_nth by blast
        thus False by(auto simp add: start_heap_obs_not_Read)
      qed
      let ?n = "length ?start_heap_obs"
      from r r_len E have r: "?r - ?n ∈ read_actions E''"
        by(fastforce elim!: read_actions.cases simp add: actions_lappend action_obs_def lnth_lappend2 elim: actionsE intro: read_actions.intros)
      
      from r have "?r - ?n ∈ actions E''" by(auto)
      hence "enat (?r - ?n) < llength E''" by(rule actionsE)
      with τRuns obtain r_m r_n t_r ta_r 
        where E_r: "lnth E'' (?r - ?n) = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
        and r_n: "r_n < length ⦃ta_r⦄⇘o⇙" and r_m: "enat r_m < llength E'"
        and r_conv: "?r - ?n = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n"
        and E'_r_m: "lnth E' r_m = (t_r, ta_r)"
        unfolding E' by(rule mthr.if.actions_ℰE_aux)

      let ?E' = "ldropn (Suc r_m) E'"
      let ?r_m_E' = "ltake (enat r_m) E'"
      have E'_unfold: "E' = lappend (ltake (enat r_m) E') (LCons (lnth E' r_m) ?E')"
        unfolding ldropn_Suc_conv_ldropn[OF r_m] by simp
      hence "mthr.if.mthr.Runs ?start_state (lappend ?r_m_E' (LCons (lnth E' r_m) ?E'))"
        using τRuns by simp
      then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?r_m_E') σ'"
        and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' r_m) ?E')"
        by(rule mthr.if.mthr.Runs_lappendE) simp
      from τRuns' obtain σ''' where red_ra: "mthr.if.redT σ' (t_r, ta_r) σ'''"
        and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
        unfolding E'_r_m by cases

      let ?vs = "mrw_values P Map.empty (map snd ?start_heap_obs)"
      { fix a
        assume "enat a < enat ?r"
          and "a ∈ read_actions E"
        have "a < r"
        proof(rule ccontr)
          assume "¬ a < r"
          with ‹a ∈ read_actions E› have "?P a" by simp
          hence "?r ≤ a" by(rule Least_le)
          with ‹enat a < enat ?r› show False by simp
        qed
        hence "P,E ⊢ a ↝mrw ws a" using ‹a ∈ read_actions E› by(rule mrw) }
      with ‹E ∈ ?ℰ'› wf have "ta_seq_consist P Map.empty (lmap snd (ltake (enat ?r) E))"
        by(rule jmm.ta_seq_consist_mrwI)

      hence start_sc: "ta_seq_consist P Map.empty (llist_of (map snd ?start_heap_obs))"
        and "ta_seq_consist P ?vs (lmap snd (ltake (enat (?r - ?n)) E''))"
        using ‹?n ≤ ?r› unfolding E ltake_lappend lmap_lappend_distrib
        by(simp_all add: ta_seq_consist_lappend o_def)

      note this(2) also from r_m
      have r_m_sum_len_eq: "(∑i<r_m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E') i)) = enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)"
        by(subst sum_comp_morphism[symmetric, where h=enat])(auto simp add: zero_enat_def split_def less_trans[where y="enat r_m"] intro: sum.cong)
      hence "ltake (enat (?r - ?n)) E'' = 
            lappend (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E')) 
                    (ltake (enat r_n) (ldrop (enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) E''))"
        unfolding ltake_lmap[symmetric] lconcat_ltake r_conv plus_enat_simps(1)[symmetric] ltake_plus_conv_lappend
        unfolding E' by simp
      finally have "ta_seq_consist P ?vs (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E')))"
        and sc_ta_r: "ta_seq_consist P (mrw_values P ?vs (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))))) (lmap snd (ltake (enat r_n) (ldropn (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) E'')))"
        unfolding lmap_lappend_distrib by(simp_all add: ta_seq_consist_lappend split_def ldrop_enat)
      note this(1) also
      have "lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E')))
            = llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E')))"
        unfolding lmap_lconcat llist.map_comp o_def split_def lconcat_llist_of[symmetric] map_map lmap_llist_of[symmetric]
        by simp
      finally have "ta_seq_consist P ?vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E'))))" .
      from if.sequential_completion[OF cut_and_update ta_seq_consist_convert_RA σ_σ'[folded mthr.if.RedT_def] this red_ra]
      obtain ta' ttas' 
        where "mthr.if.mthr.Runs σ' (LCons (t_r, ta') ttas')"
        and sc: "ta_seq_consist P (mrw_values P Map.empty (map snd ?start_heap_obs)) 
                   (lconcat (lmap (λ(t, ta). llist_of ⦃ta⦄⇘o⇙) (lappend (llist_of (list_of ?r_m_E')) (LCons (t_r, ta') ttas'))))"
          and eq_ta: "eq_upto_seq_inconsist P ⦃ta_r⦄⇘o⇙ ⦃ta'⦄⇘o⇙ (mrw_values P ?vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of ?r_m_E'))))"
          by blast

      let ?E_sc' = "lappend (llist_of (list_of ?r_m_E')) (LCons (t_r, ta') ttas')"
      let ?E_sc'' = "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?E_sc')"
      let ?E_sc = "lappend (llist_of ?start_heap_obs) ?E_sc''"

      from σ_σ' ‹mthr.if.mthr.Runs σ' (LCons (t_r, ta') ttas')›
      have "mthr.if.mthr.Runs ?start_state ?E_sc'" by(rule mthr.if.mthr.Trsys_into_Runs)
      hence "?E_sc'' ∈ mthr.if.ℰ ?start_state" by(rule mthr.if.ℰ.intros)
      hence "?E_sc ∈ ?ℰ" by(rule imageI)
      moreover from ‹?E_sc'' ∈ mthr.if.ℰ ?start_state›
      have tsa_ok: "thread_start_actions_ok ?E_sc" by(rule thread_start_actions_ok_init_fin) 
        
      from sc have "ta_seq_consist P Map.empty (lmap snd ?E_sc)"
        by(simp add: lmap_lappend_distrib o_def lmap_lconcat llist.map_comp split_def ta_seq_consist_lappend start_sc)
      from ta_seq_consist_imp_sequentially_consistent[OF tsa_ok jmm.ℰ_new_actions_for_fun[OF ‹?E_sc ∈ ?ℰ›] this]
      obtain ws_sc where "sequentially_consistent P (?E_sc, ws_sc)"
        and "P ⊢ (?E_sc, ws_sc) √" unfolding start_heap_obs_def[symmetric] by iprover
      moreover {
        have enat_sum_r_m_eq: "enat (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) = llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))"
          by(auto intro: sum.cong simp add: less_trans[OF _ r_m] lnth_ltake llength_lconcat_lfinite_conv_sum sum_comp_morphism[symmetric, where h=enat] zero_enat_def[symmetric] split_beta)
        also have "… ≤ llength E''" unfolding E'
          by(blast intro: lprefix_llength_le lprefix_lconcatI lmap_lprefix)
        finally have r_m_E: "ltake (enat (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙))) E = ltake (enat (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙))) ?E_sc"
          by(simp add: ltake_lappend lappend_eq_lappend_conv lmap_lappend_distrib r_m_sum_len_eq ltake_lmap[symmetric] min_def zero_enat_def[symmetric] E E' lconcat_ltake ltake_all del: ltake_lmap)

        have drop_r_m_E: "ldropn (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) E = lappend (llist_of (map (Pair t_r) ⦃ta_r⦄⇘o⇙)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ldropn (Suc r_m) E')))"
          (is "_ = ?drop_r_m_E") using E'_r_m unfolding E E'
          by(subst (2) E'_unfold)(simp add: ldropn_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric])

        have drop_r_m_E_sc: "ldropn (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) ?E_sc =
          lappend (llist_of (map (Pair t_r) ⦃ta'⦄⇘o⇙)) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas'))"
          by(simp add: ldropn_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric])

        let ?vs_r_m = "mrw_values P ?vs (map snd (list_of (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ?r_m_E'))))"
        note sc_ta_r also
        from drop_r_m_E have "ldropn (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) E'' = ?drop_r_m_E"
          unfolding E by(simp add: ldropn_lappend2)
        also have "lmap snd (ltake (enat r_n) …) = llist_of (take r_n ⦃ta_r⦄⇘o⇙)" using r_n
          by(simp add: ltake_lappend lmap_lappend_distrib ltake_lmap[symmetric] take_map o_def zero_enat_def[symmetric] del: ltake_lmap)
        finally have sc_ta_r: "ta_seq_consist P ?vs_r_m (llist_of (take r_n ⦃ta_r⦄⇘o⇙))" .
        note eq_ta
        also have "⦃ta_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙ @ drop r_n ⦃ta_r⦄⇘o⇙" by simp
        finally have "eq_upto_seq_inconsist P (take r_n ⦃ta_r⦄⇘o⇙ @ drop r_n ⦃ta_r⦄⇘o⇙) ⦃ta'⦄⇘o⇙ ?vs_r_m"
          by(simp add: list_of_lconcat split_def o_def map_concat)
        from eq_upto_seq_inconsist_appendD[OF this sc_ta_r]
        have r_n': "r_n ≤ length ⦃ta'⦄⇘o⇙"
          and take_r_n_eq: "take r_n ⦃ta'⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
          and eq_r_n: "eq_upto_seq_inconsist P (drop r_n ⦃ta_r⦄⇘o⇙) (drop r_n ⦃ta'⦄⇘o⇙) (mrw_values P ?vs_r_m (take r_n ⦃ta_r⦄⇘o⇙))"
          using r_n by(simp_all add: min_def)
        from r_conv ‹?n ≤ ?r› have r_conv': "?r = (?n + (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙)) + r_n" by simp
        from r_n' r_n take_r_n_eq r_m_E drop_r_m_E drop_r_m_E_sc
        have take_r'_eq: "ltake (enat ?r) E = ltake (enat ?r) ?E_sc" unfolding r_conv'
          apply(subst (1 2) plus_enat_simps(1)[symmetric])
          apply(subst (1 2) ltake_plus_conv_lappend)
          apply(simp add: lappend_eq_lappend_conv ltake_lappend1 ldrop_enat take_map)
          done
        hence take_r_eq: "ltake (enat r) E = ltake (enat r) ?E_sc"
          by(rule ltake_eq_ltake_antimono)(simp add: ‹?P ?r›)
        
        from eq_r_n Cons_nth_drop_Suc[OF r_n, symmetric]
        have "drop r_n ⦃ta'⦄⇘o⇙ ≠ []" by(auto simp add: eq_upto_seq_inconsist_simps)
        hence r_n': "r_n < length ⦃ta'⦄⇘o⇙" by simp
        hence eq_r_n: "⦃ta_r⦄⇘o⇙ ! r_n ≈ ⦃ta'⦄⇘o⇙ ! r_n"
          using eq_r_n Cons_nth_drop_Suc[OF r_n, symmetric] Cons_nth_drop_Suc[OF r_n', symmetric]
          by(simp add: eq_upto_seq_inconsist_simps split: action.split_asm obs_event.split_asm if_split_asm)
        obtain tid_eq: "action_tid E r = action_tid ?E_sc r" 
          and obs_eq: "action_obs E r ≈ action_obs ?E_sc r"
        proof(cases "r < ?r")
          case True
          { from True have "action_tid E r = action_tid (ltake (enat ?r) E) r"
              by(simp add: action_tid_def lnth_ltake)
            also note take_r'_eq
            also have "action_tid (ltake (enat ?r) ?E_sc) r = action_tid ?E_sc r"
              using True by(simp add: action_tid_def lnth_ltake)
            finally have "action_tid E r = action_tid ?E_sc r" . }
          moreover
          { from True have "action_obs E r = action_obs (ltake (enat ?r) E) r"
              by(simp add: action_obs_def lnth_ltake)
            also note take_r'_eq
            also have "action_obs (ltake (enat ?r) ?E_sc) r = action_obs ?E_sc r"
              using True by(simp add: action_obs_def lnth_ltake)
            finally have "action_obs E r ≈ action_obs ?E_sc r" by simp }
          ultimately show thesis by(rule that)
        next
          case False
          with ‹?P ?r› have r_eq: "r = ?r" by simp
          hence "lnth E r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)" using E_r r_conv' E by(simp add: lnth_lappend2)
          moreover have "lnth ?E_sc r = (t_r, ⦃ta'⦄⇘o⇙ ! r_n)" using ‹?n ≤ ?r› r_n'
            by(subst r_eq)(simp add: r_conv lnth_lappend2 lmap_lappend_distrib enat_sum_r_m_eq[symmetric] lnth_lappend1 del: length_lift_start_obs)
          ultimately have "action_tid E r = action_tid ?E_sc r" "action_obs E r ≈ action_obs ?E_sc r"
            using eq_r_n by(simp_all add: action_tid_def action_obs_def)
          thus thesis by(rule that)
        qed
        
        have "enat r < enat ?n + llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend ?r_m_E' (LCons (t_r, ta') LNil))))"
          using ‹?P ?r› r_n' unfolding lmap_lappend_distrib
          by(simp add: enat_sum_r_m_eq[symmetric] r_conv')
        also have "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend ?r_m_E' (LCons (t_r, ta') LNil)))) ≤ llength ?E_sc''"
          by(rule lprefix_llength_le[OF lprefix_lconcatI])(simp add: lmap_lprefix)
        finally have "r ∈ actions ?E_sc" by(simp add: actions_def add_left_mono)
        note this tid_eq obs_eq take_r_eq }
      ultimately show ?thesis by blast
    qed
  qed(rule ℰ_new_actions_for_unique)
qed

lemma sc_legal:
  assumes hb_completion:
    "if.hb_completion (init_fin_lift_state status (start_state f P C M vs)) (lift_start_obs start_tid start_heap_obs)"
    (is "if.hb_completion ?start_state ?start_heap_obs")
  and wf: "wf_syscls P"
  and wfx_start: "ts_ok wfx (thr (start_state f P C M vs)) start_heap"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) vs) ⊆ allocated start_heap"
  shows "sc_legal (ℰ_start f P C M vs status) P"
  (is "sc_legal ?ℰ P")
proof -
  interpret jmm: executions_sc_hb ?ℰ P
    using wf wfx_start ka by(rule executions_sc_hb)

  interpret jmm: executions_aux ?ℰ P
    using wf wfx_start ka by(rule executions_aux)

  show ?thesis
  proof
    fix E ws r
    assume E: "E ∈ ?ℰ" and wf_exec: "P ⊢ (E, ws) √"
      and mrw: "⋀a. ⟦a < r; a ∈ read_actions E⟧ ⟹ P,E ⊢ a ↝mrw ws a"


    from E obtain E'' where E: "E = lappend (llist_of ?start_heap_obs) E''"
      and E'': "E'' ∈ mthr.if.ℰ ?start_state" by auto
    
    from E'' obtain E' where E': "E'' = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) E')"
      and τRuns: "mthr.if.mthr.Runs ?start_state E'"
      by(rule mthr.if.ℰ.cases)
    
    show "∃E'∈?ℰ. ∃ws'. P ⊢ (E', ws') √ ∧ ltake (enat r) E = ltake (enat r) E' ∧
                         (∀a∈read_actions E'. if a < r then ws' a = ws a else P,E' ⊢ ws' a ≤hb a) ∧
                         action_tid E' r = action_tid E r ∧
                         (if r ∈ read_actions E then sim_action else (=)) (action_obs E' r) (action_obs E r) ∧
                         (r ∈ actions E ⟶ r ∈ actions E')"
      (is "∃E'∈?ℰ. ∃ws'. _ ∧ ?same E' ∧ ?read E' ws' ∧ ?tid E' ∧ ?obs E' ∧ ?actions E'")
    proof(cases "r < length ?start_heap_obs")
      case True

      from if.hb_completion_Runs[OF hb_completion ta_hb_consistent_convert_RA]
      obtain ttas where Runs: "mthr.if.mthr.Runs ?start_state ttas"
        and hb: "ta_hb_consistent P ?start_heap_obs (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
        by blast

      from Runs have ℰ: "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas) ∈ mthr.if.ℰ ?start_state"
        by(rule mthr.if.ℰ.intros)
        
      let ?E = "lappend (llist_of ?start_heap_obs) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas))"
      from ℰ have E': "?E ∈ ?ℰ" by blast

      from ℰ have tsa: "thread_start_actions_ok ?E" by(rule thread_start_actions_ok_init_fin)

      from start_heap_obs_not_Read
      have ws: "is_write_seen P (llist_of (lift_start_obs start_tid start_heap_obs)) ws"
        by(unfold in_set_conv_nth)(rule is_write_seenI, auto simp add: action_obs_def actions_def lift_start_obs_def lnth_LCons elim!: read_actions.cases split: nat.split_asm)

      with hb tsa
      have "∃ws'. P ⊢ (?E, ws') √ ∧
                  (∀n. n ∈ read_actions ?E ⟶ length ?start_heap_obs ≤ n ⟶ P,?E ⊢ ws' n ≤hb n) ∧
                  (∀n<length ?start_heap_obs. ws' n = ws n)"
        by(rule ta_hb_consistent_Read_hb)(rule jmm.ℰ_new_actions_for_fun[OF E'])
      then obtain ws' where wf_exec': "P ⊢ (?E, ws') √" 
        and read_hb: "⋀n. ⟦ n ∈ read_actions ?E; length ?start_heap_obs ≤ n ⟧ ⟹ P,?E ⊢ ws' n ≤hb n"
        and same: "⋀n. n<length ?start_heap_obs ⟹ ws' n = ws n" by blast

      from True have "?same ?E" unfolding E by(simp add: ltake_lappend1)
      moreover {
        fix a
        assume a: "a ∈ read_actions ?E"
        have "if a < r then ws' a = ws a else P,?E ⊢ ws' a ≤hb a"
        proof(cases "a < length ?start_heap_obs")
          case True
          with a have False using start_heap_obs_not_Read
            by cases(auto simp add: action_obs_def actions_def lnth_lappend1 lift_start_obs_def lnth_LCons in_set_conv_nth split: nat.split_asm)
          thus ?thesis ..
        next
          case False
          with read_hb[of a] True a show ?thesis by auto
        qed }
      hence "?read ?E ws'" by blast
      moreover from True E have "?tid ?E" by(simp add: action_tid_def lnth_lappend1)
      moreover from True E have "?obs ?E" by(simp add: action_obs_def lnth_lappend1)
      moreover from True have "?actions ?E" by(simp add: actions_def enat_less_enat_plusI)
      ultimately show ?thesis using E' wf_exec' by blast
    next
      case False
      hence r: "length ?start_heap_obs ≤ r" by simp

      show ?thesis
      proof(cases "enat r < llength E")
        case False
        then obtain "?same E" "?read E ws" "?tid E" "?obs E" "?actions E"
          by(cases "llength E")(fastforce elim!: read_actions.cases simp add: actions_def split: if_split_asm)+
        with wf_exec ‹E ∈ ?ℰ› show ?thesis by blast
      next
        case True
        note r' = this

        let ?r = "r - length ?start_heap_obs"
        from E r r' have "enat ?r < llength E''" by(cases "llength E''")(auto)
        with τRuns obtain r_m r_n t_r ta_r 
          where E_r: "lnth E'' ?r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
          and r_n: "r_n < length ⦃ta_r⦄⇘o⇙" and r_m: "enat r_m < llength E'"
          and r_conv: "?r = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n"
          and E'_r_m: "lnth E' r_m = (t_r, ta_r)"
          unfolding E' by(rule mthr.if.actions_ℰE_aux)

        let ?E' = "ldropn (Suc r_m) E'"
        let ?r_m_E' = "ltake (enat r_m) E'"
        have E'_unfold: "E' = lappend (ltake (enat r_m) E') (LCons (lnth E' r_m) ?E')"
          unfolding ldropn_Suc_conv_ldropn[OF r_m] by simp
        hence "mthr.if.mthr.Runs ?start_state (lappend ?r_m_E' (LCons (lnth E' r_m) ?E'))"
          using τRuns by simp
        then obtain σ' where σ_σ': "mthr.if.mthr.Trsys ?start_state (list_of ?r_m_E') σ'"
          and τRuns': "mthr.if.mthr.Runs σ' (LCons (lnth E' r_m) ?E')"
          by(rule mthr.if.mthr.Runs_lappendE) simp
        from τRuns' obtain σ''' where red_ra: "mthr.if.redT σ' (t_r, ta_r) σ'''"
          and τRuns'': "mthr.if.mthr.Runs σ''' ?E'"
          unfolding E'_r_m by cases

        let ?vs = "mrw_values P Map.empty (map snd ?start_heap_obs)"
        from ‹E ∈ ?ℰ› wf_exec have "ta_seq_consist P Map.empty (lmap snd (ltake (enat r) E))"
          by(rule jmm.ta_seq_consist_mrwI)(simp add: mrw)
        hence ns: "non_speculative P (λ_. {}) (lmap snd (ltake (enat r) E))"
          by(rule ta_seq_consist_into_non_speculative) simp
        also note E also note ltake_lappend2 also note E'
        also note E'_unfold also note lmap_lappend_distrib also note lmap_lappend_distrib 
        also note lconcat_lappend also note llist.map(2) also note E'_r_m also note prod.simps(2)
        also note ltake_lappend2 also note lconcat_LCons also note ltake_lappend1
        also note non_speculative_lappend also note lmap_lappend_distrib also note non_speculative_lappend
        also have "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E')) = 
                  llist_of (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))"
          by(simp add: lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)
        ultimately
        have "non_speculative P (λ_. {}) (lmap snd (llist_of ?start_heap_obs))"
          and "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs)) 
                 (lmap snd (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (ltake (enat r_m) E'))))"
          and ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?start_heap_obs)) (map snd (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))))
               (lmap snd (ltake (enat r_n) (llist_of (map (Pair t_r) ⦃ta_r⦄⇘o⇙))))"
          using r r_conv r_m r_n
          by(simp_all add: length_concat o_def split_def sum_list_sum_nth length_list_of_conv_the_enat less_min_eq1 atLeast0LessThan lnth_ltake split: if_split_asm cong: sum.cong_simp)
        hence ns: "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs)) 
                     (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E')))))"
          unfolding lconcat_llist_of[symmetric] lmap_lconcat lmap_llist_of[symmetric] llist.map_comp o_def split_def
          by(simp)

        from ns'
        have ns': "non_speculative P (w_values P (w_values P (λ_. {}) (map snd ?start_heap_obs))  (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))))) (llist_of (take r_n ⦃ta_r⦄⇘o⇙))"
          unfolding map_concat map_map by(simp add: take_map[symmetric] o_def split_def)

        let ?hb = "λta'_r  :: ('addr, 'thread_id, status × 'x, 'heap, 'addr, ('addr, 'thread_id) obs_event action) thread_action. 
             ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙)))"
        let ?sim = "λta'_r. (if ∃ad al v. ⦃ta_r⦄⇘o⇙ ! r_n = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta_r⦄⇘o⇙ ! r_n) (⦃ta'_r⦄⇘o⇙ ! r_n)"

        from red_ra obtain ta'_r σ''''
          where red_ra': "mthr.if.redT σ' (t_r, ta'_r) σ''''"
          and eq: "take r_n ⦃ta'_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
          and hb: "?hb ta'_r"
          and r_n': "r_n < length ⦃ta'_r⦄⇘o⇙"
          and sim: "?sim ta'_r"
        proof(cases)
          case (redT_normal x x' m')
          note tst = ‹thr σ' t_r = ⌊(x, no_wait_locks)⌋›
            and red = ‹t_r ⊢ (x, shr σ') -ta_r→i (x', m')›
            and aok = ‹mthr.if.actions_ok σ' t_r ta_r›
            and σ''' = ‹redT_upd σ' t_r ta_r x' m' σ'''›
          from if.hb_completionD[OF hb_completion σ_σ'[folded mthr.if.RedT_def] ns tst red aok ns'] r_n
          obtain ta'_r x'' m''
            where red': "t_r ⊢ (x, shr σ') -ta'_r→i (x'', m'')"
            and aok': "mthr.if.actions_ok σ' t_r ta'_r"
            and eq': "take r_n ⦃ta'_r⦄⇘o⇙ = take r_n ⦃ta_r⦄⇘o⇙"
            and hb: "?hb ta'_r" 
            and r_n': "r_n < length ⦃ta'_r⦄⇘o⇙"
            and sim: "?sim ta'_r" by blast
          from redT_updWs_total[of t_r "wset σ'" "⦃ta'_r⦄⇘w⇙"]
          obtain σ'''' where "redT_upd σ' t_r ta'_r x'' m'' σ''''" by fastforce
          with red' tst aok' have "mthr.if.redT σ' (t_r, ta'_r) σ''''" ..
          thus thesis using eq' hb r_n' sim by(rule that)
        next
          case (redT_acquire x n ln)
          hence "?hb ta_r" using set_convert_RA_not_Read[where ln=ln]
            by -(rule ta_hb_consistent_not_ReadI, fastforce simp del: set_convert_RA_not_Read dest!: in_set_dropD)
          with red_ra r_n show ?thesis by(auto intro: that)
        qed
        from hb
        have "non_speculative P (w_values P (λ_. {}) (map snd (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)))) (lmap snd (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))))"
          by(rule ta_hb_consistent_into_non_speculative)
        with ns' eq[symmetric] have "non_speculative P (w_values P (λ_. {}) (map snd (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E')))))) (llist_of (map snd (map (Pair t_r) ⦃ta'_r⦄⇘o⇙)))"
          by(subst append_take_drop_id[where xs="⦃ta'_r⦄⇘o⇙" and n=r_n, symmetric])(simp add: o_def map_concat split_def lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: append_take_drop_id lappend_llist_of_llist_of)
        with ns have ns'': "non_speculative P (w_values P (λ_. {}) (map snd ?start_heap_obs)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)]))))"
          unfolding lconcat_llist_of[symmetric] map_append lappend_llist_of_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp
          by(simp add: o_def split_def non_speculative_lappend list_of_lconcat map_concat)
        from σ_σ' red_ra' have "mthr.if.RedT ?start_state (list_of ?r_m_E' @ [(t_r, ta'_r)]) σ''''"
          unfolding mthr.if.RedT_def ..
        with hb_completion
        have hb_completion': "if.hb_completion σ'''' (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)])))"
          using ns'' by(rule if.hb_completion_shift)
        from if.hb_completion_Runs[OF hb_completion' ta_hb_consistent_convert_RA]
        obtain ttas' where Runs': "mthr.if.mthr.Runs σ'''' ttas'"
          and hb': "ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E') @ [(t_r, ta'_r)]))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas'))"
          by blast

        let ?E = "lappend (llist_of ?start_heap_obs) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend (ltake (enat r_m) E') (LCons (t_r, ta'_r) ttas'))))"

        have ℰ: "lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) (lappend (ltake (enat r_m) E') (LCons (t_r, ta'_r) ttas'))) ∈ mthr.if.ℰ ?start_state"
          by(subst (4) llist_of_list_of[symmetric])(simp, blast intro: mthr.if.ℰ.intros mthr.if.mthr.Trsys_into_Runs σ_σ' mthr.if.mthr.Runs.Step red_ra' Runs')
        hence ℰ': "?E ∈ ?ℰ" by blast

        from ℰ have tsa: "thread_start_actions_ok ?E" by(rule thread_start_actions_ok_init_fin)
        also let ?E' = "lappend (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙))) (lappend (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas')))"
        have "?E = ?E'"
          using eq[symmetric]
          by(simp add: lmap_lappend_distrib lappend_assoc lappend_llist_of_llist_of[symmetric] lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)(simp add: lappend_assoc[symmetric] lmap_lappend_distrib[symmetric] map_append[symmetric] lappend_llist_of_llist_of del: map_append)
        finally have tsa': "thread_start_actions_ok ?E'" .

        from hb hb' eq[symmetric]
        have HB: "ta_hb_consistent P (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) (lappend (llist_of (map (Pair t_r) (drop r_n ⦃ta'_r⦄⇘o⇙))) (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) ⦃ta⦄⇘o⇙)) ttas')))"
          by -(rule ta_hb_consistent_lappendI, simp_all add: take_map[symmetric] drop_map[symmetric])
        
        define EE where "EE = llist_of (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙))"

        from r r_conv have r_conv': "r = (∑i<r_m. length ⦃snd (lnth E' i)⦄⇘o⇙) + r_n + length ?start_heap_obs" by auto
        hence len_EE: "llength EE = enat r" using r_m r_n
          by(auto simp add: EE_def length_concat sum_list_sum_nth atLeast0LessThan lnth_ltake less_min_eq1 split_def min_def length_list_of_conv_the_enat cong: sum.cong_simp)
        
        from r_conv r_m
        have r_conv3: "llength (lconcat (lmap (λx. llist_of (map (Pair (fst x)) ⦃snd x⦄⇘o⇙)) (ltake (enat r_m) E'))) = enat (r - Suc (length start_heap_obs) - r_n)" 
          apply(simp add: llength_lconcat_lfinite_conv_sum lnth_ltake cong: sum.cong_simp conj_cong)
          apply(auto simp add: sum_comp_morphism[where h=enat, symmetric] zero_enat_def less_trans[where y="enat r_m"] intro: sum.cong)
          done            

        have is_ws: "is_write_seen P EE ws"
        proof(rule is_write_seenI)
          fix a ad al v
          assume a: "a ∈ read_actions EE"
            and a_obs: "action_obs EE a = NormalAction (ReadMem ad al v)"
          from a have a_r: "a < r" by cases(simp add: len_EE actions_def)

          from r E'_r_m r_m r_n r_conv3
          have eq: "ltake (enat r) EE = ltake (enat r) E"
            unfolding E E' EE_def
            apply(subst (2) E'_unfold)
            apply(simp add: ltake_lappend2 lappend_llist_of_llist_of[symmetric] lappend_eq_lappend_conv lmap_lappend_distrib lconcat_llist_of[symmetric] o_def split_def lmap_llist_of[symmetric] del: lappend_llist_of_llist_of lmap_llist_of)
            apply(subst ltake_lappend1)
            defer
            apply(simp add: ltake_lmap[symmetric] take_map[symmetric] ltake_llist_of[symmetric] del: ltake_lmap ltake_llist_of)
            apply(auto simp add: min_def)
            done
          hence sim: "ltake (enat r) EE [≈] ltake (enat r) E" by(rule eq_into_sim_actions)
          
          from a sim have a': "a ∈ read_actions E"
            by(rule read_actions_change_prefix)(simp add: a_r)
          from action_obs_change_prefix_eq[OF eq, of a] a_r a_obs
          have a_obs': "action_obs E a = NormalAction (ReadMem ad al v)" by simp
          
          have a_mrw: "P,E ⊢ a ↝mrw ws a" using a_r a' by(rule mrw)
          with ‹E ∈ ?ℰ› wf_exec have ws_a_a: "ws a < a"
            by(rule jmm.mrw_before)(auto intro: a_r less_trans mrw)
          hence [simp]: "ws a < r" using a_r by simp

          from wf_exec have ws: "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
          from is_write_seenD[OF this a' a_obs']
          have "ws a ∈ write_actions E"
            and "(ad, al) ∈ action_loc P E (ws a)"
            and "value_written P E (ws a) (ad, al) = v"
            and "¬ P,E ⊢ a ≤hb ws a"
            and "is_volatile P al ⟹ ¬ P,E ⊢ a ≤so ws a"
            and between: "⋀a'. ⟦ a' ∈ write_actions E; (ad, al) ∈ action_loc P E a'; 
                        P,E ⊢ ws a ≤hb a' ∧ P,E ⊢ a' ≤hb a ∨ is_volatile P al ∧ P,E ⊢ ws a ≤so a' ∧ P,E ⊢ a' ≤so a ⟧
                      ⟹ a' = ws a" by simp_all

          from ‹ws a ∈ write_actions E› sim[symmetric]
          show "ws a ∈ write_actions EE" by(rule write_actions_change_prefix) simp
          
          from action_loc_change_prefix[OF sim, of "ws a" P] ‹(ad, al) ∈ action_loc P E (ws a)›
          show "(ad, al) ∈ action_loc P EE (ws a)" by(simp)

          from value_written_change_prefix[OF eq, of "ws a" P] ‹value_written P E (ws a) (ad, al) = v›
          show "value_written P EE (ws a) (ad, al) = v" by simp
          
           from wf_exec have tsa_E: "thread_start_actions_ok E"
              by(rule wf_exec_thread_start_actions_okD)

          from ‹¬ P,E ⊢ a ≤hb ws a› show "¬ P,EE ⊢ a ≤hb ws a"
          proof(rule contrapos_nn)
            assume "P,EE ⊢ a ≤hb ws a"
            thus "P,E ⊢ a ≤hb ws a" using tsa_E sim
              by(rule happens_before_change_prefix)(simp_all add: a_r)
          qed

          { assume "is_volatile P al"
            hence "¬ P,E ⊢ a ≤so ws a" by fact
            thus "¬ P,EE ⊢ a ≤so ws a"
              by(rule contrapos_nn)(rule sync_order_change_prefix[OF _ sim], simp_all add: a_r) }
          
          fix a'
          assume "a' ∈ write_actions EE" "(ad, al) ∈ action_loc P EE a'"
          moreover
          hence [simp]: "a' < r" by cases(simp add: actions_def len_EE)
          ultimately have a': "a' ∈ write_actions E" "(ad, al) ∈ action_loc P E a'"
            using sim action_loc_change_prefix[OF sim, of a' P]
            by(auto intro: write_actions_change_prefix)
          { assume "P,EE ⊢ ws a ≤hb a'" "P,EE ⊢ a' ≤hb a"
            hence "P,E ⊢ ws a ≤hb a'" "P,E ⊢ a' ≤hb a"
              using tsa_E sim a_r by(auto elim!: happens_before_change_prefix)
            with between[OF a'] show "a' = ws a" by simp }
          { assume "is_volatile P al " "P,EE ⊢ ws a ≤so a'" "P,EE ⊢ a' ≤so a"
            with sim a_r between[OF a'] show "a' = ws a"
              by(fastforce elim: sync_order_change_prefix intro!: disjI2 del: disjCI) }
        qed

        with HB tsa'
        have "∃ws'. P ⊢ (?E', ws') √ ∧
                    (∀n. n ∈ read_actions ?E' ⟶ length (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) ≤ n ⟶ P,?E' ⊢ ws' n ≤hb n) ∧
                    (∀n<length (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)). ws' n = ws n)"
          unfolding EE_def
          by(rule ta_hb_consistent_Read_hb)(rule jmm.ℰ_new_actions_for_fun[OF ℰ'[unfolded ‹?E = ?E'›]])
        also have r_conv'': "length (?start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (list_of (ltake (enat r_m) E'))) @ map (Pair t_r) (take r_n ⦃ta_r⦄⇘o⇙)) = r"
          using r_n r_m unfolding r_conv'
          by(auto simp add: length_concat sum_list_sum_nth atLeast0LessThan lnth_ltake split_def o_def less_min_eq1 min_def length_list_of_conv_the_enat cong: sum.cong_simp)
        finally obtain ws' where wf_exec': "P ⊢ (?E', ws') √" 
          and read_hb: "⋀n. ⟦ n ∈ read_actions ?E'; r ≤ n ⟧ ⟹ P,?E' ⊢ ws' n ≤hb n"
          and read_same: "⋀n. n < r ⟹ ws' n = ws n" by blast

        have "?same ?E'"
          apply(subst ltake_lappend1, simp add: r_conv''[symmetric] length_list_of_conv_the_enat)
          unfolding E E' lappend_llist_of_llist_of[symmetric]
          apply(subst (1 2) ltake_lappend2, simp add: r[simplified])
          apply(subst lappend_eq_lappend_conv, simp)
          apply safe
          apply(subst E'_unfold)
          unfolding lmap_lappend_distrib 
          apply(subst lconcat_lappend, simp)
          apply(subst lconcat_llist_of[symmetric])
          apply(subst (3) lmap_llist_of[symmetric])
          apply(subst (3) lmap_llist_of[symmetric])
          apply(subst llist.map_comp)
          apply(simp only: split_def o_def)
          apply(subst llist_of_list_of, simp)
          apply(subst (1 2) ltake_lappend2, simp add: r_conv3)
          apply(subst lappend_eq_lappend_conv, simp)
          apply safe
          unfolding llist.map(2) lconcat_LCons E'_r_m snd_conv fst_conv take_map
          apply(subst ltake_lappend1)
           defer
           apply(subst append_take_drop_id[where xs="⦃ta_r⦄⇘o⇙" and n=r_n, symmetric])
           unfolding map_append lappend_llist_of_llist_of[symmetric]
           apply(subst ltake_lappend1)
            using r_n
            apply(simp add: min_def r_conv3)
           apply(rule refl)
          apply(simp add: r_conv3)
          using r_n by arith

        moreover {
          fix a
          assume "a ∈ read_actions ?E'"
          with read_hb[of a] read_same[of a]
          have "if a < r then ws' a = ws a else P,?E' ⊢ ws' a ≤hb a" by simp }
        hence "?read ?E' ws'" by blast
        moreover from r_m r_n r_n'
        have E'_r: "lnth ?E' r = (t_r, ⦃ta'_r⦄⇘o⇙ ! r_n)" unfolding r_conv'
          by(auto simp add: lnth_lappend nth_append length_concat sum_list_sum_nth atLeast0LessThan split_beta lnth_ltake less_min_eq1 length_list_of_conv_the_enat cong: sum.cong_simp)
        from E_r r have E_r: "lnth E r = (t_r, ⦃ta_r⦄⇘o⇙ ! r_n)"
          unfolding E by(simp add: lnth_lappend)
        have "r ∈ read_actions E ⟷ (∃ad al v. ⦃ta_r⦄⇘o⇙ ! r_n = NormalAction (ReadMem ad al v))" using True
          by(auto elim!: read_actions.cases simp add: action_obs_def E_r actions_def intro!: read_actions.intros)
        with sim E'_r E_r have "?tid ?E'" "?obs ?E'"
          by(auto simp add: action_tid_def action_obs_def)
        moreover have "?actions ?E'" using r_n r_m r_n' unfolding r_conv'
          by(cases "llength ?E'")(auto simp add: actions_def less_min_eq2 length_concat sum_list_sum_nth atLeast0LessThan split_beta lnth_ltake less_min_eq1 length_list_of_conv_the_enat enat_plus_eq_enat_conv cong: sum.cong_simp)
        ultimately show ?thesis using wf_exec' ℰ'
          unfolding ‹?E = ?E'› by blast
      qed
    qed
  qed
qed

end

lemma w_value_mrw_value_conf:
  assumes "set_option (vs' adal) ⊆ vs adal × UNIV"
  shows "set_option (mrw_value P vs' ob adal) ⊆ w_value P vs ob adal × UNIV"
using assms by(cases adal)(cases ob rule: w_value_cases, auto)

lemma w_values_mrw_values_conf:
  assumes "set_option (vs' adal) ⊆ vs adal × UNIV"
  shows "set_option (mrw_values P vs' obs adal) ⊆ w_values P vs obs adal × UNIV"
using assms
by(induct obs arbitrary: vs' vs)(auto del: subsetI intro: w_value_mrw_value_conf)

lemma w_value_mrw_value_dom_eq_preserve:
  assumes "dom vs' = {adal. vs adal ≠ {}}"
  shows "dom (mrw_value P vs' ob) = {adal. w_value P vs ob adal ≠ {}}"
using assms
apply(cases ob rule: w_value_cases)
apply(simp_all add: dom_def split_beta del: not_None_eq)
apply(blast elim: equalityE dest: subsetD)+
done

lemma w_values_mrw_values_dom_eq_preserve:
  assumes "dom vs' = {adal. vs adal ≠ {}}"
  shows "dom (mrw_values P vs' obs) = {adal. w_values P vs obs adal ≠ {}}"
using assms
by(induct obs arbitrary: vs vs')(auto del: equalityI intro: w_value_mrw_value_dom_eq_preserve)

context jmm_multithreaded begin

definition non_speculative_read :: 
  "nat ⇒ ('l, 'thread_id, 'x, 'm, 'w) state ⇒ ('addr × addr_loc ⇒ 'addr val set) ⇒ bool"
where
  "non_speculative_read n s vs ⟷
   (∀ttas s' t x ta x' m' i ad al v v'.
       s -▹ttas→* s' ⟶ non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) ⟶
       thr s' t = ⌊(x, no_wait_locks)⌋ ⟶ t ⊢ (x, shr s') -ta→ (x', m') ⟶ actions_ok s' t ta ⟶ 
       i < length ⦃ta⦄⇘o⇙ ⟶ 
       non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)) ⟶
       ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) ⟶ 
       v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟶
       (∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
                      i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
                      length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)))" 

lemma non_speculative_readI [intro?]:
  "(⋀ttas s' t x ta x' m' i ad al v v'. 
    ⟦ s -▹ttas→* s'; non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
     thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
     i < length ⦃ta⦄⇘o⇙; non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙));
     ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v);
     v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟧
    ⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
                      i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
                      length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙))
  ⟹ non_speculative_read n s vs"
unfolding non_speculative_read_def by blast

lemma non_speculative_readD:
  "⟦ non_speculative_read n s vs; s -▹ttas→* s'; non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)));
     thr s' t = ⌊(x, no_wait_locks)⌋; t ⊢ (x, shr s') -ta→ (x', m'); actions_ok s' t ta;
     i < length ⦃ta⦄⇘o⇙; non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙)); 
     ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v);
     v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take i ⦃ta⦄⇘o⇙) (ad, al) ⟧
  ⟹ ∃ta' x'' m''. t ⊢ (x, shr s') -ta'→ (x'', m'') ∧ actions_ok s' t ta' ∧
                      i < length ⦃ta'⦄⇘o⇙ ∧ take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ ⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v') ∧
                      length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
unfolding non_speculative_read_def by blast

end

subsection ‹@{term "non_speculative"} generalises @{term "cut_and_update"} and @{term "ta_hb_consistent"}›

context known_addrs_typing begin

lemma read_non_speculative_new_actions_for:
  fixes status f C M params E
  defines "E ≡ lift_start_obs start_tid start_heap_obs"
  and "vs ≡ w_values P (λ_. {}) (map snd E)"
  and "s ≡ init_fin_lift_state status (start_state f P C M params)"
  assumes wf: "wf_syscls P"
  and RedT: "mthr.if.RedT s ttas s'"
  and redT: "mthr.if.redT s' (t, ta') s''"
  and read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙"
  and ns: "non_speculative P (λ_. {}) (llist_of (map snd E @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
  and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and type_adal: "P,shr s' ⊢ ad@al : T"
  shows "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
  (is "∃w. ?new_w w")
using RedT redT read ns[unfolded E_def] ka unfolding s_def
proof(cases rule: read_ex_NewHeapElem)
  case (start CTn)
  then obtain n where n: "start_heap_obs ! n = NewHeapElem ad CTn"
    and len: "n < length start_heap_obs"
    unfolding in_set_conv_nth by blast
  from ns have "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    unfolding lappend_llist_of_llist_of[symmetric]
    by(simp add: non_speculative_lappend del: lappend_llist_of_llist_of)
  with RedT wt have hext: "start_heap ⊴ shr s'"
    unfolding s_def E_def using start_state_vs_conf[OF wf]
    by(auto dest!: init_fin_RedT_hext_incr simp add: start_state_def split_beta init_fin_lift_state_conv_simps)
  
  from start have "typeof_addr start_heap ad = ⌊CTn⌋"
    by(auto dest: NewHeapElem_start_heap_obsD[OF wf])
  with hext have "typeof_addr (shr s') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
  with type_adal have "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))" using n len 
    by cases (auto simp add: action_obs_def lnth_lappend1 lift_start_obs_def)
  with n len have "?new_w (Suc n)"
    by(simp add: new_actions_for_def actions_def E_def action_obs_def lift_start_obs_def nth_append)
  thus ?thesis ..
next
  case (Red ttas' s'' t' ta' s''' ttas'' CTn)
  note ttas = ‹ttas = ttas' @ (t', ta') # ttas''›
  
  from ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
  obtain obs obs' where obs: "⦃ta'⦄⇘o⇙ = obs @ NormalAction (NewHeapElem ad CTn) # obs'"
    by(auto dest: split_list)
  
  let ?n = "length (lift_start_obs start_tid start_heap_obs)"
  let ?wa = "?n + length (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')) + length obs"
  
  have "?wa = ?n + length (concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas')) + length obs"
    by(simp add: length_concat o_def split_def)
  also have "… < length (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))"
    using obs ttas by(simp add: E_def)
  also
  from ttas obs
  have "(E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas)) ! ?wa = (t', NormalAction (NewHeapElem ad CTn))"
    by(auto simp add: E_def lift_start_obs_def nth_append o_def split_def length_concat)
  moreover
  from ‹mthr.if.redT s'' (t', ta') s'''› ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙›
  obtain x_wa x_wa' where ts''t': "thr s'' t' = ⌊(x_wa, no_wait_locks)⌋"
    and red_wa: "mthr.init_fin t' (x_wa, shr s'') ta' (x_wa', shr s''')"
    by(cases) fastforce+

  from start_state_vs_conf[OF wf]
  have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
    by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)
  
  from ns
  have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
    and ns': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) (llist_of ⦃ta'⦄⇘o⇙)"
    and ns'': "non_speculative P (w_values P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'')))"
    unfolding ttas vs_def
    by(simp_all add: lappend_llist_of_llist_of[symmetric] non_speculative_lappend del: lappend_llist_of_llist_of)
  from ‹mthr.if.RedT (init_fin_lift_state status (start_state f P C M params)) ttas' s''› wt ns
  have ts_ok'': "ts_ok (init_fin_lift wfx) (thr s'') (shr s'')" using vs unfolding vs_def s_def
    by(rule if_RedT_non_speculative_invar)
  with ts''t' have wfxt': "wfx t' (snd x_wa) (shr s'')" by(cases x_wa)(auto dest: ts_okD)

  from ‹mthr.if.RedT (init_fin_lift_state status (start_state f P C M params)) ttas' s''› wt ns
  have vs'': "vs_conf P (shr s'') (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas')))"
    unfolding s_def E_def vs_def
    by(rule if_RedT_non_speculative_invar)(simp add: start_state_def split_beta init_fin_lift_state_conv_simps start_state_vs_conf[OF wf])
  from if_redT_non_speculative_vs_conf[OF ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' _ vs'', of "length ⦃ta'⦄⇘o⇙"] ns'
  have vs''': "vs_conf P (shr s''') (w_values P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas'))) ⦃ta'⦄⇘o⇙)"
    by(simp add: vs_def)

  from ‹mthr.if.redT s'' (t', ta') s'''› ts_ok'' ns' vs''
  have "ts_ok (init_fin_lift wfx) (thr s''') (shr s''')" 
    unfolding vs_def by(rule if_redT_non_speculative_invar)
  with ‹mthr.if.RedT s''' ttas'' s'›
  have hext: "shr s''' ⊴ shr s'" using ns'' vs'''
    by(rule init_fin_RedT_hext_incr)
  
  from red_wa have "typeof_addr (shr s''') ad = ⌊CTn⌋"
    using wfxt' ‹NormalAction (NewHeapElem ad CTn) ∈ set ⦃ta'⦄⇘o⇙› by cases(auto dest: red_NewHeapElemD)
  with hext have "typeof_addr (shr s') ad = ⌊CTn⌋" by(rule typeof_addr_hext_mono)
  with type_adal have "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))" by cases auto
  ultimately have "?new_w ?wa"
    by(simp add: new_actions_for_def actions_def action_obs_def)
  thus ?thesis ..
qed

lemma non_speculative_read_into_cut_and_update:
  fixes status f C M params E
  defines "E ≡ lift_start_obs start_tid start_heap_obs"
  and "vs ≡ w_values P (λ_. {}) (map snd E)"
  and "s ≡ init_fin_lift_state status (start_state f P C M params)"
  and "vs' ≡ mrw_values P Map.empty (map snd E)"
  assumes wf: "wf_syscls P"
  and nsr: "if.non_speculative_read n s vs"
  and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
  shows "if.cut_and_update s vs'"
proof(rule if.cut_and_updateI)
  fix ttas s' t x ta x' m'
  assume Red: "mthr.if.RedT s ttas s'"
    and sc: "ta_seq_consist P vs' (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    and tst: "thr s' t = ⌊(x, no_wait_locks)⌋"
    and red: "t ⊢ (x, shr s') -ta→i (x', m')"
    and aok: "mthr.if.actions_ok s' t ta"
  let ?vs = "w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"
  let ?vs' = "mrw_values P vs' (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"

  from start_state_vs_conf[OF wf]
  have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
    by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)

  from sc have ns: "non_speculative P vs (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    by(rule ta_seq_consist_into_non_speculative)(auto simp add: vs'_def vs_def del: subsetI intro: w_values_mrw_values_conf)

  from ns have ns': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    unfolding lappend_llist_of_llist_of[symmetric] vs_def
    by(simp add: non_speculative_lappend E_def non_speculative_start_heap_obs del: lappend_llist_of_llist_of)

  have vs_vs'': "⋀adal. set_option (?vs' adal) ⊆ ?vs adal × UNIV"
    by(rule w_values_mrw_values_conf)(auto simp add: vs'_def vs_def del: subsetI intro: w_values_mrw_values_conf)
  from Red wt ns vs
  have wt': "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
    by(rule if_RedT_non_speculative_invar)
  hence wtt: "init_fin_lift wfx t x (shr s')" using tst by(rule ts_okD)

  { fix i
    have "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧
                        length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙) ∧
                        ta_seq_consist P ?vs' (llist_of (take i ⦃ta'⦄⇘o⇙)) ∧
                        eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙) (take i ⦃ta'⦄⇘o⇙) ?vs' ∧
                        (ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙)) ⟶ ta' = ta)"
    proof(induct i)
      case 0 
      show ?case using red aok
        by(auto simp del: split_paired_Ex simp add: eq_upto_seq_inconsist_simps)
    next
      case (Suc i)
      then obtain ta' x'' m''
        where red': "t ⊢ (x, shr s') -ta'→i (x'', m'')"
        and aok': "mthr.if.actions_ok s' t ta'"
        and len: "length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
        and sc': "ta_seq_consist P ?vs' (llist_of (take i ⦃ta'⦄⇘o⇙))"
        and eusi: "eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙) (take i ⦃ta'⦄⇘o⇙) ?vs'" 
        and ta'_ta: "ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙)) ⟹ ta' = ta"
        by blast
      let ?vs'' = "mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙)"
      show ?case
      proof(cases "i < length ⦃ta'⦄⇘o⇙ ∧ ¬ ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta'⦄⇘o⇙)) ∧ ¬ ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙))")
        case True
        hence i: "i < length ⦃ta'⦄⇘o⇙" and "¬ ta_seq_consist P ?vs'' (LCons (⦃ta'⦄⇘o⇙ ! i) LNil)" using sc'
          by(auto simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend simp del: lappend_llist_of_llist_of)
        then obtain ad al v where ta'_i: "⦃ta'⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v)"
          by(auto split: action.split_asm obs_event.split_asm)
        from ta'_i True have read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙" by(auto simp add: in_set_conv_nth)
        with red' have "ad ∈ known_addrs_if t x" by(rule if_red_read_knows_addr)
        hence "ad ∈ if.known_addrs_state s'" using tst by(rule if.known_addrs_stateI)
        moreover from init_fin_red_read_typeable[OF red' wtt read]
        obtain T where type_adal: "P,shr s' ⊢ ad@al : T" ..

        from redT_updWs_total[of t "wset s'" "⦃ta'⦄⇘w⇙"] red' tst aok'
        obtain s'' where redT': "mthr.if.redT s' (t, ta') s''" by(auto dest!: mthr.if.redT.redT_normal)
        with wf Red
        have "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
          (is "∃w. ?new_w w")
          using read ns' ka wt type_adal unfolding s_def E_def by(rule read_non_speculative_new_actions_for)
        then obtain w where w: "?new_w w" ..
        have "(ad, al) ∈ dom ?vs'"
        proof(cases "w < length E")
          case True
          with w have "(ad, al) ∈ dom vs'" unfolding vs'_def new_actions_for_def
            by(clarsimp)(erule mrw_values_new_actionD[rotated 1], auto simp del: split_paired_Ex simp add: set_conv_nth action_obs_def nth_append intro!: exI[where x=w])
          also have "dom vs' ⊆ dom ?vs'" by(rule mrw_values_dom_mono)
          finally show ?thesis .
        next
          case False
          with w show ?thesis unfolding new_actions_for_def
            apply(clarsimp)
            apply(erule mrw_values_new_actionD[rotated 1])
            apply(simp_all add: set_conv_nth action_obs_def nth_append actions_def)
            apply(rule exI[where x="w - length E"])
            apply(subst nth_map[where f=snd, symmetric])
            apply(simp_all add: length_concat o_def split_def map_concat)
            done
        qed
        hence "(ad, al) ∈ dom (mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙))"
          by(rule subsetD[OF mrw_values_dom_mono])
        then obtain v' b where v': "mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙) (ad, al) = ⌊(v', b)⌋" by auto
        moreover from vs_vs''[of "(ad, al)"]
        have "set_option (mrw_values P ?vs' (take i ⦃ta'⦄⇘o⇙) (ad, al)) ⊆ w_values P ?vs (take i ⦃ta'⦄⇘o⇙) (ad, al) × UNIV"
          by(rule w_values_mrw_values_conf)
        ultimately have "v' ∈ w_values P ?vs (take i ⦃ta'⦄⇘o⇙) (ad, al)" by simp
        moreover from sc'
        have "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta'⦄⇘o⇙))"
          by(blast intro: ta_seq_consist_into_non_speculative vs_vs'' del: subsetI)
        ultimately obtain ta'' x'' m''
          where red'': "t ⊢ (x, shr s') -ta''→i (x'', m'')"
          and aok'': "mthr.if.actions_ok s' t ta''"
          and i': "i < length ⦃ta''⦄⇘o⇙"
          and eq: "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta'⦄⇘o⇙"
          and ta''_i: "⦃ta''⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v')"
          and len': "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta'⦄⇘o⇙)"
          using if.non_speculative_readD[OF nsr Red ns tst red' aok' i _ ta'_i, of v'] by auto
        from len' len have "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)" by simp
        moreover have "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta''⦄⇘o⇙))"
          using eq sc' i' ta''_i v'
          by(simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend del: lappend_llist_of_llist_of)
        moreover
        have eusi': "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta''⦄⇘o⇙) ?vs'"
        proof(cases "i < length ⦃ta⦄⇘o⇙")
          case True
          with i' i len eq eusi ta'_i ta''_i v' show ?thesis
            by(auto simp add: take_Suc_conv_app_nth ta'_ta eq_upto_seq_inconsist_simps intro: eq_upto_seq_inconsist_appendI)
        next
          case False
          with i ta'_ta have "¬ ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙))" by auto
          then show ?thesis using False i' eq eusi
            by(simp add: take_Suc_conv_app_nth eq_upto_seq_inconsist_append2)
        qed
        moreover {
          assume "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙))"
          with True have "ta'' = ta" by simp }
        ultimately show ?thesis using red'' aok'' True by blast
      next
        case False
        hence "ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta⦄⇘o⇙)) ∨ 
               length ⦃ta'⦄⇘o⇙ ≤ i ∨ 
               ta_seq_consist P ?vs' (llist_of (take (Suc i) ⦃ta'⦄⇘o⇙))" 
          (is "?case1 ∨ ?case2 ∨ ?case3") by auto
        thus ?thesis
        proof(elim disjCE)
          assume "?case1"
          moreover
          hence "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta⦄⇘o⇙) ?vs'"
            by(rule ta_seq_consist_imp_eq_upto_seq_inconsist_refl)
          ultimately show ?thesis using red aok by fastforce
        next
          assume "?case2" and "¬ ?case1"
          have "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta'⦄⇘o⇙) ?vs'"
          proof(cases "i < length ⦃ta⦄⇘o⇙")
            case True
            from ‹?case2› ‹¬ ?case1› have "¬ ta_seq_consist P ?vs' (llist_of (take i ⦃ta⦄⇘o⇙))" by(auto simp add: ta'_ta)
            hence "eq_upto_seq_inconsist P (take i ⦃ta⦄⇘o⇙ @ [⦃ta⦄⇘o⇙ ! i]) (take i ⦃ta'⦄⇘o⇙ @ []) ?vs'"
              by(blast intro: eq_upto_seq_inconsist_appendI[OF eusi])
            thus ?thesis using True ‹?case2› by(simp add: take_Suc_conv_app_nth)
          next
            case False with eusi ‹?case2› show ?thesis by simp
          qed
          with red' aok' len sc' eusi ‹?case2› ‹¬ ?case1›show ?thesis
            by (fastforce simp add: take_all simp del: split_paired_Ex)
        next
          assume "?case3" and "¬ ?case1" and "¬ ?case2"
          with len eusi ta'_ta
          have "eq_upto_seq_inconsist P (take (Suc i) ⦃ta⦄⇘o⇙) (take (Suc i) ⦃ta'⦄⇘o⇙) ?vs'"
            by(cases "i < length ⦃ta⦄⇘o⇙")(auto simp add: take_Suc_conv_app_nth lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend intro: eq_upto_seq_inconsist_appendI eq_upto_seq_inconsist_append2 cong: action.case_cong obs_event.case_cong)
          with red' aok' ‹?case3› len ‹¬ ?case1› show ?thesis by blast
        qed
      qed
    qed }
  from this[of "max n (length ⦃ta⦄⇘o⇙)"]
  show "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧ ta_seq_consist P ?vs' (llist_of ⦃ta'⦄⇘o⇙) ∧ eq_upto_seq_inconsist P ⦃ta⦄⇘o⇙ ⦃ta'⦄⇘o⇙ ?vs'"
    by(auto simp del: split_paired_Ex cong: conj_cong)
qed

lemma non_speculative_read_into_hb_completion:
  fixes status f C M params E
  defines "E ≡ lift_start_obs start_tid start_heap_obs"
  and "vs ≡ w_values P (λ_. {}) (map snd E)"
  and "s ≡ init_fin_lift_state status (start_state f P C M params)"
  assumes wf: "wf_syscls P"
  and nsr: "if.non_speculative_read n s vs"
  and wt: "ts_ok (init_fin_lift wfx) (thr s) (shr s)"
  and ka: "known_addrs start_tid (f (fst (method P C M)) M (fst (snd (method P C M))) (fst (snd (snd (method P C M)))) (the (snd (snd (snd (method P C M))))) params) ⊆ allocated start_heap"
  shows "if.hb_completion s E"
proof
  fix ttas s' t x ta x' m' i
  assume Red: "mthr.if.RedT s ttas s'"
    and ns: "non_speculative P (w_values P (λ_. {}) (map snd E)) (llist_of (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    and tst: "thr s' t = ⌊(x, no_wait_locks)⌋"
    and red: "t ⊢ (x, shr s') -ta→i (x', m')"
    and aok: "mthr.if.actions_ok s' t ta"
    and nsi: "non_speculative P (w_values P (w_values P (λ_. {}) (map snd E)) (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take i ⦃ta⦄⇘o⇙))"

  let ?E = "E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas) @ map (Pair t) (take i ⦃ta⦄⇘o⇙)"
  let ?vs = "w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))"

  from ns have ns': "non_speculative P (λ_. {}) (llist_of (map snd (lift_start_obs start_tid start_heap_obs) @ concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas)))"
    unfolding lappend_llist_of_llist_of[symmetric]
    by(simp add: non_speculative_lappend E_def non_speculative_start_heap_obs del: lappend_llist_of_llist_of)

  from start_state_vs_conf[OF wf]
  have vs: "vs_conf P (shr s) vs" unfolding vs_def E_def s_def
    by(simp add: init_fin_lift_state_conv_simps start_state_def split_def)

  from Red wt ns vs
  have wt': "ts_ok (init_fin_lift wfx) (thr s') (shr s')"
    unfolding vs_def by(rule if_RedT_non_speculative_invar)
  hence wtt: "init_fin_lift wfx t x (shr s')" using tst by(rule ts_okD)

  { fix j
    have "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧ length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙) ∧
                        take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ 
                        ta_hb_consistent P ?E (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙)))) ∧
                        (i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
                        (if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
    proof(induct j)
      case 0 from red aok show ?case by(fastforce simp del: split_paired_Ex)
    next
      case (Suc j)
      then obtain ta' x'' m''
        where red': "t ⊢ (x, shr s') -ta'→i (x'', m'')"
        and aok': "mthr.if.actions_ok s' t ta'"
        and len: "length ⦃ta'⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)"
        and eq: "take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙"
        and hb: "ta_hb_consistent P ?E (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙))))"
        and len_i: "i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙"
        and sim_i: "(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
        by blast
      show ?case
      proof(cases "i + j < length ⦃ta'⦄⇘o⇙")
        case False
        with red' aok' len eq hb len_i sim_i show ?thesis by(fastforce simp del: split_paired_Ex)
      next
        case True
        note j = this
        show ?thesis
        proof(cases "∃ad al v. ⦃ta'⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v)")
          case True
          then obtain ad al v where ta'_j: "⦃ta'⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v)" by blast
          hence read: "NormalAction (ReadMem ad al v) ∈ set ⦃ta'⦄⇘o⇙" using j by(auto simp add: in_set_conv_nth)
          with red' have "ad ∈ known_addrs_if t x" by(rule if_red_read_knows_addr)
          hence "ad ∈ if.known_addrs_state s'" using tst by(rule if.known_addrs_stateI)
          from init_fin_red_read_typeable[OF red' wtt read] obtain T 
            where type_adal: "P,shr s' ⊢ ad@al : T" ..

          from redT_updWs_total[of t "wset s'" "⦃ta'⦄⇘w⇙"] red' tst aok'
          obtain s'' where redT': "mthr.if.redT s' (t, ta') s''" by(auto dest!: mthr.if.redT.redT_normal)
          with wf Red
          have "∃w. w ∈ new_actions_for P (llist_of (E @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) ttas))) (ad, al)"
            (is "∃w. ?new_w w")
            using read ns' ka wt type_adal unfolding s_def E_def
            by(rule read_non_speculative_new_actions_for)
          then obtain w where w: "?new_w w" ..

          define E'' where "E'' = ?E @ map (Pair t) (take (Suc j) (drop i ⦃ta'⦄⇘o⇙))"

          from Red redT' have "mthr.if.RedT s (ttas @ [(t, ta')]) s''" unfolding mthr.if.RedT_def ..
          hence tsa: "thread_start_actions_ok (llist_of (lift_start_obs start_tid start_heap_obs @ concat (map (λ(t, ta). map (Pair t) ⦃ta⦄⇘o⇙) (ttas @ [(t, ta')]))))"
            unfolding s_def by(rule thread_start_actions_ok_init_fin_RedT)
          hence "thread_start_actions_ok (llist_of E'')" unfolding E_def[symmetric] E''_def
            by(rule thread_start_actions_ok_prefix)(rule lprefix_llist_ofI, simp, metis append_take_drop_id eq map_append)
          moreover from w have "w ∈ actions (llist_of E'')"
            unfolding E''_def by(auto simp add: new_actions_for_def actions_def)
          moreover have "length ?E + j ∈ actions (llist_of E'')" using j by(auto simp add: E''_def actions_def)
          moreover from w have "is_new_action (action_obs (llist_of E'') w)"
            by(auto simp add: new_actions_for_def action_obs_def actions_def nth_append E''_def)
          moreover have "¬ is_new_action (action_obs (llist_of E'') (length ?E + j))"
            using j ta'_j by(auto simp add: action_obs_def nth_append min_def E''_def)(subst (asm) nth_map, simp_all)
          ultimately have hb_w: "P,llist_of E'' ⊢ w ≤hb length ?E + j"
            by(rule happens_before_new_not_new)
          
          define writes where
            "writes = {w. P,llist_of E'' ⊢ w ≤hb length ?E + j ∧ w ∈ write_actions (llist_of E'') ∧ 
                 (ad, al) ∈ action_loc P (llist_of E'') w}"

          define w' where "w' = Max_torder (action_order (llist_of E'')) writes"

          have writes_actions: "writes ⊆ actions (llist_of E'')" unfolding writes_def actions_def
            by(auto dest!: happens_before_into_action_order elim!: action_orderE simp add: actions_def)
          also have "finite …" by(simp add: actions_def)
          finally (finite_subset) have "finite writes" .
          moreover from hb_w w have w_writes: "w ∈ writes"
            by(auto 4 3 simp add: writes_def new_actions_for_def action_obs_def actions_def nth_append E''_def intro!: write_actions.intros elim!: is_new_action.cases)
          hence "writes ≠ {}" by auto

          with torder_action_order ‹finite writes› 
          have w'_writes: "w' ∈ writes" using writes_actions unfolding w'_def by(rule Max_torder_in_set)
          moreover
          { fix w''
            assume "w'' ∈ writes"
            with torder_action_order ‹finite writes›
            have "llist_of E'' ⊢ w'' ≤a w'" using writes_actions unfolding w'_def by(rule Max_torder_above) }
          note w'_maximal = this

          define v' where "v' = value_written P (llist_of E'') w' (ad, al)"

          from nsi ta_hb_consistent_into_non_speculative[OF hb]
          have nsi': "non_speculative P (w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas))) (llist_of (take (i + j) ⦃ta'⦄⇘o⇙))"
            unfolding take_add lappend_llist_of_llist_of[symmetric] non_speculative_lappend vs_def eq
            by(simp add: non_speculative_lappend o_def map_concat split_def del: lappend_llist_of_llist_of)
            
          from w'_writes have adal_w': "(ad, al) ∈ action_loc P (llist_of E'') w'" by(simp add: writes_def)
          from w'_writes have "w' ∈ write_actions (llist_of E'')"
            unfolding writes_def by blast
          then obtain "is_write_action (action_obs (llist_of E'') w')" 
            and w'_actions: "w' ∈ actions (llist_of E'')" by cases
          hence "v' ∈ w_values P (λ_. {}) (map snd E'') (ad, al)"
          proof cases
            case (NewHeapElem ad' CTn)
            hence "NormalAction (NewHeapElem ad' CTn) ∈ set (map snd E'')"
              using w'_actions unfolding in_set_conv_nth
              by(auto simp add: actions_def action_obs_def cong: conj_cong)
            moreover have "ad' = ad" 
              and "(ad, al) ∈ action_loc_aux P (NormalAction (NewHeapElem ad CTn))"
              using adal_w' NewHeapElem by auto
            ultimately show ?thesis using NewHeapElem unfolding v'_def
              by(simp add: value_written.simps w_values_new_actionD)
          next
            case (WriteMem ad' al' v'')
            hence "NormalAction (WriteMem ad' al' v'') ∈ set (map snd E'')"
              using w'_actions unfolding in_set_conv_nth
              by(auto simp add: actions_def action_obs_def cong: conj_cong)
            moreover have "ad' = ad" "al' = al" using adal_w' WriteMem by auto
            ultimately show ?thesis using WriteMem unfolding v'_def
              by(simp add: value_written.simps w_values_WriteMemD)
          qed
          hence "v' ∈ w_values P vs (concat (map (λ(t, ta). ⦃ta⦄⇘o⇙) ttas) @ take (i + j) ⦃ta'⦄⇘o⇙) (ad, al)"
            using j ta'_j eq unfolding E''_def vs_def
            by(simp add: o_def split_def map_concat take_add take_Suc_conv_app_nth)
          from if.non_speculative_readD[OF nsr Red ns[folded vs_def] tst red' aok' j nsi' ta'_j this]
          obtain ta'' x'' m'' 
            where red'': "t ⊢ (x, shr s') -ta''→i (x'', m'')"
            and aok'': "mthr.if.actions_ok s' t ta''"
            and j': "i + j < length ⦃ta''⦄⇘o⇙"
            and eq': "take (i + j) ⦃ta''⦄⇘o⇙ = take (i + j) ⦃ta'⦄⇘o⇙"
            and ta''_j: "⦃ta''⦄⇘o⇙ ! (i + j) = NormalAction (ReadMem ad al v')"
            and len': "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta'⦄⇘o⇙)" by blast

          define EE where "EE = ?E @ map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙))"
          define E' where "E' = ?E @ map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙)) @ [(t, NormalAction (ReadMem ad al v'))]"

          from len' len have "length ⦃ta''⦄⇘o⇙ ≤ max n (length ⦃ta⦄⇘o⇙)" by simp
          moreover from eq' eq j j' have "take i ⦃ta''⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙"
            by(auto simp add: take_add min_def)
          moreover {
            note hb
            also have eq'': "take j (drop i ⦃ta'⦄⇘o⇙) = take j (drop i ⦃ta''⦄⇘o⇙)"
              using eq' j j' by(simp add: take_add min_def)
            also have "ta_hb_consistent P (?E @ list_of (llist_of (map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙))))) (llist_of [(t, ⦃ta''⦄⇘o⇙ ! (i + j))])"
              unfolding llist_of.simps ta_hb_consistent_LCons ta_hb_consistent_LNil ta''_j prod.simps action.simps obs_event.simps list_of_llist_of append_assoc E'_def[symmetric, unfolded append_assoc]
              unfolding EE_def[symmetric, unfolded append_assoc]
            proof(intro conjI TrueI exI[where x=w'] strip)
              have "llist_of E'' [≈] llist_of E'" using j len eq'' ta'_j unfolding E''_def E'_def
                by(auto simp add: sim_actions_def list_all2_append List.list_all2_refl split_beta take_Suc_conv_app_nth take_map[symmetric])
              moreover have "length E'' = length E'" using j j' by(simp add: E''_def E'_def)
              ultimately have sim: "ltake (enat (length E')) (llist_of E'') [≈] ltake (enat (length E')) (llist_of E')" by simp

              from w'_actions ‹length E'' = length E'›
              have w'_len: "w' < length E'" by(simp add: actions_def)

              from ‹w' ∈ write_actions (llist_of E'')› sim
              show "w' ∈ write_actions (llist_of E')" by(rule write_actions_change_prefix)(simp add: w'_len)
              from adal_w' action_loc_change_prefix[OF sim, of w' P]
              show "(ad, al) ∈ action_loc P (llist_of E') w'" by(simp add: w'_len)

              from ta'_j j have "length ?E + j ∈ read_actions (llist_of E'')"
                by(auto intro!: read_actions.intros simp add: action_obs_def actions_def E''_def min_def nth_append)(auto)
              hence "w' ≠ length ?E + j" using ‹w' ∈ write_actions (llist_of E'')›
                by(auto dest: read_actions_not_write_actions)
              with w'_len have "w' < length ?E + j" by(simp add: E'_def)
              from j j' len' eq''
              have "ltake (enat (length ?E + j)) (llist_of E'') = ltake (enat (length ?E + j)) (llist_of E')"
                by(auto simp add: E''_def E'_def min_def take_Suc_conv_app_nth)
              from value_written_change_prefix[OF this, of w' P] ‹w' < length ?E + j›
              show "value_written P (llist_of E') w' (ad, al) = v'" unfolding v'_def by simp

              from ‹thread_start_actions_ok (llist_of E'')› ‹llist_of E'' [≈] llist_of E'›
              have tsa'': "thread_start_actions_ok (llist_of E')"
                by(rule thread_start_actions_ok_change)
                
              from w'_writes j j' len len' have "P,llist_of E'' ⊢ w' ≤hb length EE"
                by(auto simp add: EE_def writes_def min_def ac_simps)
              thus "P,llist_of E' ⊢ w' ≤hb length EE" using tsa'' sim
                by(rule happens_before_change_prefix)(simp add: w'_len, simp add: EE_def E'_def)
              
              fix w''
              assume w'': "w'' ∈ write_actions (llist_of E')"
                and adal_w'': "(ad, al) ∈ action_loc P (llist_of E') w''"

              from w'' have w''_len: "w'' < length E'" by(cases)(simp add: actions_def)
              
              from w'' sim[symmetric] have w'': "w'' ∈ write_actions (llist_of E'')"
                by(rule write_actions_change_prefix)(simp add: w''_len)
              from adal_w'' action_loc_change_prefix[OF sim[symmetric], of w'' P] w''_len
              have adal_w'': "(ad, al) ∈ action_loc P (llist_of E'') w''" by simp
              {
                presume w'_w'': "llist_of E' ⊢ w' ≤a w''"
                  and w''_hb: "P,llist_of E' ⊢ w'' ≤hb length EE"
                from w''_hb ‹thread_start_actions_ok (llist_of E'')› sim[symmetric]
                have "P,llist_of E'' ⊢ w'' ≤hb length EE"
                  by(rule happens_before_change_prefix)(simp add: w''_len, simp add: E'_def EE_def)
                with w'' adal_w'' j j' len len' have "w'' ∈ writes"
                  by(auto simp add: writes_def EE_def min_def ac_simps split: if_split_asm)
                hence "llist_of E'' ⊢ w'' ≤a w'" by(rule w'_maximal)
                hence "llist_of E' ⊢ w'' ≤a w'" using sim
                  by(rule action_order_change_prefix)(simp_all add: w'_len w''_len)
                thus "w'' = w'" "w'' = w'" using w'_w'' by(rule antisymPD[OF antisym_action_order])+ 
              }

              { assume "P,llist_of E' ⊢ w' ≤hb w'' ∧ P,llist_of E' ⊢ w'' ≤hb length EE"
                thus "llist_of E' ⊢ w' ≤a w''" "P,llist_of E' ⊢ w'' ≤hb length EE"
                  by(blast dest: happens_before_into_action_order)+ }
              { assume "is_volatile P al ∧ P,llist_of E' ⊢ w' ≤so w'' ∧ P,llist_of E' ⊢ w'' ≤so length EE"
                then obtain vol: "is_volatile P al"
                  and so: "P,llist_of E' ⊢ w' ≤so w''" 
                  and so': "P,llist_of E' ⊢ w'' ≤so length EE" by blast
                from so show "llist_of E' ⊢ w' ≤a w''" by(blast elim: sync_orderE)

                show "P,llist_of E' ⊢ w'' ≤hb length EE"
                proof(cases "is_new_action (action_obs (llist_of E') w'')")
                  case True
                  with ‹w'' ∈ write_actions (llist_of E')› ta''_j show ?thesis
                    by cases(rule happens_before_new_not_new[OF tsa''], auto simp add: actions_def EE_def E'_def action_obs_def min_def nth_append)
                next
                  case False
                  with ‹w'' ∈ write_actions (llist_of E')› ‹(ad, al) ∈ action_loc P (llist_of E') w''›
                  obtain v'' where "action_obs (llist_of E') w'' = NormalAction (WriteMem ad al v'')"
                    by cases(auto elim: is_write_action.cases)
                  with ta''_j w'' j j' len len'
                  have "P ⊢ (action_tid (llist_of E') w'', action_obs (llist_of E') w'') ↝sw (action_tid (llist_of E') (length EE), action_obs (llist_of E') (length EE))"
                    by(auto simp add: E'_def EE_def action_obs_def min_def nth_append Volatile)
                  with so' have "P,llist_of E' ⊢ w'' ≤sw length EE" by(rule sync_withI)
                  thus ?thesis unfolding po_sw_def [abs_def] by(blast intro: tranclp.r_into_trancl)
                qed }
            qed
            ultimately have "ta_hb_consistent P ?E (lappend (llist_of (map (Pair t) (take j (drop i ⦃ta''⦄⇘o⇙)))) (llist_of ([(t, ⦃ta''⦄⇘o⇙ ! (i + j))])))"
              by(rule ta_hb_consistent_lappendI) simp
            hence "ta_hb_consistent P ?E (llist_of (map (Pair t) (take (Suc j) (drop i ⦃ta''⦄⇘o⇙))))"
              using j' unfolding lappend_llist_of_llist_of by(simp add: take_Suc_conv_app_nth) }
          moreover from len_i have "i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta''⦄⇘o⇙" using eq' j' by auto
          moreover from sim_i eq' ta''_j ta'_j
          have "(if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta''⦄⇘o⇙ ! i)"
            by(cases "j = 0")(auto split: if_split_asm, (metis add_strict_left_mono add_0_right nth_take)+)
          ultimately show ?thesis using red'' aok'' by blast
        next
          case False
          hence "ta_hb_consistent P (?E @ list_of (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙))))) (llist_of [(t, ⦃ta'⦄⇘o⇙ ! (i + j))])"
            by(simp add: ta_hb_consistent_LCons split: action.split obs_event.split)
          with hb
          have "ta_hb_consistent P ?E (lappend (llist_of (map (Pair t) (take j (drop i ⦃ta'⦄⇘o⇙)))) (llist_of ([(t, ⦃ta'⦄⇘o⇙ ! (i + j))])))"
            by(rule ta_hb_consistent_lappendI) simp
          hence "ta_hb_consistent P ?E (llist_of (map (Pair t) (take (Suc j) (drop i ⦃ta'⦄⇘o⇙))))"
            using j unfolding lappend_llist_of_llist_of by(simp add: take_Suc_conv_app_nth)
          with red' aok' len eq len_i sim_i show ?thesis by blast
        qed
      qed
    qed }
  from this[of "max n (length ⦃ta⦄⇘o⇙)"]
  show "∃ta' x'' m''. t ⊢ (x, shr s') -ta'→i (x'', m'') ∧ mthr.if.actions_ok s' t ta' ∧ 
                      take i ⦃ta'⦄⇘o⇙ = take i ⦃ta⦄⇘o⇙ ∧ 
                      ta_hb_consistent P ?E (llist_of (map (Pair t) (drop i ⦃ta'⦄⇘o⇙))) ∧ 
                      (i < length ⦃ta⦄⇘o⇙ ⟶ i < length ⦃ta'⦄⇘o⇙) ∧
                      (if ∃ad al v. ⦃ta⦄⇘o⇙ ! i = NormalAction (ReadMem ad al v) then sim_action else (=)) (⦃ta⦄⇘o⇙ ! i) (⦃ta'⦄⇘o⇙ ! i)"
    by(simp del: split_paired_Ex cong: conj_cong split del: if_split) blast
qed

end

end