Theory Compositionality

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
header {* Compositionality Proof for SIFUM-Security Property *}

theory Compositionality
imports Main Security
begin

context sifum_security
begin

(* Set of variables that differs between two memory states: *)
definition differing_vars :: "('Var, 'Val) Mem => (_, _) Mem => 'Var set"
  where
  "differing_vars mem⇩1 mem⇩2 = {x. mem⇩1 x ≠ mem⇩2 x}"

definition differing_vars_lists :: "('Var, 'Val) Mem => (_, _) Mem =>
  ((_, _) Mem × (_, _) Mem) list => nat => 'Var set"
  where
  "differing_vars_lists mem⇩1 mem⇩2 mems i =
   (differing_vars mem⇩1 (fst (mems ! i)) ∪ differing_vars mem⇩2 (snd (mems ! i)))"

lemma differing_finite: "finite (differing_vars mem⇩1 mem⇩2)"
  by (metis UNIV_def Un_UNIV_left finite_Un finite_memory)

lemma differing_lists_finite: "finite (differing_vars_lists mem⇩1 mem⇩2 mems i)"
  by (simp add: differing_finite differing_vars_lists_def)

(* Suggestive notation for substitution / function application *)
definition subst :: "('a \<rightharpoonup> 'b) => ('a => 'b) => ('a => 'b)"
  where
  "subst f mem = (λ x. case f x of
                         None => mem x |
                         Some v => v)"

abbreviation subst_abv :: "('a => 'b) => ('a \<rightharpoonup> 'b) => ('a => 'b)" ("_ [\<mapsto>_]" [900, 0] 1000)
  where
  "f [\<mapsto> σ] ≡ subst σ f"

lemma subst_not_in_dom : "[| x ∉ dom σ |] ==> mem [\<mapsto> σ] x = mem x"
  by (simp add: domIff subst_def)

fun makes_compatible ::
  "('Com, 'Var, 'Val) GlobalConf =>
   ('Com, 'Var, 'Val) GlobalConf =>
   ((_, _) Mem × (_, _) Mem) list =>
  bool"
  where
  "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems =
  (length cms⇩1 = length cms⇩2 ∧ length cms⇩1 = length mems ∧
   (∀ i. i < length cms⇩1 -->
       (∀ σ. dom σ = differing_vars_lists mem⇩1 mem⇩2 mems i -->
         (cms⇩1 ! i, (fst (mems ! i)) [\<mapsto> σ]) ≈ (cms⇩2 ! i, (snd (mems ! i)) [\<mapsto> σ])) ∧
       (∀ x. (mem⇩1 x = mem⇩2 x ∨ dma x = High) -->
             x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i)) ∧
    ((length cms⇩1 = 0 ∧ mem⇩1 =⇧l mem⇩2) ∨ (∀ x. ∃ i. i < length cms⇩1 ∧
                                          x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i)))"

(* This just restates the previous definition using meta-quantification. This allows
  more readable proof blocks that prove each part separately. *)
lemma makes_compatible_intro [intro]:
  "[| length cms⇩1 = length cms⇩2 ∧ length cms⇩1 = length mems;
     (!! i σ. [| i < length cms⇩1; dom σ = differing_vars_lists mem⇩1 mem⇩2 mems i |] ==>
          (cms⇩1 ! i, (fst (mems ! i)) [\<mapsto> σ]) ≈ (cms⇩2 ! i, (snd (mems ! i)) [\<mapsto> σ]));
     (!! i x. [| i < length cms⇩1; mem⇩1 x = mem⇩2 x ∨ dma x = High |] ==> 
          x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i);
     (length cms⇩1 = 0 ∧ mem⇩1 =⇧l mem⇩2) ∨
     (∀ x. ∃ i. i < length cms⇩1 ∧ x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i) |] ==>
  makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  by auto

(* First, some auxiliary lemmas about makes_compatible: *)
lemma compat_low:
  "[| makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems;
     i < length cms⇩1;
     x ∈ differing_vars_lists mem⇩1 mem⇩2 mems i |] ==> dma x = Low"
proof -
  assume "i < length cms⇩1" and "x ∈ differing_vars_lists mem⇩1 mem⇩2 mems i" and
    "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  then also have
    "(mem⇩1 x = mem⇩2 x ∨ dma x = High) --> x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i"
    by (simp add: Let_def, blast)
  ultimately show "dma x = Low"
    by (cases "dma x", blast)
qed

lemma compat_different:
  "[| makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems;
     i < length cms⇩1;
     x ∈ differing_vars_lists mem⇩1 mem⇩2 mems i |] ==> mem⇩1 x ≠ mem⇩2 x ∧ dma x = Low"
  by (cases "dma x", auto)

lemma sound_modes_no_read :
  "[| sound_mode_use (cms, mem); x ∈ (map snd cms ! i) GuarNoRead; i < length cms |] ==>
  doesnt_read (fst (cms ! i)) x"
proof -
  fix cms mem x i
  assume sound_modes: "sound_mode_use (cms, mem)" and "i < length cms"
  hence "locally_sound_mode_use (cms ! i, mem)"
    by (auto simp: sound_mode_use_def list_all_length)
  moreover
  assume "x ∈ (map snd cms ! i) GuarNoRead"
  ultimately show "doesnt_read (fst (cms !i)) x"
    apply (simp add: locally_sound_mode_use_def)
    by (metis PairE `i < length cms` fst_conv loc_reach.refl nth_map snd_conv)
qed

lemma compat_different_vars:
  "[| fst (mems ! i) x = snd (mems ! i) x;
     x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i |] ==>
    mem⇩1 x = mem⇩2 x"
proof -
  assume "x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i"
  hence "fst (mems ! i) x = mem⇩1 x ∧ snd (mems ! i) x = mem⇩2 x"
    by (simp add: differing_vars_lists_def differing_vars_def)
  moreover assume "fst (mems ! i) x = snd (mems ! i) x"
  ultimately show "mem⇩1 x = mem⇩2 x" by auto
qed

lemma differing_vars_subst [rule_format]:
  assumes domσ: "dom σ ⊇ differing_vars mem⇩1 mem⇩2"
  shows "mem⇩1 [\<mapsto> σ] = mem⇩2 [\<mapsto> σ]"
proof (rule ext)
  fix x
  from domσ show "mem⇩1 [\<mapsto> σ] x = mem⇩2 [\<mapsto> σ] x"
    unfolding subst_def differing_vars_def
    by (cases "σ x", auto)
qed

lemma mm_equiv_low_eq:
  "[| ⟨ c⇩1, mds, mem⇩1 ⟩ ≈ ⟨ c⇩2, mds, mem⇩2 ⟩ |] ==> mem⇩1 =⇘mds⇙⇧l mem⇩2"
  unfolding mm_equiv.simps strong_low_bisim_mm_def
  by fast

lemma globally_sound_modes_compatible:
  "[| globally_sound_mode_use (cms, mem) |] ==> compatible_modes (map snd cms)"
  by (simp add: globally_sound_mode_use_def reachable_mode_states_def, auto)

(* map snd cms1 = map snd cms2 states that both global configurations use the same modes *)
lemma compatible_different_no_read :
  assumes sound_modes: "sound_mode_use (cms⇩1, mem⇩1)"
                       "sound_mode_use (cms⇩2, mem⇩2)"
  assumes compat: "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  assumes modes_eq: "map snd cms⇩1 = map snd cms⇩2"
  assumes ile: "i < length cms⇩1"
  assumes x: "x ∈ differing_vars_lists mem⇩1 mem⇩2 mems i"
  shows "doesnt_read (fst (cms⇩1 ! i)) x ∧ doesnt_read (fst (cms⇩2 ! i)) x"
proof -
  from compat have len: "length cms⇩1 = length cms⇩2"
    by simp

  let ?X⇩i = "differing_vars_lists mem⇩1 mem⇩2 mems i"

  from compat ile x have a: "dma x = Low"
    by (metis compat_low)

  from compat ile x have b: "mem⇩1 x ≠ mem⇩2 x"
    by (metis compat_different)

  with a and compat ile x obtain j where
    jprop: "j < length cms⇩1 ∧ x ∉ differing_vars_lists mem⇩1 mem⇩2 mems j"
    by fastforce

  let ?X⇩j = "differing_vars_lists mem⇩1 mem⇩2 mems j"
  obtain σ :: "'Var \<rightharpoonup> 'Val" where domσ: "dom σ = ?X⇩j"
  proof
    let ?σ = "λ x. if (x ∈ ?X⇩j) then Some some_val else None"
    show "dom ?σ = ?X⇩j" unfolding dom_def by auto
  qed
  let ?mdss = "map snd cms⇩1" and
      ?mems⇩1j = "fst (mems ! j)" and
      ?mems⇩2j = "snd (mems ! j)"

  from jprop domσ have subst_eq:
  "?mems⇩1j [\<mapsto> σ] x = ?mems⇩1j x ∧ ?mems⇩2j [\<mapsto> σ] x = ?mems⇩2j x"
  by (metis subst_not_in_dom)

  from compat jprop domσ
  have "(cms⇩1 ! j, ?mems⇩1j [\<mapsto> σ]) ≈ (cms⇩2 ! j, ?mems⇩2j [\<mapsto> σ])"
    by (auto simp: Let_def)

  hence low_eq: "?mems⇩1j [\<mapsto> σ] =⇘?mdss ! j⇙⇧l ?mems⇩2j [\<mapsto> σ]" using modes_eq
    by (metis (no_types) jprop len mm_equiv_low_eq nth_map surjective_pairing)

  with jprop and b have "x ∈ (?mdss ! j) AsmNoRead"
  proof -
    { assume "x ∉ (?mdss ! j) AsmNoRead"
      then have mems_eq: "?mems⇩1j x = ?mems⇩2j x"
        using `dma x = Low` low_eq subst_eq
        by (metis (full_types) low_mds_eq_def subst_eq)

      hence "mem⇩1 x = mem⇩2 x"
        by (metis compat_different_vars jprop)

      hence False by (metis b)
    }
    thus ?thesis by metis
  qed

  hence "x ∈ (?mdss ! i) GuarNoRead"
    using sound_modes jprop
    by (metis compatible_modes_def globally_sound_modes_compatible
      length_map sound_mode_use.simps x ile)

  thus "doesnt_read (fst (cms⇩1 ! i)) x ∧ doesnt_read (fst (cms⇩2 ! i)) x" using sound_modes ile
    by (metis len modes_eq sound_modes_no_read)
qed

definition func_le :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> 'b) => bool" (infixl "\<preceq>" 60)
  where "f \<preceq> g = (∀ x ∈ dom f. f x = g x)"

fun change_respecting ::
  "('Com, 'Var, 'Val) LocalConf =>
   ('Com, 'Var, 'Val) LocalConf =>
   'Var set =>
   (('Var \<rightharpoonup> 'Val) =>
   ('Var \<rightharpoonup> 'Val)) => bool"
  where "change_respecting (cms, mem) (cms', mem') X g =
      ((cms, mem) \<leadsto> (cms', mem') ∧
       (∀ σ. dom σ = X --> g σ \<preceq> σ) ∧
       (∀ σ σ'. dom σ = X ∧ dom σ' = X --> dom (g σ) = dom (g σ')) ∧
       (∀ σ. dom σ = X --> (cms, mem [\<mapsto> σ]) \<leadsto> (cms', mem' [\<mapsto> g σ])))"

lemma change_respecting_dom_unique:
  "[| change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X g |] ==>
   ∃ d. ∀ f. dom f = X --> d = dom (g f)"
  by (metis change_respecting.simps)

lemma func_le_restrict: "[| f \<preceq> g; X ⊆ dom f |] ==> f |` X \<preceq> g"
  by (auto simp: func_le_def)

definition to_partial :: "('a => 'b) => ('a \<rightharpoonup> 'b)"
  where "to_partial f = (λ x. Some (f x))"

lemma func_le_dom: "f \<preceq> g ==> dom f ⊆ dom g"
  by (auto simp add: func_le_def, metis domIff option.simps(2))

lemma doesnt_read_mutually_exclusive:
  assumes noread: "doesnt_read c x"
  assumes eval: "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
  assumes unchanged: "∀ v. ⟨c, mds, mem (x := v)⟩ \<leadsto> ⟨c', mds', mem' (x := v)⟩"
  shows "¬ (∀ v. ⟨c, mds, mem (x := v)⟩ \<leadsto> ⟨c', mds', mem'⟩)"
  using assms
  apply (case_tac "mem' x = some_val")
   apply (metis (full_types) Pair_eq deterministic different_values fun_upd_same)
  by (metis (full_types) Pair_eq deterministic fun_upd_same)

lemma doesnt_read_mutually_exclusive':
  assumes noread: "doesnt_read c x"
  assumes eval: "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
  assumes overwrite: "∀ v. ⟨c, mds, mem (x := v)⟩ \<leadsto> ⟨c', mds', mem'⟩"
  shows "¬ (∀ v. ⟨c, mds, mem (x := v)⟩ \<leadsto> ⟨c', mds', mem' (x := v)⟩)"
  by (metis assms doesnt_read_mutually_exclusive)

lemma change_respecting_dom:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X g"
  assumes domσ: "dom σ = X"
  shows "dom (g σ) ⊆ X"
  by (metis assms change_respecting.simps func_le_dom)
  
lemma change_respecting_intro [iff]:
  "[| ⟨ c, mds, mem ⟩ \<leadsto> ⟨ c', mds', mem' ⟩;
     !! f. dom f = X ==>
           g f \<preceq> f ∧
           (∀ f'. dom f' = X --> dom (g f) = dom (g f')) ∧
           (⟨ c, mds, mem [\<mapsto> f] ⟩ \<leadsto> ⟨ c', mds', mem' [\<mapsto> g f] ⟩) |]
  ==> change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X g"
  unfolding change_respecting.simps
  by blast

(* Used for a proof block in the following lemma *)
lemma conjI3: "[| A; B; C |] ==> A ∧ B ∧ C"
  by simp

lemma noread_exists_change_respecting:
  assumes fin: "finite (X :: 'Var set)"
  assumes eval: "⟨ c, mds, mem ⟩ \<leadsto> ⟨ c', mds', mem' ⟩"
  assumes noread: "∀ x ∈ X. doesnt_read c x"
  shows "∃ (g :: ('Var \<rightharpoonup> 'Val) => ('Var \<rightharpoonup> 'Val)).  change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X g"
proof -
  let ?lc = "⟨c, mds, mem⟩" and ?lc' = "⟨c', mds', mem'⟩"
  from fin eval noread show "∃ g. change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X g"
  proof (induct "X" arbitrary: mem mem' rule: finite_induct)
    case empty
    let ?g = "λ σ. empty"
    have "mem [\<mapsto> empty] = mem" "mem' [\<mapsto> ?g empty] = mem'"
      unfolding subst_def
      by auto
    hence "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ {} ?g"
      using empty
      unfolding change_respecting.simps func_le_def subst_def
      by auto
    thus ?case by auto
  next
    case (insert x X)
    then obtain g⇩X where IH: "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X g⇩X"
      by (metis insert_iff)
    (* Unfortunately, it is necessary to define the required function in advance for
       all case distinctions we want to make. *)
    def g ≡
    "λ σ :: ('Var \<rightharpoonup> 'Val).
       (let σ' = σ |` X in
        (if (∀ v. ⟨c, mds, mem [\<mapsto> σ'] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X σ'] (x := v)⟩)
         then (λ y :: 'Var.
                    if x = y
                    then σ y
                    else g⇩X σ' y)
         else (λ y. g⇩X σ' y)))"
    have "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ (insert x X) g"
    proof
      show "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩" using insert by auto
    next -- "We first show that property (2) is satisfied."
      fix σ :: "'Var \<rightharpoonup> 'Val"
      let ?σ⇩X = "σ |` X"
      assume "dom σ = insert x X"
      hence "dom ?σ⇩X = X"
        by (metis dom_restrict inf_absorb2 subset_insertI)
      from insert also have "doesnt_read c x" by auto
      moreover
      from IH have eval⇩X: "⟨c, mds, mem [\<mapsto> ?σ⇩X]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩"
        using `dom ?σ⇩X = X`
        unfolding change_respecting.simps
        by auto
      ultimately have
        noread⇩x:
        "(∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v) ⟩) ∨
        (∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩)"
        unfolding doesnt_read_def by auto
      show "g σ \<preceq> σ ∧
            (∀ σ'. dom σ' = insert x X --> dom (g σ) = dom (g σ')) ∧
            ⟨c, mds, mem [\<mapsto> σ]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g σ]⟩"
      proof (rule conjI3)
        from noread⇩x show "g σ \<preceq> σ"
        proof
          assume nowrite: "∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto>
                 ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩"
          then have g_simp [simp]: "g σ = (λ y. if y = x then σ y else g⇩X ?σ⇩X y)"
            unfolding g_def
            by auto
          thus "g σ \<preceq> σ"
            using IH
            unfolding g_simp func_le_def
            by (auto, metis `dom (σ |\` X) = X` domI func_le_def restrict_in)
        next
          assume overwrites: "∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto>
            ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩"
          hence
            "¬ (∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩)"
            by (metis `doesnt_read c x` doesnt_read_mutually_exclusive eval⇩X)
          hence g_simp [simp]: "g σ = g⇩X ?σ⇩X"
            unfolding g_def
            by (auto simp: Let_def)

          from IH also have "g⇩X ?σ⇩X \<preceq> ?σ⇩X"
            by (metis `dom (σ |\` X) = X` change_respecting.simps)

          ultimately show "g σ \<preceq> σ"
            unfolding func_le_def
            by (auto, metis `dom (σ |\` X) = X` domI restrict_in)
        qed
      next -- "This part proves that the domain of the family is unique"
        {
        fix σ' :: "'Var \<rightharpoonup> 'Val"
        assume "dom σ' = insert x X"
        let ?σ'⇩X = "σ' |` X"
        have "dom ?σ'⇩X = X"
          by (metis `dom (σ |\` X) = X` `dom σ = insert x X` `dom σ' = insert x X` dom_restrict)
        -- "We first show, that we are always in the same case of the no read assumption:"
        have same_case:
          "((∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩) ∧
            (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X] (x := v)⟩))
           ∨
           ((∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩) ∧
            (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X]⟩))"
          (is "(?N ∧ ?N') ∨ (?O ∧ ?O')")
        proof -
          -- "By deriving a contradiction under the assumption that we are in different cases:"
          have not_different:
            "!! h h'. [| dom h = insert x X; dom h' = insert x X;
                        ∀ v. ⟨c, mds, mem [\<mapsto> h |` X] (x := v)⟩ \<leadsto>
                             ⟨c', mds', mem' [\<mapsto> g⇩X (h |` X)] (x := v)⟩;
                        ∀ v. ⟨c, mds, mem [\<mapsto> h' |` X] (x := v)⟩ \<leadsto>
                             ⟨c', mds', mem' [\<mapsto> g⇩X (h' |` X)]⟩ |]
                      ==> False"
          proof -
            -- "Introduce new names to avoid clashes with functions in the outer scope."
            fix h h' :: "'Var \<rightharpoonup> 'Val"
            assume doms: "dom h = insert x X" "dom h' = insert x X"
            assume nowrite: "∀ v. ⟨c, mds, mem [\<mapsto> h |` X] (x := v)⟩ \<leadsto>
              ⟨c', mds', mem' [\<mapsto> g⇩X (h |` X)] (x := v)⟩"
            assume overwrite: "∀ v. ⟨c, mds, mem [\<mapsto> h' |` X] (x := v)⟩ \<leadsto>
              ⟨c', mds', mem' [\<mapsto> g⇩X (h' |` X)]⟩"

            let ?h⇩X = "h |` X"
            let ?h'⇩X = "h' |` X"

            have "dom ?h⇩X = X"
              by (metis `dom (σ |\` X) = X` `dom σ = insert x X` dom_restrict doms(1))
            have "dom ?h'⇩X = X"
              by (metis `dom (σ |\` X) = X` `dom σ = insert x X` dom_restrict doms(2))

            with IH have eval⇩X': "⟨c, mds, mem [\<mapsto> ?h'⇩X]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?h'⇩X]⟩"
              unfolding change_respecting.simps
              by auto
            with `doesnt_read c x` have noread⇩x':
             "(∀ v. ⟨c, mds, mem [\<mapsto> ?h'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?h'⇩X] (x := v)⟩) ∨
              (∀ v. ⟨c, mds, mem [\<mapsto> ?h'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?h'⇩X]⟩)"
              unfolding doesnt_read_def
              by auto

            from overwrite obtain v where
              "¬ (⟨c, mds, mem [\<mapsto> h' |` X] (x := v)⟩ \<leadsto>
              ⟨c', mds', mem' [\<mapsto> g⇩X (h' |` X)] (x := v)⟩)"
              by (metis `doesnt_read c x` doesnt_read_mutually_exclusive fun_upd_triv)
            moreover

            have "x ∉ dom (?h'⇩X)"
              by (metis `dom (h' |\` X) = X` insert(2))
            with IH have "x ∉ dom (g⇩X ?h'⇩X)"
              by (metis `dom (h' |\` X) = X` change_respecting.simps func_le_dom set_rev_mp)

            ultimately have "mem' x ≠ v"
              by (metis fun_upd_triv overwrite subst_not_in_dom)

            let ?mem⇩v = "mem (x := v)"

            obtain mem⇩v' where "⟨c, mds, ?mem⇩v⟩ \<leadsto> ⟨c', mds', mem⇩v'⟩"
              using insert `doesnt_read c x`
              unfolding doesnt_read_def
              by (auto, metis)
            also have "∀ x ∈ X. doesnt_read c x"
              by (metis insert(5) insert_iff)
              
            ultimately obtain g⇩v where
              IH⇩v: "change_respecting ⟨c, mds, ?mem⇩v⟩ ⟨c', mds', mem⇩v'⟩ X g⇩v"
              by (metis insert(3))

            hence eval⇩v: "⟨c, mds, ?mem⇩v [\<mapsto> ?h⇩X]⟩ \<leadsto> ⟨c', mds', mem⇩v' [\<mapsto> g⇩v ?h⇩X]⟩"
                         "⟨c, mds, ?mem⇩v [\<mapsto> ?h'⇩X]⟩ \<leadsto> ⟨c', mds', mem⇩v' [\<mapsto> g⇩v ?h'⇩X]⟩"
              apply (metis `dom (h |\` X) = X` change_respecting.simps)
              by (metis IH⇩v `dom (h' |\` X) = X` change_respecting.simps)

            from eval⇩v(1) have "mem⇩v' x = v"
            proof -
              assume "⟨c, mds, mem (x := v) [\<mapsto> ?h⇩X]⟩ \<leadsto> ⟨c', mds', mem⇩v' [\<mapsto> g⇩v ?h⇩X]⟩"
              have "?mem⇩v [\<mapsto> ?h⇩X] = mem [\<mapsto> ?h⇩X] (x := v)"
                apply (rule ext, rename_tac y)
                apply (case_tac "y = x")
                 apply (auto simp: subst_def)
                 apply (metis (full_types) `dom (h |\` X) = X` fun_upd_def
                  insert(2) subst_def subst_not_in_dom)
                by (metis fun_upd_other)

              with nowrite have "mem⇩v' [\<mapsto> g⇩v ?h⇩X] = mem' [\<mapsto> g⇩X ?h⇩X] (x := v)"
                using deterministic
                by (erule_tac x = v in allE, auto, metis eval⇩v(1))

              hence "mem⇩v' [\<mapsto> g⇩v ?h⇩X] x = v"
                by simp
              also have "x ∉ dom (g⇩v ?h⇩X)"
                using IH⇩v `dom ?h⇩X = X` change_respecting_dom
                by (metis func_le_dom insert(2) set_rev_mp)
              ultimately show "mem⇩v' x = v"
                by (metis subst_not_in_dom)
            qed
            moreover
            from eval⇩v(2) have "mem⇩v' x = mem' x"
            proof -
              assume "⟨c, mds, ?mem⇩v [\<mapsto> ?h'⇩X]⟩ \<leadsto> ⟨c', mds', mem⇩v' [\<mapsto> g⇩v ?h'⇩X]⟩"
              moreover
              from overwrite have
                "⟨c, mds, mem [\<mapsto> ?h'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?h'⇩X]⟩"
                by auto
              moreover
              have "?mem⇩v [\<mapsto> ?h'⇩X] = mem [\<mapsto> ?h'⇩X] (x := v)"
                apply (rule ext, rename_tac "y")
                apply (case_tac "y = x")
                 apply (metis `x ∉ dom (h' |\` X)` fun_upd_apply subst_not_in_dom)
                apply (auto simp: subst_def)
                by (metis fun_upd_other)
              ultimately have "mem' [\<mapsto> g⇩X ?h'⇩X] = mem⇩v' [\<mapsto> g⇩v ?h'⇩X]"
                using deterministic
                by auto
              also have "x ∉ dom (g⇩v ?h'⇩X)"
                using IH⇩v `dom ?h'⇩X = X` change_respecting_dom
                by (metis func_le_dom insert(2) set_mp)
              ultimately show "mem⇩v' x = mem' x"
                using `x ∉ dom (g⇩X ?h'⇩X)`
                by (metis subst_not_in_dom)
            qed
            ultimately show False
              using `mem' x ≠ v`
              by auto
          qed

          moreover
          have "dom ?σ'⇩X = X"
            by (metis `dom (σ |\` X) = X` `dom σ = insert x X` `dom σ' = insert x X` dom_restrict)

          with IH have eval⇩X': "⟨c, mds, mem [\<mapsto> ?σ'⇩X]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X]⟩"
            unfolding change_respecting.simps
            by auto
          with `doesnt_read c x` have noread⇩x':
             "(∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X] (x := v)⟩)
              ∨
              (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X]⟩)"
            unfolding doesnt_read_def
            by auto

          ultimately show ?thesis
            using noread⇩x not_different `dom σ = insert x X` `dom σ' = insert x X`
            by auto
        qed
        hence "dom (g σ) = dom (g σ')"
        proof
          assume
            "(∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩) ∧
            (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X] (x := v)⟩)"
          hence g_simp [simp]: "g σ = (λ y. if y = x then σ y else g⇩X ?σ⇩X y) ∧
                                g σ' = (λ y. if y = x then σ' y else g⇩X ?σ'⇩X y)"
            unfolding g_def
            by auto
          thus ?thesis
            using IH `dom σ = insert x X` `dom σ' = insert x X`
            unfolding change_respecting.simps
            apply (auto simp: domD)
             apply (metis `dom (σ |\` X) = X` `dom (σ' |\` X) = X` domD domI)
            by (metis `dom (σ |\` X) = X` `dom (σ' |\` X) = X` domD domI)
        next
          assume
            "(∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩) ∧
            (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X]⟩)"
          hence
            "¬ (∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩)
            ∧
            ¬ (∀ v. ⟨c, mds, mem [\<mapsto> ?σ'⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ'⇩X] (x := v)⟩)"
            by (metis `doesnt_read c x` doesnt_read_mutually_exclusive' fun_upd_triv)

          hence g_simp [simp]: "g σ = g⇩X ?σ⇩X ∧ g σ' = g⇩X ?σ'⇩X"
            unfolding g_def
            by (auto simp: Let_def)
          with IH show ?thesis
            unfolding change_respecting.simps
            by (metis `dom (σ |\` X) = X` `dom (σ' |\` X) = X`)
        qed
      }
      thus "∀ σ'. dom σ' = insert x X --> dom (g σ) = dom (g σ')" by blast
    next
      (* Do a case distinction on the no-read statement: *)
      from noread⇩x show "⟨c, mds, mem [\<mapsto> σ]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g σ]⟩"
      proof
        assume nowrite:
          "∀ v. ⟨c, mds, mem[\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩"
        then have g_simp [simp]: "g σ = (λ y. if y = x then σ y else g⇩X ?σ⇩X y)"
          unfolding g_def
          by auto
        obtain v where "σ x = Some v"
          by (metis `dom σ = insert x X` domD insertI1)

        from nowrite have
          "⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩"
          by auto
        moreover
        have "mem [\<mapsto> ?σ⇩X] (x := v) = mem [\<mapsto> σ]"
          apply (rule ext, rename_tac y)
          apply (case_tac "y = x")
           apply (auto simp: subst_def)
           apply (metis `σ x = Some v` option.simps(5))
          by (metis `dom (σ |\` X) = X` `dom σ = insert x X` insertE
            restrict_in subst_def subst_not_in_dom)
        moreover
        have "mem' [\<mapsto> g⇩X ?σ⇩X] (x := v) = mem' [\<mapsto> g σ]"
          apply (rule ext, rename_tac y)
          apply (case_tac "y = x")
           by (auto simp: subst_def option.simps `σ x = Some v`)
        ultimately show ?thesis
          by auto
      next
        assume overwrites:
          "∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X]⟩"
        hence
          "¬ (∀ v. ⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g⇩X ?σ⇩X] (x := v)⟩)"
          by (metis `doesnt_read c x` doesnt_read_mutually_exclusive' eval⇩X)
        hence g_simp [simp]: "g σ = g⇩X ?σ⇩X"
          unfolding g_def
          by (auto simp: Let_def)
        obtain v where "σ x = Some v"
          by (metis `dom σ = insert x X` domD insertI1)
        have "mem [\<mapsto> ?σ⇩X] (x := v) = mem [\<mapsto> σ]"
          apply (rule ext, rename_tac y)
          apply (case_tac "y = x")
           apply (auto simp: subst_def)
           apply (metis `σ x = Some v` option.simps(5))
          by (metis `dom (σ |\` X) = X` `dom σ = insert x X` insertE
            restrict_in subst_def subst_not_in_dom)
        moreover
        from overwrites have "⟨c, mds, mem [\<mapsto> ?σ⇩X] (x := v)⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g σ]⟩"
          by (metis g_simp)
        ultimately show "⟨c, mds, mem [\<mapsto> σ]⟩ \<leadsto> ⟨c', mds', mem' [\<mapsto> g σ]⟩"
            by auto
        qed
      qed
    qed
    thus "∃ g. change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ (insert x X) g"
      by metis
  qed
qed

lemma differing_vars_neg: "x ∉ differing_vars_lists mem1 mem2 mems i ==>
  (fst (mems ! i) x = mem1 x ∧ snd (mems ! i) x = mem2 x)"
  by (simp add: differing_vars_lists_def differing_vars_def)

lemma differing_vars_neg_intro:
  "[| mem⇩1 x = fst (mems ! i) x;
  mem⇩2 x = snd (mems ! i) x |] ==> x ∉ differing_vars_lists mem⇩1 mem⇩2 mems i"
  by (auto simp: differing_vars_lists_def differing_vars_def)

lemma differing_vars_elim [elim]:
  "x ∈ differing_vars_lists mem⇩1 mem⇩2 mems i ==>
  (fst (mems ! i) x ≠ mem⇩1 x) ∨ (snd (mems ! i) x ≠ mem⇩2 x)"
  by (auto simp: differing_vars_lists_def differing_vars_def)

lemma subst_overrides: "dom σ = dom τ ==> mem [\<mapsto> τ] [\<mapsto> σ] = mem [\<mapsto> σ]"
  unfolding subst_def
  by (metis domIff option.exhaust option.simps(4) option.simps(5))

lemma dom_restrict_total: "dom (to_partial f |` X) = X"
  unfolding to_partial_def
  by (metis Int_UNIV_left dom_const dom_restrict)

lemma update_nth_eq:
  "[| xs = ys; n < length xs |] ==> xs = ys [n := xs ! n]"
  by (metis list_update_id)

text {* This property is obvious,
  so an unreadable apply-style proof is acceptable here: *}
lemma mm_equiv_step:
  assumes bisim: "(cms⇩1, mem⇩1) ≈ (cms⇩2, mem⇩2)"
  assumes modes_eq: "snd cms⇩1 = snd cms⇩2"
  assumes step: "(cms⇩1, mem⇩1) \<leadsto> (cms⇩1', mem⇩1')"
  shows "∃ c⇩2' mem⇩2'. (cms⇩2, mem⇩2) \<leadsto> ⟨ c⇩2', snd cms⇩1', mem⇩2' ⟩ ∧
  (cms⇩1', mem⇩1') ≈ ⟨ c⇩2', snd cms⇩1', mem⇩2' ⟩"
  using assms mm_equiv_strong_low_bisim
  unfolding strong_low_bisim_mm_def
  apply auto
  apply (erule_tac x = "fst cms⇩1" in allE)
  apply (erule_tac x = "snd cms⇩1" in allE)
  by (metis surjective_pairing)

lemma change_respecting_doesnt_modify:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X g"
  assumes eval: "(cms, mem) \<leadsto> (cms', mem')"
  assumes domf: "dom f = X"
  assumes x_in_dom: "x ∈ dom (g f)"
  assumes noread: "doesnt_read (fst cms) x"
  shows "mem x = mem' x"
proof -
  let ?f' = "to_partial mem |` X"
  have domf': "dom ?f' = X"
    by (metis dom_restrict_total)

  from cr and eval have "∀ f. dom f = X --> (cms, mem [\<mapsto> f]) \<leadsto> (cms', mem' [\<mapsto> g f])"
    unfolding change_respecting.simps
    by metis
  hence eval': "(cms, mem [\<mapsto> ?f']) \<leadsto> (cms', mem' [\<mapsto> g ?f'])"
    by (metis domf')

  have mem_eq: "mem [\<mapsto> ?f'] = mem"
  proof
    fix x
    show "mem [\<mapsto> ?f'] x = mem x"
      unfolding subst_def
      apply (cases "x ∈ X")
       apply (metis option.simps(5) restrict_in to_partial_def)
      by (metis domf' subst_def subst_not_in_dom)
  qed

  then also have mem'_eq: "mem' [\<mapsto> g ?f'] = mem'"
    using eval eval' deterministic
    by (metis Pair_inject)

  moreover
  have "dom (g ?f') = dom (g f)"
    by (metis change_respecting.simps cr domf domf')
  hence x_in_dom': "x ∈ dom (g ?f')"
    by (metis x_in_dom)
  have "x ∈ X"
    by (metis change_respecting.simps cr domf func_le_dom in_mono x_in_dom)
  hence "?f' x = Some (mem x)"
    by (metis restrict_in to_partial_def)
  hence "g ?f' x = Some (mem x)"
    using cr func_le_def
    by (metis change_respecting.simps domf' x_in_dom')

  hence "mem' [\<mapsto> g ?f'] x = mem x"
    using subst_def x_in_dom'
    by (metis option.simps(5))
  thus "mem x = mem' x"
    by (metis mem'_eq)
qed

(* Some machinery for making use of closedness under globally consistent changes:
   - We introduce the notion of an "adaptation" that replaces (finitely many)
     variables in two memory states with (possibly different) other values.
   - We then define a function to apply adaptations to memory states
*)

type_synonym ('var, 'val) adaptation = "'var \<rightharpoonup> ('val × 'val)"

definition apply_adaptation ::
  "bool => ('Var, 'Val) Mem => ('Var, 'Val) adaptation => ('Var, 'Val) Mem"
  where "apply_adaptation first mem A =
         (λ x. case (A x) of
               Some (v⇩1, v⇩2) => if first then v⇩1 else v⇩2
             | None => mem x)"

abbreviation apply_adaptation⇩1 ::
  "('Var, 'Val) Mem => ('Var, 'Val) adaptation => ('Var, 'Val) Mem"
  ("_ [\<parallel>⇩1 _]" [900, 0] 1000)
  where "mem [\<parallel>⇩1 A] ≡ apply_adaptation True mem A"

abbreviation apply_adaptation⇩2 ::
  "('Var, 'Val) Mem => ('Var, 'Val) adaptation => ('Var, 'Val) Mem"
  ("_ [\<parallel>⇩2 _]" [900, 0] 1000)
  where "mem [\<parallel>⇩2 A] ≡ apply_adaptation False mem A"

definition restrict_total :: "('a => 'b) => 'a set => 'a \<rightharpoonup> 'b" (infix "|'" 60)
  where "restrict_total f A = to_partial f |` A"

lemma differing_empty_eq:
  "[| differing_vars mem mem' = {} |] ==> mem = mem'"
  unfolding differing_vars_def
  by auto

definition globally_consistent_var :: "('Var, 'Val) adaptation => 'Var Mds => 'Var => bool"
  where "globally_consistent_var A mds x ≡
  (case A x of
     Some (v, v') => x ∉ mds AsmNoWrite ∧ (dma x = Low --> v = v')
   | None => True)"

definition globally_consistent  :: "('Var, 'Val) adaptation => 'Var Mds => bool"
  where "globally_consistent A mds ≡ finite (dom A) ∧
  (∀ x ∈ dom A. globally_consistent_var A mds x)"

definition gc2 :: "('Var, 'Val) adaptation => 'Var Mds => bool"
  where "gc2 A mds = (∀ x ∈ dom A. globally_consistent_var A mds x)"

lemma globally_consistent_dom:
  "[| globally_consistent A mds; X ⊆ dom A |] ==> globally_consistent (A |` X) mds"
  unfolding globally_consistent_def globally_consistent_var_def
  by (metis (no_types) IntE dom_restrict inf_absorb2 restrict_in rev_finite_subset)

lemma globally_consistent_writable:
  "[| x ∈ dom A; globally_consistent A mds |] ==> x ∉ mds AsmNoWrite"
  unfolding globally_consistent_def globally_consistent_var_def
  by (metis (no_types) domD option.simps(5) split_part)

lemma globally_consistent_loweq:
  assumes globally_consistent: "globally_consistent A mds"
  assumes some: "A x = Some (v, v')"
  assumes low: "dma x = Low"
  shows "v = v'"
proof -
  from some have "x ∈ dom A"
    by (metis domI)
  hence "case A x of None => True | Some (v, v') => (dma x = Low --> v = v')"
    using globally_consistent
    unfolding globally_consistent_def globally_consistent_var_def
    by (metis option.simps(5) some split_part)
  with `dma x = Low` show ?thesis
    unfolding some
    by auto
qed

lemma globally_consistent_adapt_bisim:
  assumes bisim: "⟨c⇩1, mds, mem⇩1⟩ ≈ ⟨c⇩2, mds, mem⇩2⟩"
  assumes globally_consistent: "globally_consistent A mds"
  shows "⟨c⇩1, mds, mem⇩1 [\<parallel>⇩1 A]⟩ ≈ ⟨c⇩2, mds, mem⇩2 [\<parallel>⇩2 A]⟩"
proof -
  from globally_consistent have "finite (dom A)"
    by (auto simp: globally_consistent_def)
  thus ?thesis
    using globally_consistent
  proof (induct "dom A" arbitrary: A rule: finite_induct)
    case empty
    hence "!! x. A x = None"
      by auto
    hence "mem⇩1 [\<parallel>⇩1 A] = mem⇩1" and "mem⇩2 [\<parallel>⇩2 A] = mem⇩2"
      unfolding apply_adaptation_def
      by auto
    with bisim show ?case
      by auto
  next
    case (insert x X)
    def A' ≡ "A |` X"
    hence "dom A' = X"
      by (metis Int_insert_left_if0 dom_restrict inf_absorb2 insert(2) insert(4) order_refl)
    moreover
    from insert have "globally_consistent A' mds"
      by (metis A'_def globally_consistent_dom subset_insertI)
    ultimately have bisim': "⟨c⇩1, mds, mem⇩1 [\<parallel>⇩1 A']⟩ ≈ ⟨c⇩2, mds, mem⇩2 [\<parallel>⇩2 A']⟩"
      using insert
      by metis
    with insert have writable: "x ∉ mds AsmNoWrite"
      by (metis globally_consistent_writable insertI1)
    from insert obtain v v' where "A x = Some (v, v')"
      unfolding globally_consistent_def globally_consistent_var_def
      by (metis (no_types) domD insert_iff option.simps(5) splitE)

    have A_A': "!! y. y ≠ x ==> A y = A' y"
      unfolding A'_def
      by (metis domIff insert(4) insert_iff restrict_in restrict_out)

    (* The following equalities may have more elegant proofs, but
        this should suffice, since the propositions are
        quite obvious. *)
    have eq⇩1: "mem⇩1 [\<parallel>⇩1 A'] (x := v) = mem⇩1 [\<parallel>⇩1 A]"
      unfolding apply_adaptation_def A'_def
      apply (rule ext, rename_tac y)
      apply (case_tac "x = y")
       apply auto
       apply (metis `A x = Some (v, v')` option.simps(5) split_conv)
      by (metis A'_def A_A')
    have eq⇩2: "mem⇩2 [\<parallel>⇩2 A'] (x := v') = mem⇩2 [\<parallel>⇩2 A]"
      unfolding apply_adaptation_def A'_def
      apply (rule ext, rename_tac y)
      apply (case_tac "x = y")
       apply auto
       apply (metis `A x = Some (v, v')` option.simps(5) split_conv)
      by (metis A'_def A_A')

    show ?case
    proof (cases "dma x")
      assume "dma x = High"
      hence "⟨c⇩1, mds, mem⇩1 [\<parallel>⇩1 A'] (x := v)⟩ ≈ ⟨c⇩2, mds, mem⇩2 [\<parallel>⇩2 A'] (x := v')⟩"
        using mm_equiv_glob_consistent
        unfolding closed_glob_consistent_def
        by (metis bisim' `x ∉ mds AsmNoWrite`)
      thus ?case using eq⇩1 eq⇩2
        by auto
    next
      assume "dma x = Low"
      hence "v = v'"
        by (metis `A x = Some (v, v')` globally_consistent_loweq insert.prems)
      moreover
      from writable and bisim have
        "⟨c⇩1, mds, mem⇩1 [\<parallel>⇩1 A'] (x := v)⟩ ≈ ⟨c⇩2, mds, mem⇩2 [\<parallel>⇩2 A'] (x := v)⟩"
        using mm_equiv_glob_consistent
        unfolding closed_glob_consistent_def
        by (metis `dma x = Low` bisim')
      ultimately show ?case using eq⇩1 eq⇩2
        by auto
    qed
  qed
qed

(* This is the central lemma. Unfortunately, I didn't find
   a nice partitioning into several easier lemmas: *)
lemma makes_compatible_invariant:
  assumes sound_modes: "sound_mode_use (cms⇩1, mem⇩1)"
                      "sound_mode_use (cms⇩2, mem⇩2)"
  assumes compat: "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  assumes modes_eq: "map snd cms⇩1 = map snd cms⇩2"
  assumes eval: "(cms⇩1, mem⇩1) -> (cms⇩1', mem⇩1')"
  obtains cms⇩2' mem⇩2' mems' where
      "map snd cms⇩1' = map snd cms⇩2' ∧
       (cms⇩2, mem⇩2) -> (cms⇩2', mem⇩2') ∧
       makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
proof -
  let ?X = "λ i. differing_vars_lists mem⇩1 mem⇩2 mems i"
  from sound_modes compat modes_eq have
    a: "∀ i < length cms⇩1. ∀ x ∈ (?X i). doesnt_read (fst (cms⇩1 ! i)) x ∧
                                          doesnt_read (fst (cms⇩2 ! i)) x"
    by (metis compatible_different_no_read)
  from eval obtain k where
    b: "k < length cms⇩1 ∧ (cms⇩1 ! k, mem⇩1) \<leadsto> (cms⇩1' ! k, mem⇩1') ∧
        cms⇩1' = cms⇩1 [k := cms⇩1' ! k]"
    by (metis meval_elim nth_list_update_eq)

  from modes_eq have equal_size: "length cms⇩1 = length cms⇩2"
    by (metis length_map)

  let ?mds⇩k = "snd (cms⇩1 ! k)" and
      ?mds⇩k' = "snd (cms⇩1' ! k)" and
      ?mems⇩1k = "fst (mems ! k)" and
      ?mems⇩2k = "snd (mems ! k)" and
      ?n = "length cms⇩1"

  have "finite (?X k)"
    by (metis differing_lists_finite)

  (* Obtaining cms' and mem⇩2' is not in a proof block, since we
     need some of the following statements later: *)
  then obtain g1 where
    c: "change_respecting (cms⇩1 ! k, mem⇩1) (cms⇩1' ! k, mem⇩1') (?X k) g1"
    using noread_exists_change_respecting b a
    by (metis surjective_pairing)

  from compat have "!! σ. dom σ = ?X k ==> ?mems⇩1k [\<mapsto> σ] = mem⇩1 [\<mapsto> σ]"
    by (metis (no_types) Un_upper1 differing_vars_lists_def differing_vars_subst)

  with b and c have
    eval⇩σ: "!! σ. dom σ = ?X k ==> (cms⇩1 ! k, ?mems⇩1k [\<mapsto> σ]) \<leadsto> (cms⇩1' ! k, mem⇩1' [\<mapsto> g1 σ])"
    by auto

  moreover
  with b and compat have
    bisim⇩σ: "!! σ. dom σ = ?X k ==> (cms⇩1 ! k, ?mems⇩1k [\<mapsto> σ]) ≈ (cms⇩2 ! k, ?mems⇩2k [\<mapsto> σ])"
    by auto

  moreover have "snd (cms⇩1 ! k) = snd (cms⇩2 ! k)"
    by (metis b equal_size modes_eq nth_map)
    
  ultimately have d: "!! σ. dom σ = ?X k ==> ∃ c⇩f' mem⇩f'.
    (cms⇩2 ! k, ?mems⇩2k [\<mapsto> σ]) \<leadsto> ⟨ c⇩f', ?mds⇩k', mem⇩f' ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [\<mapsto> g1 σ]) ≈ ⟨ c⇩f', ?mds⇩k', mem⇩f' ⟩"
    by (metis mm_equiv_step)

  obtain h :: "'Var \<rightharpoonup> 'Val" where domh: "dom h = ?X k"
    by (metis dom_restrict_total)

  then obtain c⇩h mem⇩h where h_prop:
    "(cms⇩2 ! k, ?mems⇩2k [\<mapsto> h]) \<leadsto> ⟨ c⇩h, ?mds⇩k', mem⇩h ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [\<mapsto> g1 h]) ≈ ⟨ c⇩h, ?mds⇩k', mem⇩h ⟩"
    using d
    by metis

  then obtain g2 where e:
    "change_respecting (cms⇩2 ! k, ?mems⇩2k [\<mapsto> h]) ⟨ c⇩h, ?mds⇩k', mem⇩h ⟩ (?X k) g2"
    using a b noread_exists_change_respecting
    by (metis differing_lists_finite surjective_pairing)

  -- "The following statements are universally quantified
      since they are reused later:"
  with h_prop have
    "∀ σ. dom σ = ?X k -->
      (cms⇩2 ! k, ?mems⇩2k [\<mapsto> h] [\<mapsto> σ]) \<leadsto> ⟨ c⇩h, ?mds⇩k', mem⇩h [\<mapsto> g2 σ] ⟩"
    unfolding change_respecting.simps
    by auto

  with domh have f:
    "∀ σ. dom σ = ?X k -->
      (cms⇩2 ! k, ?mems⇩2k [\<mapsto> σ]) \<leadsto> ⟨ c⇩h, ?mds⇩k', mem⇩h [\<mapsto> g2 σ] ⟩"
    by (auto simp: subst_overrides)

  from d and f have g: "!! σ. dom σ = ?X k ==>
    (cms⇩2 ! k, ?mems⇩2k [\<mapsto> σ]) \<leadsto> ⟨ c⇩h, ?mds⇩k', mem⇩h [\<mapsto> g2 σ] ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [\<mapsto> g1 σ]) ≈ ⟨ c⇩h, ?mds⇩k', mem⇩h [\<mapsto> g2 σ] ⟩"
    using h_prop
    by (metis deterministic)
  let ?σ_mem⇩2 = "to_partial mem⇩2 |` ?X k"
  def mem⇩2' ≡ "mem⇩h [\<mapsto> g2 ?σ_mem⇩2]"
  def c⇩2' ≡ c⇩h

  have domσ_mem⇩2: "dom ?σ_mem⇩2 = ?X k"
    by (metis dom_restrict_total)

  have "mem⇩2 = ?mems⇩2k [\<mapsto> ?σ_mem⇩2]"
  proof (rule ext)
    fix x
    show "mem⇩2 x = ?mems⇩2k [\<mapsto> ?σ_mem⇩2] x"
      using domσ_mem⇩2
      unfolding to_partial_def subst_def
      apply (cases "x ∈ ?X k")
      apply auto
      by (metis differing_vars_neg)
  qed

  with f domσ_mem⇩2 have i: "(cms⇩2 ! k, mem⇩2) \<leadsto> ⟨ c⇩2', ?mds⇩k', mem⇩2' ⟩"
    unfolding mem⇩2'_def c⇩2'_def
    by metis

  def cms⇩2' ≡ "cms⇩2 [k := (c⇩2', ?mds⇩k')]"

  with i b equal_size have "(cms⇩2, mem⇩2) -> (cms⇩2', mem⇩2')"
    by (metis meval_intro)

  moreover
  from equal_size have new_length: "length cms⇩1' = length cms⇩2'"
    unfolding cms⇩2'_def
    by (metis eval length_list_update meval_elim)

  with modes_eq have "map snd cms⇩1' = map snd cms⇩2'"
    unfolding cms⇩2'_def
    by (metis b map_update snd_conv)

  moreover
  from c and e obtain dom_g1 dom_g2 where
    dom_uniq: "!! σ. dom σ = ?X k ==> dom_g1 = dom (g1 σ)"
              "!! σ. dom σ = ?X k ==> dom_g2 = dom (g2 σ)"
    by (metis change_respecting.simps domh)

  -- "This is the complicated part of the proof."
  obtain mems' where "makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
  proof
    def mems'_k ≡ "λ x.
      if x ∉ ?X k
      then (mem⇩1' x, mem⇩2' x)
      else if (x ∉ dom_g1) ∨ (x ∉ dom_g2)
           then (mem⇩1' x, mem⇩2' x)
           else (?mems⇩1k x, ?mems⇩2k x)"
    -- "This is used in two of the following cases, so we prove it beforehand:"
    have x_unchanged: "!! x. [| x ∈ ?X k; x ∈ dom_g1; x ∈ dom_g2 |] ==>
      mem⇩1 x = mem⇩1' x ∧ mem⇩2 x = mem⇩2' x"
    proof
      fix x
      assume "x ∈ ?X k" and "x ∈ dom_g1"
      thus "mem⇩1 x = mem⇩1' x"
        using a b c
        by (metis change_respecting_doesnt_modify dom_uniq(1) domh)
    next
      fix x
      assume "x ∈ ?X k" and "x ∈ dom_g2"

      hence eq_mem⇩2: "?σ_mem⇩2 x = Some (mem⇩2 x)"
        by (metis restrict_in to_partial_def)
      hence "?mems⇩2k [\<mapsto> h] [\<mapsto> ?σ_mem⇩2] x = mem⇩2 x"
        by (auto simp: subst_def)

      moreover
      from `x ∈ dom_g2` dom_uniq e have g_eq: "g2 ?σ_mem⇩2 x = Some (mem⇩2 x)"
        unfolding change_respecting.simps func_le_def
        by (metis dom_restrict_total eq_mem⇩2)
      hence "mem⇩h [\<mapsto> g2 ?σ_mem⇩2] x = mem⇩2 x"
        by (auto simp: subst_def)

      ultimately have "?mems⇩2k [\<mapsto> h] [\<mapsto> ?σ_mem⇩2] x = mem⇩h [\<mapsto> g2 ?σ_mem⇩2] x"
        by auto
      thus "mem⇩2 x = mem⇩2' x"
        by (metis `mem⇩2 = ?mems⇩2k [\<mapsto> ?σ_mem⇩2]` domσ_mem⇩2 domh mem⇩2'_def subst_overrides)
    qed

    def mems'_i ≡ "λ i x.
      if ((mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x) ∧
          (mem⇩1' x = mem⇩2' x ∨ dma x = High))
         then (mem⇩1' x, mem⇩2' x)
         else if ((mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x) ∧
                  (mem⇩1' x ≠ mem⇩2' x ∧ dma x = Low))
              then (some_val, some_val)
              else (fst (mems ! i) x, snd (mems ! i) x)"

    def mems' ≡
      "map (λ i.
            if i = k
            then (fst o mems'_k, snd o mems'_k)
            else (fst o mems'_i i, snd o mems'_i i))
      [0..< length cms⇩1]"
    from b have mems'_k_simp: "mems' ! k = (fst o mems'_k, snd o mems'_k)"
      unfolding mems'_def
      by auto

    have mems'_simp2: "[| i ≠ k; i < length cms⇩1 |] ==>
      mems' ! i = (fst o mems'_i i, snd o mems'_i i)"
      unfolding mems'_def
      by auto
    (* Some auxiliary statements to allow reasoning about these definitions as if they were given
       by cases instead of nested if clauses. *)
    have mems'_k_1 [simp]: "!! x. [| x ∉ ?X k |] ==>
      fst (mems' ! k) x = mem⇩1' x ∧ snd (mems' ! k) x = mem⇩2' x"
      unfolding mems'_k_simp mems'_k_def
      by auto
    have mems'_k_2 [simp]: "!! x. [| x ∈ ?X k; x ∉ dom_g1 ∨ x ∉ dom_g2 |] ==>
      fst (mems' ! k) x = mem⇩1' x ∧ snd (mems' ! k) x = mem⇩2' x"
      unfolding mems'_k_simp mems'_k_def
      by auto
    have mems'_k_3 [simp]: "!! x. [| x ∈ ?X k; x ∈ dom_g1; x ∈ dom_g2 |] ==>
      fst (mems' ! k) x = fst (mems ! k) x ∧ snd (mems' ! k) x = snd (mems ! k) x"
      unfolding mems'_k_simp mems'_k_def
      by auto

    have mems'_k_cases:
      "!! P x.
        [|
         [| x ∉ ?X k ∨ x ∉ dom_g1 ∨ x ∉ dom_g2;
           fst (mems' ! k) x = mem⇩1' x;
           snd (mems' ! k) x = mem⇩2' x |] ==> P x;
         [| x ∈ ?X k; x ∈ dom_g1; x ∈ dom_g2;
           fst (mems' ! k) x = fst (mems ! k) x;
           snd (mems' ! k) x = snd (mems ! k) x |] ==> P x |] ==> P x"
      using mems'_k_1 mems'_k_2 mems'_k_3
      by blast

    have mems'_i_simp:
      "!! i. [| i < length cms⇩1; i ≠ k |] ==> mems' ! i = (fst o mems'_i i, snd o mems'_i i)"
      unfolding mems'_def
      by auto

    have mems'_i_1 [simp]:
      "!! i x. [| i ≠ k; i < length cms⇩1;
                 mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x;
                 mem⇩1' x = mem⇩2' x ∨ dma x = High |] ==>
               fst (mems' ! i) x = mem⇩1' x ∧ snd (mems' ! i) x = mem⇩2' x"
      unfolding mems'_i_def mems'_i_simp
      by auto

    have mems'_i_2 [simp]:
      "!! i x. [| i ≠ k; i < length cms⇩1;
                 mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x;
                 mem⇩1' x ≠ mem⇩2' x; dma x = Low |] ==>
              fst (mems' ! i) x = some_val ∧ snd (mems' ! i) x = some_val"
      unfolding mems'_i_def mems'_i_simp
      by auto
    have mems'_i_3 [simp]:
      "!! i x. [| i ≠ k; i < length cms⇩1;
                 mem⇩1 x = mem⇩1' x; mem⇩2 x = mem⇩2' x |] ==>
              fst (mems' ! i) x = fst (mems ! i) x ∧ snd (mems' ! i) x = snd (mems ! i) x"
      unfolding mems'_i_def mems'_i_simp
      by auto
    (* This may look complicated, but is actually a rather
       mechanical definition, as it merely spells out the cases
       of the definition: *)
    have mems'_i_cases:
      "!! P i x.
         [| i ≠ k; i < length cms⇩1;
           [| mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x;
             mem⇩1' x = mem⇩2' x ∨ dma x = High;
             fst (mems' ! i) x = mem⇩1' x; snd (mems' ! i) x = mem⇩2' x |] ==> P x;
      [| mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x;
        mem⇩1' x ≠  mem⇩2' x; dma x = Low;
        fst (mems' ! i) x = some_val; snd (mems' ! i) x = some_val |] ==> P x;
      [| mem⇩1 x = mem⇩1' x; mem⇩2 x = mem⇩2' x;
        fst (mems' ! i) x = fst (mems ! i) x; snd (mems' ! i) x = snd (mems ! i) x |] ==> P x |]
      ==> P x"
      using mems'_i_1 mems'_i_2 mems'_i_3
      by (metis (full_types) Sec.exhaust)

    let ?X' = "λ i. differing_vars_lists mem⇩1' mem⇩2' mems' i"
    show "makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
    proof
      have "length cms⇩1' = length cms⇩1"
        by (metis cms⇩2'_def equal_size length_list_update new_length)
      then show "length cms⇩1' = length cms⇩2' ∧ length cms⇩1' = length mems'"
        using compat new_length
        unfolding mems'_def
        by auto
    next
      fix i
      fix σ :: "'Var \<rightharpoonup> 'Val"
      let ?mems⇩1'i = "fst (mems' ! i)"
      let ?mems⇩2'i = "snd (mems' ! i)"
      assume i_le: "i < length cms⇩1'"
      assume domσ: "dom σ = ?X' i"
      show "(cms⇩1' ! i, (fst (mems' ! i)) [\<mapsto> σ]) ≈ (cms⇩2' ! i, (snd (mems' ! i)) [\<mapsto> σ])"
      proof (cases "i = k")
        assume [simp]: "i = k"
        -- "We define another  function from this and reuse the universally quantified statements
          from the first part of the proof."
        def σ' ≡
          "λ x. if x ∈ ?X k
                then if x ∈ ?X' k
                     then σ x
                     else if (x ∈ dom (g1 h))
                             then Some (?mems⇩1'i x)
                             else if (x ∈ dom (g2 h))
                                  then Some (?mems⇩2'i x)
                                  else Some some_val
                else None"
        then have domσ': "dom σ' = ?X k"
          by (auto, metis domI domIff, metis `i = k` domD domσ)

        have diff_vars_impl [simp]: "!!x. x ∈ ?X' k ==> x ∈ ?X k"
        proof (rule ccontr)
          fix x
          assume "x ∉ ?X k"
          hence "mem⇩1 x = ?mems⇩1k x ∧ mem⇩2 x = ?mems⇩2k x"
            by (metis differing_vars_neg)
          from `x ∉ ?X k` also have "?mems⇩1'i x = mem⇩1' x ∧ ?mems⇩2'i x = mem⇩2' x"
            by auto
          moreover
          assume "x ∈ ?X' k"
          hence "mem⇩1' x ≠ ?mems⇩1'i x ∨ mem⇩2' x ≠ ?mems⇩2'i x"
            by (metis `i = k` differing_vars_elim)
          ultimately show False
            by auto
        qed

        have differing_in_dom: "!!x. [| x ∈ ?X k; x ∈ ?X' k |] ==> x ∈ dom_g1 ∧ x ∈ dom_g2"
        proof (rule ccontr)
          fix x
          assume "x ∈ ?X k"
          assume "¬ (x ∈ dom_g1 ∧ x ∈ dom_g2)"
          hence not_in_dom: "x ∉ dom_g1 ∨ x ∉ dom_g2" by auto
          hence "?mems⇩1'i x = mem⇩1' x" "?mems⇩2'i x = mem⇩2' x"
            using `i = k` `x ∈ ?X k` mems'_k_2
            by auto

          moreover assume "x ∈ ?X' k"
          ultimately show False
            by (metis `i = k` differing_vars_elim)
        qed

        (* We now show that we can reuse the earlier statements
           by showing the following equality: *)
        have "?mems⇩1'i [\<mapsto> σ] = mem⇩1' [\<mapsto> g1 σ']"
        proof (rule ext)
          fix x

          show "?mems⇩1'i [\<mapsto> σ] x = mem⇩1' [\<mapsto> g1 σ'] x"
          proof (cases "x ∈ ?X' k")
            assume x_in_X'k: "x ∈ ?X' k"

            then obtain v where "σ x = Some v"
              by (metis domσ domD `i = k`)
            hence "?mems⇩1'i [\<mapsto> σ] x = v"
              using `x ∈ ?X' k` domσ
              by (auto simp: subst_def)
            moreover
            from c have le: "g1 σ' \<preceq> σ'"
              using domσ'
              by auto
            from domσ' and `x ∈ ?X' k` have "x ∈ dom (g1 σ')"
              by (metis diff_vars_impl differing_in_dom dom_uniq(1))
             
            hence "mem⇩1' [\<mapsto> g1 σ'] x = v"
              using domσ' c le
              unfolding func_le_def subst_def
              by (metis σ'_def `σ x = Some v` diff_vars_impl option.simps(5) x_in_X'k)

            ultimately show "?mems⇩1'i [\<mapsto> σ] x = mem⇩1' [\<mapsto> g1 σ'] x" ..
          next
            assume "x ∉ ?X' k"

            hence "?mems⇩1'i [\<mapsto> σ] x = ?mems⇩1'i x"
              using domσ
              by (metis `i = k` subst_not_in_dom)
            show ?thesis
            proof (cases "x ∈ dom_g1")
              assume "x ∈ dom_g1"
              hence "x ∈ dom (g1 σ')"
                using domσ' dom_uniq
                by auto
              hence "g1 σ' x = σ' x"
                using c domσ'
                by (metis change_respecting.simps func_le_def)
              then have "σ' x = Some (?mems⇩1'i x)"
                unfolding σ'_def
                using domσ' domh
                by (metis `g1 σ' x = σ' x` `x ∈ dom (g1 σ')` `x ∉ ?X' k` domIff dom_uniq(1))

              hence "mem⇩1' [\<mapsto> g1 σ'] x = ?mems⇩1'i x"
                unfolding subst_def
                by (metis `g1 σ' x = σ' x` option.simps(5))
              thus ?thesis
                by (metis `?mems⇩1'i [\<mapsto>σ] x = ?mems⇩1'i x`)
            next
              assume "x ∉ dom_g1"
              then have "mem⇩1' [\<mapsto> g1 σ'] x = mem⇩1' x"
                by (metis domσ' dom_uniq(1) subst_not_in_dom)
              moreover
              have "?mems⇩1'i x = mem⇩1' x"
                by (metis `i = k` `x ∉ ?X' k` differing_vars_neg)
              ultimately show ?thesis
                by (metis `?mems⇩1'i [\<mapsto>σ] x = ?mems⇩1'i x`)
            qed
          qed
        qed
        (* And the same for the second memories: *)
        moreover have "?mems⇩2'i [\<mapsto> σ] = mem⇩h [\<mapsto> g2 σ']"
        proof (rule ext)
          fix x

          show "?mems⇩2'i [\<mapsto> σ] x = mem⇩h [\<mapsto> g2 σ'] x"
          proof (cases "x ∈ ?X' k")
            assume "x ∈ ?X' k"

            then obtain v where "σ x = Some v"
              using domσ
              by (metis domD `i = k`)
            hence "?mems⇩2'i [\<mapsto> σ] x = v"
              using `x ∈ ?X' k` domσ
              unfolding subst_def
              by (metis option.simps(5))
            moreover
            from e have le: "g2 σ' \<preceq> σ'"
              using domσ'
              by auto
            from `x ∈ ?X' k` have "x ∈ ?X k"
              by auto
            hence "x ∈ dom (g2 σ')"
              by (metis differing_in_dom domσ' dom_uniq(2) `x ∈ ?X' k`)
            hence "mem⇩2' [\<mapsto> g2 σ'] x = v"
              using domσ' c le
              unfolding func_le_def subst_def
              by (metis σ'_def `σ x = Some v` diff_vars_impl option.simps(5) `x ∈ ?X' k`)

            ultimately show ?thesis
              by (metis domσ' dom_restrict_total dom_uniq(2) mem⇩2'_def subst_overrides)
          next
            assume "x ∉ ?X' k"

            hence "?mems⇩2'i [\<mapsto> σ] x = ?mems⇩2'i x"
              using domσ
              by (metis `i = k` subst_not_in_dom)
            show ?thesis
            proof (cases "x ∈ dom_g2")
              assume "x ∈ dom_g2"
              hence "x ∈ dom (g2 σ')"
                using domσ'
                by (metis dom_uniq)
              hence "g2 σ' x = σ' x"
                using e domσ'
                by (metis change_respecting.simps func_le_def)
              then have "σ' x = Some (?mems⇩2'i x)"
              proof (cases "x ∈ dom_g1")
                -- "This can't happen, so derive a contradiction."
                assume "x ∈ dom_g1"

                have "x ∉ ?X k"
                proof (rule ccontr)
                  assume "¬ (x ∉ ?X k)"
                  hence "x ∈ ?X k" by auto
                  have "mem⇩1 x = mem⇩1' x ∧ mem⇩2 x = mem⇩2' x"
                    by (metis σ'_def `g2 σ' x = σ' x` `x ∈ dom (g2 σ')`
                      `x ∈ dom_g1` `x ∈ dom_g2` domIff x_unchanged)
                  moreover
                  from `x ∉ ?X' k` have
                    "?mems⇩1'i x = ?mems⇩1k x ∧ ?mems⇩2'i x = ?mems⇩2k x"
                    using `x ∈ ?X k` `x ∈ dom_g1` `x ∈ dom_g2`
                    by auto
                  ultimately show False
                    using `x ∈ ?X k` `x ∉ ?X' k`
                    by (metis `i = k` differing_vars_elim differing_vars_neg)
                qed
                hence False
                  by (metis σ'_def `g2 σ' x = σ' x` `x ∈ dom (g2 σ')` domIff)
                thus ?thesis
                  by blast
              next
                assume "x ∉ dom_g1"
                thus ?thesis
                  unfolding σ'_def
                  by (metis `g2 σ' x = σ' x` `x ∈ dom (g2 σ')` `x ∉ ?X' k` 
                    domIff domσ' dom_uniq domh)
              qed
              hence "mem⇩2' [\<mapsto> g2 σ'] x = ?mems⇩2'i x"
                unfolding subst_def
                by (metis `g2 σ' x = σ' x` option.simps(5))
              thus ?thesis
                using `x ∉ ?X' k` domσ domσ'
                by (metis `i = k` dom_restrict_total dom_uniq(2)
                  mem⇩2'_def subst_not_in_dom subst_overrides)
            next
              assume "x ∉ dom_g2"
              then have "mem⇩h [\<mapsto> g2 σ'] x = mem⇩h x"
                by (metis domσ' dom_uniq(2) subst_not_in_dom)
              moreover
              have "?mems⇩2'i x = mem⇩2' x"
                by (metis `i = k` `x ∉ dom_g2` mems'_k_1 mems'_k_2)

              hence "?mems⇩2'i x = mem⇩h x"
                unfolding mem⇩2'_def
                by (metis `x ∉ dom_g2` domσ_mem⇩2 dom_uniq(2) subst_not_in_dom)
              ultimately show ?thesis
                by (metis `?mems⇩2'i [\<mapsto>σ] x = ?mems⇩2'i x`)
            qed
          qed
        qed

        ultimately show
          "(cms⇩1' ! i, (fst (mems' ! i)) [\<mapsto> σ]) ≈ (cms⇩2' ! i, (snd (mems' ! i)) [\<mapsto> σ])"
          using domσ domσ' g b `i = k`
          by (metis c⇩2'_def cms⇩2'_def equal_size nth_list_update_eq)

      next
        assume "i ≠ k"
        def σ' ≡ "λ x. if x ∈ ?X i
                       then if x ∈ ?X' i
                            then σ x
                            else Some (mem⇩1' x)
                       else None"
        let ?mems⇩1i = "fst (mems ! i)" and
            ?mems⇩2i = "snd (mems ! i)"
        have "dom σ' = ?X i"
          unfolding σ'_def
          apply auto
           apply (metis option.simps(2))
          by (metis domD domσ)
        have o: "!! x.
                 (?mems⇩1'i [\<mapsto> σ] x ≠ ?mems⇩1i [\<mapsto> σ'] x ∨
                  ?mems⇩2'i [\<mapsto> σ] x ≠ ?mems⇩2i [\<mapsto> σ'] x)
                 --> (mem⇩1' x ≠ mem⇩1 x ∨ mem⇩2' x ≠ mem⇩2 x)"
        proof -
          fix x
          {
            assume eq_mem: "mem⇩1' x = mem⇩1 x ∧ mem⇩2' x = mem⇩2 x"
            hence mems'_simp [simp]: "?mems⇩1'i x = ?mems⇩1i x ∧ ?mems⇩2'i x = ?mems⇩2i x"
              using mems'_i_3
              by (metis `i ≠ k` b i_le length_list_update)
            have
              "?mems⇩1'i [\<mapsto> σ] x = ?mems⇩1i [\<mapsto> σ'] x ∧ ?mems⇩2'i [\<mapsto> σ] x = ?mems⇩2i [\<mapsto> σ'] x"
            proof (cases "x ∈ ?X' i")
              assume "x ∈ ?X' i"
              hence "?mems⇩1'i x ≠ mem⇩1' x ∨ ?mems⇩2'i x ≠ mem⇩2' x"
                by (metis differing_vars_neg_intro)
              hence "x ∈ ?X i"
                using eq_mem mems'_simp
                by (metis differing_vars_neg)
              hence "σ' x = σ x"
                by (metis σ'_def `x ∈ ?X' i`)
              thus ?thesis
                apply (auto simp: subst_def)
                 apply (metis mems'_simp)
                by (metis mems'_simp)
            next
              assume "x ∉ ?X' i"
              hence "?mems⇩1'i x = mem⇩1' x ∧ ?mems⇩2'i x = mem⇩2' x"
                by (metis differing_vars_neg)
              hence "x ∉ ?X i"
                using eq_mem mems'_simp
                by (auto simp: differing_vars_neg_intro)
              thus ?thesis
                by (metis `dom σ' = ?X i` `x ∉ ?X' i` domσ mems'_simp subst_not_in_dom)
            qed
          }
          thus "?thesis x" by blast
        qed

        from o have
          p: "!! x. [| ?mems⇩1'i [\<mapsto> σ] x ≠ ?mems⇩1i [\<mapsto> σ'] x ∨
                      ?mems⇩2'i [\<mapsto> σ] x ≠ ?mems⇩2i [\<mapsto> σ'] x |] ==>
          x ∉ snd (cms⇩1 ! i) AsmNoWrite"
        proof
          fix x
          assume mems_neq:
            "?mems⇩1'i [\<mapsto> σ] x ≠ ?mems⇩1i [\<mapsto> σ'] x ∨ ?mems⇩2'i [\<mapsto> σ] x ≠ ?mems⇩2i [\<mapsto> σ'] x"
          hence modified:
            "¬ (doesnt_modify (fst (cms⇩1 ! k)) x) ∨ ¬ (doesnt_modify (fst (cms⇩2 ! k)) x)"
            using b i o
            unfolding doesnt_modify_def
            by (metis surjective_pairing)
          moreover
          from sound_modes have loc_modes:
            "locally_sound_mode_use (cms⇩1 ! k, mem⇩1) ∧
             locally_sound_mode_use (cms⇩2 ! k, mem⇩2)"
            unfolding sound_mode_use.simps
            by (metis b equal_size list_all_length)
          moreover
          have "snd (cms⇩1 ! k) = snd (cms⇩2 ! k)"
            by (metis b equal_size modes_eq nth_map)
          have "(cms⇩1 ! k, mem⇩1) ∈ loc_reach (cms⇩1 ! k, mem⇩1)"
            by (metis loc_reach.refl pair_collapse)
          hence guars:
                "x ∈ snd (cms⇩1 ! k) GuarNoWrite --> doesnt_modify (fst (cms⇩1 ! k)) x ∧
                 x ∈ snd (cms⇩2 ! k) GuarNoWrite --> doesnt_modify (fst (cms⇩1 ! k)) x"
            using loc_modes
            unfolding locally_sound_mode_use_def `snd (cms⇩1 ! k) = snd (cms⇩2 ! k)`
            by (metis loc_reach.refl surjective_pairing)

          hence "x ∉ snd (cms⇩1 ! k) GuarNoWrite"
            using modified loc_modes locally_sound_mode_use_def
            by (metis `snd (cms⇩1 ! k) = snd (cms⇩2 ! k)` loc_reach.refl pair_collapse)
          moreover
          from sound_modes have "compatible_modes (map snd cms⇩1)"
            by (metis globally_sound_modes_compatible sound_mode_use.simps)

          ultimately show "x ∉ snd (cms⇩1 ! i) AsmNoWrite"
            unfolding compatible_modes_def
            using `i ≠ k` i_le
            by (metis (no_types) b length_list_update length_map nth_map)
        qed

        have q:
          "!! x. [| dma x = Low;
                   ?mems⇩1'i [\<mapsto> σ] x ≠ ?mems⇩1i [\<mapsto> σ'] x ∨
                   ?mems⇩2'i [\<mapsto> σ] x ≠ ?mems⇩2i [\<mapsto> σ'] x;
                   x ∉ ?X' i |] ==>
                 mem⇩1' x = mem⇩2' x"
          by (metis `i ≠ k` b compat_different_vars i_le length_list_update mems'_i_2 o)
        have "i < length cms⇩1"
          by (metis cms⇩2'_def equal_size i_le length_list_update new_length)
        with compat and `dom σ' = ?X i` have
          bisim: "(cms⇩1 ! i, ?mems⇩1i [\<mapsto> σ']) ≈ (cms⇩2 ! i, ?mems⇩2i [\<mapsto> σ'])"
          by auto

        let ?Δ = "differing_vars (?mems⇩1i [\<mapsto> σ']) (?mems⇩1'i [\<mapsto> σ]) ∪
                  differing_vars (?mems⇩2i [\<mapsto> σ']) (?mems⇩2'i [\<mapsto> σ])"

        have Δ_finite: "finite ?Δ"
          by (metis (no_types) differing_finite finite_UnI)
        -- "We first define the adaptation, then prove that it does the right thing."
        def A ≡ "λ x. if x ∈ ?Δ
                      then if dma x = High
                           then Some (?mems⇩1'i [\<mapsto> σ] x, ?mems⇩2'i [\<mapsto> σ] x)
                           else if x ∈ ?X' i
                                then (case σ x of
                                        Some v => Some (v, v)
                                      | None => None)
                                else Some (mem⇩1' x, mem⇩1' x)
                      else None"
        have domA: "dom A = ?Δ"
        proof
          show "dom A ⊆ ?Δ"
            using A_def
            apply (auto simp: domD)
            by (metis option.simps(2))
        next
          show "?Δ ⊆ dom A"
            unfolding A_def
            apply auto
             apply (metis (no_types) domIff domσ option.exhaust option.simps(5))
            by (metis (no_types) domIff domσ option.exhaust option.simps(5))
        qed

        have A_correct:
              "!! x.
               globally_consistent_var A (snd (cms⇩1 ! i)) x ∧
               ?mems⇩1i [\<mapsto> σ'] [\<parallel>⇩1 A] x = ?mems⇩1'i [\<mapsto> σ] x ∧
               ?mems⇩2i [\<mapsto> σ'] [\<parallel>⇩2 A] x = ?mems⇩2'i [\<mapsto> σ] x"
        proof -
          fix x
          show "?thesis x"
            (is "?A ∧ ?Eq⇩1 ∧ ?Eq⇩2")
          proof (cases "x ∈ ?Δ")
            assume "x ∈ ?Δ"
            hence diff:
              "?mems⇩1'i [\<mapsto> σ] x ≠ ?mems⇩1i [\<mapsto> σ'] x ∨ ?mems⇩2'i [\<mapsto> σ] x ≠ ?mems⇩2i [\<mapsto> σ'] x"
              by (auto simp: differing_vars_def)
            from p and diff have writable: "x ∉ snd (cms⇩1 ! i) AsmNoWrite"
              by auto
            show ?thesis
            proof (cases "dma x")
              assume "dma x = High"
              from `dma x = High` have A_simp [simp]:
                "A x = Some (?mems⇩1'i [\<mapsto> σ] x, ?mems⇩2'i [\<mapsto> σ] x)"
                unfolding A_def
                by (metis `x ∈ ?Δ`)
              from writable have "?A"
                unfolding globally_consistent_var_def A_simp
                using `dma x = High`
                by auto
              moreover
              from A_simp have ?Eq⇩1 ?Eq⇩2
                unfolding A_def apply_adaptation_def
                by auto
              ultimately show ?thesis
                by auto
            next
              assume "dma x = Low"
              show ?thesis
              proof (cases "x ∈ ?X' i")
                assume "x ∈ ?X' i"
                then obtain v where "σ x = Some v"
                  by (metis domD domσ)
                hence eq: "?mems⇩1'i [\<mapsto> σ] x = v ∧ ?mems⇩2'i [\<mapsto> σ] x = v"
                  unfolding subst_def
                  by auto
                moreover
                from `x ∈ ?X' i` and `dma x = Low` have A_simp [simp]:
                  "A x = (case σ x of
                            Some v => Some (v, v)
                          | None => None)"
                  unfolding A_def
                  by (metis Sec.simps(1) `x ∈ ?Δ`)
                with writable eq `σ x = Some v` have "?A"
                  unfolding globally_consistent_var_def
                  by auto
                ultimately show ?thesis
                  using domA `x ∈ ?Δ` `σ x = Some v`
                  by (auto simp: apply_adaptation_def)

              next
                assume "x ∉ ?X' i"
                hence A_simp [simp]: "A x = Some (mem⇩1' x, mem⇩1' x)"
                  unfolding A_def
                  using `x ∈ ?Δ` `dma x = Low`
                  by auto
                from q have "mem⇩1' x = mem⇩2' x"
                  by (metis `dma x = Low` diff `x ∉ ?X' i`)
                with writable have ?A
                  unfolding globally_consistent_var_def
                  by auto

                moreover
                from `x ∉ ?X' i` have
                  "?mems⇩1'i [\<mapsto> σ] x = ?mems⇩1'i x ∧ ?mems⇩2'i [\<mapsto> σ] x = ?mems⇩2'i x"
                  by (metis domσ subst_not_in_dom)
                moreover
                from `x ∉ ?X' i` have "?mems⇩1'i x = mem⇩1' x ∧ ?mems⇩2'i x = mem⇩2' x"
                  by (metis differing_vars_neg)
                ultimately show ?thesis
                  using `mem⇩1' x = mem⇩2' x`
                  by (auto simp: apply_adaptation_def)
              qed
            qed
          next
            assume "x ∉ ?Δ"
            hence "A x = None"
              by (metis domA domIff)
            hence "globally_consistent_var A (snd (cms⇩1 ! i)) x"
              by (auto simp: globally_consistent_var_def)
            moreover
            from `A x = None` have "x ∉ dom A"
              by (metis domIff)
            from `x ∉ ?Δ` have "?mems⇩1i [\<mapsto> σ'] [\<parallel>⇩1 A] x = ?mems⇩1'i [\<mapsto> σ] x ∧
                                 ?mems⇩2i [\<mapsto> σ'] [\<parallel>⇩2 A] x = ?mems⇩2'i [\<mapsto> σ] x"
              using `A x = None`
              unfolding differing_vars_def apply_adaptation_def
              by auto

            ultimately show ?thesis
              by auto
          qed
        qed
        hence "?mems⇩1i [\<mapsto> σ'] [\<parallel>⇩1 A] = ?mems⇩1'i [\<mapsto> σ] ∧
               ?mems⇩2i [\<mapsto> σ'] [\<parallel>⇩2 A] = ?mems⇩2'i [\<mapsto> σ]"
          by auto
        moreover
        from A_correct have "globally_consistent A (snd (cms⇩1 ! i))"
          by (metis Δ_finite globally_consistent_def domA)

        have "snd (cms⇩1 ! i) = snd (cms⇩2 ! i)"
          by (metis `i < length cms⇩1` equal_size modes_eq nth_map)

        with bisim have "(cms⇩1 ! i, ?mems⇩1i [\<mapsto> σ'] [\<parallel>⇩1 A]) ≈ (cms⇩2 ! i, ?mems⇩2i [\<mapsto> σ'] [\<parallel>⇩2 A])"
          using `globally_consistent A (snd (cms⇩1 ! i))`
          apply (subst surjective_pairing[of "cms⇩1 ! i"])
          apply (subst surjective_pairing[of "cms⇩2 ! i"])
          by (metis surjective_pairing globally_consistent_adapt_bisim)

        ultimately show ?thesis
          by (metis `i ≠ k` b cms⇩2'_def nth_list_update_neq)
      qed
    next
      fix i x

      let ?mems⇩1'i = "fst (mems' ! i)"
      let ?mems⇩2'i = "snd (mems' ! i)"
      assume i_le: "i < length cms⇩1'"
      assume mem_eq: "mem⇩1' x = mem⇩2' x ∨ dma x = High"
      show "x ∉ ?X' i"
      proof (cases "i = k")
        assume "i = k"
        thus "x ∉ ?X' i"
          apply (cases "x ∉ ?X k ∨ x ∉ dom_g1 ∨ x ∉ dom_g2")
           apply (metis differing_vars_neg_intro mems'_k_1 mems'_k_2)
          by (metis Sec.simps(2) b compat compat_different mem_eq x_unchanged)
      next
        assume "i ≠ k"
        thus "x ∉ ?X' i"
        proof (rule mems'_i_cases)
          from b i_le show "i < length cms⇩1"
            by (metis length_list_update)
        next
          assume "fst (mems' ! i) x = mem⇩1' x"
            "snd (mems' ! i) x = mem⇩2' x"
          thus "x ∉ ?X' i"
            by (metis differing_vars_neg_intro)
        next
          assume "mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x"
            "mem⇩1' x ≠ mem⇩2' x" and "dma x = Low"
          -- "In this case, for example, the values of (mems' ! i) are not needed."
          thus "x ∉ ?X' i"
            by (metis Sec.simps(2) mem_eq)
        next
          assume case3: "mem⇩1 x = mem⇩1' x" "mem⇩2 x = mem⇩2' x"
            "fst (mems' ! i) x = fst (mems ! i) x"
            "snd (mems' ! i) x = snd (mems ! i) x"
          have "x ∈ ?X' i ==> mem⇩1' x ≠ mem⇩2' x ∧ dma x = Low"
          proof -
            assume "x ∈ ?X' i"
            from case3 and `x ∈ ?X' i` have "x ∈ ?X i"
              by (metis differing_vars_neg differing_vars_elim)
            with case3 show ?thesis
              by (metis b compat compat_different i_le length_list_update)
          qed
          with `mem⇩1' x = mem⇩2' x ∨ dma x = High` show "x ∉ ?X' i"
            by auto
        qed
      qed
    next
      { fix x
        have "∃ i < length cms⇩1. x ∉ ?X' i"
        proof (cases "mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x")
          assume var_changed: "mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x"
          have "x ∉ ?X' k"
            apply (rule mems'_k_cases)
             apply (metis differing_vars_neg_intro)
            by (metis var_changed x_unchanged)
          thus ?thesis by (metis b)
        next
          assume "¬ (mem⇩1 x ≠ mem⇩1' x ∨ mem⇩2 x ≠ mem⇩2' x)"
          hence assms: "mem⇩1 x = mem⇩1' x" "mem⇩2 x = mem⇩2' x" by auto

          have "length cms⇩1 ≠ 0"
            using b
            by (metis less_zeroE)
          then obtain i where i_prop: "i < length cms⇩1 ∧ x ∉ ?X i"
            using compat
            by (auto, blast)
          show ?thesis
          proof (cases "i = k")
            assume "i = k"
            have "x ∉ ?X' k"
              apply (rule mems'_k_cases)
               apply (metis differing_vars_neg_intro)
              by (metis i_prop `i = k`)
            thus ?thesis
              by (metis b)
          next
            assume "i ≠ k"
            hence "fst (mems' ! i) x = fst (mems ! i) x"
                  "snd (mems' ! i) x = snd (mems ! i) x"
              using i_prop assms mems'_i_3
              by auto
            with i_prop have "x ∉ ?X' i"
              by (metis assms differing_vars_neg differing_vars_neg_intro)
            with i_prop show ?thesis
              by auto
          qed
        qed
      }
      thus "(length cms⇩1' = 0 ∧ mem⇩1' =⇧l mem⇩2') ∨ (∀ x. ∃ i < length cms⇩1'. x ∉ ?X' i)"
        by (metis cms⇩2'_def equal_size length_list_update new_length)
    qed
  qed

  ultimately show ?thesis using that by blast
qed

text {* The Isar proof language provides a readable
way of specifying assumptions while also giving them names for subsequent
usage. *}
lemma compat_low_eq:
  assumes compat: "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  assumes modes_eq: "map snd cms⇩1 = map snd cms⇩2"
  assumes x_low: "dma x = Low"
  assumes x_readable: "∀ i < length cms⇩1. x ∉ snd (cms⇩1 ! i) AsmNoRead"
  shows "mem⇩1 x = mem⇩2 x"
proof -
  let ?X = "λ i. differing_vars_lists mem⇩1 mem⇩2 mems i"
  from compat have "(length cms⇩1 = 0 ∧ mem⇩1 =⇧l mem⇩2) ∨
                    (∀ x. ∃ j. j < length cms⇩1 ∧ x ∉ ?X j)"
    by auto
  thus "mem⇩1 x = mem⇩2 x"
  proof
    assume "length cms⇩1 = 0 ∧ mem⇩1 =⇧l mem⇩2"
    with x_low show ?thesis
      by (simp add: low_eq_def)
  next
    assume "∀ x. ∃ j. j < length cms⇩1 ∧ x ∉ ?X j"
    then obtain j where j_prop: "j < length cms⇩1 ∧ x ∉ ?X j"
      by auto
    let ?mems⇩1j = "fst (mems ! j)" and
        ?mems⇩2j = "snd (mems ! j)"

    obtain σ :: "'Var \<rightharpoonup> 'Val" where "dom σ = ?X j"
      by (metis dom_restrict_total)

    with compat and j_prop have "(cms⇩1 ! j, ?mems⇩1j [\<mapsto> σ]) ≈ (cms⇩2 ! j, ?mems⇩2j [\<mapsto> σ])"
      by auto
    
    moreover
    have "snd (cms⇩1 ! j) = snd (cms⇩2 ! j)"
      using modes_eq
      by (metis j_prop length_map nth_map)

    ultimately have "?mems⇩1j [\<mapsto> σ] =⇘snd (cms⇩1 ! j)⇙⇧l ?mems⇩2j [\<mapsto> σ]"
      using modes_eq j_prop
      by (metis pair_collapse mm_equiv_low_eq)
    hence "?mems⇩1j x = ?mems⇩2j x"
      using x_low x_readable j_prop `dom σ = ?X j`
      unfolding low_mds_eq_def
      by (metis subst_not_in_dom)

    thus ?thesis
      using j_prop
      by (metis compat_different_vars)
  qed
qed

lemma loc_reach_subset:
  assumes eval: "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
  shows "loc_reach ⟨c', mds', mem'⟩ ⊆ loc_reach ⟨c, mds, mem⟩"
proof (clarify)
  fix c'' mds'' mem''
  from eval have "⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem⟩"
    by (metis loc_reach.refl loc_reach.step surjective_pairing)
  assume "⟨c'', mds'', mem''⟩ ∈ loc_reach ⟨c', mds', mem'⟩"
  thus "⟨c'', mds'', mem''⟩ ∈ loc_reach ⟨c, mds, mem⟩"
    apply induct
      apply (metis `⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem⟩` surjective_pairing)
     apply (metis loc_reach.step)
    by (metis loc_reach.mem_diff)
qed

lemma locally_sound_modes_invariant:
  assumes sound_modes: "locally_sound_mode_use ⟨c, mds, mem⟩"
  assumes eval: "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
  shows "locally_sound_mode_use ⟨c', mds', mem'⟩"
proof -
  from eval have "⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem⟩"
    by (metis fst_conv loc_reach.refl loc_reach.step snd_conv)
  thus ?thesis
    using sound_modes
    unfolding locally_sound_mode_use_def
    by (metis (no_types) Collect_empty_eq eval loc_reach_subset subsetD)
qed

lemma reachable_modes_subset:
  assumes eval: "(cms, mem) -> (cms', mem')"
  shows "reachable_mode_states (cms', mem') ⊆ reachable_mode_states (cms, mem)"
proof
  fix mdss
  assume "mdss ∈ reachable_mode_states (cms', mem')"
  thus "mdss ∈ reachable_mode_states (cms, mem)"
    using reachable_mode_states_def
    apply auto
    by (metis (hide_lams, no_types) assms converse_rtrancl_into_rtrancl)
qed

lemma globally_sound_modes_invariant:
  assumes globally_sound: "globally_sound_mode_use (cms, mem)"
  assumes eval: "(cms, mem) -> (cms', mem')"
  shows "globally_sound_mode_use (cms', mem')"
  using assms reachable_modes_subset
  unfolding globally_sound_mode_use_def
  by (metis (no_types) subsetD)

lemma loc_reach_mem_diff_subset:
  assumes mem_diff: "∀ x. x ∈ mds AsmNoWrite --> mem⇩1 x = mem⇩2 x"
  shows "⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem⇩1⟩ ==> ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem⇩2⟩"
proof -
  let ?lc = "⟨c', mds', mem'⟩"
  assume "?lc ∈ loc_reach ⟨c, mds, mem⇩1⟩"
  thus ?thesis
  proof (induct)
    case refl
    thus ?case
      by (metis fst_conv loc_reach.mem_diff loc_reach.refl local.mem_diff snd_conv)
  next
    case step
    thus ?case
      by (metis loc_reach.step)
  next
    case mem_diff
    thus ?case
      by (metis loc_reach.mem_diff)
  qed
qed

lemma loc_reach_mem_diff_eq:
  assumes mem_diff: "∀ x. x ∈ mds AsmNoWrite --> mem' x = mem x"
  shows "loc_reach ⟨c, mds, mem⟩ = loc_reach ⟨c, mds, mem'⟩"
  using assms loc_reach_mem_diff_subset
  by (auto, metis)

lemma sound_modes_invariant:
  assumes sound_modes: "sound_mode_use (cms, mem)"
  assumes eval: "(cms, mem) -> (cms', mem')"
  shows "sound_mode_use (cms', mem')"
proof -
  from sound_modes and eval have "globally_sound_mode_use (cms', mem')"
    by (metis globally_sound_modes_invariant sound_mode_use.simps)
  moreover
  from sound_modes have loc_sound: "∀ i < length cms. locally_sound_mode_use (cms ! i, mem)"
    unfolding sound_mode_use_def
    by simp (metis list_all_length)
  from eval obtain k cms⇩k' where
    ev: "(cms ! k, mem) \<leadsto> (cms⇩k', mem') ∧ k < length cms ∧ cms' = cms [k := cms⇩k']"
    by (metis meval_elim)
  hence "length cms = length cms'"
    by auto
  have "!! i. i < length cms' ==> locally_sound_mode_use (cms' ! i, mem')"
  proof -
    fix i
    assume i_le: "i < length cms'"
    thus "?thesis i"
    proof (cases "i = k")
      assume "i = k"
      thus ?thesis
        using i_le ev loc_sound
        by (metis (hide_lams, no_types) locally_sound_modes_invariant nth_list_update surj_pair)
    next
      assume "i ≠ k"
      hence "cms' ! i = cms ! i"
        by (metis ev nth_list_update_neq)
      from sound_modes have "compatible_modes (map snd cms)"
        unfolding sound_mode_use.simps
        by (metis globally_sound_modes_compatible)
      hence "!! x. x ∈ snd (cms ! i) AsmNoWrite ==> x ∈ snd (cms ! k) GuarNoWrite"
        unfolding compatible_modes_def
        by (metis (no_types) `i ≠ k` `length cms = length cms'` ev i_le length_map nth_map)
      hence "!! x. x ∈ snd (cms ! i) AsmNoWrite --> doesnt_modify (fst (cms ! k)) x"
        using ev loc_sound
        unfolding locally_sound_mode_use_def
        by (metis loc_reach.refl surjective_pairing)
      with eval have "!! x. x ∈ snd (cms ! i) AsmNoWrite --> mem x = mem' x"
        by (metis (no_types) doesnt_modify_def ev pair_collapse)
      then have "loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)"
        by (metis loc_reach_mem_diff_eq pair_collapse)
      thus ?thesis
        using loc_sound i_le `length cms = length cms'`
        unfolding locally_sound_mode_use_def
        by (metis `cms' ! i = cms ! i`)
    qed
  qed
  ultimately show ?thesis
    unfolding sound_mode_use.simps
    by (metis (no_types) list_all_length)
qed

lemma makes_compatible_eval_k:
  assumes compat: "makes_compatible (cms⇩1, mem⇩1) (cms⇩2, mem⇩2) mems"
  assumes modes_eq: "map snd cms⇩1 = map snd cms⇩2"
  assumes sound_modes: "sound_mode_use (cms⇩1, mem⇩1)" "sound_mode_use (cms⇩2, mem⇩2)"
  assumes eval: "(cms⇩1, mem⇩1) ->⇘k⇙ (cms⇩1', mem⇩1')"
  shows "∃ cms⇩2' mem⇩2' mems'. sound_mode_use (cms⇩1', mem⇩1') ∧
                              sound_mode_use (cms⇩2', mem⇩2') ∧
                              map snd cms⇩1' = map snd cms⇩2' ∧
                              (cms⇩2, mem⇩2) ->⇘k⇙ (cms⇩2', mem⇩2') ∧
                              makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
proof -
  (* cms⇩1' and mem⇩1' need to be arbitrary so
     that the induction hypothesis is sufficiently general. *)
  from eval show ?thesis
  proof (induct "k" arbitrary: cms⇩1' mem⇩1')
    case 0
    hence "cms⇩1' = cms⇩1 ∧ mem⇩1' = mem⇩1"
      by (metis Pair_eq meval_k.simps(1))
    thus ?case
      by (metis compat meval_k.simps(1) modes_eq sound_modes)
  next
    case (Suc k)
    then obtain cms⇩1'' mem⇩1'' where eval'':
      "(cms⇩1, mem⇩1) ->⇘k⇙ (cms⇩1'', mem⇩1'') ∧ (cms⇩1'', mem⇩1'') -> (cms⇩1', mem⇩1')"
      by (metis meval_k.simps(2) prod_cases3 snd_conv)
    hence "(cms⇩1'', mem⇩1'') -> (cms⇩1', mem⇩1')" ..
    moreover
    from eval'' obtain cms⇩2'' mem⇩2'' mems'' where IH:
      "sound_mode_use (cms⇩1'', mem⇩1'') ∧
       sound_mode_use (cms⇩2'', mem⇩2'') ∧
       map snd cms⇩1'' = map snd cms⇩2'' ∧
       (cms⇩2, mem⇩2) ->⇘k⇙ (cms⇩2'', mem⇩2'') ∧
       makes_compatible (cms⇩1'', mem⇩1'') (cms⇩2'', mem⇩2'') mems''"
      using Suc
      by metis
    ultimately obtain cms⇩2' mem⇩2' mems' where
      "map snd cms⇩1' = map snd cms⇩2' ∧
       (cms⇩2'', mem⇩2'') -> (cms⇩2', mem⇩2') ∧
       makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
      using makes_compatible_invariant
      by blast
    thus ?case
      by (metis IH eval'' meval_k.simps(2) sound_modes_invariant)
  qed
qed

lemma differing_vars_initially_empty:
  "i < n ==> x ∉ differing_vars_lists mem⇩1 mem⇩2 (zip (replicate n mem⇩1) (replicate n mem⇩2)) i"
  unfolding differing_vars_lists_def differing_vars_def
  by auto

lemma compatible_refl:
  assumes coms_secure: "list_all com_sifum_secure cmds"
  assumes low_eq: "mem⇩1 =⇧l mem⇩2"
  shows "makes_compatible (add_initial_modes cmds, mem⇩1)
                          (add_initial_modes cmds, mem⇩2)
                          (replicate (length cmds) (mem⇩1, mem⇩2))"
proof -
  let ?n = "length cmds"
  let ?mems = "replicate ?n (mem⇩1, mem⇩2)" and
      ?mdss = "replicate ?n mds⇩s"
  let ?X = "differing_vars_lists mem⇩1 mem⇩2 ?mems"
  have diff_empty: "∀ i < ?n. ?X i = {}"
    by (metis differing_vars_initially_empty ex_in_conv min_max.inf_idem zip_replicate)

  show ?thesis
    unfolding add_initial_modes_def
  proof
    show "length (zip cmds ?mdss) = length (zip cmds ?mdss) ∧ length (zip cmds ?mdss) = length ?mems"
      by auto
  next
    fix i σ
    let ?mems⇩1i = "fst (?mems ! i)" and ?mems⇩2i = "snd (?mems ! i)"
    assume i: "i < length (zip cmds ?mdss)"
    with coms_secure have "com_sifum_secure (cmds ! i)"
      using coms_secure
      by (metis length_map length_replicate list_all_length map_snd_zip)
    with i have "!! mem⇩1 mem⇩2. mem⇩1 =⇘mds⇩s⇙⇧l mem⇩2 ==>
      (zip cmds (replicate ?n mds⇩s) ! i, mem⇩1) ≈ (zip cmds (replicate ?n mds⇩s) ! i, mem⇩2)"
      using com_sifum_secure_def low_indistinguishable_def
      by auto

    moreover
    from i have "?mems⇩1i = mem⇩1" "?mems⇩2i = mem⇩2"
      by auto
    with low_eq have "?mems⇩1i [\<mapsto> σ] =⇘mds⇩s⇙⇧l ?mems⇩2i [\<mapsto> σ]"
      by (auto simp: subst_def mds⇩s_def low_mds_eq_def low_eq_def, case_tac "σ x", auto)

    ultimately show "(zip cmds ?mdss ! i, ?mems⇩1i [\<mapsto> σ]) ≈ (zip cmds ?mdss ! i, ?mems⇩2i [\<mapsto> σ])"
      by simp
  next
    fix i x
    assume "i < length (zip cmds ?mdss)"
    with diff_empty show "x ∉ ?X i" by auto
  next
    show "(length (zip cmds ?mdss) = 0 ∧ mem⇩1 =⇧l mem⇩2) ∨ (∀ x. ∃ i < length (zip cmds ?mdss). x ∉ ?X i)"
      using diff_empty
      by (metis bot_less bot_nat_def empty_iff length_zip low_eq min_0L)
  qed
qed

theorem sifum_compositionality:
  assumes com_secure: "list_all com_sifum_secure cmds"
  assumes no_assms: "no_assumptions_on_termination cmds"
  assumes sound_modes: "∀ mem. sound_mode_use (add_initial_modes cmds, mem)"
  shows "prog_sifum_secure cmds"
  unfolding prog_sifum_secure_def
  using assms
proof (clarify)
  fix mem⇩1 mem⇩2 :: "'Var => 'Val"
  fix k cms⇩1' mem⇩1'
  let ?n = "length cmds"
  let ?mems = "zip (replicate ?n mem⇩1) (replicate ?n mem⇩2)"
  assume low_eq: "mem⇩1 =⇧l mem⇩2"
  with com_secure have compat:
    "makes_compatible (add_initial_modes cmds, mem⇩1) (add_initial_modes cmds, mem⇩2) ?mems"
    by (metis compatible_refl fst_conv length_replicate map_replicate snd_conv zip_eq_conv)

  also assume eval: "(add_initial_modes cmds, mem⇩1) ->⇘k⇙ (cms⇩1', mem⇩1')"

  ultimately obtain cms⇩2' mem⇩2' mems'
    where p: "map snd cms⇩1' = map snd cms⇩2' ∧
             (add_initial_modes cmds, mem⇩2) ->⇘k⇙ (cms⇩2', mem⇩2') ∧
             makes_compatible (cms⇩1', mem⇩1') (cms⇩2', mem⇩2') mems'"
    using sound_modes makes_compatible_eval_k
    by blast

  thus "∃ cms⇩2' mem⇩2'. (add_initial_modes cmds, mem⇩2) ->⇘k⇙ (cms⇩2', mem⇩2') ∧
                        map snd cms⇩1' = map snd cms⇩2' ∧
                        length cms⇩2' = length cms⇩1' ∧
                        (∀ x. dma x = Low ∧ (∀ i < length cms⇩1'. x ∉ snd (cms⇩1' ! i) AsmNoRead)
          --> mem⇩1' x = mem⇩2' x)"
    using p compat_low_eq
    by (metis length_map)
qed

end

end