Quelle  Lang.thy

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