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) tao)) E')   σ"

lemma actions_ℰE_aux:
  fixes σ E'
  defines "E == lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E')"
  assumes mthr: "mthr.Runs σ E'"
  and a: "enat a < llength E"
  obtains m n t ta
  where "lnth E a = (t, tao ! n)"
  and "n < length tao" 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) tao)) E') m) n"
    and "enat n < llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E') m)"
    and "enat m < llength (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E')"
    and "enat a = (i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) tao)) 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, tao ! n)"
    and n: "n < length tao"
    and m: "enat m < llength E'"
    and a: "enat a = (i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) tao)) E') i)) + enat n"
    by(simp_all)
  note a
  also have "(i<m. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) tao)) 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) tao)) E')"
  and "mthr.Runs σ E'"
  and "lnth E a = (t, tao ! n)"
  and "n < length tao" 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) tao)) 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) tao)) ` 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) tao)) (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) tao)) (llist_of_tllist E')))"
      unfolding E by(simp add: lconcat_lfilter_neq_LNil)
    also have " = lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) (lmap (λ(tls, s', tta, s''). tta) (lfilter (λ(tls, s', (t, ta), s''). tao  []) (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''). tao  []) (llist_of_tllist E'')) = 
          lfilter (λ(t, ta). tao  []) (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''). tao  []) (llist_of_tllist E'')))"
          (is "¬ lnull ?lhs'")
          and "¬ lnull (lfilter (λ(t, ta). tao  []) (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''). tao  []) (llist_of_tllist E'')) 
           ltl ?rhs' = lfilter (λ(t, ta). tao  []) (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) tao)) ?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) tao) 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, tao ! 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) tao) 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) tao) (take i ttas)))"
      let ?i = "length ?obs_prefix + ?i'"

      from i m nth_i
      have "?i' < length (concat (map (λ(t, ta). map (Pair t) tao) (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) tao)) 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) tao)) E'))"
      by(cases "llength (lconcat (lmap (λ(t, ta). llist_of (map (Pair t) tao)) 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) tao)) E')) (a - length ?start_heap_obs) = (t, tao ! n)"
      and n: "n < length tao" 
      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 = tao ! 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 "tao = [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) tao)) 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) tao)) E') i)) + enat l"
        by(fastforce simp add: split_beta)

      have "(i<k. llength (lnth (lmap (λ(t, ta). llist_of (map (Pair t) tao)) 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 tao 
   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 tao"
  and red_New_same_addr_same:
  " t  (x, m) -ta (x', m'); 
     tao ! i = NewHeapElem a CTn; i < length tao;
     tao ! j = NewHeapElem a CTn'; j < length tao 
   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 tao"
  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 tao"
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 "tao ! i = NormalAction (NewHeapElem a CTn)" "i < length tao"
  and "tao ! j = NormalAction (NewHeapElem a CTn')" "j < length tao"
  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 tao"
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 tao"
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) tao)) 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_ao ! a_n)"
        and a_n: "a_n < length ta_ao" 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_ao ! 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_ao"
        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_ao
      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'_ao ! a_n = NewHeapElem ad CTn"
        and a_n': "a_n < length ta'_ao" by auto
      hence "NewHeapElem ad CTn  set ta'_ao" 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_ao"
      proof(rule ccontr)
        assume "¬ ?thesis"
        hence a'_greater: "(a - n) - a_n + length ta_ao  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'_ao"
        and New_ta'_a': "ta'_ao ! 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 tao"
  and red_known_addrs_new_thread:
  " t  x, m -ta x', m'; NewThread t' x'' m''  set tat 
   known_addrs t' x''  known_addrs t x"
  and red_read_knows_addr:
  " t  x, m -ta x', m'; ReadMem ad al v  set tao 
   ad  known_addrs t x"
  and red_write_knows_addr:
  " t  x, m -ta x', m'; tao ! n = WriteMem ad al (Addr ad'); n < length tao 
   ad'  known_addrs t x  ad'  new_obs_addrs (take n tao)"
  ― ‹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 tao"
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 tat"
  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 tao"
  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 "tao ! n = NormalAction (WriteMem ad al (Addr ad'))" "n < length tao"
  shows "ad'  known_addrs_if t x  ad'  new_obs_addrs_if (take n tao)"
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 tao"
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 tao"
    proof(cases "thr s t'")
      case None
      with redT_normal thr s' t' = (x'', ln'')
      obtain m'' where "NewThread t' x'' m''  set tat"
        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 tao" by simp
      finally have "ad  known_addrs_if t x  new_obs_addrs_if tao" 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 tao" 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 tao"
  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 tao)"
  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 tao)  allocated (shr s')" (is "?thesis2")
proof