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