Theory JMM_Spec

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

section ‹Axiomatic specification of the JMM›

theory JMM_Spec
imports
  Orders
  "../Common/Observable_Events"
  Coinductive.Coinductive_List
begin

subsection ‹Definitions›

type_synonym JMM_action = nat
type_synonym ('addr, 'thread_id) execution = "('thread_id × ('addr, 'thread_id) obs_event action) llist"

definition "actions" :: "('addr, 'thread_id) execution ⇒ JMM_action set"
where "actions E = {n. enat n < llength E}"

definition action_tid :: "('addr, 'thread_id) execution ⇒ JMM_action ⇒ 'thread_id"
where "action_tid E a = fst (lnth E a)"

definition action_obs :: "('addr, 'thread_id) execution ⇒ JMM_action ⇒ ('addr, 'thread_id) obs_event action"
where "action_obs E a = snd (lnth E a)"

definition tactions :: "('addr, 'thread_id) execution ⇒ 'thread_id ⇒ JMM_action set"
where "tactions E t = {a. a ∈ actions E ∧ action_tid E a = t}"

inductive is_new_action :: "('addr, 'thread_id) obs_event action ⇒ bool"
where
  NewHeapElem: "is_new_action (NormalAction (NewHeapElem a hT))"

inductive is_write_action :: "('addr, 'thread_id) obs_event action ⇒ bool"
where
  NewHeapElem: "is_write_action (NormalAction (NewHeapElem ad hT))"
| WriteMem: "is_write_action (NormalAction (WriteMem ad al v))"

text ‹
  Initialisation actions are synchronisation actions iff they initialize volatile
  fields -- cf. JMM mailing list, message no. 62 (5 Nov. 2006).
  However, intuitively correct programs might not be correctly synchronized:
\begin{verbatim}
     x = 0
---------------
r1 = x | r2 = x
\end{verbatim}
  Here, if x is not volatile, the initial write can belong to at most one thread.
  Hence, it is happens-before to either r1 = x or r2 = x, but not both.
  In any sequentially consistent execution, both reads must read from the initilisation
  action x = 0, but it is not happens-before ordered to one of them.

  Moreover, if only volatile initialisations synchronize-with all thread-start actions,
  this breaks the proof of the DRF guarantee since it assumes that the happens-before relation
  $<=hb$ a for an action $a$ in a topologically sorted action sequence depends only on the 
  actions before it. Counter example: (y is volatile)

  [(t1, start), (t1, init x), (t2, start), (t1, init y), ...

  Here, (t1, init x) $<=hb$ (t2, start) via: (t1, init x) $<=po$ (t1, init y) $<=sw$ (t2, start),
  but in [(t1, start), (t1, init x), (t2, start)], not (t1, init x) $<=hb$ (t2, start).

  Sevcik speculated that one might add an initialisation thread which performs all initialisation
  actions. All normal threads' start action would then synchronize on the final action of the initialisation thread.
  However, this contradicts the memory chain condition in the final field extension to the JMM
  (threads must read addresses of objects that they have not created themselves before they can
  access the fields of the object at that address) -- not modelled here.

  Instead, we leave every initialisation action in the thread it belongs to, but order it explicitly
  before the thread's start action and add synchronizes-with edges from \emph{all} initialisation
  actions to \emph{all} thread start actions.
›

inductive saction :: "'m prog ⇒ ('addr, 'thread_id) obs_event action ⇒ bool"
for P :: "'m prog"
where
  NewHeapElem: "saction P (NormalAction (NewHeapElem a hT))"
| Read: "is_volatile P al ⟹ saction P (NormalAction (ReadMem a al v))"
| Write: "is_volatile P al ⟹ saction P (NormalAction (WriteMem a al v))"
| ThreadStart: "saction P (NormalAction (ThreadStart t))"
| ThreadJoin: "saction P (NormalAction (ThreadJoin t))"
| SyncLock: "saction P (NormalAction (SyncLock a))"
| SyncUnlock: "saction P (NormalAction (SyncUnlock a))"
| ObsInterrupt: "saction P (NormalAction (ObsInterrupt t))"
| ObsInterrupted: "saction P (NormalAction (ObsInterrupted t))"
| InitialThreadAction: "saction P InitialThreadAction"
| ThreadFinishAction: "saction P ThreadFinishAction"


definition sactions :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action set"
where "sactions P E = {a. a ∈ actions E ∧ saction P (action_obs E a)}"

inductive_set write_actions :: "('addr, 'thread_id) execution ⇒ JMM_action set"
for E :: "('addr, 'thread_id) execution"
where 
  write_actionsI: "⟦ a ∈ actions E; is_write_action (action_obs E a) ⟧ ⟹ a ∈ write_actions E"

text ‹
  @{term NewObj} and @{term NewArr} actions only initialize those fields and array cells that
  are in fact in the object or array. Hence, they are not a write for
  - reads from addresses for which no object/array is created during the whole execution
  - reads from fields/cells that are not part of the object/array at the specified address.
›

primrec addr_locs :: "'m prog ⇒ htype ⇒ addr_loc set"
where 
  "addr_locs P (Class_type C) = {CField D F|D F. ∃fm T. P ⊢ C has F:T (fm) in D}"
| "addr_locs P (Array_type T n) = ({ACell n'|n'. n' < n} ∪ {CField Object F|F. ∃fm T. P ⊢ Object has F:T (fm) in Object})"

text ‹
  ‹action_loc_aux› would naturally be an inductive set,
  but inductive\_set does not allow to pattern match on parameters.
  Hence, specify it using function and derive the setup manually.
›

fun action_loc_aux :: "'m prog ⇒ ('addr, 'thread_id) obs_event action ⇒ ('addr × addr_loc) set"
where
  "action_loc_aux P (NormalAction (NewHeapElem ad (Class_type C))) = 
  {(ad, CField D F)|D F T fm. P ⊢ C has F:T (fm) in D}"
| "action_loc_aux P (NormalAction (NewHeapElem ad (Array_type T n'))) = 
  {(ad, ACell n)|n. n < n'} ∪ {(ad, CField D F)|D F T fm. P ⊢ Object has F:T (fm) in D}"
| "action_loc_aux P (NormalAction (WriteMem ad al v)) = {(ad, al)}"
| "action_loc_aux P (NormalAction (ReadMem ad al v)) = {(ad, al)}"
| "action_loc_aux _ _ = {}"

lemma action_loc_aux_intros [intro?]:
  "P ⊢ class_type_of hT has F:T (fm) in D ⟹ (ad, CField D F) ∈ action_loc_aux P (NormalAction (NewHeapElem ad hT))"
  "n < n' ⟹ (ad, ACell n) ∈ action_loc_aux P (NormalAction (NewHeapElem ad (Array_type T n')))"
  "(ad, al) ∈ action_loc_aux P (NormalAction (WriteMem ad al v))"
  "(ad, al) ∈ action_loc_aux P (NormalAction (ReadMem ad al v))"
by(cases hT) auto

lemma action_loc_aux_cases [elim?, cases set: action_loc_aux]:
  assumes "adal ∈ action_loc_aux P obs"
  obtains (NewHeapElem) hT F T fm D ad where "obs = NormalAction (NewHeapElem ad hT)" "adal = (ad, CField D F)" "P ⊢ class_type_of hT has F:T (fm) in D"
  | (NewArr) n n' ad T where "obs = NormalAction (NewHeapElem ad (Array_type T n'))" "adal = (ad, ACell n)" "n < n'"
  | (WriteMem) ad al v where "obs = NormalAction (WriteMem ad al v)" "adal = (ad, al)"
  | (ReadMem) ad al v where "obs = NormalAction (ReadMem ad al v)" "adal = (ad, al)"
using assms by(cases "(P, obs)" rule: action_loc_aux.cases) fastforce+

lemma action_loc_aux_simps [simp]:
  "(ad', al') ∈ action_loc_aux P (NormalAction (NewHeapElem ad hT)) ⟷ 
   (∃D F T fm. ad = ad' ∧ al' = CField D F ∧ P ⊢ class_type_of hT has F:T (fm) in D) ∨ 
   (∃n T n'. ad = ad' ∧ al' = ACell n ∧ hT = Array_type T n' ∧ n < n')"
  "(ad', al') ∈ action_loc_aux P (NormalAction (WriteMem ad al v)) ⟷ ad = ad' ∧ al = al'"
  "(ad', al') ∈ action_loc_aux P (NormalAction (ReadMem ad al v)) ⟷ ad = ad' ∧ al = al'"
  "(ad', al') ∉ action_loc_aux P InitialThreadAction"
  "(ad', al') ∉ action_loc_aux P ThreadFinishAction"
  "(ad', al') ∉ action_loc_aux P (NormalAction (ExternalCall a m vs v))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (ThreadStart t))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (ThreadJoin t))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (SyncLock a))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (SyncUnlock a))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (ObsInterrupt t))"
  "(ad', al') ∉ action_loc_aux P (NormalAction (ObsInterrupted t))"
by(cases hT) auto

declare action_loc_aux.simps [simp del]

abbreviation action_loc :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ ('addr × addr_loc) set"
where "action_loc P E a ≡ action_loc_aux P (action_obs E a)"

inductive_set read_actions :: "('addr, 'thread_id) execution ⇒ JMM_action set"
for E :: "('addr, 'thread_id) execution"
where 
  ReadMem: "⟦ a ∈ actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧ ⟹ a ∈ read_actions E"

fun addr_loc_default :: "'m prog ⇒ htype ⇒ addr_loc ⇒ 'addr val"
where
  "addr_loc_default P (Class_type C) (CField D F) = default_val (fst (the (map_of (fields P C) (F, D))))"
| "addr_loc_default P (Array_type T n) (ACell n') = default_val T"
| addr_loc_default_Array_CField: 
  "addr_loc_default P (Array_type T n) (CField D F) = default_val (fst (the (map_of (fields P Object) (F, Object))))"
| "addr_loc_default P _ _ = undefined"

definition new_actions_for :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ ('addr × addr_loc) ⇒ JMM_action set"
where 
  "new_actions_for P E adal =
   {a. a ∈ actions E ∧ adal ∈ action_loc P E a ∧ is_new_action (action_obs E a)}"

inductive_set external_actions :: "('addr, 'thread_id) execution ⇒ JMM_action set"
for E :: "('addr, 'thread_id) execution"
where
  "⟦ a ∈ actions E; action_obs E a = NormalAction (ExternalCall ad M vs v) ⟧ 
  ⟹ a ∈ external_actions E"

fun value_written_aux :: "'m prog ⇒ ('addr, 'thread_id) obs_event action ⇒ addr_loc ⇒ 'addr val"
where
  "value_written_aux P (NormalAction (NewHeapElem ad' hT)) al = addr_loc_default P hT al"
| value_written_aux_WriteMem':
  "value_written_aux P (NormalAction (WriteMem ad al' v)) al = (if al = al' then v else undefined)"
| value_written_aux_undefined:
  "value_written_aux P _ al = undefined"

primrec value_written :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ ('addr × addr_loc) ⇒ 'addr val"
where "value_written P E a (ad, al) = value_written_aux P (action_obs E a) al"

definition value_read :: "('addr, 'thread_id) execution ⇒ JMM_action ⇒ 'addr val"
where
  "value_read E a = 
  (case action_obs E a of
     NormalAction obs ⇒
        (case obs of
           ReadMem ad al v ⇒ v
         | _ ⇒ undefined)
   | _ ⇒ undefined)"

definition action_order :: "('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool" (‹_ ⊢ _ ≤a _› [51,0,50] 50)
where
  "E ⊢ a ≤a a' ⟷
   a ∈ actions E ∧ a' ∈ actions E ∧ 
   (if is_new_action (action_obs E a)
    then is_new_action (action_obs E a') ⟶ a ≤ a'
    else ¬ is_new_action (action_obs E a') ∧ a ≤ a')"

definition program_order :: "('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool" (‹_ ⊢ _ ≤po _› [51,0,50] 50)
where
  "E ⊢ a ≤po a' ⟷ E ⊢ a ≤a a' ∧ action_tid E a = action_tid E a'"

inductive synchronizes_with :: 
  "'m prog 
  ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) ⇒ bool" 
  (‹_ ⊢ _ ↝sw _› [51, 51, 51] 50)
  for P :: "'m prog"
where
  ThreadStart: "P ⊢ (t, NormalAction (ThreadStart t')) ↝sw (t', InitialThreadAction)"
| ThreadFinish: "P ⊢ (t, ThreadFinishAction) ↝sw (t', NormalAction (ThreadJoin t))"
| UnlockLock: "P ⊢ (t, NormalAction (SyncUnlock a)) ↝sw (t', NormalAction (SyncLock a))"
| ― ‹Only volatile writes synchronize with volatile reads. 
       We could check volatility of @{term "al"} here, but this is checked by @{term "sactions"}
       in @{text sync_with} anyway.›
  Volatile: "P ⊢ (t, NormalAction (WriteMem a al v)) ↝sw (t', NormalAction (ReadMem a al v'))"
| VolatileNew: "
    al ∈ addr_locs P hT
    ⟹ P ⊢ (t, NormalAction (NewHeapElem a hT)) ↝sw (t', NormalAction (ReadMem a al v))"
| NewHeapElem: "P ⊢ (t, NormalAction (NewHeapElem a hT)) ↝sw (t', InitialThreadAction)"
| Interrupt: "P ⊢ (t, NormalAction (ObsInterrupt t')) ↝sw (t'', NormalAction (ObsInterrupted t'))"

definition sync_order :: 
  "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool"
  (‹_,_ ⊢ _ ≤so _› [51,0,0,50] 50)
where
  "P,E ⊢ a ≤so a' ⟷ a ∈ sactions P E ∧ a' ∈ sactions P E ∧ E ⊢ a ≤a a'"

definition sync_with :: 
  "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool"
  (‹_,_ ⊢ _ ≤sw _› [51, 0, 0, 50] 50)
where
  "P,E ⊢ a ≤sw a' ⟷
   P,E ⊢ a ≤so a' ∧ P ⊢ (action_tid E a, action_obs E a) ↝sw (action_tid E a', action_obs E a')"

definition po_sw :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool"
where "po_sw P E a a' ⟷ E ⊢ a ≤po a' ∨ P,E ⊢ a ≤sw a'"

abbreviation happens_before :: 
  "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool"
  (‹_,_ ⊢ _ ≤hb _› [51, 0, 0, 50] 50)
where "happens_before P E ≡ (po_sw P E)^++"

type_synonym write_seen = "JMM_action ⇒ JMM_action"

definition is_write_seen :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ write_seen ⇒ bool" where 
  "is_write_seen P E ws ⟷
   (∀a ∈ read_actions E. ∀ad al v. action_obs E a = NormalAction (ReadMem ad al v) ⟶ 
       ws a ∈ write_actions E ∧ (ad, al) ∈ action_loc P E (ws a) ∧
       value_written P E (ws a) (ad, al) = v ∧ ¬ P,E ⊢ a ≤hb ws a ∧
       (is_volatile P al ⟶ ¬ P,E ⊢ a ≤so ws a) ∧
       (∀w' ∈ write_actions E. (ad, al) ∈ action_loc P E w' ⟶ 
          (P,E ⊢ ws a ≤hb w' ∧ P,E ⊢ w' ≤hb a ∨ is_volatile P al ∧ P,E ⊢ ws a ≤so w' ∧ P,E ⊢ w' ≤so a) ⟶
          w' = ws a))"

definition thread_start_actions_ok :: "('addr, 'thread_id) execution ⇒ bool"
where
  "thread_start_actions_ok E ⟷ 
  (∀a ∈ actions E. ¬ is_new_action (action_obs E a) ⟶ 
     (∃i. i ≤ a ∧ action_obs E i = InitialThreadAction ∧ action_tid E i = action_tid E a))"

primrec wf_exec :: "'m prog ⇒ ('addr, 'thread_id) execution × write_seen ⇒ bool" (‹_ ⊢ _ √› [51, 50] 51)
where "P ⊢ (E, ws) √ ⟷ is_write_seen P E ws ∧ thread_start_actions_ok E"

inductive most_recent_write_for :: "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool"
  (‹_,_ ⊢ _ ↝mrw _› [50, 0, 51] 51)
for P :: "'m prog" and E :: "('addr, 'thread_id) execution" and ra :: JMM_action and wa :: JMM_action
where
  "⟦ ra ∈ read_actions E; adal ∈ action_loc P E ra; E ⊢ wa ≤a ra;
     wa ∈ write_actions E; adal ∈ action_loc P E wa;
     ⋀wa'. ⟦ wa' ∈ write_actions E; adal ∈ action_loc P E wa' ⟧
     ⟹ E ⊢ wa' ≤a wa ∨ E ⊢ ra ≤a wa' ⟧
  ⟹ P,E ⊢ ra ↝mrw wa"

primrec sequentially_consistent :: "'m prog ⇒ (('addr, 'thread_id) execution × write_seen) ⇒ bool"
where 
  "sequentially_consistent P (E, ws) ⟷ (∀r ∈ read_actions E. P,E ⊢ r ↝mrw ws r)"


subsection ‹Actions›

inductive_cases is_new_action_cases [elim!]:
  "is_new_action (NormalAction (ExternalCall a M vs v))"
  "is_new_action (NormalAction (ReadMem a al v))"
  "is_new_action (NormalAction (WriteMem a al v))"
  "is_new_action (NormalAction (NewHeapElem a hT))"
  "is_new_action (NormalAction (ThreadStart t))"
  "is_new_action (NormalAction (ThreadJoin t))"
  "is_new_action (NormalAction (SyncLock a))"
  "is_new_action (NormalAction (SyncUnlock a))"
  "is_new_action (NormalAction (ObsInterrupt t))"
  "is_new_action (NormalAction (ObsInterrupted t))"
  "is_new_action InitialThreadAction"
  "is_new_action ThreadFinishAction"

inductive_simps is_new_action_simps [simp]:
  "is_new_action (NormalAction (NewHeapElem a hT))"
  "is_new_action (NormalAction (ExternalCall a M vs v))"
  "is_new_action (NormalAction (ReadMem a al v))"
  "is_new_action (NormalAction (WriteMem a al v))"
  "is_new_action (NormalAction (ThreadStart t))"
  "is_new_action (NormalAction (ThreadJoin t))"
  "is_new_action (NormalAction (SyncLock a))"
  "is_new_action (NormalAction (SyncUnlock a))"
  "is_new_action (NormalAction (ObsInterrupt t))"
  "is_new_action (NormalAction (ObsInterrupted t))"
  "is_new_action InitialThreadAction"
  "is_new_action ThreadFinishAction"

lemmas is_new_action_iff = is_new_action.simps

inductive_simps is_write_action_simps [simp]:
  "is_write_action InitialThreadAction"
  "is_write_action ThreadFinishAction"
  "is_write_action (NormalAction (ExternalCall a m vs v))"
  "is_write_action (NormalAction (ReadMem a al v))"
  "is_write_action (NormalAction (WriteMem a al v))"
  "is_write_action (NormalAction (NewHeapElem a hT))"
  "is_write_action (NormalAction (ThreadStart t))"
  "is_write_action (NormalAction (ThreadJoin t))"
  "is_write_action (NormalAction (SyncLock a))"
  "is_write_action (NormalAction (SyncUnlock a))"
  "is_write_action (NormalAction (ObsInterrupt t))"
  "is_write_action (NormalAction (ObsInterrupted t))"

declare saction.intros [intro!]

inductive_cases saction_cases [elim!]:
  "saction P (NormalAction (ExternalCall a M vs v))"
  "saction P (NormalAction (ReadMem a al v))"
  "saction P (NormalAction (WriteMem a al v))"
  "saction P (NormalAction (NewHeapElem a hT))"
  "saction P (NormalAction (ThreadStart t))"
  "saction P (NormalAction (ThreadJoin t))"
  "saction P (NormalAction (SyncLock a))"
  "saction P (NormalAction (SyncUnlock a))"
  "saction P (NormalAction (ObsInterrupt t))"
  "saction P (NormalAction (ObsInterrupted t))"
  "saction P InitialThreadAction"
  "saction P ThreadFinishAction"

inductive_simps saction_simps [simp]:
  "saction P (NormalAction (ExternalCall a M vs v))"
  "saction P (NormalAction (ReadMem a al v))"
  "saction P (NormalAction (WriteMem a al v))"
  "saction P (NormalAction (NewHeapElem a hT))"
  "saction P (NormalAction (ThreadStart t))"
  "saction P (NormalAction (ThreadJoin t))"
  "saction P (NormalAction (SyncLock a))"
  "saction P (NormalAction (SyncUnlock a))"
  "saction P (NormalAction (ObsInterrupt t))"
  "saction P (NormalAction (ObsInterrupted t))"
  "saction P InitialThreadAction"
  "saction P ThreadFinishAction"

lemma new_action_saction [simp, intro]: "is_new_action a ⟹ saction P a"
by(blast elim: is_new_action.cases)

lemmas saction_iff = saction.simps

lemma actionsD: "a ∈ actions E ⟹ enat a < llength E"
unfolding actions_def by blast

lemma actionsE: 
  assumes "a ∈ actions E"
  obtains "enat a < llength E"
using assms unfolding actions_def by blast

lemma actions_lappend:
  "llength xs = enat n ⟹ actions (lappend xs ys) = actions xs ∪ ((+) n) ` actions ys"
unfolding actions_def
apply safe
  apply(erule contrapos_np)
  apply(rule_tac x="x - n" in image_eqI)
   apply simp_all
  apply(case_tac [!] "llength ys")
 apply simp_all
done

lemma tactionsE:
  assumes "a ∈ tactions E t"
  obtains obs where "a ∈ actions E" "action_tid E a = t" "action_obs E a = obs"
using assms
by(cases "lnth E a")(auto simp add: tactions_def action_tid_def action_obs_def)

lemma sactionsI:
  "⟦ a ∈ actions E; saction P (action_obs E a) ⟧ ⟹ a ∈ sactions P E"
unfolding sactions_def by blast

lemma sactionsE:
  assumes "a ∈ sactions P E"
  obtains "a ∈ actions E" "saction P (action_obs E a)"
using assms unfolding sactions_def by blast

lemma sactions_actions [simp]:
  "a ∈ sactions P E ⟹ a ∈ actions E"
by(rule sactionsE)

lemma value_written_aux_WriteMem [simp]:
  "value_written_aux P (NormalAction (WriteMem ad al v)) al = v"
by simp

declare value_written_aux_undefined [simp del]
declare value_written_aux_WriteMem' [simp del]

inductive_simps is_write_action_iff:
  "is_write_action a"

inductive_simps write_actions_iff:
  "a ∈ write_actions E"

lemma write_actions_actions [simp]:
  "a ∈ write_actions E ⟹ a ∈ actions E"
by(rule write_actions.induct)

inductive_simps read_actions_iff:
  "a ∈ read_actions E"

lemma read_actions_actions [simp]:
  "a ∈ read_actions E ⟹ a ∈ actions E"
by(rule read_actions.induct)

lemma read_action_action_locE:
  assumes "r ∈ read_actions E"
  obtains ad al where "(ad, al) ∈ action_loc P E r"
using assms by cases auto

lemma read_actions_not_write_actions:
  "⟦ a ∈ read_actions E; a ∈ write_actions E ⟧ ⟹ False"
by(auto elim!: read_actions.cases write_actions.cases)

lemma read_actions_Int_write_actions [simp]:
  "read_actions E ∩ write_actions E = {}"
  "write_actions E ∩ read_actions E = {}"
by(blast dest: read_actions_not_write_actions)+

lemma action_loc_addr_fun:
  "⟦ (ad, al) ∈ action_loc P E a; (ad', al') ∈ action_loc P E a ⟧ ⟹ ad = ad'"
by(auto elim!: action_loc_aux_cases)

lemma value_written_cong [cong]:
  "⟦ P = P'; a = a'; action_obs E a' = action_obs E' a' ⟧ 
  ⟹ value_written P E a = value_written P' E' a'"
by(rule ext)(auto split: action.splits)

declare value_written.simps [simp del]

lemma new_actionsI:
  "⟦ a ∈ actions E; adal ∈ action_loc P E a; is_new_action (action_obs E a) ⟧
  ⟹ a ∈ new_actions_for P E adal"
unfolding new_actions_for_def by blast

lemma new_actionsE:
  assumes "a ∈ new_actions_for P E adal"
  obtains "a ∈ actions E" "adal ∈ action_loc P E a" "is_new_action (action_obs E a)"
using assms unfolding new_actions_for_def by blast

lemma action_loc_read_action_singleton:
  "⟦ r ∈ read_actions E; adal ∈ action_loc P E r; adal' ∈ action_loc P E r ⟧ ⟹ adal = adal'"
by(cases adal, cases adal')(fastforce elim: read_actions.cases action_loc_aux_cases)

lemma addr_locsI:
  "P ⊢ class_type_of hT has F:T (fm) in D ⟹ CField D F ∈ addr_locs P hT"
  "⟦ hT = Array_type T n; n' < n ⟧ ⟹ ACell n' ∈ addr_locs P hT"
by(cases hT)(auto dest: has_field_decl_above)

subsection ‹Orders›
subsection ‹Action order›

lemma action_orderI:
  assumes "a ∈ actions E" "a' ∈ actions E"
  and "⟦ is_new_action (action_obs E a); is_new_action (action_obs E a') ⟧ ⟹ a ≤ a'"
  and "¬ is_new_action (action_obs E a) ⟹ ¬ is_new_action (action_obs E a') ∧ a ≤ a'"
  shows "E ⊢ a ≤a a'"
using assms unfolding action_order_def by simp

lemma action_orderE:
  assumes "E ⊢ a ≤a a'"
  obtains "a ∈ actions E" "a' ∈ actions E" 
          "is_new_action (action_obs E a)" "is_new_action (action_obs E a') ⟶ a ≤ a'"
        | "a ∈ actions E" "a' ∈ actions E" 
          "¬ is_new_action (action_obs E a)" "¬ is_new_action (action_obs E a')" "a ≤ a'"
using assms unfolding action_order_def by(simp split: if_split_asm)

lemma refl_action_order:
  "refl_onP (actions E) (action_order E)"
by(rule refl_onPI)(auto elim: action_orderE intro: action_orderI)

lemma antisym_action_order:
  "antisymp (action_order E)"
by(rule antisympI)(auto elim!: action_orderE)

lemma trans_action_order:
  "transp (action_order E)"
by(rule transpI)(auto elim!: action_orderE intro: action_orderI)

lemma porder_action_order:
  "porder_on (actions E) (action_order E)"
by(blast intro: porder_onI refl_action_order antisym_action_order trans_action_order)

lemma total_action_order:
  "total_onP (actions E) (action_order E)"
by(rule total_onPI)(auto simp add: action_order_def)

lemma torder_action_order:
  "torder_on (actions E) (action_order E)"
by(blast intro: torder_onI total_action_order porder_action_order)

lemma wf_action_order: "wfP (action_order E)⇧≠⇧≠"
unfolding wfp_eq_minimal
proof(intro strip)
  fix Q and x :: JMM_action
  assume "x ∈ Q"
  show "∃z ∈ Q. ∀y. (action_order E)⇧≠⇧≠ y z ⟶ y ∉ Q"
  proof(cases "∃a ∈ Q. a ∈ actions E ∧ is_new_action (action_obs E a)")
    case True
    then obtain a where a: "a ∈ actions E ∧ is_new_action (action_obs E a) ∧ a ∈ Q" by blast
    define a' where "a' = (LEAST a'. a' ∈ actions E ∧ is_new_action (action_obs E a') ∧ a' ∈ Q)"
    from a have a': "a' ∈ actions E ∧ is_new_action (action_obs E a') ∧ a' ∈ Q"
      unfolding a'_def by(rule LeastI)
    { fix y
      assume y_le_a': "(action_order E)⇧≠⇧≠ y a'"
      have "y ∉ Q"
      proof
        assume "y ∈ Q"
        with y_le_a' a' have y: "y ∈ actions E ∧ is_new_action (action_obs E y) ∧ y ∈ Q"
          by(auto elim: action_orderE)
        hence "a' ≤ y" unfolding a'_def by(rule Least_le)
        with y_le_a' a' show False by(auto elim: action_orderE)
      qed }
    with a' show ?thesis by blast
  next
    case False
    hence not_new: "⋀a. ⟦ a ∈ Q; a ∈ actions E ⟧ ⟹ ¬ is_new_action (action_obs E a)" by blast
    show ?thesis
    proof(cases "Q ∩ actions E = {}")
      case True
      with ‹x ∈ Q› show ?thesis by(auto elim: action_orderE)
    next
      case False
      define a' where "a' = (LEAST a'. a' ∈ Q ∧ a' ∈ actions E ∧ ¬ is_new_action (action_obs E a'))"
      from False obtain a where "a ∈ Q" "a ∈ actions E" by blast
      with not_new[OF this] have "a ∈ Q ∧ a ∈ actions E ∧ ¬ is_new_action (action_obs E a)" by blast
      hence a': "a' ∈ Q ∧ a' ∈ actions E ∧ ¬ is_new_action (action_obs E a')"
        unfolding a'_def by(rule LeastI)
      { fix y
        assume y_le_a': "(action_order E)⇧≠⇧≠ y a'"
        hence "y ∈ actions E" by(auto elim: action_orderE)
        have "y ∉ Q"
        proof
          assume "y ∈ Q"
          hence y_not_new: "¬ is_new_action (action_obs E y)"
            using ‹y ∈ actions E› by(rule not_new)
          with ‹y ∈ Q› ‹y ∈ actions E› have "a' ≤ y"
            unfolding a'_def by -(rule Least_le, blast)
          with y_le_a' y_not_new show False by(auto elim: action_orderE)
        qed }
      with a' show ?thesis by blast
    qed
  qed
qed

lemma action_order_is_new_actionD:
  "⟦ E ⊢ a ≤a a'; is_new_action (action_obs E a') ⟧ ⟹ is_new_action (action_obs E a)"
by(auto elim: action_orderE)

subsection ‹Program order›

lemma program_orderI:
  assumes "E ⊢ a ≤a a'" and "action_tid E a = action_tid E a'"
  shows "E ⊢ a ≤po a'"
using assms unfolding program_order_def by auto

lemma program_orderE:
  assumes "E ⊢ a ≤po a'"
  obtains t obs obs'
  where "E ⊢ a ≤a a'"
  and "action_tid E a = t" "action_obs E a = obs"
  and "action_tid E a' = t" "action_obs E a' = obs'"
using assms unfolding program_order_def
by(cases "lnth E a")(cases "lnth E a'", auto simp add: action_obs_def action_tid_def)

lemma refl_on_program_order:
  "refl_onP (actions E) (program_order E)"
by(rule refl_onPI)(auto elim: action_orderE program_orderE intro: program_orderI refl_onPD[OF refl_action_order])

lemma antisym_program_order:
  "antisymp (program_order E)"
using antisympD[OF antisym_action_order]
by(auto intro: antisympI elim!: program_orderE)

lemma trans_program_order:
  "transp (program_order E)"
by(rule transpI)(auto elim!: program_orderE intro: program_orderI dest: transPD[OF trans_action_order])

lemma porder_program_order:
  "porder_on (actions E) (program_order E)"
by(blast intro: porder_onI refl_on_program_order antisym_program_order trans_program_order)

lemma total_program_order_on_tactions:
  "total_onP (tactions E t) (program_order E)"
by(rule total_onPI)(auto elim: tactionsE simp add: program_order_def dest: total_onD[OF total_action_order])


subsection ‹Synchronization order›

lemma sync_orderI:
  "⟦ E ⊢ a ≤a a'; a ∈ sactions P E; a' ∈ sactions P E ⟧ ⟹ P,E ⊢ a ≤so a'"
unfolding sync_order_def by blast

lemma sync_orderE:
  assumes "P,E ⊢ a ≤so a'"
  obtains "a ∈ sactions P E" "a' ∈ sactions P E" "E ⊢ a ≤a a'"
using assms unfolding sync_order_def by blast

lemma refl_on_sync_order:
  "refl_onP (sactions P E) (sync_order P E)"
by(rule refl_onPI)(fastforce elim: sync_orderE intro: sync_orderI refl_onPD[OF refl_action_order])+

lemma antisym_sync_order:
  "antisymp (sync_order P E)"
using antisympD[OF antisym_action_order]
by(rule antisympI)(auto elim!: sync_orderE)

lemma trans_sync_order:
  "transp (sync_order P E)"
by(rule transpI)(auto elim!: sync_orderE intro: sync_orderI dest: transPD[OF trans_action_order])

lemma porder_sync_order:
  "porder_on (sactions P E) (sync_order P E)"
by(blast intro: porder_onI refl_on_sync_order antisym_sync_order trans_sync_order)

lemma total_sync_order:
  "total_onP (sactions P E) (sync_order P E)"
apply(rule total_onPI)
apply(simp add: sync_order_def)
apply(rule total_onPD[OF total_action_order])
apply simp_all
done

lemma torder_sync_order:
  "torder_on (sactions P E) (sync_order P E)"
by(blast intro: torder_onI porder_sync_order total_sync_order)

subsection ‹Synchronizes with›

lemma sync_withI:
  "⟦ P,E ⊢ a ≤so a'; P ⊢ (action_tid E a, action_obs E a) ↝sw (action_tid E a', action_obs E a') ⟧
  ⟹ P,E ⊢ a ≤sw a'"
unfolding sync_with_def by blast

lemma sync_withE:
  assumes "P,E ⊢ a ≤sw a'"
  obtains "P,E ⊢ a ≤so a'" "P ⊢ (action_tid E a, action_obs E a) ↝sw (action_tid E a', action_obs E a')"
using assms unfolding sync_with_def by blast

lemma irrefl_synchronizes_with:
  "irreflP (synchronizes_with P)"
by(rule irreflPI)(auto elim: synchronizes_with.cases)

lemma irrefl_sync_with:
  "irreflP (sync_with P E)"
by(rule irreflPI)(auto elim: sync_withE intro: irreflPD[OF irrefl_synchronizes_with])

lemma anitsym_sync_with:
  "antisymp (sync_with P E)"
using antisymPD[OF antisym_sync_order, of P E]
by -(rule antisymPI, auto elim: sync_withE)

lemma consistent_program_order_sync_order:
  "order_consistent (program_order E) (sync_order P E)"
apply(rule order_consistent_subset)
apply(rule antisym_order_consistent_self[OF antisym_action_order[of E]])
apply(blast elim: program_orderE sync_orderE)+
done

lemma consistent_program_order_sync_with:
  "order_consistent (program_order E) (sync_with P E)"
by(rule order_consistent_subset[OF consistent_program_order_sync_order])(blast elim: sync_withE)+

subsection ‹Happens before›

lemma porder_happens_before:
  "porder_on (actions E) (happens_before P E)"
unfolding po_sw_def [abs_def]
by(rule porder_on_sub_torder_on_tranclp_porder_onI[OF porder_program_order torder_sync_order consistent_program_order_sync_order])(auto elim: sync_withE)

lemma porder_tranclp_po_so:
  "porder_on (actions E) (λa a'. program_order E a a' ∨ sync_order P E a a')^++"
by(rule porder_on_torder_on_tranclp_porder_onI[OF porder_program_order torder_sync_order consistent_program_order_sync_order]) auto

lemma happens_before_refl:
  assumes "a ∈ actions E"
  shows "P,E ⊢ a ≤hb a"
using porder_happens_before[of E P]
by(rule porder_onE)(erule refl_onPD[OF _ assms])

lemma happens_before_into_po_so_tranclp:
  assumes "P,E ⊢ a ≤hb a'"
  shows "(λa a'. E ⊢ a ≤po a' ∨ P,E ⊢ a ≤so a')^++ a a'"
using assms unfolding po_sw_def [abs_def]
by(induct)(blast elim: sync_withE intro: tranclp.trancl_into_trancl)+

lemma po_sw_into_action_order:
  "po_sw P E a a' ⟹ E ⊢ a ≤a a'"
by(auto elim: program_orderE sync_withE sync_orderE simp add: po_sw_def)

lemma happens_before_into_action_order:
  assumes "P,E ⊢ a ≤hb a'"
  shows "E ⊢ a ≤a a'"
using assms
by induct(blast intro: po_sw_into_action_order transPD[OF trans_action_order])+

lemma action_order_consistent_with_happens_before:
  "order_consistent (action_order E) (happens_before P E)"
by(blast intro: order_consistent_subset antisym_order_consistent_self antisym_action_order happens_before_into_action_order)

lemma happens_before_new_actionD:
  assumes hb: "P,E ⊢ a ≤hb a'"
  and new: "is_new_action (action_obs E a')"
  shows "is_new_action (action_obs E a)" "action_tid E a = action_tid E a'" "a ≤ a'"
using hb
proof(induct rule: converse_tranclp_induct)
  case (base a)

  case 1 from new base show ?case
    by(auto dest: po_sw_into_action_order elim: action_orderE)
  case 2 from new base show ?case
    by(auto simp add: po_sw_def elim!: sync_withE elim: program_orderE synchronizes_with.cases)
  case 3 from new base show ?case
    by(auto dest: po_sw_into_action_order elim: action_orderE)
next
  case (step a a'')
  
  note po_sw = ‹po_sw P E a a''›
    and new = ‹is_new_action (action_obs E a'')›
    and tid = ‹action_tid E a'' = action_tid E a'›
  
  case 1 from new po_sw show ?case
    by(auto dest: po_sw_into_action_order elim: action_orderE)
  case 2 from new po_sw tid show ?case
    by(auto simp add: po_sw_def elim!: sync_withE elim: program_orderE synchronizes_with.cases)
  case 3 from new po_sw ‹a'' ≤ a'› show ?case
    by(auto dest!: po_sw_into_action_order elim!: action_orderE)
qed

lemma external_actions_not_new:
  "⟦ a ∈ external_actions E; is_new_action (action_obs E a) ⟧ ⟹ False"
by(erule external_actions.cases)(simp)

subsection ‹Most recent writes and sequential consistency›

lemma most_recent_write_for_fun:
  "⟦ P,E ⊢ ra ↝mrw wa; P,E ⊢ ra ↝mrw wa' ⟧ ⟹ wa = wa'"
apply(erule most_recent_write_for.cases)+
apply clarsimp
apply(erule meta_allE)+
apply(erule meta_impE)
 apply(rotate_tac 3)
 apply assumption
apply(erule (1) meta_impE)
apply(frule (1) action_loc_read_action_singleton)
 apply(rotate_tac 1)
 apply assumption
apply(fastforce dest: antisymPD[OF antisym_action_order] elim: write_actions.cases read_actions.cases)
done

lemma THE_most_recent_writeI: "P,E ⊢ r ↝mrw w ⟹ (THE w. P,E ⊢ r ↝mrw w) = w"
by(blast dest: most_recent_write_for_fun)+

lemma most_recent_write_for_write_actionsD:
  assumes "P,E ⊢ ra ↝mrw wa"
  shows "wa ∈ write_actions E"
using assms by cases

lemma most_recent_write_recent:
  "⟦ P,E ⊢ r ↝mrw w; adal ∈ action_loc P E r; w' ∈ write_actions E; adal ∈ action_loc P E w' ⟧ 
  ⟹ E ⊢ w' ≤a w ∨ E ⊢ r ≤a w'"
apply(erule most_recent_write_for.cases)
apply(drule (1) action_loc_read_action_singleton)
 apply(rotate_tac 1)
 apply assumption
apply clarsimp
done

lemma is_write_seenI:
  "⟦ ⋀a ad al v. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧
     ⟹ ws a ∈ write_actions E;
     ⋀a ad al v. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧
     ⟹ (ad, al) ∈ action_loc P E (ws a);
     ⋀a ad al v. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧
     ⟹ value_written P E (ws a) (ad, al) = v;
     ⋀a ad al v. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧
     ⟹ ¬ P,E ⊢ a ≤hb ws a;
     ⋀a ad al v. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al ⟧
     ⟹ ¬ P,E ⊢ a ≤so ws a;
     ⋀a ad al v a'. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v);
                      a' ∈ write_actions E; (ad, al) ∈ action_loc P E a'; P,E ⊢ ws a ≤hb a';
                      P,E ⊢ a' ≤hb a ⟧ ⟹ a' = ws a;
     ⋀a ad al v a'. ⟦ a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v);
                      a' ∈ write_actions E; (ad, al) ∈ action_loc P E a'; is_volatile P al; P,E ⊢ ws a ≤so a';
                      P,E ⊢ a' ≤so a ⟧ ⟹ a' = ws a ⟧
  ⟹ is_write_seen P E ws"
unfolding is_write_seen_def
by(blast 30)

lemma is_write_seenD:
  "⟦ is_write_seen P E ws; a ∈ read_actions E; action_obs E a = NormalAction (ReadMem ad al v) ⟧
  ⟹ ws a ∈ write_actions E ∧ (ad, al) ∈ action_loc P E (ws a) ∧ value_written P E (ws a) (ad, al) = v ∧ ¬ P,E ⊢ a ≤hb ws a ∧ (is_volatile P al ⟶ ¬ P,E ⊢ a ≤so ws 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)"
unfolding is_write_seen_def by blast

lemma thread_start_actions_okI:
  "(⋀a. ⟦ a ∈ actions E; ¬ is_new_action (action_obs E a) ⟧ 
    ⟹ ∃i. i ≤ a ∧ action_obs E i = InitialThreadAction ∧ action_tid E i = action_tid E a)
  ⟹ thread_start_actions_ok E"
unfolding thread_start_actions_ok_def by blast

lemma thread_start_actions_okD:
  "⟦ thread_start_actions_ok E; a ∈ actions E; ¬ is_new_action (action_obs E a) ⟧ 
  ⟹ ∃i. i ≤ a ∧ action_obs E i = InitialThreadAction ∧ action_tid E i = action_tid E a"
unfolding thread_start_actions_ok_def by blast

lemma thread_start_actions_ok_prefix:
  "⟦ thread_start_actions_ok E'; lprefix E E' ⟧ ⟹ thread_start_actions_ok E"
  apply(clarsimp simp add: lprefix_conv_lappend)
  apply(rule thread_start_actions_okI)
  apply(drule_tac a=a in thread_start_actions_okD)
    apply(simp add: actions_def)
    apply(auto simp add: action_obs_def lnth_lappend1 actions_def action_tid_def le_less_trans[where y="enat a" for a])
  apply (metis add.right_neutral add_strict_mono not_gr_zero)
  done

lemma wf_execI [intro?]:
  "⟦ is_write_seen P E ws;
    thread_start_actions_ok E ⟧
  ⟹ P ⊢ (E, ws) √"
by simp

lemma wf_exec_is_write_seenD:
  "P ⊢ (E, ws) √ ⟹ is_write_seen P E ws"
by simp

lemma wf_exec_thread_start_actions_okD:
  "P ⊢ (E, ws) √ ⟹ thread_start_actions_ok E"
by simp

lemma sequentially_consistentI:
  "(⋀r. r ∈ read_actions E ⟹ P,E ⊢ r ↝mrw ws r)
  ⟹ sequentially_consistent P (E, ws)"
by simp

lemma sequentially_consistentE:
  assumes "sequentially_consistent P (E, ws)" "a ∈ read_actions E"
  obtains "P,E ⊢ a ↝mrw ws a"
using assms by simp

declare sequentially_consistent.simps [simp del]

subsection ‹Similar actions›

text ‹Similar actions differ only in the values written/read.›

inductive sim_action :: 
  "('addr, 'thread_id) obs_event action ⇒ ('addr, 'thread_id) obs_event action ⇒ bool" 
  (‹_ ≈ _› [50, 50] 51)
where
  InitialThreadAction: "InitialThreadAction ≈ InitialThreadAction"
| ThreadFinishAction: "ThreadFinishAction ≈ ThreadFinishAction"
| NewHeapElem: "NormalAction (NewHeapElem a hT) ≈ NormalAction (NewHeapElem a hT)"
| ReadMem: "NormalAction (ReadMem ad al v) ≈ NormalAction (ReadMem ad al v')"
| WriteMem: "NormalAction (WriteMem ad al v) ≈ NormalAction (WriteMem ad al v')"
| ThreadStart: "NormalAction (ThreadStart t) ≈ NormalAction (ThreadStart t)"
| ThreadJoin: "NormalAction (ThreadJoin t) ≈ NormalAction (ThreadJoin t)"
| SyncLock: "NormalAction (SyncLock a) ≈ NormalAction (SyncLock a)"
| SyncUnlock: "NormalAction (SyncUnlock a) ≈ NormalAction (SyncUnlock a)"
| ExternalCall: "NormalAction (ExternalCall a M vs v) ≈ NormalAction (ExternalCall a M vs v)"
| ObsInterrupt: "NormalAction (ObsInterrupt t) ≈ NormalAction (ObsInterrupt t)"
| ObsInterrupted: "NormalAction (ObsInterrupted t) ≈ NormalAction (ObsInterrupted t)"

definition sim_actions :: "('addr, 'thread_id) execution ⇒ ('addr, 'thread_id) execution ⇒ bool" (‹_ [≈] _› [51, 50] 51)
where "sim_actions = llist_all2 (λ(t, a) (t', a'). t = t' ∧ a ≈ a')"

lemma sim_action_refl [intro!, simp]:
  "obs ≈ obs"
apply(cases obs)
 apply(rename_tac obs')
 apply(case_tac "obs'")
apply(auto intro: sim_action.intros)
done

inductive_cases sim_action_cases [elim!]:
  "InitialThreadAction ≈ obs"
  "ThreadFinishAction ≈ obs"
  "NormalAction (NewHeapElem a hT) ≈ obs"
  "NormalAction (ReadMem ad al v) ≈ obs"
  "NormalAction (WriteMem ad al v) ≈ obs"
  "NormalAction (ThreadStart t) ≈ obs"
  "NormalAction (ThreadJoin t) ≈ obs"
  "NormalAction (SyncLock a) ≈ obs"
  "NormalAction (SyncUnlock a) ≈ obs"
  "NormalAction (ObsInterrupt t) ≈ obs"
  "NormalAction (ObsInterrupted t) ≈ obs"
  "NormalAction (ExternalCall a M vs v) ≈ obs"

  "obs ≈ InitialThreadAction"
  "obs ≈ ThreadFinishAction"
  "obs ≈ NormalAction (NewHeapElem a hT)"
  "obs ≈ NormalAction (ReadMem ad al v')"
  "obs ≈ NormalAction (WriteMem ad al v')"
  "obs ≈ NormalAction (ThreadStart t)"
  "obs ≈ NormalAction (ThreadJoin t)"
  "obs ≈ NormalAction (SyncLock a)"
  "obs ≈ NormalAction (SyncUnlock a)"
  "obs ≈ NormalAction (ObsInterrupt t)"
  "obs ≈ NormalAction (ObsInterrupted t)"
  "obs ≈ NormalAction (ExternalCall a M vs v)"

inductive_simps sim_action_simps [simp]:
  "InitialThreadAction ≈ obs"
  "ThreadFinishAction ≈ obs"
  "NormalAction (NewHeapElem a hT) ≈ obs"
  "NormalAction (ReadMem ad al v) ≈ obs"
  "NormalAction (WriteMem ad al v) ≈ obs"
  "NormalAction (ThreadStart t) ≈ obs"
  "NormalAction (ThreadJoin t) ≈ obs"
  "NormalAction (SyncLock a) ≈ obs"
  "NormalAction (SyncUnlock a) ≈ obs"
  "NormalAction (ObsInterrupt t) ≈ obs"
  "NormalAction (ObsInterrupted t) ≈ obs"
  "NormalAction (ExternalCall a M vs v) ≈ obs"

  "obs ≈ InitialThreadAction"
  "obs ≈ ThreadFinishAction"
  "obs ≈ NormalAction (NewHeapElem a hT)"
  "obs ≈ NormalAction (ReadMem ad al v')"
  "obs ≈ NormalAction (WriteMem ad al v')"
  "obs ≈ NormalAction (ThreadStart t)"
  "obs ≈ NormalAction (ThreadJoin t)"
  "obs ≈ NormalAction (SyncLock a)"
  "obs ≈ NormalAction (SyncUnlock a)"
  "obs ≈ NormalAction (ObsInterrupt t)"
  "obs ≈ NormalAction (ObsInterrupted t)"
  "obs ≈ NormalAction (ExternalCall a M vs v)"

lemma sim_action_trans [trans]:
  "⟦ obs ≈ obs'; obs' ≈ obs'' ⟧ ⟹ obs ≈ obs''"
by(erule sim_action.cases) auto

lemma sim_action_sym [sym]:
  assumes "obs ≈ obs'"
  shows "obs' ≈ obs"
using assms by cases simp_all

lemma sim_actions_sym [sym]:
  "E [≈] E' ⟹ E' [≈] E"
unfolding sim_actions_def
by(auto simp add: llist_all2_conv_all_lnth split_beta intro: sim_action_sym)

lemma sim_actions_action_obsD:
  "E [≈] E' ⟹ action_obs E a ≈ action_obs E' a"
unfolding sim_actions_def action_obs_def
by(cases "enat a < llength E")(auto dest: llist_all2_lnthD llist_all2_llengthD simp add: split_beta lnth_beyond split: enat.split)

lemma sim_actions_action_tidD:
  "E [≈] E' ⟹ action_tid E a = action_tid E' a"
unfolding sim_actions_def action_tid_def
by(cases "enat a < llength E")(auto dest: llist_all2_lnthD llist_all2_llengthD simp add: lnth_beyond split: enat.split)

lemma action_loc_aux_sim_action:
  "a ≈ a' ⟹ action_loc_aux P a = action_loc_aux P a'"
by(auto elim!: action_loc_aux_cases intro: action_loc_aux_intros)

lemma eq_into_sim_actions: 
  assumes "E = E'"
  shows "E [≈] E'"
unfolding sim_actions_def assms
by(rule llist_all2_reflI)(auto)

subsection ‹Well-formedness conditions for execution sets›

locale executions_base =
  fixes ℰ :: "('addr, 'thread_id) execution set"
  and P :: "'m prog"

locale drf =
  executions_base ℰ P
  for ℰ :: "('addr, 'thread_id) execution set"
  and P :: "'m prog" +
  assumes ℰ_new_actions_for_fun:
  "⟦ E ∈ ℰ; a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'"
  and ℰ_sequential_completion:
  "⟦ E ∈ ℰ; P ⊢ (E, ws) √; ⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a ⟧
  ⟹ ∃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')"

locale executions_aux =
  executions_base ℰ P
  for ℰ :: "('addr, 'thread_id) execution set"
  and P :: "'m prog" +
  assumes init_before_read:
  "⟦  E ∈ ℰ; P ⊢ (E, ws) √; r ∈ read_actions E; adal ∈ action_loc P E r; 
      ⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a ⟧
  ⟹ ∃i<r. i ∈ new_actions_for P E adal"
  and ℰ_new_actions_for_fun:
  "⟦ E ∈ ℰ; a ∈ new_actions_for P E adal; a' ∈ new_actions_for P E adal ⟧ ⟹ a = a'"

locale sc_legal =
  executions_aux ℰ P
  for ℰ :: "('addr, 'thread_id) execution set"
  and P :: "'m prog" +
  assumes ℰ_hb_completion:
  "⟦ E ∈ ℰ; P ⊢ (E, ws) √; ⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a ⟧
  ⟹ ∃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')"

locale jmm_consistent =
  drf?: drf ℰ P +
  sc_legal ℰ P
  for ℰ :: "('addr, 'thread_id) execution set"
  and P :: "'m prog"

subsection ‹Legal executions›

record ('addr, 'thread_id) pre_justifying_execution =
  committed :: "JMM_action set"
  justifying_exec :: "('addr, 'thread_id) execution"
  justifying_ws :: "write_seen"

record ('addr, 'thread_id) justifying_execution = 
  "('addr, 'thread_id) pre_justifying_execution" +
  action_translation :: "JMM_action ⇒ JMM_action"

type_synonym ('addr, 'thread_id) justification = "nat ⇒ ('addr, 'thread_id) justifying_execution"

definition wf_action_translation_on :: 
  "('addr, 'thread_id) execution ⇒ ('addr, 'thread_id) execution ⇒ JMM_action set ⇒ (JMM_action ⇒ JMM_action) ⇒ bool"
where
  "wf_action_translation_on E E' A f ⟷
   inj_on f (actions E) ∧ 
   (∀a ∈ A. action_tid E a = action_tid E' (f a) ∧ action_obs E a ≈ action_obs E' (f a))"

abbreviation wf_action_translation :: "('addr, 'thread_id) execution ⇒ ('addr, 'thread_id) justifying_execution ⇒ bool"
where
  "wf_action_translation E J ≡ 
   wf_action_translation_on (justifying_exec J) E (committed J) (action_translation J)"

context
  fixes P :: "'m prog"
  and E :: "('addr, 'thread_id) execution"
  and ws :: "write_seen"
  and J :: "('addr, 'thread_id) justification"
begin

text ‹
  This context defines the causality constraints for the JMM.
  The weak versions are for the fixed JMM as presented by Sevcik and Aspinall at ECOOP 2008.
›

text ‹Committed actions are an ascending chain with all actions of E as a limit›
definition is_commit_sequence :: bool where 
  "is_commit_sequence ⟷ 
   committed (J 0) = {} ∧
   (∀n. action_translation (J n) ` committed (J n) ⊆ action_translation (J (Suc n)) ` committed (J (Suc n))) ∧
   actions E = (⋃n. action_translation (J n) ` committed (J n))"

definition justification_well_formed :: bool where
  "justification_well_formed ⟷ (∀n. P ⊢ (justifying_exec (J n), justifying_ws (J n)) √)"

definition committed_subset_actions :: bool where ― ‹JMM constraint 1›
  "committed_subset_actions ⟷ (∀n. committed (J n) ⊆ actions (justifying_exec (J n)))"

definition happens_before_committed :: bool where ― ‹JMM constraint 2›
  "happens_before_committed ⟷ 
  (∀n. happens_before P (justifying_exec (J n)) |` committed (J n) =
       inv_imageP (happens_before P E) (action_translation (J n)) |` committed (J n))"

definition happens_before_committed_weak :: bool where ― ‹relaxed JMM constraint›
  "happens_before_committed_weak ⟷
  (∀n. ∀r ∈ read_actions (justifying_exec (J n)) ∩ committed (J n).
       let r' = action_translation (J n) r;
           w' = ws r';
           w = inv_into (actions (justifying_exec (J n))) (action_translation (J n)) w' in
         (P,E ⊢ w' ≤hb r' ⟷ P,justifying_exec (J n) ⊢ w ≤hb r) ∧
         ¬ P,justifying_exec (J n) ⊢ r ≤hb w)"

definition sync_order_committed :: bool where ― ‹JMM constraint 3›
  "sync_order_committed ⟷
  (∀n. sync_order P (justifying_exec (J n)) |` committed (J n) =
       inv_imageP (sync_order P E) (action_translation (J n)) |` committed (J n))"

definition value_written_committed :: bool where ― ‹JMM constraint 4›
  "value_written_committed ⟷
  (∀n. ∀w ∈ write_actions (justifying_exec (J n)) ∩ committed (J n). 
       let w' = action_translation (J n) w
       in (∀adal ∈ action_loc P E w'. value_written P (justifying_exec (J n)) w adal = value_written P E w' adal))"

definition write_seen_committed :: bool where ― ‹JMM constraint 5›
  "write_seen_committed ⟷
  (∀n. ∀r' ∈ read_actions (justifying_exec (J n)) ∩ committed (J n).
       let r = action_translation (J n) r';
           r'' = inv_into (actions (justifying_exec (J (Suc n)))) (action_translation (J (Suc n))) r
       in action_translation (J (Suc n)) (justifying_ws (J (Suc n)) r'') = ws r)"

text ‹uncommited reads see writes that happen before them -- JMM constraint 6›
(* this constraint does not apply to the 0th justifying execution, so reads may see arbitrary writes,
   but this cannot be exploited because reads cannot be committed in the 1st justifying execution
   since no writes are committed in the 0th execution *)
definition uncommitted_reads_see_hb :: bool where
  "uncommitted_reads_see_hb ⟷
  (∀n. ∀r' ∈ read_actions (justifying_exec (J (Suc n))).
       action_translation (J (Suc n)) r' ∈ action_translation (J n) ` committed (J n) ∨ 
       P,justifying_exec (J (Suc n)) ⊢ justifying_ws (J (Suc n)) r' ≤hb r')"

text ‹
  newly committed reads see already committed writes and write-seen
  relationship must not change any more  -- JMM constraint 7
›
definition committed_reads_see_committed_writes :: bool where
  "committed_reads_see_committed_writes ⟷
  (∀n. ∀r' ∈ read_actions (justifying_exec (J (Suc n))) ∩ committed (J (Suc n)).
       let r = action_translation (J (Suc n)) r';
           committed_n = action_translation (J n) ` committed (J n)
       in r ∈ committed_n ∨
          (action_translation (J (Suc n)) (justifying_ws (J (Suc n)) r') ∈ committed_n ∧ ws r ∈ committed_n))"
definition committed_reads_see_committed_writes_weak :: bool where
  "committed_reads_see_committed_writes_weak ⟷
  (∀n. ∀r' ∈ read_actions (justifying_exec (J (Suc n))) ∩ committed (J (Suc n)).
       let r = action_translation (J (Suc n)) r';
           committed_n = action_translation (J n) ` committed (J n)
       in r ∈ committed_n ∨ ws r ∈ committed_n)"

text ‹external actions must be committed as soon as hb-subsequent actions are committed  -- JMM constraint 9›
definition external_actions_committed :: bool where
  "external_actions_committed ⟷
  (∀n. ∀a ∈ external_actions (justifying_exec (J n)). ∀a' ∈ committed (J n).
       P,justifying_exec (J n) ⊢ a ≤hb a' ⟶ a ∈ committed (J n))"

text ‹well-formedness conditions for action translations›
definition wf_action_translations :: bool where
  "wf_action_translations ⟷
  (∀n. wf_action_translation_on (justifying_exec (J n)) E (committed (J n)) (action_translation (J n)))"

end

text ‹
  Rule 8 of the justification for the JMM is incorrect because there might be no
  transitive reduction of the happens-before relation for an infinite execution, if
  infinitely many initialisation actions have to be ordered before the start
  action of every thread.
  Hence, ‹is_justified_by› omits this constraint.
›

primrec is_justified_by ::
  "'m prog ⇒ ('addr, 'thread_id) execution × write_seen ⇒ ('addr, 'thread_id) justification ⇒ bool" 
  (‹_ ⊢ _ justified'_by _› [51, 50, 50] 50)
where
  "P ⊢ (E, ws) justified_by J ⟷
   is_commit_sequence E J ∧
   justification_well_formed P J ∧
   committed_subset_actions J ∧
   happens_before_committed P E J ∧
   sync_order_committed P E J ∧
   value_written_committed P E J ∧
   write_seen_committed ws J ∧ 
   uncommitted_reads_see_hb P J ∧
   committed_reads_see_committed_writes ws J ∧ 
   external_actions_committed P J ∧ 
   wf_action_translations E J"

text ‹
  Sevcik requires in the fixed JMM that external actions may
  only be committed when everything that happens before has 
  already been committed. On the level of legality, this constraint
  is vacuous because it is always possible to delay committing
  external actions, so we omit it here.
›
primrec is_weakly_justified_by ::
  "'m prog ⇒ ('addr, 'thread_id) execution × write_seen ⇒ ('addr, 'thread_id) justification ⇒ bool" 
  (‹_ ⊢ _ weakly'_justified'_by _› [51, 50, 50] 50)
where
  "P ⊢ (E, ws) weakly_justified_by J ⟷
   is_commit_sequence E J ∧
   justification_well_formed P J ∧
   committed_subset_actions J ∧
   happens_before_committed_weak P E ws J ∧
   ― ‹no ‹sync_order› constraint›
   value_written_committed P E J ∧
   write_seen_committed ws J ∧ 
   uncommitted_reads_see_hb P J ∧
   committed_reads_see_committed_writes_weak ws J ∧ 
   wf_action_translations E J"

text ‹
  Notion of conflict is strengthened to explicitly exclude volatile locations.
  Otherwise, the following program is not correctly synchronised:

\begin{verbatim}
  volatile x = 0;
  ---------------
  r = x; | x = 1;
\end{verbatim}

  because in the SC execution [Init x 0, (t1, Read x 0), (t2, Write x 1)],
  the read and write are unrelated in hb, because synchronises-with is 
  asymmetric for volatiles.

  The JLS considers conflicting volatiles for data races, but this is only a 
  remark on the DRF guarantee. See JMM mailing list posts \#2477 to 2488.
›
(* Problem already exists in Sevcik's formalisation *)

definition non_volatile_conflict ::
  "'m prog ⇒ ('addr, 'thread_id) execution ⇒ JMM_action ⇒ JMM_action ⇒ bool" 
  (‹_,_ ⊢/(_)†(_)› [51,50,50,50] 51)
where 
  "P,E ⊢ a † a' ⟷
   (a ∈ read_actions E ∧ a' ∈ write_actions E ∨
    a ∈ write_actions E ∧ a' ∈ read_actions E ∨
    a ∈ write_actions E ∧ a' ∈ write_actions E) ∧
   (∃ad al. (ad, al) ∈ action_loc P E a ∩ action_loc P E a' ∧ ¬ is_volatile P al)"

definition correctly_synchronized :: "'m prog ⇒ ('addr, 'thread_id) execution set ⇒ bool"
where
  "correctly_synchronized P ℰ ⟷
  (∀E ∈ ℰ. ∀ws. P ⊢ (E, ws) √ ⟶ sequentially_consistent P (E, ws) 
    ⟶ (∀a ∈ actions E. ∀a' ∈ actions E. P,E ⊢ a † a' 
          ⟶ P,E ⊢ a ≤hb a' ∨ P,E ⊢ a' ≤hb a))"

primrec gen_legal_execution ::
  "('m prog ⇒ ('addr, 'thread_id) execution × write_seen ⇒ ('addr, 'thread_id) justification ⇒ bool)
  ⇒ 'm prog ⇒ ('addr, 'thread_id) execution set ⇒ ('addr, 'thread_id) execution × write_seen ⇒ bool"
where
  "gen_legal_execution is_justification P ℰ (E, ws) ⟷
   E ∈ ℰ ∧ P ⊢ (E, ws) √ ∧ 
   (∃J. is_justification P (E, ws) J ∧ range (justifying_exec ∘ J) ⊆ ℰ)"

abbreviation legal_execution :: 
  "'m prog ⇒ ('addr, 'thread_id) execution set ⇒ ('addr, 'thread_id) execution × write_seen ⇒ bool"
where
  "legal_execution ≡ gen_legal_execution is_justified_by"

abbreviation weakly_legal_execution :: 
  "'m prog ⇒ ('addr, 'thread_id) execution set ⇒ ('addr, 'thread_id) execution × write_seen ⇒ bool"
where
  "weakly_legal_execution ≡ gen_legal_execution is_weakly_justified_by"

declare gen_legal_execution.simps [simp del]

lemma sym_non_volatile_conflict:
  "symP (non_volatile_conflict P E)"
unfolding non_volatile_conflict_def
by(rule symPI) blast

lemma legal_executionI:
  "⟦ E ∈ ℰ; P ⊢ (E, ws) √; is_justification P (E, ws) J; range (justifying_exec ∘ J) ⊆ ℰ ⟧
  ⟹ gen_legal_execution is_justification P ℰ (E, ws)"
unfolding gen_legal_execution.simps by blast

lemma legal_executionE:
  assumes "gen_legal_execution is_justification P ℰ (E, ws)"
  obtains J where "E ∈ ℰ" "P ⊢ (E, ws) √" "is_justification P (E, ws) J" "range (justifying_exec ∘ J) ⊆ ℰ"
using assms unfolding gen_legal_execution.simps by blast

lemma legal_ℰD: "gen_legal_execution is_justification P ℰ (E, ws) ⟹ E ∈ ℰ"
by(erule legal_executionE)

lemma legal_wf_execD:
  "gen_legal_execution is_justification P ℰ Ews ⟹ P ⊢ Ews √"
by(cases Ews)(auto elim: legal_executionE)

lemma correctly_synchronizedD:
  "⟦ correctly_synchronized P ℰ; E ∈ ℰ; P ⊢ (E, ws) √; sequentially_consistent P (E, ws) ⟧
  ⟹ ∀a a'. a ∈ actions E ⟶ a' ∈ actions E ⟶ P,E ⊢ a † a' ⟶ P,E ⊢ a ≤hb a' ∨ P,E ⊢ a' ≤hb a"
unfolding correctly_synchronized_def by blast

lemma wf_action_translation_on_actionD:
  "⟦ wf_action_translation_on E E' A f; a ∈ A ⟧ 
  ⟹ action_tid E a = action_tid E' (f a) ∧ action_obs E a ≈ action_obs E' (f a)"
unfolding wf_action_translation_on_def by blast

lemma wf_action_translation_on_inj_onD:
  "wf_action_translation_on E E' A f ⟹ inj_on f (actions E)"
unfolding wf_action_translation_on_def by simp

lemma wf_action_translation_on_action_locD:
  "⟦ wf_action_translation_on E E' A f; a ∈ A ⟧
  ⟹ action_loc P E a = action_loc P E' (f a)"
apply(drule (1) wf_action_translation_on_actionD)
apply(cases "(P, action_obs E a)" rule: action_loc_aux.cases)
apply auto
done

lemma weakly_justified_write_seen_hb_read_committed:
  assumes J: "P ⊢ (E, ws) weakly_justified_by J"
  and r: "r ∈ read_actions (justifying_exec (J n))" "r ∈ committed (J n)"
  shows "ws (action_translation (J n) r) ∈ action_translation (J n) ` committed (J n)"
using r
proof(induct n arbitrary: r)
  case 0
  from J have [simp]: "committed (J 0) = {}"
    by(simp add: is_commit_sequence_def)
  with 0 show ?case by simp
next
  case (Suc n)
  let ?E = "λn. justifying_exec (J n)"
    and ?ws = "λn. justifying_ws (J n)"
    and ?C = "λn. committed (J n)"
    and ?φ = "λn. action_translation (J n)"
    
  note r = ‹r ∈ read_actions (?E (Suc n))›
  hence "r ∈ actions (?E (Suc n))" by simp
  
  from J have wfan: "wf_action_translation_on (?E n) E (?C n) (?φ n)"
    and wfaSn: "wf_action_translation_on (?E (Suc n)) E (?C (Suc n)) (?φ (Suc n))"
    by(simp_all add: wf_action_translations_def)
  
  from wfaSn have injSn: "inj_on (?φ (Suc n)) (actions (?E (Suc n)))"
    by(rule wf_action_translation_on_inj_onD)
  from J have C_sub_A: "?C (Suc n) ⊆ actions (?E (Suc n))"
    by(simp add: committed_subset_actions_def)
  from J have CnCSn: "?φ n ` ?C n ⊆ ?φ (Suc n) ` ?C (Suc n)"
    by(simp add: is_commit_sequence_def)
    
  from J have wsSn: "is_write_seen P (?E (Suc n)) (?ws (Suc n))"
    by(simp add: justification_well_formed_def)
  from r obtain ad al v where "action_obs (?E (Suc n)) r = NormalAction (ReadMem ad al v)" by cases
  from is_write_seenD[OF wsSn r this]
  have wsSn: "?ws (Suc n) r ∈ actions (?E (Suc n))" by simp

  show ?case
  proof(cases "?φ (Suc n) r ∈ ?φ n ` ?C n")
    case True
    then obtain r' where r': "r' ∈ ?C n"
      and r_r': "?φ (Suc n) r = ?φ n r'" by(auto)
    from r' wfan have "action_tid (?E n) r' = action_tid E (?φ n r')"
      and "action_obs (?E n) r' ≈ action_obs E (?φ n r')"
      by(blast dest: wf_action_translation_on_actionD)+
    moreover from r' CnCSn have "?φ (Suc n) r ∈ ?φ (Suc n) ` ?C (Suc n)" 
      unfolding r_r' by auto
    hence "r ∈ ?C (Suc n)"
      unfolding inj_on_image_mem_iff[OF injSn ‹r ∈ actions (?E (Suc n))› C_sub_A] .
    with wfaSn have "action_tid (?E (Suc n)) r = action_tid E (?φ (Suc n) r)"
      and "action_obs (?E (Suc n)) r ≈ action_obs E (?φ (Suc n) r)"
      by(blast dest: wf_action_translation_on_actionD)+
    ultimately have tid: "action_tid (?E n) r' = action_tid (?E (Suc n)) r"
      and obs: "action_obs (?E n) r' ≈ action_obs (?E (Suc n)) r"
      unfolding r_r' by(auto intro: sim_action_trans sim_action_sym)
    
    from J have "?C n ⊆ actions (?E n)" by(simp add: committed_subset_actions_def)
    with r' have "r' ∈ actions (?E n)" by blast
    with r obs have "r' ∈ read_actions (?E n)"
      by cases(auto intro: read_actions.intros)
    hence ws: "ws (?φ n r') ∈ ?φ n ` ?C n" using r' by(rule Suc)

    have r_conv_inv: "r = inv_into (actions (?E (Suc n))) (?φ (Suc n)) (?φ n r')"
      using ‹r ∈ actions (?E (Suc n))› unfolding r_r'[symmetric]
      by(simp add: inv_into_f_f[OF injSn])
    with ‹r' ∈ ?C n› r J ‹r' ∈ read_actions (?E n)›
    have ws_eq: "?φ (Suc n) (?ws (Suc n) r) = ws (?φ n r')"
      by(simp add: Let_def write_seen_committed_def)
    with ws CnCSn have "?φ (Suc n) (?ws (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)" by auto
    hence "?ws (Suc n) r ∈ ?C (Suc n)"
      by(subst (asm) inj_on_image_mem_iff[OF injSn wsSn C_sub_A])
    moreover from ws CnCSn have "ws (?φ (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
      unfolding r_r' by auto
    ultimately show ?thesis by simp
  next
    case False
    with r ‹r ∈ ?C (Suc n)› J
    have "ws (?φ (Suc n) r) ∈ ?φ n ` ?C n"
      unfolding is_weakly_justified_by.simps Let_def committed_reads_see_committed_writes_weak_def
      by blast
    hence "ws (?φ (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
      using CnCSn by blast+
    thus ?thesis by(simp add: inj_on_image_mem_iff[OF injSn wsSn C_sub_A])
  qed
qed

lemma justified_write_seen_hb_read_committed:
  assumes J: "P ⊢ (E, ws) justified_by J"
  and r: "r ∈ read_actions (justifying_exec (J n))" "r ∈ committed (J n)"
  shows "justifying_ws (J n) r ∈ committed (J n)" (is ?thesis1)
  and "ws (action_translation (J n) r) ∈ action_translation (J n) ` committed (J n)" (is ?thesis2)
proof -
  have "?thesis1 ∧ ?thesis2" using r
  proof(induct n arbitrary: r)
    case 0
    from J have [simp]: "committed (J 0) = {}"
      by(simp add: is_commit_sequence_def)
    with 0 show ?case by simp
  next
    case (Suc n)
    let ?E = "λn. justifying_exec (J n)"
      and ?ws = "λn. justifying_ws (J n)"
      and ?C = "λn. committed (J n)"
      and ?φ = "λn. action_translation (J n)"
    
    note r = ‹r ∈ read_actions (?E (Suc n))›
    hence "r ∈ actions (?E (Suc n))" by simp
    
    from J have wfan: "wf_action_translation_on (?E n) E (?C n) (?φ n)"
      and wfaSn: "wf_action_translation_on (?E (Suc n)) E (?C (Suc n)) (?φ (Suc n))"
      by(simp_all add: wf_action_translations_def)
    
    from wfaSn have injSn: "inj_on (?φ (Suc n)) (actions (?E (Suc n)))"
      by(rule wf_action_translation_on_inj_onD)
    from J have C_sub_A: "?C (Suc n) ⊆ actions (?E (Suc n))"
      by(simp add: committed_subset_actions_def)
    from J have CnCSn: "?φ n ` ?C n ⊆ ?φ (Suc n) ` ?C (Suc n)"
      by(simp add: is_commit_sequence_def)
    
    from J have wsSn: "is_write_seen P (?E (Suc n)) (?ws (Suc n))"
      by(simp add: justification_well_formed_def)
    from r obtain ad al v where "action_obs (?E (Suc n)) r = NormalAction (ReadMem ad al v)" by cases
    from is_write_seenD[OF wsSn r this]
    have wsSn: "?ws (Suc n) r ∈ actions (?E (Suc n))" by simp

    show ?case
    proof(cases "?φ (Suc n) r ∈ ?φ n ` ?C n")
      case True
      then obtain r' where r': "r' ∈ ?C n"
        and r_r': "?φ (Suc n) r = ?φ n r'" by(auto)
      from r' wfan have "action_tid (?E n) r' = action_tid E (?φ n r')"
        and "action_obs (?E n) r' ≈ action_obs E (?φ n r')"
        by(blast dest: wf_action_translation_on_actionD)+
      moreover from r' CnCSn have "?φ (Suc n) r ∈ ?φ (Suc n) ` ?C (Suc n)" 
        unfolding r_r' by auto
      hence "r ∈ ?C (Suc n)"
        unfolding inj_on_image_mem_iff[OF injSn ‹r ∈ actions (?E (Suc n))› C_sub_A] .
      with wfaSn have "action_tid (?E (Suc n)) r = action_tid E (?φ (Suc n) r)"
        and "action_obs (?E (Suc n)) r ≈ action_obs E (?φ (Suc n) r)"
        by(blast dest: wf_action_translation_on_actionD)+
      ultimately have tid: "action_tid (?E n) r' = action_tid (?E (Suc n)) r"
        and obs: "action_obs (?E n) r' ≈ action_obs (?E (Suc n)) r"
        unfolding r_r' by(auto intro: sim_action_trans sim_action_sym)
      
      from J have "?C n ⊆ actions (?E n)" by(simp add: committed_subset_actions_def)
      with r' have "r' ∈ actions (?E n)" by blast
      with r obs have "r' ∈ read_actions (?E n)"
        by cases(auto intro: read_actions.intros)
      hence "?ws n r' ∈ ?C n ∧ ws (?φ n r') ∈ ?φ n ` ?C n" using r' by(rule Suc)
      then obtain ws: "ws (?φ n r') ∈ ?φ n ` ?C n" ..

      have r_conv_inv: "r = inv_into (actions (?E (Suc n))) (?φ (Suc n)) (?φ n r')"
        using ‹r ∈ actions (?E (Suc n))› unfolding r_r'[symmetric]
        by(simp add: inv_into_f_f[OF injSn])
      with ‹r' ∈ ?C n› r J ‹r' ∈ read_actions (?E n)›
      have ws_eq: "?φ (Suc n) (?ws (Suc n) r) = ws (?φ n r')"
        by(simp add: Let_def write_seen_committed_def)
      with ws CnCSn have "?φ (Suc n) (?ws (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)" by auto
      hence "?ws (Suc n) r ∈ ?C (Suc n)"
        by(subst (asm) inj_on_image_mem_iff[OF injSn wsSn C_sub_A])
      moreover from ws CnCSn have "ws (?φ (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
        unfolding r_r' by auto
      ultimately show ?thesis by simp
    next
      case False
      with r ‹r ∈ ?C (Suc n)› J
      have "?φ (Suc n) (?ws (Suc n) r) ∈ ?φ n ` ?C n" 
        and "ws (?φ (Suc n) r) ∈ ?φ n ` ?C n"
        unfolding is_justified_by.simps Let_def committed_reads_see_committed_writes_def
        by blast+
      hence "?φ (Suc n) (?ws (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
        and "ws (?φ (Suc n) r) ∈ ?φ (Suc n) ` ?C (Suc n)"
        using CnCSn by blast+
      thus ?thesis by(simp add: inj_on_image_mem_iff[OF injSn wsSn C_sub_A])
    qed
  qed
  thus ?thesis1 ?thesis2 by simp_all
qed

lemma is_justified_by_imp_is_weakly_justified_by:
  assumes justified: "P ⊢ (E, ws) justified_by J"
  and wf: "P ⊢ (E, ws) √"
  shows "P ⊢ (E, ws) weakly_justified_by J"
  unfolding is_weakly_justified_by.simps
proof(intro conjI)
  let ?E = "λn. justifying_exec (J n)"
    and ?ws = "λn. justifying_ws (J n)"
    and ?C = "λn. committed (J n)"
    and ?φ = "λn. action_translation (J n)"

  from justified
  show "is_commit_sequence E J" "justification_well_formed P J" "committed_subset_actions J"
    "value_written_committed P E J" "write_seen_committed ws J" "uncommitted_reads_see_hb P J"
    "wf_action_translations E J" by(simp_all)
  
  show "happens_before_committed_weak P E ws J"
    unfolding happens_before_committed_weak_def Let_def
  proof(intro strip conjI)
    fix n r
    assume "r ∈ read_actions (?E n) ∩ ?C n"
    hence read: "r ∈ read_actions (?E n)" and committed: "r ∈ ?C n" by simp_all
    with justified have committed_ws: "?ws n r ∈ ?C n"
      and committed_ws': "ws (?φ n r) ∈ ?φ n ` ?C n"
      by(rule justified_write_seen_hb_read_committed)+
    from committed_ws' obtain w where w: "ws (?φ n r) = ?φ n w"
      and committed_w: "w ∈ ?C n" by blast

    from committed_w justified have "w ∈ actions (?E n)" by(auto simp add: committed_subset_actions_def)
    moreover from justified have "inj_on (?φ n) (actions (?E n))"
      by(auto simp add: wf_action_translations_def dest: wf_action_translation_on_inj_onD)
    ultimately have w_def: "w = inv_into (actions (?E n)) (?φ n) (ws (?φ n r))"
      by(simp_all add: w)

    from committed committed_w
    have "P,?E n ⊢ w ≤hb r ⟷ (happens_before P (?E n) |` ?C n) w r" by auto
    also have "… ⟷ (inv_imageP (happens_before P E) (?φ n) |` ?C n) w r"
      using justified by(simp add: happens_before_committed_def)
    also have "… ⟷ P,E ⊢ ?φ n w ≤hb ?φ n r" using committed committed_w by auto
    finally show "P,E ⊢ ws (?φ n r) ≤hb ?φ n r ⟷ P,?E n ⊢ inv_into (actions (?E n)) (?φ n) (ws (?φ n r)) ≤hb r"
      unfolding w[symmetric] unfolding w_def ..

    have "P,?E n⊢ r ≤hb w ⟷ (happens_before P (?E n) |` ?C n) r w" 
      using committed committed_w by auto
    also have "… ⟷ (inv_imageP (happens_before P E) (?φ n) |` ?C n) r w"
      using justified by(simp add: happens_before_committed_def)
    also have "… ⟷ P,E ⊢ ?φ n r ≤hb ws (?φ n r)" using w committed committed_w by auto
    also {
      from read obtain ad al v where "action_obs (?E n) r = NormalAction (ReadMem ad al v)" by cases auto
      with justified committed obtain v' where obs': "action_obs E (?φ n r) = NormalAction (ReadMem ad al v')"
        by(fastforce simp add: wf_action_translations_def dest!: wf_action_translation_on_actionD)
      moreover from committed justified have "?φ n r ∈ actions E"
        by(auto simp add: is_commit_sequence_def)
      ultimately have read': "?φ n r ∈ read_actions E" by(auto intro: read_actions.intros)
      from wf have "is_write_seen P E ws" by(rule wf_exec_is_write_seenD)
      from is_write_seenD[OF this read' obs']
      have "¬ P,E ⊢ ?φ n r ≤hb ws (?φ n r)" by simp }
    ultimately show "¬ P,?E n ⊢ r ≤hb inv_into (actions (?E n)) (?φ n) (ws (?φ n r))"
      unfolding w_def by simp
  qed

  from justified have "committed_reads_see_committed_writes ws J" by simp
  thus "committed_reads_see_committed_writes_weak ws J"
    by(auto simp add: committed_reads_see_committed_writes_def committed_reads_see_committed_writes_weak_def)
qed

corollary legal_imp_weakly_legal_execution:
  "legal_execution P ℰ Ews ⟹ weakly_legal_execution P ℰ Ews"
by(cases Ews)(auto 4 4 simp add: gen_legal_execution.simps simp del: is_justified_by.simps is_weakly_justified_by.simps intro: is_justified_by_imp_is_weakly_justified_by)

lemma drop_0th_justifying_exec:
  assumes "P ⊢ (E, ws) justified_by J"
  and wf: "P ⊢ (E', ws') √"
  shows "P ⊢ (E, ws) justified_by (J(0 := ⦇committed = {}, justifying_exec = E', justifying_ws = ws', action_translation = id⦈))"
  (is "_ ⊢ _ justified_by ?J")
using assms
unfolding is_justified_by.simps is_commit_sequence_def
  justification_well_formed_def committed_subset_actions_def happens_before_committed_def
  sync_order_committed_def value_written_committed_def write_seen_committed_def uncommitted_reads_see_hb_def
  committed_reads_see_committed_writes_def external_actions_committed_def wf_action_translations_def
proof(intro conjI strip)
  let ?E = "λn. justifying_exec (?J n)"
    and ?φ = "λn. action_translation (?J n)"
    and ?C = "λn. committed (?J n)"
    and ?ws = "λn. justifying_ws (?J n)"

  show "?C 0 = {}" by simp

  from assms have C_0: "committed (J 0) = {}" by(simp add: is_commit_sequence_def)
  hence "(⋃n. ?φ n ` ?C n) = (⋃n. action_translation (J n) ` committed (J n))"
    by -(rule SUP_cong, simp_all)
  also have "… = actions E" using assms by(simp add: is_commit_sequence_def)
  finally show "actions E = (⋃n. ?φ n ` ?C n)" .. 

  fix n
  { fix r'
    assume "r' ∈ read_actions (?E (Suc n))"
    thus "?φ (Suc n) r' ∈ ?φ n ` ?C n ∨ P,?E (Suc n) ⊢ ?ws (Suc n) r' ≤hb r'"
      using assms by(auto dest!: bspec simp add: uncommitted_reads_see_hb_def is_commit_sequence_def) }
  { fix r'
    assume r': "r' ∈ read_actions (?E (Suc n)) ∩ ?C (Suc n)"

    have "n ≠ 0"
    proof
      assume "n = 0"
      hence "r' ∈ read_actions (justifying_exec (J 1)) ∩ committed (J 1)" using r' by simp
      hence "action_translation (J 1) r' ∈ action_translation (J 0) ` committed (J 0) ∨ 
             ws (action_translation (J 1) r') ∈ action_translation (J 0) ` committed (J 0)" using assms
        unfolding One_nat_def is_justified_by.simps Let_def committed_reads_see_committed_writes_def
        by(metis (lifting))
      thus False unfolding C_0 by simp
    qed
    thus "let r = ?φ (Suc n) r'; committed_n = ?φ n ` ?C n
       in r ∈ committed_n ∨
          (?φ (Suc n) (?ws (Suc n) r') ∈ committed_n ∧ ws r ∈ committed_n)"
      using assms r' by(simp add: committed_reads_see_committed_writes_def) }
  { fix a a'
    assume "a ∈ external_actions (?E n)" 
      and "a' ∈ ?C n" "P,?E n ⊢ a ≤hb a'"
    moreover hence "n > 0" by(simp split: if_split_asm)
    ultimately show "a ∈ ?C n" using assms
      by(simp add: external_actions_committed_def) blast }
    
  from assms have "wf_action_translation E (?J 0)"
    by(simp add: wf_action_translations_def wf_action_translation_on_def)
  thus "wf_action_translation E (?J n)" using assms by(simp add: wf_action_translations_def)
qed auto

lemma drop_0th_weakly_justifying_exec:
  assumes "P ⊢ (E, ws) weakly_justified_by J"
  and wf: "P ⊢ (E', ws') √"
  shows "P ⊢ (E, ws) weakly_justified_by (J(0 := ⦇committed = {}, justifying_exec = E', justifying_ws = ws', action_translation = id⦈))"
  (is "_ ⊢ _ weakly_justified_by ?J")
using assms
unfolding is_weakly_justified_by.simps is_commit_sequence_def
  justification_well_formed_def committed_subset_actions_def happens_before_committed_weak_def
  value_written_committed_def write_seen_committed_def uncommitted_reads_see_hb_def
  committed_reads_see_committed_writes_weak_def external_actions_committed_def wf_action_translations_def
proof(intro conjI strip)
  let ?E = "λn. justifying_exec (?J n)"
    and ?φ = "λn. action_translation (?J n)"
    and ?C = "λn. committed (?J n)"
    and ?ws = "λn. justifying_ws (?J n)"

  show "?C 0 = {}" by simp

  from assms have C_0: "committed (J 0) = {}" by(simp add: is_commit_sequence_def)
  hence "(⋃n. ?φ n ` ?C n) = (⋃n. action_translation (J n) ` committed (J n))"
    by -(rule SUP_cong, simp_all)
  also have "… = actions E" using assms by(simp add: is_commit_sequence_def)
  finally show "actions E = (⋃n. ?φ n ` ?C n)" .. 

  fix n
  { fix r'
    assume "r' ∈ read_actions (?E (Suc n))"
    thus "?φ (Suc n) r' ∈ ?φ n ` ?C n ∨ P,?E (Suc n) ⊢ ?ws (Suc n) r' ≤hb r'"
      using assms by(auto dest!: bspec simp add: uncommitted_reads_see_hb_def is_commit_sequence_def) }
  { fix r'
    assume r': "r' ∈ read_actions (?E (Suc n)) ∩ ?C (Suc n)"

    have "n ≠ 0"
    proof
      assume "n = 0"
      hence "r' ∈ read_actions (justifying_exec (J 1)) ∩ committed (J 1)" using r' by simp
      hence "action_translation (J 1) r' ∈ action_translation (J 0) ` committed (J 0) ∨ 
             ws (action_translation (J 1) r') ∈ action_translation (J 0) ` committed (J 0)" using assms
        unfolding One_nat_def is_weakly_justified_by.simps Let_def committed_reads_see_committed_writes_weak_def
        by(metis (lifting))
      thus False unfolding C_0 by simp
    qed
    thus "let r = ?φ (Suc n) r'; committed_n = ?φ n ` ?C n
       in r ∈ committed_n ∨ ws r ∈ committed_n"
      using assms r' by(simp add: committed_reads_see_committed_writes_weak_def) }
    
  from assms have "wf_action_translation E (?J 0)"
    by(simp add: wf_action_translations_def wf_action_translation_on_def)
  thus "wf_action_translation E (?J n)" using assms by(simp add: wf_action_translations_def)
qed auto

subsection ‹Executions with common prefix›

lemma actions_change_prefix:
  assumes read: "a ∈ actions E"
  and prefix: "ltake n E [≈] ltake n E'"
  and rn: "enat a < n"
  shows "a ∈ actions E'"
using llist_all2_llengthD[OF prefix[unfolded sim_actions_def]] read rn
by(simp add: actions_def min_def split: if_split_asm)

lemma action_obs_change_prefix:
  assumes prefix: "ltake n E [≈] ltake n E'"
  and rn: "enat a < n"
  shows "action_obs E a ≈ action_obs E' a"
proof -
  from rn have "action_obs E a = action_obs (ltake n E) a"
    by(simp add: action_obs_def lnth_ltake)
  also from prefix have "… ≈ action_obs (ltake n E') a"
    by(rule sim_actions_action_obsD)
  also have "… = action_obs E' a" using rn
    by(simp add: action_obs_def lnth_ltake)
  finally show ?thesis .
qed

lemma action_obs_change_prefix_eq:
  assumes prefix: "ltake n E = ltake n E'"
  and rn: "enat a < n"
  shows "action_obs E a = action_obs E' a"
proof -
  from rn have "action_obs E a = action_obs (ltake n E) a"
    by(simp add: action_obs_def lnth_ltake)
  also from prefix have "… = action_obs (ltake n E') a"
    by(simp add: action_obs_def)
  also have "… = action_obs E' a" using rn
    by(simp add: action_obs_def lnth_ltake)
  finally show ?thesis .
qed

lemma read_actions_change_prefix:
  assumes read: "r ∈ read_actions E"
  and prefix: "ltake n E [≈] ltake n E'" "enat r < n"
  shows "r ∈ read_actions E'"
using read action_obs_change_prefix[OF prefix] actions_change_prefix[OF _ prefix]
by(cases)(auto intro: read_actions.intros)

lemma sim_action_is_write_action_eq:
  assumes "obs ≈ obs'"
  shows "is_write_action obs ⟷ is_write_action obs'"
using assms by cases simp_all

lemma write_actions_change_prefix:
  assumes "write": "w ∈ write_actions E"
  and prefix: "ltake n E [≈] ltake n E'" "enat w < n"
  shows "w ∈ write_actions E'"
using "write" action_obs_change_prefix[OF prefix] actions_change_prefix[OF _ prefix]
by(cases)(auto intro: write_actions.intros dest: sim_action_is_write_action_eq)

lemma action_loc_change_prefix:
  assumes "ltake n E [≈] ltake n E'" "enat a < n"
  shows "action_loc P E a = action_loc P E' a"
using action_obs_change_prefix[OF assms]
by(fastforce elim!: action_loc_aux_cases intro: action_loc_aux_intros)

lemma sim_action_is_new_action_eq:
  assumes "obs ≈ obs'"
  shows "is_new_action obs = is_new_action obs'"
using assms by cases auto

lemma action_order_change_prefix:
  assumes ao: "E ⊢ a ≤a a'"
  and prefix: "ltake n E [≈] ltake n E'" 
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "E' ⊢ a ≤a a'"
using ao actions_change_prefix[OF _ prefix an] actions_change_prefix[OF _ prefix a'n] action_obs_change_prefix[OF prefix an] action_obs_change_prefix[OF prefix a'n]
by(auto simp add: action_order_def split: if_split_asm dest: sim_action_is_new_action_eq)


lemma value_written_change_prefix:
  assumes eq: "ltake n E = ltake n E'"
  and an: "enat a < n"
  shows "value_written P E a = value_written P E' a"
using action_obs_change_prefix_eq[OF eq an]
by(simp add: value_written_def fun_eq_iff)

lemma action_tid_change_prefix:
  assumes prefix: "ltake n E [≈] ltake n E'" 
  and an: "enat a < n"
  shows "action_tid E a = action_tid E' a"
proof -
  from an have "action_tid E a = action_tid (ltake n E) a"
    by(simp add: action_tid_def lnth_ltake)
  also from prefix have "… = action_tid (ltake n E') a"
    by(rule sim_actions_action_tidD)
  also from an have "… = action_tid E' a"
    by(simp add: action_tid_def lnth_ltake)
  finally show ?thesis .
qed

lemma program_order_change_prefix:
  assumes po: "E ⊢ a ≤po a'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "E' ⊢ a ≤po a'"
using po action_order_change_prefix[OF _ prefix an a'n]
  action_tid_change_prefix[OF prefix an] action_tid_change_prefix[OF prefix a'n]
by(auto elim!: program_orderE intro: program_orderI)

lemma sim_action_sactionD:
  assumes "obs ≈ obs'"
  shows "saction P obs ⟷ saction P obs'"
using assms by cases simp_all

lemma sactions_change_prefix:
  assumes sync: "a ∈ sactions P E"
  and prefix: "ltake n E [≈] ltake n E'"
  and rn: "enat a < n"
  shows "a ∈ sactions P E'"
using sync action_obs_change_prefix[OF prefix rn] actions_change_prefix[OF _ prefix rn]
unfolding sactions_def by(simp add: sim_action_sactionD)

lemma sync_order_change_prefix:
  assumes so: "P,E ⊢ a ≤so a'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "P,E' ⊢ a ≤so a'"
using so action_order_change_prefix[OF _ prefix an a'n] sactions_change_prefix[OF _ prefix an, of P] sactions_change_prefix[OF _ prefix a'n, of P]
by(simp add: sync_order_def)

lemma sim_action_synchronizes_withD:
  assumes "obs ≈ obs'" "obs'' ≈ obs'''"
  shows "P ⊢ (t, obs) ↝sw (t', obs'') ⟷ P ⊢ (t, obs') ↝sw (t', obs''')"
using assms
by(auto elim!: sim_action.cases synchronizes_with.cases intro: synchronizes_with.intros)

lemma sync_with_change_prefix:
  assumes sw: "P,E ⊢ a ≤sw a'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "P,E' ⊢ a ≤sw a'"
using sw sync_order_change_prefix[OF _ prefix an a'n, of P] 
  action_tid_change_prefix[OF prefix an] action_tid_change_prefix[OF prefix a'n]
  action_obs_change_prefix[OF prefix an] action_obs_change_prefix[OF prefix a'n]
by(auto simp add: sync_with_def dest: sim_action_synchronizes_withD)


lemma po_sw_change_prefix:
  assumes posw: "po_sw P E a a'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "po_sw P E' a a'"
using posw sync_with_change_prefix[OF _ prefix an a'n, of P] program_order_change_prefix[OF _ prefix an a'n]
by(auto simp add: po_sw_def)


lemma happens_before_new_not_new:
  assumes tsa_ok: "thread_start_actions_ok E"
  and a: "a ∈ actions E" 
  and a': "a' ∈ actions E"
  and new_a: "is_new_action (action_obs E a)"
  and new_a': "¬ is_new_action (action_obs E a')"
  shows "P,E ⊢ a ≤hb a'"
proof -
  from thread_start_actions_okD[OF tsa_ok a' new_a']
  obtain i where "i ≤ a'"
    and obs_i: "action_obs E i = InitialThreadAction" 
    and "action_tid E i = action_tid E a'" by auto
  from ‹i ≤ a'› a' have "i ∈ actions E"
    by(auto simp add: actions_def le_less_trans[where y="enat a'"])
  with ‹i ≤ a'› obs_i a' new_a' have "E ⊢ i ≤a a'" by(simp add: action_order_def)
  hence "E ⊢ i ≤po a'" using ‹action_tid E i = action_tid E a'›
    by(rule program_orderI)
  
  moreover {
    from ‹i ∈ actions E› obs_i
    have "i ∈ sactions P E" by(auto intro: sactionsI)
    from a ‹i ∈ actions E› new_a obs_i have "E ⊢ a ≤a i" by(simp add: action_order_def)
    moreover from a new_a have "a ∈ sactions P E" by(auto intro: sactionsI)
    ultimately have "P,E ⊢ a ≤so i" using ‹i ∈ sactions P E› by(rule sync_orderI)
    moreover from new_a obs_i have "P ⊢ (action_tid E a, action_obs E a) ↝sw (action_tid E i, action_obs E i)"
      by cases(auto intro: synchronizes_with.intros)
    ultimately have "P,E ⊢ a ≤sw i" by(rule sync_withI) }
  ultimately show ?thesis unfolding po_sw_def [abs_def] by(blast intro: tranclp.r_into_trancl tranclp_trans)
qed

lemma happens_before_change_prefix:
  assumes hb: "P,E ⊢ a ≤hb a'"
  and tsa_ok: "thread_start_actions_ok E'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat a < n"
  and a'n: "enat a' < n"
  shows "P,E' ⊢ a ≤hb a'"
using hb an a'n
proof induct
  case (base a')
  thus ?case by(rule tranclp.r_into_trancl[where r="po_sw P E'", OF po_sw_change_prefix[OF _ prefix]])
next
  case (step a' a'')
  show ?case
  proof(cases "is_new_action (action_obs E a') ∧ ¬ is_new_action (action_obs E a'')")
    case False
    from ‹po_sw P E a' a''› have "E ⊢ a' ≤a a''" by(rule po_sw_into_action_order)
    with ‹enat a'' < n› False have "enat a' < n"
      by(safe elim!: action_orderE)(metis Suc_leI Suc_n_not_le_n enat_ord_simps(2) le_trans nat_neq_iff xtrans(10))+
    with ‹enat a < n› have "P,E' ⊢ a ≤hb a'" by(rule step)
    moreover from ‹po_sw P E a' a''› prefix ‹enat a' < n› ‹enat a'' < n›
    have "po_sw P E' a' a''" by(rule po_sw_change_prefix)
    ultimately show ?thesis ..
  next
    case True
    then obtain new_a': "is_new_action (action_obs E a')"
      and "¬ is_new_action (action_obs E a'')" ..
    from ‹P,E ⊢ a ≤hb a'› new_a'
    have new_a: "is_new_action (action_obs E a)"
      and tid: "action_tid E a = action_tid E a'"
      and "a ≤ a'" by(rule happens_before_new_actionD)+
    
    note tsa_ok moreover
    from porder_happens_before[of E P] have "a ∈ actions E"
      by(rule porder_onE)(erule refl_onPD1, rule ‹P,E ⊢ a ≤hb a'›)
    hence "a ∈ actions E'" using an by(rule actions_change_prefix[OF _ prefix])
    moreover
    from ‹po_sw P E a' a''› refl_on_program_order[of E] refl_on_sync_order[of P E]
    have "a'' ∈ actions E"
      unfolding po_sw_def by(auto dest: refl_onPD2 elim!: sync_withE)
    hence "a'' ∈ actions E'" using ‹enat a'' < n› by(rule actions_change_prefix[OF _ prefix])
    moreover
    from new_a action_obs_change_prefix[OF prefix an] 
    have "is_new_action (action_obs E' a)" by(cases) auto
    moreover
    from ‹¬ is_new_action (action_obs E a'')› action_obs_change_prefix[OF prefix ‹enat a'' < n›]
    have "¬ is_new_action (action_obs E' a'')" by(auto elim: is_new_action.cases)
    ultimately show "P,E' ⊢ a ≤hb a''" by(rule happens_before_new_not_new)
  qed
qed

lemma thread_start_actions_ok_change:
  assumes tsa: "thread_start_actions_ok E"
  and sim: "E [≈] E'"
  shows "thread_start_actions_ok E'"
proof(rule thread_start_actions_okI)
  fix a
  assume "a ∈ actions E'" "¬ is_new_action (action_obs E' a)"
  from sim have len_eq: "llength E = llength E'" by(simp add: sim_actions_def)(rule llist_all2_llengthD)
  with sim have sim': "ltake (llength E) E [≈] ltake (llength E) E'" by(simp add: ltake_all)

  from ‹a ∈ actions E'› len_eq have "enat a < llength E" by(simp add: actions_def)
  with ‹a ∈ actions E'› sim'[symmetric] have "a ∈ actions E" by(rule actions_change_prefix)
  moreover have "¬ is_new_action (action_obs E a)"
    using action_obs_change_prefix[OF sim' ‹enat a < llength E›] ‹¬ is_new_action (action_obs E' a)›
    by(auto elim!: is_new_action.cases)
  ultimately obtain i where "i ≤ a" "action_obs E i = InitialThreadAction" "action_tid E i = action_tid E a"
    by(blast dest: thread_start_actions_okD[OF tsa])
  thus "∃i ≤ a. action_obs E' i = InitialThreadAction ∧ action_tid E' i = action_tid E' a"
    using action_tid_change_prefix[OF sim', of i] action_tid_change_prefix[OF sim', of a] ‹enat a < llength E›
      action_obs_change_prefix[OF sim', of i]
    by(cases "llength E")(auto intro!: exI[where x=i])
qed

context executions_aux begin

lemma ℰ_new_same_addr_singleton:
  assumes E: "E ∈ ℰ"
  shows "∃a. new_actions_for P E adal ⊆ {a}"
by(blast dest: ℰ_new_actions_for_fun[OF E])

lemma new_action_before_read:
  assumes E: "E ∈ ℰ"
  and wf: "P ⊢ (E, ws) √"
  and ra: "ra ∈ read_actions E"
  and adal: "adal ∈ action_loc P E ra"
  and new: "wa ∈ new_actions_for P E adal"
  and sc: "⋀a. ⟦ a < ra; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
  shows "wa < ra"
using ℰ_new_same_addr_singleton[OF E, of adal] init_before_read[OF E wf ra adal sc] new
by auto

lemma mrw_before:
  assumes E: "E ∈ ℰ"
  and wf: "P ⊢ (E, ws) √"
  and mrw: "P,E ⊢ r ↝mrw w"
  and sc: "⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
  shows "w < r"
using mrw read_actions_not_write_actions[of r E]
apply cases
apply(erule action_orderE)
 apply(erule (1) new_action_before_read[OF E wf])
  apply(simp add: new_actions_for_def)
 apply(erule (1) sc)
apply(cases "w = r")
apply auto
done

lemma mrw_change_prefix:
  assumes E': "E' ∈ ℰ"
  and mrw: "P,E ⊢ r ↝mrw w"
  and tsa_ok: "thread_start_actions_ok E'"
  and prefix: "ltake n E [≈] ltake n E'"
  and an: "enat r < n"
  and a'n: "enat w < n"
  shows "P,E' ⊢ r ↝mrw w"
using mrw
proof cases
  fix adal
  assume r: "r ∈ read_actions E"
    and adal_r: "adal ∈ action_loc P E r"
    and war: "E ⊢ w ≤a r"
    and w: "w ∈ write_actions E"
    and adal_w: "adal ∈ action_loc P E w"
    and mrw: "⋀wa'. ⟦wa' ∈ write_actions E; adal ∈ action_loc P E wa'⟧
              ⟹ E ⊢ wa' ≤a w ∨ E ⊢ r ≤a wa'"
  show ?thesis
  proof(rule most_recent_write_for.intros)
    from r prefix an show r': "r ∈ read_actions E'"
      by(rule read_actions_change_prefix)
    from adal_r show "adal ∈ action_loc P E' r"
      by(simp add: action_loc_change_prefix[OF prefix[symmetric] an])
    from war prefix a'n an show "E' ⊢ w ≤a r" by(rule action_order_change_prefix)
    from w prefix a'n show w': "w ∈ write_actions E'" by(rule write_actions_change_prefix)
    from adal_w show adal_w': "adal ∈ action_loc P E' w" by(simp add: action_loc_change_prefix[OF prefix[symmetric] a'n])

    fix wa'
    assume wa': "wa' ∈ write_actions E'" 
      and adal_wa': "adal ∈ action_loc P E' wa'"
    show "E' ⊢ wa' ≤a w ∨ E' ⊢ r ≤a wa'"
    proof(cases "enat wa' < n")
      case True
      note wa'n = this
      with wa' prefix[symmetric] have "wa' ∈ write_actions E" by(rule write_actions_change_prefix)
      moreover from adal_wa' have "adal ∈ action_loc P E wa'"
        by(simp add: action_loc_change_prefix[OF prefix wa'n])
      ultimately have "E ⊢ wa' ≤a w ∨ E ⊢ r ≤a wa'" by(rule mrw)
      thus ?thesis
      proof
        assume "E ⊢ wa' ≤a w"
        hence "E' ⊢ wa' ≤a w" using prefix wa'n a'n by(rule action_order_change_prefix)
        thus ?thesis ..
      next
        assume "E ⊢ r ≤a wa'"
        hence "E' ⊢ r ≤a wa'" using prefix an wa'n by(rule action_order_change_prefix)
        thus ?thesis ..
      qed
    next
      case False note wa'n = this
      show ?thesis
      proof(cases "is_new_action (action_obs E' wa')")
        case False
        hence "E' ⊢ r ≤a wa'" using wa'n r' wa' an
          by(auto intro!: action_orderI) (metis enat_ord_code(1) linorder_le_cases order_le_less_trans)
        thus ?thesis ..
      next
        case True
        with wa' adal_wa' have new: "wa' ∈ new_actions_for P E' adal" by(simp add: new_actions_for_def)
        show ?thesis
        proof(cases "is_new_action (action_obs E' w)")
          case True
          with adal_w' a'n w' have "w ∈ new_actions_for P E' adal" by(simp add: new_actions_for_def)
          with E' new have "wa' = w" by(rule ℰ_new_actions_for_fun)
          thus ?thesis using w' by(auto intro: refl_onPD[OF refl_action_order])
        next
          case False
          with True wa' w' show ?thesis by(auto intro!: action_orderI)
        qed
      qed
    qed
  qed
qed

lemma action_order_read_before_write:
  assumes E: "E ∈ ℰ" "P ⊢ (E, ws) √"
  and ao: "E ⊢ w ≤a r"
  and r: "r ∈ read_actions E"
  and w: "w ∈ write_actions E"
  and adal: "adal ∈ action_loc P E r" "adal ∈ action_loc P E w"
  and sc: "⋀a. ⟦ a < r; a ∈ read_actions E ⟧ ⟹ P,E ⊢ a ↝mrw ws a"
  shows "w < r"
using ao
proof(cases rule: action_orderE)
  case 1
  from init_before_read[OF E r adal(1) sc]
  obtain i where "i < r" "i ∈ new_actions_for P E adal" by blast
  moreover from ‹is_new_action (action_obs E w)› adal(2) ‹w ∈ actions E›
  have "w ∈ new_actions_for P E adal" by(simp add: new_actions_for_def)
  ultimately show "w < r" using E by(auto dest: ℰ_new_actions_for_fun)
next
  case 2
  with r w show ?thesis
    by(cases "w = r")(auto dest: read_actions_not_write_actions)
qed

end

end