section ‹Imperative Concurrent Language›

text ‹This file defines the syntax and semantics of the concurrent programming language described in
  paper, based on Viktor Vafeiadis' Isabelle soundness proof of CSL~\cite{cslsound},
  adapted to Isabelle 2016-1 by Qin Yu and James Brotherston
 see https://people.mpi-sws.org/~viktor/cslsound/). We also prove some useful lemmas about the semantics.›

theory Lang
imports Main StateModel
begin

subsection ‹Language Syntax and Semantics›

type_synonym  state = "store × normal_heap"        (*r States *)

datatype exp =                  (*r Arithmetic expressions *)
    Evar var                    (*r Variable *)
  | Enum nat                    (*r Constant *)
  | Eplus exp exp               (*r Addition *)

datatype bexp =                 (*r Boolean expressions *)
    Beq exp exp                 (*r Equality of expressions *)
  | Band bexp bexp              (*r Conjunction *)
  | Bnot bexp                   (*r Negation *)
  | Btrue

datatype cmd =                  (*r Commands *)
    Cskip                       (*r Empty command *)
  | Cassign var exp             (*r Assignment *)
  | Cread   var exp             (*r Memory load *)
  | Cwrite  exp exp             (*r Memory store *)
  | Calloc  var exp             (*r Memory allocation *)
  | Cdispose exp                (*r Memory de-allocation *)
  | Cseq   cmd cmd              (*r Sequential composition *)
  | Cpar   cmd cmd              (*r Parallel composition *)
  | Cif    bexp cmd cmd         (*r If-then-else *)
  | Cwhile bexp cmd             (*r While loops *)
  | Catomic   cmd         (*r Atomic block *)


text ‹Arithmetic expressions (@{text exp}) consist of variables, constants, and
  operations. Boolean expressions (@{text bexp}) consist of comparisons
  arithmetic expressions. Commands (@{text cmd}) include the empty command,
  assignments, memory reads, writes, allocations and deallocations,
  and parallel composition, conditionals, while loops, local variable
 , and atomic statements.›



subsubsection ‹Semantics of expressions›

text ‹Denotational semantics for arithmetic and boolean expressions.›

primrec
  edenot :: "exp → store → nat"
where
    "edenot (Evar v) s = s v"
  | "edenot (Enum n) s = n"
  | "edenot (Eplus e1 e2) s = edenot e1 s + edenot e2 s"

primrec
  bdenot :: "bexp → store → bool" 
where
    "bdenot (Beq e1 e2) s = (edenot e1 s = edenot e2 s)"
  | "bdenot (Band b1 b2) s = (bdenot b1 s ∧ bdenot b2 s)"
  | "bdenot (Bnot b) s = (¬ bdenot b s)"
  | "bdenot Btrue _ = True"

subsubsection ‹Semantics of commands›

text ‹We give a standard small-step operational semantics to commands with configurations being command-state pairs.›

inductive
  red :: "cmd → state → cmd → state → bool"
and red_rtrans :: "cmd → state → cmd → state → bool"
where
  red_Seq1[intro]: "red (Cseq Cskip C) σ C σ"
| red_Seq2[elim]: "red C1 σ C1' σ' ==> red (Cseq C1 C2) σ (Cseq C1' C2) σ'" 
| red_If1[intro]: "bdenot B (fst σ) ==> red (Cif B C1 C2) σ C1 σ"
| red_If2[intro]: "¬ bdenot B (fst σ) ==> red (Cif B C1 C2) σ C2 σ"
| red_Atomic[intro]:  "red_rtrans C σ Cskip σ' ==> red (Catomic C) σ Cskip σ'"
| red_Par1[elim]: "red C1 σ C1' σ' ==> red (Cpar C1 C2) σ (Cpar C1' C2) σ'" 
| red_Par2[elim]: "red C2 σ C2' σ' ==> red (Cpar C1 C2) σ (Cpar C1 C2') σ'"
| red_Par3[intro]: "red (Cpar Cskip Cskip) σ (Cskip) σ"
| red_Loop[intro]: "red (Cwhile B C) σ (Cif B (Cseq C (Cwhile B C)) Cskip) σ"
| red_Assign[intro]:"[ σ = (s,h); σ' = (s(x := edenot E s), h) ] ==> red (Cassign x E) σ Cskip σ'"
| red_Read[intro]:  "[ σ = (s,h); h(edenot E s) = Some v; σ' = (s(x := v), h) ] ==> red (Cread x E) σ Cskip σ'"
| red_Write[intro]: "[ σ = (s,h); σ' = (s, h(edenot E s ↦ edenot E' s)) ] ==> red (Cwrite E E') σ Cskip σ'"
| red_Alloc[intro]: "[ σ = (s,h); v ∉ dom h; σ' = (s(x := v), h(v ↦ edenot E s)) ] ==> red (Calloc x E) σ Cskip σ'"
| red_Free[intro]:  "[ σ = (s,h); σ' = (s, h(edenot E s := None)) ] ==> red (Cdispose E) σ Cskip σ'"

| NoStep: "red_rtrans C σ C σ"
| OneMoreStep: "[ red C σ C' σ' ; red_rtrans C' σ' C'' σ'' ] ==> red_rtrans C σ C'' σ''"


inductive_cases red_par_cases: "red (Cpar C1 C2) σ C' σ'"
inductive_cases red_atomic_cases: "red (Catomic C) σ C' σ'"

subsubsection ‹Abort semantics›

primrec
  accesses :: "cmd → store → nat set"
where
    "accesses Cskip s = {}"
  | "accesses (Cassign x E) s = {}"
  | "accesses (Cread x E) s = {edenot E s}"
  | "accesses (Cwrite E E') s = {edenot E s}"
  | "accesses (Calloc x E) s = {}"
  | "accesses (Cdispose E) s = {edenot E s}"
  | "accesses (Cseq C1 C2) s = accesses C1 s"
  | "accesses (Cpar C1 C2) s = accesses C1 s ∪ accesses C2 s"
  | "accesses (Cif B C1 C2) s = {}"
  | "accesses (Cwhile B C) s = {}"
  | "accesses (Catomic C) s = {}"


primrec
  writes :: "cmd → store → nat set "
where
    "writes Cskip s = {}"
  | "writes (Cassign x E) s = {}"
  | "writes (Cread x E) s = {}"
  | "writes (Cwrite E E') s = {edenot E s}"
  | "writes (Calloc x E) s = {}"
  | "writes (Cdispose E) s = {edenot E s}"
  | "writes (Cseq C1 C2) s = writes C1 s"
  | "writes (Cpar C1 C2) s = writes C1 s ∪ writes C2 s"
  | "writes (Cif B C1 C2) s = {}"
  | "writes (Cwhile B C) s = {}"
  | "writes (Catomic C) s = {}"


inductive
  aborts :: "cmd → state → bool"
where
  aborts_Seq[intro]:   "aborts C1 σ ==> aborts (Cseq C1 C2) σ"
| aborts_Atomic[intro]: "[ red_rtrans C σ C' σ' ; aborts C' σ' ] ==> aborts (Catomic C) σ"
| aborts_Par1[intro]:  "aborts C1 σ ==> aborts (Cpar C1 C2) σ" 
| aborts_Par2[intro]:  "aborts C2 σ ==> aborts (Cpar C1 C2) σ"
| aborts_Read[intro]:  "edenot E (fst σ) ∉ dom (snd σ) ==> aborts (Cread x E) σ"
| aborts_Write[intro]: "edenot E (fst σ) ∉ dom (snd σ) ==> aborts (Cwrite E E') σ"
| aborts_Free[intro]:  "edenot E (fst σ) ∉ dom (snd σ) ==> aborts (Cdispose E) σ"
| aborts_Race1[intro]:  "accesses C1 (fst σ) ∩ writes C2 (fst σ) ≠ {} ==> aborts (Cpar C1 C2) σ"
| aborts_Race2[intro]:  "writes C1 (fst σ) ∩ accesses C2 (fst σ) ≠ {} ==> aborts (Cpar C1 C2) σ"


inductive_cases abort_atomic_cases: "aborts (Catomic C) σ"

subsection ‹Useful Definitions and Results›

text ‹The free variables of expressions, boolean expressions, and
  are defined as expected:›

primrec
  fvE :: "exp → var set"
where
  "fvE (Evar v) = {v}"
| "fvE (Enum n) = {}"
| "fvE (Eplus e1 e2) = (fvE e1 ∪ fvE e2)"

primrec
  fvB :: "bexp → var set"
where
  "fvB (Beq e1 e2) = (fvE e1 ∪ fvE e2)"
| "fvB (Band b1 b2) = (fvB b1 ∪ fvB b2)"
| "fvB (Bnot b) = (fvB b)"
| "fvB Btrue = {}"

primrec
  fvC :: "cmd → var set"
where
  "fvC (Cskip) = {}"
| "fvC (Cassign v E) = ({v} ∪ fvE E)"
| "fvC (Cread v E) = ({v} ∪ fvE E)"
| "fvC (Cwrite E1 E2) = (fvE E1 ∪ fvE E2)"
| "fvC (Calloc v E) = ({v} ∪ fvE E)"
| "fvC (Cdispose E) = (fvE E)"
| "fvC (Cseq C1 C2) = (fvC C1 ∪ fvC C2)"
| "fvC (Cpar C1 C2) = (fvC C1 ∪ fvC C2)"
| "fvC (Cif B C1 C2) = (fvB B ∪ fvC C1 ∪ fvC C2)"
| "fvC (Cwhile B C) = (fvB B ∪ fvC C)"
| "fvC (Catomic C) = (fvC C)"

primrec
  wrC :: "cmd → var set"
where
  "wrC (Cskip) = {}"
| "wrC (Cassign v E) = {v}"
| "wrC (Cread v E) = {v}"
| "wrC (Cwrite E1 E2) = {}"
| "wrC (Calloc v E) = {v}"
| "wrC (Cdispose E) = {}"
| "wrC (Cseq C1 C2) = (wrC C1 ∪ wrC C2)"
| "wrC (Cpar C1 C2) = (wrC C1 ∪ wrC C2)"
| "wrC (Cif B C1 C2) = (wrC C1 ∪ wrC C2)"
| "wrC (Cwhile B C) = (wrC C)"
| "wrC (Catomic C) = (wrC C)"


primrec
  subE :: "var → exp → exp → exp"
where
  "subE x E (Evar y) = (if x = y then E else Evar y)"
| "subE x E (Enum n) = Enum n"
| "subE x E (Eplus e1 e2) = Eplus (subE x E e1) (subE x E e2)"

primrec
  subB :: "var → exp → bexp → bexp"
where
  "subB x E (Beq e1 e2) = Beq (subE x E e1) (subE x E e2)"
| "subB x E (Band b1 b2) = Band (subB x E b1) (subB x E b2)"
| "subB x E (Bnot b) = Bnot (subB x E b)"
| "subB x E Btrue = Btrue"

text ‹Basic properties of substitutions:›

lemma subE_assign:
 "edenot (subE x E e) s = edenot e (s(x := edenot E s))"
  by (induct e, simp_all)

lemma subB_assign:
 "bdenot (subB x E b) s = bdenot b (s(x := edenot E s))"
proof (induct b)
  case (Beq x1 x2)
  then show ?case
    using bdenot.simps(1) subB.simps(1) subE_assign by presburger
qed (simp_all)

inductive_cases red_skip_cases: "red Cskip σ C' σ'"
inductive_cases aborts_skip_cases: "aborts Cskip σ"


lemma skip_simps[simp]: 
  "¬ red Cskip σ C' σ'"
  "¬ aborts Cskip σ"
  using red_skip_cases apply blast
  using aborts_skip_cases by blast


definition 
  agrees :: "'a set → ('a → 'b) → ('a → 'b) → bool" 
where
  "agrees X s s' ≡ ∀x ∈ X. s x = s' x"

lemma agrees_union:
  "agrees (A ∪ B) s s' ⟷ agrees A s s' ∧ agrees B s s'"
  by (meson Un_iff agrees_def)

text ‹Proposition 4.1: Properties of basic properties of @{term red}.›

lemma agreesI:
  assumes "∧x. x ∈ X ==> s x = s' x"
  shows "agrees X s s'"
  using agrees_def assms by blast

lemma red_properties: 
  "red C σ C' σ' ==> fvC C' ⊆ fvC C ∧ wrC C' ⊆ wrC C ∧ agrees (- wrC C) (fst σ') (fst σ)"
  "red_rtrans C σ C' σ' ==> fvC C' ⊆ fvC C ∧ wrC C' ⊆ wrC C ∧ agrees (- wrC C) (fst σ') (fst σ)"
proof (induct rule: red_red_rtrans.inducts)
  case (OneMoreStep C σ C' σ' C'' σ'')
  then have "fvC C'' ⊆ fvC C"
    by blast
  moreover have "wrC C'' ⊆ wrC C"
    using OneMoreStep.hyps(2) OneMoreStep.hyps(4) by blast
  moreover have "agrees (- wrC C) (fst σ'') (fst σ)"
  proof (rule agreesI)
    fix x assume "x ∈ - wrC C"
    then have "x ∈ -wrC C' ∧ x ∈ -wrC C''"
      using OneMoreStep.hyps(2) OneMoreStep.hyps(4) by blast
    then show "fst σ'' x = fst σ x"
      by (metis OneMoreStep.hyps(2) OneMoreStep.hyps(4) ‹x ∈ - wrC C› agrees_def)
  qed
  ultimately show ?case by simp
qed (auto simp add: agrees_def)

text ‹Proposition 4.2: Semantics does not depend on variables not free in the term›

lemma exp_agrees: "agrees (fvE E) s s' ==> edenot E s = edenot E s'"
by (simp add: agrees_def, induct E, auto)

lemma bexp_agrees:
  "agrees (fvB B) s s' ==> bdenot B s = bdenot B s'"
proof (induct B)
  case (Beq x1 x2)
  then have "agrees (fvE x1) s s' ∧ agrees (fvE x2) s s'"
    by (simp add: agrees_def)
  then show ?case using exp_agrees
    by force
next
  case (Band B1 B2)
  then show ?case
    by (simp add: agrees_def)
qed (simp_all)

lemma red_not_in_fv_not_touched:
  "red C σ C' σ' ==> x ∉ fvC C ==> fst σ x = fst σ' x"
  "red_rtrans C σ C' σ' ==> x ∉ fvC C ==> fst σ x = fst σ' x"
proof (induct arbitrary: rule: red_red_rtrans.inducts)
  case (OneMoreStep C σ C' σ' C'' σ'')
  then show "fst σ x = fst σ'' x"
    by (metis red_properties(1) subsetD)
qed (auto)

lemma agrees_update1:
  assumes "agrees X s s'"
  shows "agrees X (s(x := v)) (s'(x := v))"
proof (rule agreesI)
  fix y show "y ∈ X ==> (s(x := v)) y = (s'(x := v)) y"
    apply (cases "y = x")
    apply simp
    using agrees_def assms by fastforce
qed

lemma agrees_update2:
  assumes "agrees X s s'"
      and "x ∉ X"
  shows "agrees X (s(x := v)) (s'(x := v'))"
proof (rule agreesI)
  fix y show "y ∈ X ==> (s(x := v)) y = (s'(x := v')) y"
    apply (cases "y = x")
    using assms(2) apply blast
    using agrees_def assms(1) by fastforce
qed

lemma red_agrees_aux:
  "red C σ C' σ' ==> (∀s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC C ⊆ X ⟶
   (∃s' h'. red C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'))"
   "red_rtrans C σ C' σ' ==> (∀s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC C ⊆ X ⟶
   (∃s' h'. red_rtrans C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'))"
proof (induct rule: red_red_rtrans.inducts)
  case (red_If1 B σ C1 C2)
  then show ?case
  proof (clarify)
    fix X s h
    assume asm0: "bdenot B (fst σ)" "agrees X (fst σ) s" "fvC (Cif B C1 C2) ⊆ X"
    then have "bdenot B s"
      using Un_iff agrees_def[of X "fst σ" s] bexp_agrees fvC.simps(9) in_mono agrees_def[of "fvB B"]
      by fastforce
    then show "∃s' h'. red (Cif B C1 C2) (s, snd σ) C1 (s', h') ∧ agrees X (fst σ) s' ∧ snd σ = h'"
      by (metis asm0(2) fst_eqD red_red_rtrans.red_If1)
  qed
next
  case (red_If2 B σ C1 C2)
  then show ?case
  proof (clarify)
    fix X s h
    assume asm0: "¬ bdenot B (fst σ)" "agrees X (fst σ) s" "fvC (Cif B C1 C2) ⊆ X"
    then have "¬ bdenot B s"
      using Un_subset_iff agrees_def[of X] agrees_def[of "fvB B"] bexp_agrees fvC.simps(9) in_mono
      by metis
    then show "∃s' h'. red (Cif B C1 C2) (s, snd σ) C2 (s', h') ∧ agrees X (fst σ) s' ∧ snd σ = h'"
      by (metis asm0(2) fst_eqD red_red_rtrans.red_If2)
  qed
next
  case (red_Assign σ ss hh σ' x E)
  then show ?case
  proof (clarify)
    fix X s h
    assume asm0: "σ' = (ss(x := edenot E ss), hh)" "σ = (ss, hh)" "agrees X (fst (ss, hh)) s" "fvC (Cassign x E) ⊆ X"
    then have "edenot E s = edenot E ss"
      using exp_agrees fst_conv fvC.simps(2)
      by (metis (mono_tags, lifting) Un_subset_iff agrees_def in_mono)
    then have "red (Cassign x E) (ss, snd (s, h)) Cskip (ss(x := edenot E s), h)"
      by force
    moreover have "agrees X (fst (s(x := edenot E s), h)) (ss(x := edenot E s))"
    proof (rule agreesI)
      fix y assume "y ∈ X"
      show "fst (s(x := edenot E s), h) y = (ss(x := edenot E s)) y"
        apply (cases "x = y")
        apply simp
        by (metis ‹y ∈ X› agrees_def asm0(3) fstI fun_upd_other)
    qed
    ultimately show "∃s' h'. red (Cassign x E) (s, snd (ss, hh)) Cskip (s', h') ∧ agrees X (fst (ss(x := edenot E ss), hh)) s' ∧ snd (ss(x := edenot E ss), hh) = h'"
      using ‹edenot E s = edenot E ss›
      by (metis agrees_update1 asm0(3) fst_conv red_red_rtrans.red_Assign snd_conv)
  qed
next
  case (red_Read σ ss hh E v σ' x)
  have "∧s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cread x E) ⊆ X ==> (∃s' h'. red (Cread x E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')"
  proof -
    fix s h assume asm0: "agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cread x E) ⊆ X"
    then have "hh (edenot E s) = Some v"
      using red_Read(1) red_Read(2) exp_agrees fstI fvC.simps(3) Un_subset_iff agrees_def[of "fvE E"] in_mono
        agrees_def[of X] by metis
    then have "agrees X (fst σ') (s(x := v))"
      by (metis asm0(1) agrees_update1 fstI red_Read.hyps(1) red_Read.hyps(3) red_Read.prems)
    then show "∃s' h'. red (Cread x E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'"
      using ‹hh (edenot E s) = Some v› red_Read.hyps(1) red_Read.hyps(3) red_Read.prems
      by (metis asm0 red_red_rtrans.red_Read snd_conv)
  qed
  then show ?case by blast
next
  case (red_Write σ ss hh σ' E E')
  have "∧s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cwrite E E') ⊆ X ==> (∃s' h'. red (Cwrite E E') (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')"
  proof -
    fix s h assume asm0: "agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cwrite E E') ⊆ X"
    then have "edenot E ss = edenot E s ∧ edenot E' ss = edenot E' s"
      using red_Write(1) exp_agrees fstI fvC.simps(4)
      by (metis (mono_tags, lifting) Un_subset_iff agrees_def in_mono)
    then show "∃s' h'. red (Cwrite E E') (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'"
      by (metis fst_conv asm0 red_Write.hyps(1) red_Write.hyps(2) red_Write.prems red_red_rtrans.red_Write snd_conv)
  qed
  then show ?case by blast
next
  case (red_Alloc σ ss hh v σ' x E)
  have "∧s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Calloc x E) ⊆ X ==> (∃s' h'. red (Calloc x E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')"
  proof -
    fix s h assume asm0: "agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Calloc x E) ⊆ X"
    then have "edenot E ss = edenot E s"
      using red_Alloc(1) exp_agrees fst_conv fvC.simps(5)
      by (metis (mono_tags, lifting) Un_iff agrees_def in_mono)
    then have "agrees X (fst σ') (s(x := v))"
      by (metis agrees_update1 asm0 fstI red_Alloc.hyps(1) red_Alloc.hyps(3) red_Alloc.prems)
    then show "∃s' h'. red (Calloc x E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'"
      by (metis ‹edenot E ss = edenot E s› red_Alloc.hyps(1) red_Alloc.hyps(2) red_Alloc.hyps(3) red_Alloc.prems red_red_rtrans.red_Alloc snd_eqD asm0)
  qed
  then show ?case by blast
next
  case (red_Free σ ss hh σ' E)
  have "∧s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cdispose E) ⊆ X ==> (∃s' h'. red (Cdispose E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')"
  proof -
    fix s h assume asm0: "agrees X (fst σ) s ∧ snd σ = h ∧ fvC (Cdispose E) ⊆ X"
    then have "edenot E ss = edenot E s"
      using red_Free(1) exp_agrees fst_eqD fvC.simps(6)
      by (metis agrees_def in_mono)
    then show "∃s' h'. red (Cdispose E) (s, h) Cskip (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'"
      using red_Free.hyps(1) red_Free.hyps(2) red_Free.prems asm0 by fastforce
  qed
  then show ?case by blast
next
  case (NoStep C σ)
  then show ?case
    using red_red_rtrans.NoStep by blast
next
  case (OneMoreStep C σ C' σ' C'' σ'')
  have "∧s h. agrees X (fst σ) s ∧ snd σ = h ∧ fvC C ⊆ X ==> (∃s' h'. red_rtrans C (s, h) C'' (s', h') ∧ agrees X (fst σ'') s' ∧ snd σ'' = h')"
  proof -
    fix s h assume asm0: "agrees X (fst σ) s ∧ snd σ = h ∧ fvC C ⊆ X"
    then obtain h' s' where "red C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'"
      using OneMoreStep(2) by auto
    then obtain h'' s'' where "red_rtrans C' (s', h') C'' (s'', h'') ∧ agrees X (fst σ'') s'' ∧ snd σ'' = h''"
      using OneMoreStep.hyps(4) asm0 red_properties(1) by fastforce
    then show "∃s' h'. red_rtrans C (s, h) C'' (s', h') ∧ agrees X (fst σ'') s' ∧ snd σ'' = h'"
      using ‹red C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h'› red_red_rtrans.OneMoreStep by blast
  qed
  then show ?case by blast
qed (fastforce+)

lemma red_agrees[rule_format]:
  "red C σ C' σ' ==> ∀X s. agrees X (fst σ) s ⟶ snd σ = h ⟶ fvC C ⊆ X ⟶
   (∃s' h'. red C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')"
  using red_agrees_aux(1) by blast

lemma writes_accesses: "writes C s ⊆ accesses C s"
  by (induct C arbitrary: s, auto)


lemma accesses_agrees: "agrees (fvC C) s s' ==> accesses C s = accesses C s'"
  apply (induct C arbitrary: s s')
  apply (simp_all add: exp_agrees agrees_def)
  by blast

lemma writes_agrees: "agrees (fvC C) s s' ==> writes C s = writes C s'"
  apply (induct C arbitrary: s s')
  apply (simp_all add: exp_agrees agrees_def)
  by blast


lemma aborts_agrees:
  assumes "aborts C σ"
      and "agrees (fvC C) (fst σ) s"
      and "snd σ = h"
    shows "aborts C (s, h)"
  using assms
proof (induct arbitrary: s h rule: aborts.induct)
  case (aborts_Atomic C σ C' σ')
  then obtain s' where "red_rtrans C (s, h) C' (s', snd σ') ∧ agrees (fvC C) (fst σ') s'"
    by (metis dual_order.refl fvC.simps(11) red_agrees_aux(2))
  moreover have "agrees (fvC C') (fst σ') s'"
    using calculation red_properties(2)
    by (meson agrees_def in_mono)
  ultimately show ?case
    using aborts_Atomic.hyps(3) by blast
next
  case (aborts_Read E σ x)
  then show ?case
    using aborts.aborts_Read[of E σ x] exp_agrees[of E "fst σ" s] fst_conv fvC.simps(3) snd_conv
    by (simp add: aborts.aborts_Read agrees_def)
next
  case (aborts_Write E σ E')
  then show ?case
    using aborts.aborts_Write[of E σ E'] exp_agrees[of _ "fst σ" s] fst_conv fvC.simps(4)[of E E'] snd_conv
    by (simp add: aborts.aborts_Write agrees_def)
next
  case (aborts_Free E σ)
  then show ?case
    using exp_agrees by auto
next
  case (aborts_Par1 C1 σ C2)
  then have "agrees (fvC C1) (fst σ) s"
    by (simp add: agrees_def)
  then show ?case using aborts.aborts_Par1
    by (simp add: aborts_Par1.hyps(2) aborts_Par1.prems(2))
next
  case (aborts_Par2 C2 σ C1)
  then have "agrees (fvC C2) (fst σ) s"
    by (simp add: agrees_def)
  then show ?case using aborts.aborts_Par2
    by (simp add: aborts_Par2.hyps(2) aborts_Par2.prems(2))
next
  case (aborts_Seq C1 σ C2)
  then have "agrees (fvC C1) (fst σ) s"
    by (simp add: agrees_def)
  then show ?case
    by (simp add: aborts.aborts_Seq aborts_Seq.hyps(2) aborts_Seq.prems(2))
next
  case (aborts_Race1 C1 σ C2)
  then show ?case using accesses_agrees[of C1 "fst σ" s] writes_agrees[of C2 "fst σ" s] aborts.aborts_Race1[of C1 "(s, h)" C2]
    by (simp add: agrees_union)
next
  case (aborts_Race2 C1 σ C2)
  then show ?case using accesses_agrees[of C2 "fst σ" s] writes_agrees[of C1 "fst σ" s] aborts.aborts_Race2[of C1 "(s, h)" C2]
    by (simp add: agrees_union)
qed

corollary exp_agrees2[simp]:
  "x ∉ fvE E ==> edenot E (s(x := v)) = edenot E s"
by (rule exp_agrees, simp add: agrees_def)

lemma agrees_update:
  assumes "a ∉ S"
  shows "agrees S s (s(a := v))"
  by (simp add: agrees_def assms)


lemma agrees_comm:
  "agrees S s s' ⟷ agrees S s' s"
  by (metis agrees_def)

lemma not_in_dom:
  assumes "x ∉ dom s"
  shows "s x = None"
  using assms by auto

lemma agrees_minusD:
  "agrees (-X) x y ==> X ∩ Y = {} ==> agrees Y x y"
  by (metis Int_Un_eq(2) agrees_union compl_le_swap1 inf.order_iff inf_shunt)

end