Theory Compositionality

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
section ‹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 ⇀ '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 ⇀ 'b) ⇒ ('a ⇒ 'b)" ("_ [↦_]" [900, 0] 1000)
  where
  "f [↦ σ] ≡ subst σ f"

lemma subst_not_in_dom : "⟦ x ∉ dom σ ⟧ ⟹ mem [↦ σ] 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)) [↦ σ]) ≈ (cms⇩2 ! i, (snd (mems ! i)) [↦ σ])) ∧
       (∀ 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)) [↦ σ]) ≈ (cms⇩2 ! i, (snd (mems ! i)) [↦ σ]));
     (⋀ 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 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)
  with * 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 prod.exhaust ‹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 [↦ σ] = mem⇩2 [↦ σ]"
proof (rule ext)
  fix x
  from domσ show "mem⇩1 [↦ σ] x = mem⇩2 [↦ σ] 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 ⇀ '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 [↦ σ] x = ?mems⇩1j x ∧ ?mems⇩2j [↦ σ] x = ?mems⇩2j x"
  by (metis subst_not_in_dom)

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

  hence low_eq: "?mems⇩1j [↦ σ] =⇘?mdss ! j⇙⇧l ?mems⇩2j [↦ σ]" 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 ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ bool" (infixl "≼" 60)
  where "f ≼ g = (∀ x ∈ dom f. f x = g x)"

fun change_respecting ::
  "('Com, 'Var, 'Val) LocalConf ⇒
   ('Com, 'Var, 'Val) LocalConf ⇒
   'Var set ⇒
   (('Var ⇀ 'Val) ⇒
   ('Var ⇀ 'Val)) ⇒ bool"
  where "change_respecting (cms, mem) (cms', mem') X g =
      ((cms, mem) ↝ (cms', mem') ∧
       (∀ σ. dom σ = X ⟶ g σ ≼ σ) ∧
       (∀ σ σ'. dom σ = X ∧ dom σ' = X ⟶ dom (g σ) = dom (g σ')) ∧
       (∀ σ. dom σ = X ⟶ (cms, mem [↦ σ]) ↝ (cms', mem' [↦ 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 ≼ g; X ⊆ dom f ⟧ ⟹ f |` X ≼ g"
  by (auto simp: func_le_def)

definition to_partial :: "('a ⇒ 'b) ⇒ ('a ⇀ 'b)"
  where "to_partial f = (λ x. Some (f x))"

lemma func_le_dom: "f ≼ 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⟩ ↝ ⟨c', mds', mem'⟩"
  assumes unchanged: "∀ v. ⟨c, mds, mem (x := v)⟩ ↝ ⟨c', mds', mem' (x := v)⟩"
  shows "¬ (∀ v. ⟨c, mds, mem (x := v)⟩ ↝ ⟨c', mds', mem'⟩)"
  using assms
  apply (case_tac "mem' x = some_val")
   apply (metis (full_types) prod.inject deterministic different_values fun_upd_same)
  by (metis (full_types) prod.inject deterministic fun_upd_same)

lemma doesnt_read_mutually_exclusive':
  assumes noread: "doesnt_read c x"
  assumes eval: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  assumes overwrite: "∀ v. ⟨c, mds, mem (x := v)⟩ ↝ ⟨c', mds', mem'⟩"
  shows "¬ (∀ v. ⟨c, mds, mem (x := v)⟩ ↝ ⟨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 ⟩ ↝ ⟨ c', mds', mem' ⟩;
     ⋀ f. dom f = X ⟹
           g f ≼ f ∧
           (∀ f'. dom f' = X ⟶ dom (g f) = dom (g f')) ∧
           (⟨ c, mds, mem [↦ f] ⟩ ↝ ⟨ c', mds', mem' [↦ 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 ⟩ ↝ ⟨ c', mds', mem' ⟩"
  assumes noread: "∀ x ∈ X. doesnt_read c x"
  shows "∃ (g :: ('Var ⇀ 'Val) ⇒ ('Var ⇀ '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 = "λ σ. Map.empty"
    have "mem [↦ Map.empty] = mem" "mem' [↦ ?g Map.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. *)
    define g where "g σ =
       (let σ' = σ |` X in
        (if (∀ v. ⟨c, mds, mem [↦ σ'] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X σ'] (x := v)⟩)
         then (λ y :: 'Var.
                    if x = y
                    then σ y
                    else g⇩X σ' y)
         else (λ y. g⇩X σ' y)))"
      for σ :: "'Var ⇀ 'Val"
    have "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ (insert x X) g"
    proof
      show "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩" using insert by auto
    next ― ‹We first show that property (2) is satisfied.›
      fix σ :: "'Var ⇀ 'Val"
      let ?σ⇩X = "σ |` X"
      assume "dom σ = insert x X"
      hence "dom ?σ⇩X = X"
        by (metis dom_restrict inf_absorb2 subset_insertI)
      from insert have "doesnt_read c x" by auto
      moreover
      from IH have eval⇩X: "⟨c, mds, mem [↦ ?σ⇩X]⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩"
        using ‹dom ?σ⇩X = X›
        unfolding change_respecting.simps
        by auto
      ultimately have
        noread⇩x:
        "(∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X] (x := v) ⟩) ∨
        (∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩)"
        unfolding doesnt_read_def by auto
      show "g σ ≼ σ ∧
            (∀ σ'. dom σ' = insert x X ⟶ dom (g σ) = dom (g σ')) ∧
            ⟨c, mds, mem [↦ σ]⟩ ↝ ⟨c', mds', mem' [↦ g σ]⟩"
      proof (rule conjI3)
        from noread⇩x show "g σ ≼ σ"
        proof
          assume nowrite: "∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝
                 ⟨c', mds', mem' [↦ 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 σ ≼ σ"
            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 [↦ ?σ⇩X] (x := v)⟩ ↝
            ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩"
          hence
            "¬ (∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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)

          also from IH have "g⇩X ?σ⇩X ≼ ?σ⇩X"
            by (metis ‹dom (σ |` X) = X› change_respecting.simps)

          ultimately show "g σ ≼ σ"
            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 ⇀ '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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X] (x := v)⟩) ∧
            (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ'⇩X] (x := v)⟩))
           ∨
           ((∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩) ∧
            (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ h |` X] (x := v)⟩ ↝
                             ⟨c', mds', mem' [↦ g⇩X (h |` X)] (x := v)⟩;
                        ∀ v. ⟨c, mds, mem [↦ h' |` X] (x := v)⟩ ↝
                             ⟨c', mds', mem' [↦ g⇩X (h' |` X)]⟩ ⟧
                      ⟹ False"
          proof -
            ― ‹Introduce new names to avoid clashes with functions in the outer scope.›
            fix h h' :: "'Var ⇀ 'Val"
            assume doms: "dom h = insert x X" "dom h' = insert x X"
            assume nowrite: "∀ v. ⟨c, mds, mem [↦ h |` X] (x := v)⟩ ↝
              ⟨c', mds', mem' [↦ g⇩X (h |` X)] (x := v)⟩"
            assume overwrite: "∀ v. ⟨c, mds, mem [↦ h' |` X] (x := v)⟩ ↝
              ⟨c', mds', mem' [↦ 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 [↦ ?h'⇩X]⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?h'⇩X]⟩"
              unfolding change_respecting.simps
              by auto
            with ‹doesnt_read c x› have noread⇩x':
             "(∀ v. ⟨c, mds, mem [↦ ?h'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?h'⇩X] (x := v)⟩) ∨
              (∀ v. ⟨c, mds, mem [↦ ?h'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?h'⇩X]⟩)"
              unfolding doesnt_read_def
              by auto

            from overwrite obtain v where
              "¬ (⟨c, mds, mem [↦ h' |` X] (x := v)⟩ ↝
              ⟨c', mds', mem' [↦ 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 rev_subsetD)

            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⟩ ↝ ⟨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 [↦ ?h⇩X]⟩ ↝ ⟨c', mds', mem⇩v' [↦ g⇩v ?h⇩X]⟩"
                         "⟨c, mds, ?mem⇩v [↦ ?h'⇩X]⟩ ↝ ⟨c', mds', mem⇩v' [↦ 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) [↦ ?h⇩X]⟩ ↝ ⟨c', mds', mem⇩v' [↦ g⇩v ?h⇩X]⟩"
              have "?mem⇩v [↦ ?h⇩X] = mem [↦ ?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' [↦ g⇩v ?h⇩X] = mem' [↦ g⇩X ?h⇩X] (x := v)"
                using deterministic
                by (erule_tac x = v in allE, auto, metis eval⇩v(1))

              hence "mem⇩v' [↦ 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) rev_subsetD)
              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 [↦ ?h'⇩X]⟩ ↝ ⟨c', mds', mem⇩v' [↦ g⇩v ?h'⇩X]⟩"
              moreover
              from overwrite have
                "⟨c, mds, mem [↦ ?h'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?h'⇩X]⟩"
                by auto
              moreover
              have "?mem⇩v [↦ ?h'⇩X] = mem [↦ ?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' [↦ g⇩X ?h'⇩X] = mem⇩v' [↦ 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) subsetD)
              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 [↦ ?σ'⇩X]⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ'⇩X]⟩"
            unfolding change_respecting.simps
            by auto
          with ‹doesnt_read c x› have noread⇩x':
             "(∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ'⇩X] (x := v)⟩)
              ∨
              (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X] (x := v)⟩) ∧
            (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩) ∧
            (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ'⇩X]⟩)"
          hence
            "¬ (∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X] (x := v)⟩)
            ∧
            ¬ (∀ v. ⟨c, mds, mem [↦ ?σ'⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ σ]⟩ ↝ ⟨c', mds', mem' [↦ g σ]⟩"
      proof
        assume nowrite:
          "∀ v. ⟨c, mds, mem[↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X] (x := v)⟩"
          by auto
        moreover
        have "mem [↦ ?σ⇩X] (x := v) = mem [↦ σ]"
          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' [↦ g⇩X ?σ⇩X] (x := v) = mem' [↦ 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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g⇩X ?σ⇩X]⟩"
        hence
          "¬ (∀ v. ⟨c, mds, mem [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ ?σ⇩X] (x := v) = mem [↦ σ]"
          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 [↦ ?σ⇩X] (x := v)⟩ ↝ ⟨c', mds', mem' [↦ g σ]⟩"
          by (metis g_simp)
        ultimately show "⟨c, mds, mem [↦ σ]⟩ ↝ ⟨c', mds', mem' [↦ 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 [↦ τ] [↦ σ] = mem [↦ σ]"
  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) ↝ (cms⇩1', mem⇩1')"
  shows "∃ c⇩2' mem⇩2'. (cms⇩2, mem⇩2) ↝ ⟨ 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) ↝ (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 [↦ f]) ↝ (cms', mem' [↦ g f])"
    unfolding change_respecting.simps
    by metis
  hence eval': "(cms, mem [↦ ?f']) ↝ (cms', mem' [↦ g ?f'])"
    by (metis domf')

  have mem_eq: "mem [↦ ?f'] = mem"
  proof
    fix x
    show "mem [↦ ?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 have mem'_eq: "mem' [↦ 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' [↦ 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 ⇀ ('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"
  ("_ [∥⇩1 _]" [900, 0] 1000)
  where "mem [∥⇩1 A] ≡ apply_adaptation True mem A"

abbreviation apply_adaptation⇩2 ::
  "('Var, 'Val) Mem ⇒ ('Var, 'Val) adaptation ⇒ ('Var, 'Val) Mem"
  ("_ [∥⇩2 _]" [900, 0] 1000)
  where "mem [∥⇩2 A] ≡ apply_adaptation False mem A"

definition restrict_total :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'a ⇀ '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 [∥⇩1 A]⟩ ≈ ⟨c⇩2, mds, mem⇩2 [∥⇩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 [∥⇩1 A] = mem⇩1" and "mem⇩2 [∥⇩2 A] = mem⇩2"
      unfolding apply_adaptation_def
      by auto
    with bisim show ?case
      by auto
  next
    case (insert x X)
    define A' where "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 [∥⇩1 A']⟩ ≈ ⟨c⇩2, mds, mem⇩2 [∥⇩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) case_prodE)

    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 [∥⇩1 A'] (x := v) = mem⇩1 [∥⇩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 [∥⇩2 A'] (x := v') = mem⇩2 [∥⇩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 [∥⇩1 A'] (x := v)⟩ ≈ ⟨c⇩2, mds, mem⇩2 [∥⇩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 [∥⇩1 A'] (x := v)⟩ ≈ ⟨c⇩2, mds, mem⇩2 [∥⇩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) ↝ (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 [↦ σ] = mem⇩1 [↦ σ]"
    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 [↦ σ]) ↝ (cms⇩1' ! k, mem⇩1' [↦ g1 σ])"
    by auto

  moreover
  with b and compat have
    bisim⇩σ: "⋀ σ. dom σ = ?X k ⟹ (cms⇩1 ! k, ?mems⇩1k [↦ σ]) ≈ (cms⇩2 ! k, ?mems⇩2k [↦ σ])"
    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 [↦ σ]) ↝ ⟨ c⇩f', ?mds⇩k', mem⇩f' ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [↦ g1 σ]) ≈ ⟨ c⇩f', ?mds⇩k', mem⇩f' ⟩"
    by (metis mm_equiv_step)

  obtain h :: "'Var ⇀ '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 [↦ h]) ↝ ⟨ c⇩h, ?mds⇩k', mem⇩h ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [↦ g1 h]) ≈ ⟨ c⇩h, ?mds⇩k', mem⇩h ⟩"
    using d
    by metis

  then obtain g2 where e:
    "change_respecting (cms⇩2 ! k, ?mems⇩2k [↦ 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 [↦ h] [↦ σ]) ↝ ⟨ c⇩h, ?mds⇩k', mem⇩h [↦ g2 σ] ⟩"
    unfolding change_respecting.simps
    by auto

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

  from d and f have g: "⋀ σ. dom σ = ?X k ⟹
    (cms⇩2 ! k, ?mems⇩2k [↦ σ]) ↝ ⟨ c⇩h, ?mds⇩k', mem⇩h [↦ g2 σ] ⟩ ∧
    (cms⇩1' ! k, mem⇩1' [↦ g1 σ]) ≈ ⟨ c⇩h, ?mds⇩k', mem⇩h [↦ g2 σ] ⟩"
    using h_prop
    by (metis deterministic)
  let ?σ_mem⇩2 = "to_partial mem⇩2 |` ?X k"
  define mem⇩2' where "mem⇩2' = mem⇩h [↦ g2 ?σ_mem⇩2]"
  define c⇩2' where "c⇩2' = c⇩h"

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

  have "mem⇩2 = ?mems⇩2k [↦ ?σ_mem⇩2]"
  proof (rule ext)
    fix x
    show "mem⇩2 x = ?mems⇩2k [↦ ?σ_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) ↝ ⟨ c⇩2', ?mds⇩k', mem⇩2' ⟩"
    unfolding mem⇩2'_def c⇩2'_def
    by metis

  define cms⇩2' where "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
    define mems'_k
      where "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))" for 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 [↦ h] [↦ ?σ_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 [↦ g2 ?σ_mem⇩2] x = mem⇩2 x"
        by (auto simp: subst_def)

      ultimately have "?mems⇩2k [↦ h] [↦ ?σ_mem⇩2] x = mem⇩h [↦ g2 ?σ_mem⇩2] x"
        by auto
      thus "mem⇩2 x = mem⇩2' x"
        by (metis ‹mem⇩2 = ?mems⇩2k [↦ ?σ_mem⇩2]› domσ_mem⇩2 domh mem⇩2'_def subst_overrides)
    qed

    define mems'_i
      where "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))" for i x

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

    have mems'_simp2: "⟦ i ≠ k; i < length cms⇩1 ⟧ ⟹
      mems' ! i = (fst ∘ mems'_i i, snd ∘ 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 ∘ mems'_i i, snd ∘ 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 ⇀ '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)) [↦ σ]) ≈ (cms⇩2' ! i, (snd (mems' ! i)) [↦ σ])"
      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.›
        define σ'
          where "σ' 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)" for x
        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› 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 [↦ σ] = mem⇩1' [↦ g1 σ']"
        proof (rule ext)
          fix x

          show "?mems⇩1'i [↦ σ] x = mem⇩1' [↦ 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 [↦ σ] x = v"
              using ‹x ∈ ?X' k› domσ
              by (auto simp: subst_def)
            moreover
            from c have le: "g1 σ' ≼ σ'"
              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' [↦ 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 [↦ σ] x = mem⇩1' [↦ g1 σ'] x" ..
          next
            assume "x ∉ ?X' k"

            hence "?mems⇩1'i [↦ σ] 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' [↦ g1 σ'] x = ?mems⇩1'i x"
                unfolding subst_def
                by (metis ‹g1 σ' x = σ' x› option.simps(5))
              thus ?thesis
                by (metis ‹?mems⇩1'i [↦σ] x = ?mems⇩1'i x›)
            next
              assume "x ∉ dom_g1"
              then have "mem⇩1' [↦ 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 [↦σ] x = ?mems⇩1'i x›)
            qed
          qed
        qed
        (* And the same for the second memories: *)
        moreover have "?mems⇩2'i [↦ σ] = mem⇩h [↦ g2 σ']"
        proof (rule ext)
          fix x

          show "?mems⇩2'i [↦ σ] x = mem⇩h [↦ 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 [↦ σ] x = v"
              using ‹x ∈ ?X' k› domσ
              unfolding subst_def
              by (metis option.simps(5))
            moreover
            from e have le: "g2 σ' ≼ σ'"
              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' [↦ 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 [↦ σ] 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' [↦ 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 [↦ 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 [↦σ] x = ?mems⇩2'i x›)
            qed
          qed
        qed

        ultimately show
          "(cms⇩1' ! i, (fst (mems' ! i)) [↦ σ]) ≈ (cms⇩2' ! i, (snd (mems' ! i)) [↦ σ])"
          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"
        define σ'
          where "σ' x = (if x ∈ ?X i
                         then if x ∈ ?X' i
                              then σ x
                              else Some (mem⇩1' x)
                         else None)" for x
        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 [↦ σ] x ≠ ?mems⇩1i [↦ σ'] x ∨
                  ?mems⇩2'i [↦ σ] x ≠ ?mems⇩2i [↦ σ'] 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 [↦ σ] x = ?mems⇩1i [↦ σ'] x ∧ ?mems⇩2'i [↦ σ] x = ?mems⇩2i [↦ σ'] 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 [↦ σ] x ≠ ?mems⇩1i [↦ σ'] x ∨
                      ?mems⇩2'i [↦ σ] x ≠ ?mems⇩2i [↦ σ'] x ⟧ ⟹
          x ∉ snd (cms⇩1 ! i) AsmNoWrite"
        proof
          fix x
          assume mems_neq:
            "?mems⇩1'i [↦ σ] x ≠ ?mems⇩1i [↦ σ'] x ∨ ?mems⇩2'i [↦ σ] x ≠ ?mems⇩2i [↦ σ'] 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 prod.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 prod.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 [↦ σ] x ≠ ?mems⇩1i [↦ σ'] x ∨
                   ?mems⇩2'i [↦ σ] x ≠ ?mems⇩2i [↦ σ'] 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 [↦ σ']) ≈ (cms⇩2 ! i, ?mems⇩2i [↦ σ'])"
          by auto

        let ?Δ = "differing_vars (?mems⇩1i [↦ σ']) (?mems⇩1'i [↦ σ]) ∪
                  differing_vars (?mems⇩2i [↦ σ']) (?mems⇩2'i [↦ σ])"

        have Δ_finite: "finite ?Δ"
          by (metis (no_types) differing_finite finite_UnI)
        ― ‹We first define the adaptation, then prove that it does the right thing.›
        define A where "A x =
                     (if x ∈ ?Δ
                      then if dma x = High
                           then Some (?mems⇩1'i [↦ σ] x, ?mems⇩2'i [↦ σ] 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)" for x
        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 [↦ σ'] [∥⇩1 A] x = ?mems⇩1'i [↦ σ] x ∧
               ?mems⇩2i [↦ σ'] [∥⇩2 A] x = ?mems⇩2'i [↦ σ] x"
        proof -
          fix x
          show "?thesis x"
            (is "?A ∧ ?Eq⇩1 ∧ ?Eq⇩2")
          proof (cases "x ∈ ?Δ")
            assume "x ∈ ?Δ"
            hence diff:
              "?mems⇩1'i [↦ σ] x ≠ ?mems⇩1i [↦ σ'] x ∨ ?mems⇩2'i [↦ σ] x ≠ ?mems⇩2i [↦ σ'] 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 [↦ σ] x, ?mems⇩2'i [↦ σ] 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 [↦ σ] x = v ∧ ?mems⇩2'i [↦ σ] 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 [↦ σ] x = ?mems⇩1'i x ∧ ?mems⇩2'i [↦ σ] 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 [↦ σ'] [∥⇩1 A] x = ?mems⇩1'i [↦ σ] x ∧
                                 ?mems⇩2i [↦ σ'] [∥⇩2 A] x = ?mems⇩2'i [↦ σ] x"
              using ‹A x = None›
              unfolding differing_vars_def apply_adaptation_def
              by auto

            ultimately show ?thesis
              by auto
          qed
        qed
        hence "?mems⇩1i [↦ σ'] [∥⇩1 A] = ?mems⇩1'i [↦ σ] ∧
               ?mems⇩2i [↦ σ'] [∥⇩2 A] = ?mems⇩2'i [↦ σ]"
          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 [↦ σ'] [∥⇩1 A]) ≈ (cms⇩2 ! i, ?mems⇩2i [↦ σ'] [∥⇩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 ⇀ 'Val" where "dom σ = ?X j"
      by (metis dom_restrict_total)

    with compat and j_prop have "(cms⇩1 ! j, ?mems⇩1j [↦ σ]) ≈ (cms⇩2 ! j, ?mems⇩2j [↦ σ])"
      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 [↦ σ] =⇘snd (cms⇩1 ! j)⇙⇧l ?mems⇩2j [↦ σ]"
      using modes_eq j_prop
      by (metis prod.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⟩ ↝ ⟨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⟩ ↝ ⟨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 (opaque_lifting, 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 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) ↝ (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 (opaque_lifting, 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 prod.collapse)
      then have "loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)"
        by (metis loc_reach_mem_diff_eq prod.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 prod.inject 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.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 [↦ σ] =⇘mds⇩s⇙⇧l ?mems⇩2i [↦ σ]"
      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 [↦ σ]) ≈ (zip cmds ?mdss ! i, ?mems⇩2i [↦ σ])"
      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