Theory Compositionality

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
section ‹Compositionality Proof for SIFUM-Security Property›

theory Compositionality
imports Security
begin

context sifum_security_init
begin

(* Set of variables that differs between two memory states: *)
definition 
  differing_vars :: "('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ 'Var set"
where
  "differing_vars mem1 mem2 ≡ {x. mem1 x ≠ mem2 x}"

definition 
  differing_vars_lists :: "('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ 
                           ((_, _) Mem × (_, _) Mem) list ⇒ nat ⇒ 'Var set"
where
  "differing_vars_lists mem1 mem2 mems i ≡
     (differing_vars mem1 (fst (mems ! i)) ∪ differing_vars mem2 (snd (mems ! i)))"

lemma differing_finite: "finite (differing_vars mem1 mem2)"
  by (metis UNIV_def Un_UNIV_left finite_Un finite_memory)

lemma differing_lists_finite: "finite (differing_vars_lists mem1 mem2 mems i)"
  by (simp add: differing_finite differing_vars_lists_def)


fun makes_compatible ::
  "('Com, 'Var, 'Val) GlobalConf ⇒
   ('Com, 'Var, 'Val) GlobalConf ⇒
   ((_, _) Mem × (_, _) Mem) list ⇒
  bool"
where
  "makes_compatible (cms1, mem1) (cms2, mem2) mems =
  (length cms1 = length cms2 ∧ length cms1 = length mems ∧
   (∀ i. i < length cms1 ⟶
       (∀ σ. dom σ = differing_vars_lists mem1 mem2 mems i ⟶
         (cms1 ! i, (fst (mems ! i)) [↦ σ]) ≈ (cms2 ! i, (snd (mems ! i)) [↦ σ])) ∧
       (∀ x. (mem1 x = mem2 x ∨ dma mem1 x = High ∨ x ∈ 𝒞) ⟶
             x ∉ differing_vars_lists mem1 mem2 mems i)) ∧
    ((length cms1 = 0 ∧ mem1 =l mem2) ∨ (∀ x. ∃ i. i < length cms1 ∧
                                          x ∉ differing_vars_lists mem1 mem2 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 cms1 = length cms2 ∧ length cms1 = length mems;
     (⋀ i σ. ⟦ i < length cms1; dom σ = differing_vars_lists mem1 mem2 mems i ⟧ ⟹
          (cms1 ! i, (fst (mems ! i)) [↦ σ]) ≈ (cms2 ! i, (snd (mems ! i)) [↦ σ]));
     (⋀ i x. ⟦ i < length cms1; mem1 x = mem2 x ∨ dma mem1 x = High ∨ x ∈ 𝒞 ⟧ ⟹ 
          x ∉ differing_vars_lists mem1 mem2 mems i);
     (length cms1 = 0 ∧ mem1 =l mem2) ∨
     (∀ x. ∃ i. i < length cms1 ∧ x ∉ differing_vars_lists mem1 mem2 mems i) ⟧ ⟹
  makes_compatible (cms1, mem1) (cms2, mem2) mems"
  by auto

(* First, some auxiliary lemmas about makes_compatible: *)
lemma compat_low:
  "⟦ makes_compatible (cms1, mem1) (cms2, mem2) mems;
     i < length cms1;
     x ∈ differing_vars_lists mem1 mem2 mems i ⟧ ⟹ dma mem1 x = Low"
proof -
  assume "i < length cms1" and *: "x ∈ differing_vars_lists mem1 mem2 mems i" and
    "makes_compatible (cms1, mem1) (cms2, mem2) mems"
  then have
    "(mem1 x = mem2 x ∨ dma mem1 x = High ∨ x ∈ 𝒞) ⟶ x ∉ differing_vars_lists mem1 mem2 mems i"
    by (simp add: Let_def, blast)
  with * show "dma mem1 x = Low"
    by (cases "dma mem1 x", blast)
qed

lemma compat_different:
  "⟦ makes_compatible (cms1, mem1) (cms2, mem2) mems;
     i < length cms1;
     x ∈ differing_vars_lists mem1 mem2 mems i ⟧ ⟹ mem1 x ≠ mem2 x ∧ dma mem1 x = Low ∧ x ∉ 𝒞"
  by (cases "dma mem1 x", auto)

lemma sound_modes_no_read :
  "⟦ sound_mode_use (cms, mem); x ∈ (map snd cms ! i) GuarNoReadOrWrite; i < length cms ⟧ ⟹
  doesnt_read_or_modify (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) GuarNoReadOrWrite"
  ultimately show "doesnt_read_or_modify (fst (cms !i)) x"
    apply (simp add: locally_sound_mode_use_def)
    using ‹i < length cms› ‹locally_sound_mode_use (cms ! i, mem)› locally_sound_respects_guarantees respects_own_guarantees_def by auto
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:
  "⟦ mem1 x = fst (mems ! i) x;
  mem2 x = snd (mems ! i) x ⟧ ⟹ x ∉ differing_vars_lists mem1 mem2 mems i"
  by (auto simp: differing_vars_lists_def differing_vars_def)

lemma differing_vars_elim [elim]:
  "x ∈ differing_vars_lists mem1 mem2 mems i ⟹
  (fst (mems ! i) x ≠ mem1 x) ∨ (snd (mems ! i) x ≠ mem2 x)"
  by (auto simp: differing_vars_lists_def differing_vars_def)

lemma makes_compatible_dma_eq:
  assumes compat: "makes_compatible (cms1, mem1) (cms2, mem2) mems"
  assumes ile: "i < length cms1"
  assumes domσ: "dom σ = differing_vars_lists mem1 mem2 mems i"
  shows "dma ((fst (mems ! i)) [↦ σ]) = dma mem1"
proof(rule dma_𝒞, clarify)
  fix x
  assume "x ∈ 𝒞"
  with compat ile have notin_diff: "x ∉ differing_vars_lists mem1 mem2 mems i"
    by simp
  hence "x ∉ dom σ"
    by(metis domσ)
  hence "(fst (mems ! i) [↦ σ]) x = (fst (mems ! i)) x"
    by(metis subst_not_in_dom)
  moreover have "(fst (mems ! i)) x = mem1 x"
    using notin_diff differing_vars_neg by metis
  ultimately show "(fst (mems ! i) [↦ σ]) x = mem1 x" by simp
qed

lemma compat_different_vars:
  "⟦ fst (mems ! i) x = snd (mems ! i) x;
     x ∉ differing_vars_lists mem1 mem2 mems i ⟧ ⟹
    mem1 x = mem2 x"
proof -
  assume "x ∉ differing_vars_lists mem1 mem2 mems i"
  hence "fst (mems ! i) x = mem1 x ∧ snd (mems ! i) x = mem2 x"
    by (simp add: differing_vars_lists_def differing_vars_def)
  moreover assume "fst (mems ! i) x = snd (mems ! i) x"
  ultimately show "mem1 x = mem2 x" by auto
qed

lemma differing_vars_subst [rule_format]:
  assumes domσ: "dom σ ⊇ differing_vars mem1 mem2"
  shows "mem1 [↦ σ] = mem2 [↦ σ]"
proof (rule ext)
  fix x
  from domσ show "mem1 [↦ σ] x = mem2 [↦ σ] x"
    unfolding subst_def differing_vars_def
    by (cases "σ x", auto)
qed

lemma mm_equiv_low_eq:
  "⟦ ⟨ c1, mds, mem1 ⟩ ≈ ⟨ c2, mds, mem2 ⟩ ⟧ ⟹ mem1 =⇘mds⇙l mem2"
  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)"
  apply (simp add: globally_sound_mode_use_def reachable_mode_states_def)
  using meval_sched.simps(1) by blast

(* 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 (cms1, mem1)"
                       "sound_mode_use (cms2, mem2)"
  assumes compat: "makes_compatible (cms1, mem1) (cms2, mem2) mems"
  assumes modes_eq: "map snd cms1 = map snd cms2"
  assumes ile: "i < length cms1"
  assumes x: "x ∈ differing_vars_lists mem1 mem2 mems i"
  shows "doesnt_read_or_modify (fst (cms1 ! i)) x ∧ doesnt_read_or_modify (fst (cms2 ! i)) x"
proof -
  from compat have len: "length cms1 = length cms2"
    by simp

  let ?Xi = "differing_vars_lists mem1 mem2 mems i"

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

  from compat ile x have b: "mem1 x ≠ mem2 x"
    by (metis compat_different)

  from compat ile x have not_in_𝒞: "x ∉ 𝒞"
    by (metis compat_different)

  with a and compat ile x obtain j where
    jprop: "j < length cms1 ∧ x ∉ differing_vars_lists mem1 mem2 mems j"
    by fastforce

  let ?Xj = "differing_vars_lists mem1 mem2 mems j"
  obtain σ :: "'Var ⇀ 'Val" where domσ: "dom σ = ?Xj"
  proof
    let ?σ = "λ x. if (x ∈ ?Xj) then Some some_val else None"
    show "dom ?σ = ?Xj" unfolding dom_def by auto
  qed
  let ?mdss = "map snd cms1" and
      ?mems1j = "fst (mems ! j)" and
      ?mems2j = "snd (mems ! j)"

  from jprop domσ have subst_eq:
  "?mems1j [↦ σ] x = ?mems1j x ∧ ?mems2j [↦ σ] x = ?mems2j x"
  by (metis subst_not_in_dom)

  from compat jprop domσ
  have "(cms1 ! j, ?mems1j [↦ σ]) ≈ (cms2 ! j, ?mems2j [↦ σ])"
    by (auto simp: Let_def)

  hence low_eq: "?mems1j [↦ σ] =⇘?mdss ! j⇙l ?mems2j [↦ σ]" 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) AsmNoReadOrWrite"
  proof -
    { assume "x ∉ (?mdss ! j) AsmNoReadOrWrite"
      then have mems_eq: "?mems1j x = ?mems2j x"
        using ‹dma mem1 x = Low› low_eq subst_eq
        makes_compatible_dma_eq[OF compat jprop[THEN conjunct1] domσ]
        low_mds_eq_def 
        by (metis (poly_guards_query))

      hence "mem1 x = mem2 x"
        by (metis compat_different_vars jprop)

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

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

  thus "doesnt_read_or_modify (fst (cms1 ! i)) x ∧ doesnt_read_or_modify (fst (cms2 ! i)) x" using sound_modes ile
    by (metis len modes_eq sound_modes_no_read)
qed

definition
  vars_and_𝒞 :: "'Var set ⇒ 'Var set"
where
  "vars_and_𝒞 X ≡ X ∪ vars_𝒞 X"

(* Toby: most of the complexity drops out as doesnt_read_or_modify now implies doesnt_modify *)
fun change_respecting ::
  "('Com, 'Var, 'Val) LocalConf ⇒
   ('Com, 'Var, 'Val) LocalConf ⇒
   'Var set ⇒ bool"
  where "change_respecting (cms, mem) (cms', mem') X =
      ((cms, mem) ↝ (cms', mem') ∧
       (∀ σ. dom σ = vars_and_𝒞 X ⟶ (cms, mem [↦ σ]) ↝ (cms', mem' [↦ σ])))"

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

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

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

lemma change_respecting_doesnt_modify':
  assumes eval: "(cms, mem) ↝ (cms', mem')"
  assumes cr: "∀ f. dom f = Y ⟶ (cms, mem [↦ f]) ↝ (cms', mem' [↦ f])"
  assumes x_in_dom: "x ∈ Y"
  shows "mem x = mem' x"
proof -
  let ?f' = "to_partial mem |` Y"
  have domf': "dom ?f' = Y"
    by (metis dom_restrict_total)

  from this cr have eval': "(cms, mem [↦ ?f']) ↝ (cms', mem' [↦ ?f'])"
    by (metis)

  have mem_eq: "mem [↦ ?f'] = mem"
  proof
    fix x
    show "mem [↦ ?f'] x = mem x"
      unfolding subst_def
      apply (cases "x ∈ Y")
       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' [↦ ?f'] = mem'"
    using eval eval' deterministic
    by (metis Pair_inject)

  moreover
  have x_in_dom': "x ∈ dom ?f'"
    by (metis x_in_dom dom_restrict_total)
  hence "?f' x = Some (mem x)"
    by (metis restrict_in to_partial_def x_in_dom)
  hence "mem' [↦ ?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

lemma change_respecting_subset':
  assumes step: "(cms, mem) ↝ (cms', mem')"
  assumes noread: "(∀ σ. dom σ = X ⟶ (cms, mem [↦ σ]) ↝ (cms', mem' [↦ σ]))"
  assumes dom_subset: "dom σ ⊆ X"
  shows "(cms, mem [↦ σ]) ↝ (cms', mem' [↦ σ])"
proof -
  define σX where "σX x = (if x ∈ X then if x ∈ dom σ then σ x else Some (mem x) else None)" for x
  have "dom σX = X" using dom_subset by(auto simp: σX_def)

  have "mem [↦ σ] = mem [↦ σX]"
    apply(rule ext)
    using dom_subset apply(auto simp: subst_def σX_def split: option.splits)
    done

  moreover have "mem' [↦ σ] = mem' [↦ σX]"
    apply(rule ext)
    using dom_subset apply(auto simp: subst_def σX_def split: option.splits simp: change_respecting_doesnt_modify'[OF step noread])
    done

  moreover from noread ‹dom σX = X› have "(cms, mem [↦ σX]) ↝ (cms', mem' [↦ σX])" by metis
  ultimately show ?thesis by simp
qed
 
lemma change_respecting_subst:
  "change_respecting (cms, mem) (cms', mem') X ⟹
       (∀ σ. dom σ = X ⟶ (cms, mem [↦ σ]) ↝ (cms', mem' [↦ σ]))"
  unfolding change_respecting.simps vars_and_𝒞_def
  using change_respecting_subset' by blast
 
lemma change_respecting_intro [iff]:
  "⟦ ⟨ c, mds, mem ⟩ ↝ ⟨ c', mds', mem' ⟩;
     ⋀ f. dom f = vars_and_𝒞 X ⟹
           (⟨ c, mds, mem [↦ f] ⟩ ↝ ⟨ c', mds', mem' [↦ f] ⟩) ⟧
  ⟹ change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X"
  unfolding change_respecting.simps
  by blast

lemma vars_𝒞_mono:
  "X ⊆ Y ⟹ vars_𝒞 X ⊆ vars_𝒞 Y"
  by(auto simp: vars_𝒞_def)

lemma vars_𝒞_Un:
  "vars_𝒞 (X ∪ Y) = (vars_𝒞 X ∪ vars_𝒞 Y)"
  by(simp add: vars_𝒞_def)

lemma vars_𝒞_insert:
  "vars_𝒞 (insert x Y) = (vars_𝒞 {x}) ∪ (vars_𝒞 Y)"
  apply(subst insert_is_Un)
  apply(rule vars_𝒞_Un)
  done

lemma vars_𝒞_empty[simp]:
  "vars_𝒞 {} = {}"
  by(simp add: vars_𝒞_def)

lemma 𝒞_vars_of_𝒞_vars_empty:
  "x ∈ 𝒞_vars y ⟹ 𝒞_vars x = {}"
  apply(drule subsetD[OF 𝒞_vars_subset_𝒞])
  apply(erule 𝒞_vars_𝒞)
  done

lemma vars_and_𝒞_mono:
  "X ⊆ X' ⟹ vars_and_𝒞 X ⊆ vars_and_𝒞 X'"
  apply(unfold vars_and_𝒞_def)
  apply(metis Un_mono vars_𝒞_mono)
  done

lemma 𝒞_vars_finite[simp]:
  "finite (𝒞_vars x)"
  apply(rule finite_subset[OF _ finite_memory])
  by blast

lemma finite_dom:
  "finite (dom (σ::'Var ⇒ 'Val option))"
  by(blast intro: finite_subset[OF _ finite_memory])

lemma doesnt_read_or_modify_subst: 
  assumes noread: "doesnt_read_or_modify c x"
  assumes step: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  assumes subset: "X ⊆ {x} ∪ 𝒞_vars x"
  shows "⋀ σ. dom σ = X ⟹ ⟨c, mds, mem[↦ σ]⟩ ↝ ⟨c', mds', mem'[↦ σ]⟩"  
proof -
  have "finite X"
    using subset apply(rule finite_subset)
    by simp
  show "⋀ σ. dom σ = X ⟹ ⟨c, mds, mem[↦ σ]⟩ ↝ ⟨c', mds', mem'[↦ σ]⟩"
    using ‹finite X› subset 
  proof(induct "X" rule: finite_subset_induct[where A="{x} ∪ 𝒞_vars x"])
    case empty
    thus "⟨c, mds, subst σ mem⟩ ↝ ⟨c', mds', subst σ mem'⟩"
      using step by(simp add: subst_def)
  next
    case (insert a X)
    show "⟨c, mds, subst σ mem⟩ ↝ ⟨c', mds', subst σ mem'⟩"
    proof -
      let ?σX = "(σ |` X)"
      have IHX: "⟨c, mds, subst ?σX mem⟩ ↝ ⟨c', mds', subst ?σX mem'⟩"
        apply(rule insert(4))
        using insert by (metis dom_restrict inf.absorb2 subset_insertI)
      from insert obtain v where σa: "σ a = Some v" by auto
      have r: "⋀mem. (subst ?σX mem)(a := v) = subst σ mem"
        apply(rule ext, rename_tac y)
        apply(simp, safe)
         apply(simp add: subst_def σa)
        using ‹a ∉ X› insert apply(auto simp: subst_def split: option.splits simp: restrict_map_def)
        done
      have "⟨c, mds, (subst ?σX mem)(a := v)⟩ ↝ ⟨c', mds', (subst ?σX mem')(a := v)⟩"
        using noread ‹a ∈ {x} ∪ 𝒞_vars x› IHX
        unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_def by metis
      thus ?thesis by(simp add: r)
    qed
  qed
qed

lemma subst_restrict_twice:
  "dom σ = A ∪ B ⟹
   mem [↦ (σ |` A)] [↦ (σ |` B)] = mem [↦ σ]"
  by(fastforce simp: subst_def split: option.splits intro!: ext simp: restrict_map_def)

(* Toby: this proof is now far simpler because change_respecting is *)
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_or_modify c x"
  shows "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X"
proof -
  let ?lc = "⟨c, mds, mem⟩" and ?lc' = "⟨c', mds', mem'⟩"
  from fin eval noread show "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X"
  proof (induct "X" arbitrary: mem mem' rule: finite_induct)
    case empty
    have "mem [↦ Map.empty] = mem" "mem' [↦ Map.empty] = mem'"
      unfolding subst_def
      by auto
    hence "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ {}"
      using empty
      unfolding change_respecting.simps subst_def vars_𝒞_def vars_and_𝒞_def
      by auto
    thus ?case by blast
  next
    case (insert x X)
    then have IH: "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ X"
      by (metis (poly_guards_query) insertCI insert_disjoint(1))
    show "change_respecting ⟨c, mds, mem⟩ ⟨c', mds', mem'⟩ (insert x X)"
    proof
      show "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩" using insert by auto
    next
      fix σ :: "'Var ⇀ 'Val"
      let ?σX = "σ |` vars_and_𝒞 X"
      let ?σx = "σ |` ({x} ∪ 𝒞_vars x)"
      assume domσ: "dom σ = vars_and_𝒞 (insert x X)"
      hence "dom ?σX = vars_and_𝒞 X"
        by (metis dom_restrict inf_absorb2 subset_insertI vars_and_𝒞_mono)
      from domσ have domσx: "dom ?σx = {x} ∪ 𝒞_vars x"
        by(simp add: domσ vars_and_𝒞_def vars_𝒞_def, blast)
      have "dom σ = vars_and_𝒞 X ∪ ({x} ∪ 𝒞_vars x)"
        by(simp add: domσ vars_and_𝒞_def vars_𝒞_def, blast)
      hence substσ: "⋀ mem. mem [↦ ?σX] [↦ ?σx] = mem [↦ σ]"
        by(rule subst_restrict_twice)
      from insert have "doesnt_read_or_modify c x" by auto
      moreover from IH have evalX: "⟨c, mds, mem [↦ ?σX]⟩ ↝ ⟨c', mds', mem' [↦ ?σX]⟩"
        using ‹dom ?σX = vars_and_𝒞 X›
        unfolding change_respecting.simps
        by auto
      ultimately have "⟨c, mds, mem [↦ ?σX] [↦ ?σx]⟩ ↝ ⟨c', mds', mem' [↦ ?σX] [↦ ?σx]⟩"
        using subset_refl domσx doesnt_read_or_modify_subst by metis
      thus "⟨c, mds, mem [↦ σ]⟩ ↝ ⟨c', mds', mem' [↦ σ]⟩"
        using substσ by metis 
    qed
  qed
qed


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: "(cms1, mem1) ≈ (cms2, mem2)"
  assumes modes_eq: "snd cms1 = snd cms2"
  assumes step: "(cms1, mem1) ↝ (cms1', mem1')"
  shows "∃ c2' mem2'. (cms2, mem2) ↝ ⟨ c2', snd cms1', mem2' ⟩ ∧
  (cms1', mem1') ≈ ⟨ c2', snd cms1', mem2' ⟩"
  using assms mm_equiv_strong_low_bisim
  unfolding strong_low_bisim_mm_def
  apply auto
  apply (erule_tac x = "fst cms1" in allE)
  apply (erule_tac x = "snd cms1" in allE)
  by (metis surjective_pairing)

lemma change_respecting_doesnt_modify:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X"
  assumes eval: "(cms, mem) ↝ (cms', mem')"
  assumes x_in_dom: "x ∈ X ∪ vars_𝒞 X"
  shows "mem x = mem' x"
  using change_respecting_doesnt_modify'[where Y="X ∪ vars_𝒞 X", OF eval] cr     
        change_respecting.simps vars_and_𝒞_def x_in_dom 
  by metis

lemma change_respecting_doesnt_modify_dma:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X"
  assumes eval: "(cms, mem) ↝ (cms', mem')"
  assumes x_in_dom: "x ∈ X"
  shows "dma mem x = dma mem' x"
proof - 
  have "⋀y. y ∈ 𝒞_vars x ⟹ mem y = mem' y"
    proof -
    fix y
    assume "y ∈ 𝒞_vars x"
    hence "y ∈ vars_𝒞 X"
      using x_in_dom by(auto simp: vars_𝒞_def)
    thus "mem y = mem' y"
      using cr eval change_respecting_doesnt_modify by blast
    qed
  thus ?thesis by(metis dma_𝒞_vars)
qed

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

lemma adaptation_finite:
  "finite (dom (A::('Var,'Val) adaptation))"
  apply(rule finite_subset[OF _ finite_memory])
  by blast

definition 
  globally_consistent  :: "('Var, 'Val) adaptation ⇒ 'Var Mds ⇒ ('Var,'Val) Mem ⇒ ('Var,'Val) Mem ⇒ bool"
where "globally_consistent A mds mem1 mem2 ≡ 
  (∀x.  case A x of Some (v,v') ⇒ (mem1 x ≠ v ∨ mem2 x ≠ v') ⟶ ¬ var_asm_not_written mds x | _ ⇒ True) ∧
        (∀x. dma mem1 [∥1 A] x ≠ dma mem1 x ⟶ ¬ var_asm_not_written mds x) ∧
          (∀x. dma (mem1 [∥1 A]) x = Low ∧ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞) ⟶ (mem1 [∥1 A]) x = (mem2 [∥2 A]) x)"

lemma globally_consistent_adapt_bisim:
  assumes bisim: "⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩"
  assumes globally_consistent: "globally_consistent A mds mem1 mem2"
  shows "⟨c1, mds, mem1 [∥1 A]⟩ ≈ ⟨c2, mds, mem2 [∥2 A]⟩"
  apply(rule mm_equiv_glob_consistent[simplified closed_glob_consistent_def, rule_format])
   apply(rule bisim)
  apply(fold globally_consistent_def)
  by(rule globally_consistent)

lemma mm_equiv_𝒞_eq: 
  "(a,b) ≈ (a',b') ⟹ snd a = snd a' ⟹
    ∀x∈𝒞. b x = b' x"
  apply(case_tac a, case_tac a')
  using mm_equiv_strong_low_bisim[simplified strong_low_bisim_mm_def, rule_format]
  by(auto simp: low_mds_eq_def 𝒞_Low)

lemma apply_adaptation_not_in_dom: 
  "x ∉ dom A ⟹ apply_adaptation b blah A x = blah x"
  apply(simp add: apply_adaptation_def domIff split: option.splits)
  done

(* 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 (cms1, mem1)"
                      "sound_mode_use (cms2, mem2)"
  assumes compat: "makes_compatible (cms1, mem1) (cms2, mem2) mems"
  assumes modes_eq: "map snd cms1 = map snd cms2"
  assumes eval: "(cms1, mem1) ↝⇘k⇙ (cms1', mem1')"
  obtains cms2' mem2' mems' where
      "map snd cms1' = map snd cms2' ∧
       (cms2, mem2) ↝⇘k⇙ (cms2', mem2') ∧
       makes_compatible (cms1', mem1') (cms2', mem2') mems'"
proof -
  let ?X = "λ i. differing_vars_lists mem1 mem2 mems i"
  from sound_modes compat modes_eq have
    a: "∀ i < length cms1. ∀ x ∈ (?X i). doesnt_read_or_modify (fst (cms1 ! i)) x ∧
                                          doesnt_read_or_modify (fst (cms2 ! i)) x"
    by (metis compatible_different_no_read)
  from eval have
    b: "k < length cms1 ∧ (cms1 ! k, mem1) ↝ (cms1' ! k, mem1') ∧
        cms1' = cms1 [k := cms1' ! k]"
    by (metis meval_elim nth_list_update_eq)

  from modes_eq have equal_size: "length cms1 = length cms2"
    by (metis length_map)

  let ?mdsk = "snd (cms1 ! k)" and
      ?mdsk' = "snd (cms1' ! k)" and
      ?mems1k = "fst (mems ! k)" and
      ?mems2k = "snd (mems ! k)" and
      ?n = "length cms1"

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

  (* Obtaining cms' and mem2' is not in a proof block, since we
     need some of the following statements later: *)
  then have
    c: "change_respecting (cms1 ! k, mem1) (cms1' ! k, mem1') (?X k)"
    using noread_exists_change_respecting b a
    by (metis surjective_pairing)

  from compat have "⋀ σ. dom σ = ?X k ⟹ ?mems1k [↦ σ] = mem1 [↦ σ]"
    using differing_vars_subst differing_vars_lists_def
    by (metis Un_upper1 Un_subset_iff)

  hence
    evalσ: "⋀ σ. dom σ = ?X k ⟹ (cms1 ! k, ?mems1k [↦ σ]) ↝ (cms1' ! k, mem1' [↦ σ])"
      by(metis change_respecting_subst[rule_format, where X="?X k"] c)

  moreover
  with b and compat have
    bisimσ: "⋀ σ. dom σ = ?X k ⟹ (cms1 ! k, ?mems1k [↦ σ]) ≈ (cms2 ! k, ?mems2k [↦ σ])"
    by auto

  moreover have "snd (cms1 ! k) = snd (cms2 ! k)"
    by (metis b equal_size modes_eq nth_map)
    
  ultimately have d: "⋀ σ. dom σ = ?X k ⟹ ∃ cf' memf'.
    (cms2 ! k, ?mems2k [↦ σ]) ↝ ⟨ cf', ?mdsk', memf' ⟩ ∧
    (cms1' ! k, mem1' [↦ σ]) ≈ ⟨ cf', ?mdsk', memf' ⟩"
    by (metis mm_equiv_step)

  obtain h :: "'Var ⇀ 'Val" where domh: "dom h = ?X k"
    by (metis dom_restrict_total)

  then obtain ch memh where h_prop:
    "(cms2 ! k, ?mems2k [↦ h]) ↝ ⟨ ch, ?mdsk', memh ⟩ ∧
    (cms1' ! k, mem1' [↦ h]) ≈ ⟨ ch, ?mdsk', memh ⟩"
    using d
    by metis

  then have
    "change_respecting (cms2 ! k, ?mems2k [↦ h]) ⟨ ch, ?mdsk', memh ⟩ (?X k)"
    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 ⟶
      (cms2 ! k, ?mems2k [↦ h] [↦ σ]) ↝ ⟨ ch, ?mdsk', memh [↦ σ] ⟩"
    by (metis change_respecting_subst)

  with domh have f:
    "∀ σ. dom σ = ?X k ⟶
      (cms2 ! k, ?mems2k [↦ σ]) ↝ ⟨ ch, ?mdsk', memh [↦ σ] ⟩"
    by (auto simp: subst_overrides)

  from d and f have g: "⋀ σ. dom σ = ?X k ⟹
    (cms2 ! k, ?mems2k [↦ σ]) ↝ ⟨ ch, ?mdsk', memh [↦ σ] ⟩ ∧
    (cms1' ! k, mem1' [↦ σ]) ≈ ⟨ ch, ?mdsk', memh [↦ σ] ⟩"
    using h_prop
    by (metis deterministic)
  let ?σ_mem2 = "to_partial mem2 |` ?X k"
  define mem2' where "mem2' = memh [↦ ?σ_mem2]"
  define c2' where "c2' = ch"

  have domσ_mem2: "dom ?σ_mem2 = ?X k"
    by (metis dom_restrict_total)

  have "mem2 = ?mems2k [↦ ?σ_mem2]"
  proof (rule ext)
    fix x
    show "mem2 x = ?mems2k [↦ ?σ_mem2] x"
      using domσ_mem2
      unfolding to_partial_def subst_def
      apply (cases "x ∈ ?X k")
      apply auto
      by (metis differing_vars_neg)
  qed

  with f domσ_mem2 have i: "(cms2 ! k, mem2) ↝ ⟨ c2', ?mdsk', mem2' ⟩"
    unfolding mem2'_def c2'_def
    by metis

  define cms2' where "cms2' = cms2 [k := (c2', ?mdsk')]"

  with i b equal_size have "(cms2, mem2) ↝⇘k⇙ (cms2', mem2')"
    by (metis meval_intro)

  moreover
  from equal_size have new_length: "length cms1' = length cms2'"
    unfolding cms2'_def
    by (metis eval length_list_update meval_elim)

  with modes_eq have "map snd cms1' = map snd cms2'"
    unfolding cms2'_def
    by (metis b map_update snd_conv)

  moreover

  ― ‹This is the complicated part of the proof.›
  obtain mems' where "makes_compatible (cms1', mem1') (cms2', mem2') mems'"
  proof
    ― ‹This is used in two of the following cases, so we prove it beforehand:›
    have x_unchanged: "⋀ x. ⟦ x ∈ ?X k ⟧ ⟹
      mem1 x = mem1' x ∧ mem2 x = mem2' x ∧ dma mem1 x = dma mem1' x"
    proof(intro conjI)
      fix x
      assume "x ∈ ?X k"
      thus "mem1 x = mem1' x"
        using a b c change_respecting_doesnt_modify domh 
        by (metis (erased, opaque_lifting) Un_upper1 contra_subsetD)
    next
      fix x
      assume "x ∈ ?X k"

      hence eq_mem2: "?σ_mem2 x = Some (mem2 x)"
        by (metis restrict_in to_partial_def)
      hence "?mems2k [↦ h] [↦ ?σ_mem2] x = mem2 x"
        by (auto simp: subst_def)

      moreover have "memh [↦ ?σ_mem2] x = mem2 x"
        by (auto simp: subst_def ‹x ∈ ?X k› eq_mem2)

      ultimately have "?mems2k [↦ h] [↦ ?σ_mem2] x = memh [↦ ?σ_mem2] x"
        by auto
      thus "mem2 x = mem2' x"
        by (metis ‹mem2 = ?mems2k [↦ ?σ_mem2]› domσ_mem2 domh mem2'_def subst_overrides)
    next
      fix x
      assume "x ∈ ?X k"
      thus "dma mem1 x = dma mem1' x"
        using a b c change_respecting_doesnt_modify_dma domh 
        by (metis (erased, opaque_lifting))      
    qed

    define mems'_k where "mems'_k x =
      (if x ∉ ?X k
       then (mem1' x, mem2' x)
       else (?mems1k x, ?mems2k x))" for x

    (* FIXME: see if we can reduce the number of cases *)
    define mems'_i where "mems'_i i x =
      (if ((mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x) ∧
          (mem1' x = mem2' x ∨ dma mem1' x = High))
         then (mem1' x, mem2' x)
         else if ((mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x) ∧
                  (mem1' x ≠ mem2' x ∧ dma mem1' x = Low))
              then (some_val, some_val)
              else if dma mem1 x = High ∧ dma mem1' x = Low then (mem1 x, mem1 x)
              else if dma mem1' x = dma mem1 x then (fst (mems ! i) x, snd (mems ! i) x)
              else (mem1' x, mem2' 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 cms1]"
    from b have mems'_k_simp: "mems' ! k = (fst ∘ mems'_k, snd ∘ mems'_k)"
      unfolding mems'_def
      by auto

    have mems'_simp2: "⋀i. ⟦ i ≠ k; i < length cms1 ⟧ ⟹
      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 = mem1' x ∧ snd (mems' ! k) x = mem2' x"
      unfolding mems'_k_simp mems'_k_def
      by auto
    have mems'_k_2 [simp]: "⋀ x. ⟦ x ∈ ?X k ⟧ ⟹
      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;
           fst (mems' ! k) x = mem1' x;
           snd (mems' ! k) x = mem2' x ⟧ ⟹ P x;
         ⟦ x ∈ ?X k; 
           fst (mems' ! k) x = fst (mems ! k) x;
           snd (mems' ! k) x = snd (mems ! k) x ⟧ ⟹ P x ⟧ ⟹ P x"
      apply(case_tac "x ∉ ?X k")
       apply simp
      apply simp
      done

    have mems'_i_simp:
      "⋀ i. ⟦ i < length cms1; 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 cms1;
                 mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x;
                 mem1' x = mem2' x ∨ dma mem1' x = High ⟧ ⟹
               fst (mems' ! i) x = mem1' x ∧ snd (mems' ! i) x = mem2' x"
      unfolding mems'_i_def mems'_i_simp
      by auto

    have mems'_i_2 [simp]:
      "⋀ i x. ⟦ i ≠ k; i < length cms1;
                 mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x;
                 mem1' x ≠ mem2' x; dma mem1' 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 cms1;
                 mem1 x = mem1' x; mem2 x = mem2' x;
                 dma mem1 x = High ∧ dma mem1' x = Low ⟧ ⟹
              fst (mems' ! i) x = mem1 x ∧ snd (mems' ! i) x = mem1 x"
      unfolding mems'_i_def mems'_i_simp
      by auto

    have mems'_i_4 [simp]:
      "⋀ i x. ⟦ i ≠ k; i < length cms1;
                 mem1 x = mem1' x; mem2 x = mem2' x;
                 dma mem1 x = Low ∨ dma mem1' x = High;
                 dma mem1' x = dma mem1 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

    have mems'_i_5 [simp]:
      "⋀ i x. ⟦ i ≠ k; i < length cms1;
                 mem1 x = mem1' x; mem2 x = mem2' x;
                 dma mem1 x = Low ∧ dma mem1' x = High;
                 dma mem1' x ≠ dma mem1 x ⟧ ⟹
              fst (mems' ! i) x = mem1' x ∧ snd (mems' ! i) x = mem2' 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 cms1;
           ⟦ mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x;
             mem1' x = mem2' x ∨ dma mem1' x = High;
             fst (mems' ! i) x = mem1' x; snd (mems' ! i) x = mem2' x ⟧ ⟹ P x;
      ⟦ mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x;
        mem1' x ≠  mem2' x; dma mem1' x = Low;
        fst (mems' ! i) x = some_val; snd (mems' ! i) x = some_val ⟧ ⟹ P x;
      ⟦ mem1 x = mem1' x; mem2 x = mem2' x; dma mem1 x = High; 
        dma mem1' x = Low;
        fst (mems' ! i) x = mem1 x; snd (mems' ! i) x = mem1 x ⟧ ⟹ P x;
      ⟦ mem1 x = mem1' x; mem2 x = mem2' x; dma mem1 x = Low ∨ dma mem1' x = High;
        dma mem1' x = dma mem1 x;
        fst (mems' ! i) x = fst (mems ! i) x; snd (mems' ! i) x = snd (mems ! i) x ⟧ ⟹ P x;
      ⟦ mem1 x = mem1' x; mem2 x = mem2' x; dma mem1 x = Low; dma mem1' x = High;
        fst (mems' ! i) x = mem1' x; snd (mems' ! i) x = mem2' x ⟧ ⟹ P x       ⟧
      ⟹ P x"
      using mems'_i_1 mems'_i_2 mems'_i_3 mems'_i_4 mems'_i_5
      by (metis (full_types) Sec.exhaust)

    let ?X' = "λ i. differing_vars_lists mem1' mem2' mems' i"

    have len_unchanged: "length cms1' = length cms1"
      by (metis cms2'_def equal_size length_list_update new_length)

    have mm_equiv': "(cms1' ! k, subst (?σ_mem2) mem1') ≈ ⟨ch, snd (cms1' ! k), mem2'⟩"
      apply(simp add: mem2'_def)
      apply(rule g[THEN conjunct2])
      apply(rule dom_restrict_total)
      done

   hence 𝒞_subst_eq: "∀x∈𝒞. (subst (?σ_mem2) mem1') x = mem2' x"
     apply(rule mm_equiv_𝒞_eq)
     by simp

   have low_mds_eq': "(subst (?σ_mem2) mem1') =⇘snd (cms1' ! k)⇙l mem2'"
     apply(rule mm_equiv_low_eq[where c1="fst (cms1' ! k)"])
     apply(force intro: mm_equiv')
     done

   have 𝒞_subst_eq_idemp: "⋀x. x ∈ 𝒞 ⟹ (subst (?σ_mem2) mem1') x = mem1' x"
     apply(rule subst_not_in_dom)
     apply(rule notI)
     apply(simp add: dom_restrict_total)
     using compat b by force

    from 𝒞_subst_eq 𝒞_subst_eq_idemp
    have 𝒞_eq: "⋀x. x ∈ 𝒞 ⟹ mem1' x = mem2' x"
     by simp

    have not_control: "⋀x i. i < length cms1' ⟹ x ∈ ?X' i ⟹ x ∉ 𝒞"
    proof(rule ccontr, clarsimp)
      fix x i
      let ?mems1i = "fst (mems ! i)"
      let ?mems2i = "snd (mems ! i)"
      let ?mems1'i = "fst (mems' ! i)"
      let ?mems2'i = "snd (mems' ! i)"
      assume "i < length cms1'"
      have "i < length cms1" by (metis len_unchanged ‹i < length cms1'›)
      assume "x ∈ ?X' i"
      assume "x ∈ 𝒞"
      have "x ∉ ?X i"
        using compat ‹i < length cms1'› len_unchanged new_length
        by (metis ‹x ∈ 𝒞› compat_different)
      from ‹x ∈ 𝒞› have  "mem1' x = mem2' x" by(rule 𝒞_eq)
      from ‹x ∈ 𝒞› have "dma mem1' x = Low" by(simp add: 𝒞_Low)
      show "False"
      proof(cases "i = k")
        assume eq[simp]: "i = k"
        show ?thesis
        using ‹x ∉ ?X i› ‹x ∈ ?X' i›
        by(force simp: differing_vars_lists_def differing_vars_def)
      next
        assume neq: "i ≠ k"
        thus ?thesis
        using ‹x ∈ ?X' i› ‹x ∉ ?X i› ‹x ∈ 𝒞› 𝒞_Low ‹mem1' x = mem2' x›
        by(force elim: mems'_i_cases[of "i" "x" "λx. False", OF _ ‹i < length cms1›]
                 simp: differing_vars_lists_def differing_vars_def)
      qed
    qed

    show "makes_compatible (cms1', mem1') (cms2', mem2') mems'"
    proof
      have "length cms1' = length cms1"
        by (metis cms2'_def equal_size length_list_update new_length)
      then show "length cms1' = length cms2' ∧ length cms1' = length mems'"
        using compat new_length
        unfolding mems'_def
        by auto
    next
      fix i
      fix σ :: "'Var ⇀ 'Val"
      let ?mems1'i = "fst (mems' ! i)"
      let ?mems2'i = "snd (mems' ! i)"
      assume i_le: "i < length cms1'"
      assume domσ: "dom σ = ?X' i"
      show "(cms1' ! i, (fst (mems' ! i)) [↦ σ]) ≈ (cms2' ! 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 Some (mem1' x)
            else None)" for x
        have domσ': "dom σ' = ?X k"
          using σ'_def [abs_def]
          apply (clarsimp, safe)
          by( 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 "mem1 x = ?mems1k x ∧ mem2 x = ?mems2k x"
            by (metis differing_vars_neg)
          from ‹x ∉ ?X k› have "?mems1'i x = mem1' x ∧ ?mems2'i x = mem2' x"
            by auto
          moreover
          assume "x ∈ ?X' k"
          hence "mem1' x ≠ ?mems1'i x ∨ mem2' x ≠ ?mems2'i x"
            by (metis ‹i = k› differing_vars_elim)
          ultimately show False
            by auto
        qed

        (* We now show that we can reuse the earlier statements
           by showing the following equality: *)
        have "?mems1'i [↦ σ] = mem1' [↦ σ']"
        proof (rule ext)
          fix x

          show "?mems1'i [↦ σ] x = mem1' [↦ σ'] 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 "?mems1'i [↦ σ] x = v"
              using ‹x ∈ ?X' k› domσ
              by (auto simp: subst_def)
            moreover
            from domσ' and ‹x ∈ ?X' k› have "x ∈ dom σ'" by simp
             
            hence "mem1' [↦ σ'] x = v"
              using domσ' 
              unfolding subst_def
              by (metis σ'_def ‹σ x = Some v› diff_vars_impl option.simps(5) x_in_X'k)

            ultimately show "?mems1'i [↦ σ] x = mem1' [↦ σ'] x" ..
          next
            assume "x ∉ ?X' k"

            hence "?mems1'i [↦ σ] x = ?mems1'i x"
              using domσ
              by (metis ‹i = k› subst_not_in_dom)
            show ?thesis
            proof(case_tac "x ∈ ?X k")
              assume "x ∈ ?X k"
              from ‹x ∉ ?X' k› have "mem1' x = ?mems1'i x"
                by(metis differing_vars_neg ‹i = k›)
              then have "σ' x = Some (?mems1'i x)"
                unfolding σ'_def
                using domσ' domh
                by(simp add: ‹x ∈ ?X k› ‹x ∉ ?X' k›)
              hence "mem1' [↦ σ'] x = ?mems1'i x"
                unfolding subst_def
                by (metis option.simps(5))
              thus ?thesis
                by (metis ‹?mems1'i [↦σ] x = ?mems1'i x›)
            next
              assume "x ∉ ?X k"
              then have "mem1' [↦ σ'] x = mem1' x"
                by (metis domσ' subst_not_in_dom)
              moreover
              have "?mems1'i x = mem1' x"
                by (metis ‹i = k› ‹x ∉ ?X' k› differing_vars_neg)
              ultimately show ?thesis
                by (metis ‹?mems1'i [↦σ] x = ?mems1'i x›)
            qed
          qed
        qed
        (* And the same for the second memories: *)
        moreover have "?mems2'i [↦ σ] = memh [↦ σ']"
        proof (rule ext)
          fix x

          show "?mems2'i [↦ σ] x = memh [↦ σ'] 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 "?mems2'i [↦ σ] x = v"
              using ‹x ∈ ?X' k› domσ
              unfolding subst_def
              by (metis option.simps(5))
            moreover
            from ‹x ∈ ?X' k› have "x ∈ ?X k"
              by auto
            hence "x ∈ dom (σ')"
              by (metis domσ'  ‹x ∈ ?X' k›)
            hence "mem2' [↦ σ'] x = v"
              using domσ' c 
              unfolding 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 mem2'_def subst_overrides)
          next
            assume "x ∉ ?X' k"

            hence "?mems2'i [↦ σ] x = ?mems2'i x"
              using domσ
              by (metis ‹i = k› subst_not_in_dom) 
            show ?thesis
            
            proof(case_tac "x ∈ ?X k")
              assume "x ∈ ?X k"  
              (* This case can't happen so derive a contradiction *)
              hence "mem1 x = mem1' x ∧ mem2 x = mem2' x" by (metis x_unchanged)

              moreover from ‹x ∉ ?X' k› ‹i = k› have "?mems1'i x = mem1' x ∧ ?mems2'i x = mem2' x"
                by(metis differing_vars_neg)
               
              moreover from ‹x ∈ ?X k› have "fst (mems ! i) x ≠ mem1 x ∨ snd (mems ! i) x ≠ mem2 x"
                by(metis differing_vars_elim ‹i = k›)

              moreover from ‹x ∈ ?X k› have "fst (mems' ! i) x = fst (mems ! i) x ∧
                                             snd (mems' ! i) x = snd (mems ! i) x"
                by(metis mems'_k_2 ‹i = k›)
                
              ultimately have "False" by auto

              thus ?thesis by blast
            next
              assume "x ∉ ?X k"
              hence "x ∉ dom σ'" by (simp add: domσ')
              then have "memh [↦ σ'] x = memh x"
                by (metis subst_not_in_dom)
              moreover
              have "?mems2'i x = mem2' x"
                by (metis ‹i = k›  mems'_k_1 ‹x ∉ ?X k›)

              hence "?mems2'i x = memh x"
                unfolding mem2'_def
                by (metis domσ_mem2 subst_not_in_dom ‹x ∉ ?X k›)
              ultimately show ?thesis
                by (metis ‹?mems2'i [↦σ] x = ?mems2'i x›)
            qed
          qed
        qed

        ultimately show
          "(cms1' ! i, (fst (mems' ! i)) [↦ σ]) ≈ (cms2' ! i, (snd (mems' ! i)) [↦ σ])"
          using domσ domσ' g b ‹i = k›
          by (metis c2'_def cms2'_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 (mem1' x)
             else None)" for x
        let ?mems1i = "fst (mems ! i)" and
            ?mems2i = "snd (mems ! i)"
        have "dom σ' = ?X i"
          unfolding σ'_def
          apply auto
           apply (metis option.simps(2))
          by (metis domD domσ)

        have o: "⋀ x.
                 ((?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨
                  ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x) ∧
                 (dma mem1 x = Low ∨ dma mem1' x = High) ∧
                 (dma mem1' x = dma mem1 x))
                 ⟶ (mem1' x ≠ mem1 x ∨ mem2' x ≠ mem2 x)"
        proof -
          fix x
          {
            assume eq_mem: "mem1' x = mem1 x ∧ mem2' x = mem2 x"
               and clas: "dma mem1 x = Low ∨ dma mem1' x = High"
               and clas_eq: "dma mem1' x = dma mem1 x"
            hence mems'_simp: "?mems1'i x = ?mems1i x ∧ ?mems2'i x = ?mems2i x"
              using mems'_i_4
              by (metis ‹i ≠ k› b i_le length_list_update)
            have
              "?mems1'i [↦ σ] x = ?mems1i [↦ σ'] x ∧ ?mems2'i [↦ σ] x = ?mems2i [↦ σ'] x"
            proof (cases "x ∈ ?X' i")
              assume "x ∈ ?X' i"
              hence "?mems1'i x ≠ mem1' x ∨ ?mems2'i x ≠ mem2' 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
                by (clarsimp simp: subst_def mems'_simp split: option.splits)
            next
              assume "x ∉ ?X' i"
              hence "?mems1'i x = mem1' x ∧ ?mems2'i x = mem2' 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

        (* FIXME: clean this up once we optimise the definition of mems'_i *)
        (* Toby: try to establish something similar to o for the downgrading case *)
        have o_downgrade: "⋀x. x ∉ ?X' i ∧ (subst σ (fst (mems' ! i)) x ≠ subst σ' (fst (mems ! i)) x ∨
                    subst σ (snd (mems' ! i)) x ≠ subst σ' (snd (mems ! i)) x) ∧
                   (dma mem1 x = High ∧ dma mem1' x = Low) ⟶
                    mem1' x ≠ mem1 x ∨ mem2' x ≠ mem2 x"
          proof -
          fix x {
            assume mem_eq: "mem1' x = mem1 x ∧ mem2' x = mem2 x"
               and clas: "(dma mem1 x = High ∧ dma mem1' x = Low)"
               and notin: "x ∉ ?X' i"
            hence mems'_simp [simp]: "?mems1'i x = mem1 x ∧ ?mems2'i x = mem1 x"
              using mems'_i_3
              by (metis ‹i ≠ k› b i_le length_list_update)
            have
              "?mems1'i [↦ σ] x = ?mems1i [↦ σ'] x ∧ ?mems2'i [↦ σ] x = ?mems2i [↦ σ'] x"
            proof (cases "x ∈ ?X' i")
              assume "x ∈ ?X' i"
              thus ?thesis using notin by blast
            next
              assume "x ∉ ?X' i"
              hence "?mems1'i x = mem1' x ∧ ?mems2'i x = mem2' x"
                by (metis differing_vars_neg)
              moreover have "x ∉ ?X i"
                using clas compat i_le len_unchanged
                by (force)
              ultimately show ?thesis
                using domσ ‹dom σ' = ?X i› ‹x ∉ ?X' i› apply(simp add: subst_not_in_dom)
                apply(simp add: mem_eq)
                apply(force simp: differing_vars_def differing_vars_lists_def)
                done
            qed
            
          } thus "?thesis x" by blast
        qed

        have modifies_no_var_asm_not_written:
             "⋀x. mem1' x ≠ mem1 x ∨ mem2' x ≠ mem2 x ∨
                   dma mem1' x ≠ dma mem1 x ∨ dma mem2' x ≠ dma mem2 x ⟹
              ¬ var_asm_not_written (snd (cms1 ! i)) x"
        proof -
          fix x
          assume "mem1' x ≠ mem1 x ∨ mem2' x ≠ mem2 x ∨ dma mem1' x ≠ dma mem1 x ∨ dma mem2' x ≠ dma mem2 x"
          hence modified: " ¬ (doesnt_modify (fst (cms1 ! k)) x) ∨ ¬ (doesnt_modify (fst (cms2 ! k)) x)"
            using b i
            unfolding doesnt_modify_def
            by (metis surjective_pairing)
          hence modified_r: " ¬ (doesnt_read_or_modify (fst (cms1 ! k)) x) ∨ ¬ (doesnt_read_or_modify (fst (cms2 ! k)) x)" using doesnt_read_or_modify_doesnt_modify by fastforce

          from sound_modes have loc_modes:
            "locally_sound_mode_use (cms1 ! k, mem1) ∧
             locally_sound_mode_use (cms2 ! k, mem2)"
            unfolding sound_mode_use.simps
            by (metis b equal_size list_all_length)
          moreover
          have "snd (cms1 ! k) = snd (cms2 ! k)"
            by (metis b equal_size modes_eq nth_map)
          have "(cms1 ! k, mem1) ∈ loc_reach (cms1 ! k, mem1)"
            using loc_reach.refl by auto
          hence guars:
                "x ∈ snd (cms1 ! k) GuarNoWrite ⟶ doesnt_modify (fst (cms1 ! k)) x ∧
                 x ∈ snd (cms2 ! k) GuarNoWrite ⟶ doesnt_modify (fst (cms1 ! k)) x ∧
                 x ∈ snd (cms1 ! k) GuarNoReadOrWrite ⟶ doesnt_read_or_modify (fst (cms1 ! k)) x ∧
                 x ∈ snd (cms2 ! k) GuarNoReadOrWrite ⟶ doesnt_read_or_modify (fst (cms1 ! k)) x"
            using loc_modes
            unfolding locally_sound_mode_use_def ‹snd (cms1 ! k) = snd (cms2 ! k)›
            by (metis loc_reach.refl surjective_pairing)

          hence "x ∉ snd (cms1 ! k) GuarNoWrite ∧ x ∉ snd (cms1 ! k) GuarNoReadOrWrite"
            using modified modified_r loc_modes locally_sound_mode_use_def
            by (metis (no_types, lifting) ‹(cms2, mem2) ↝⇘k⇙ (cms2', mem2')› b locally_sound_respects_guarantees modes_eq nth_map meval_elim respects_own_guarantees_def sifum_security_init_axioms)
          moreover
          from sound_modes have "compatible_modes (map snd cms1)"
            by (metis globally_sound_modes_compatible sound_mode_use.simps)

          ultimately show "(?thesis x)"
            unfolding compatible_modes_def var_asm_not_written_def
            using ‹i ≠ k› i_le
            by (metis (no_types) b length_list_update length_map nth_map)
        qed

        
        from o o_downgrade have
          p: "⋀ x. ⟦ ?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨
                      ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x;
                     x ∉ ?X' i ∨ ((dma mem1 x = Low ∨ dma mem1' x = High) ∧
                                   (dma mem1' x = dma mem1 x)) ⟧ ⟹
          ¬ var_asm_not_written  (snd (cms1 ! i)) x"
        proof -
          fix x
          assume mems_neq:
            "?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨ ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x"
             and nin:
            "x ∉ ?X' i ∨ ((dma mem1 x = Low ∨ dma mem1' x = High) ∧
                           (dma mem1' x = dma mem1 x))"
          hence "mem1' x ≠ mem1 x ∨ mem2' x ≠ mem2 x ∨ dma mem1' x ≠ dma mem1 x"
            (* FIXME: clean this up *)
            apply -
            apply(erule disjE[where P="x ∉ ?X' i"])
             apply(case_tac "(dma mem1 x = High ∧ dma mem1' x = Low)")
              apply(metis o_downgrade[rule_format])
             apply(case_tac "dma mem1' x = dma mem1 x")
              (* use o *)
              apply(metis (poly_guards_query) o Sec.exhaust)
             (* should follow trivially *)
             apply fastforce
            apply(metis (poly_guards_query) o Sec.exhaust)
            done
          thus "?thesis x"
            by(force simp: modifies_no_var_asm_not_written)
        qed

        have q':
          "⋀ x. ⟦ dma mem1 x = Low; dma mem1' x = Low;
                   ?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨
                   ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x;
                   x ∉ ?X' i ⟧ ⟹
                 mem1' x = mem2' x"
          by (metis ‹i ≠ k› b compat_different_vars i_le length_list_update mems'_i_2 o)
        have "i < length cms1"
          by (metis cms2'_def equal_size i_le length_list_update new_length)
        with compat and ‹dom σ' = ?X i› have
          bisim: "(cms1 ! i, ?mems1i [↦ σ']) ≈ (cms2 ! i, ?mems2i [↦ σ'])"
          by auto

        define σ'k where "σ'k x = (if x ∈ ?X k then Some (undefined::'Val) else None)" for x
        have "dom σ'k = ?X k" unfolding σ'k_def by (simp add: dom_def)
        with compat and ‹dom σ'k = ?X k› and b have
          bisimk: "(cms1 ! k, ?mems1k [↦ σ'k]) ≈ (cms2 ! k, ?mems2k [↦ σ'k])"
          by auto

        have q_downgrade:
          "⋀ x. ⟦ dma mem1 x = High; dma mem1' x = Low;
                   ?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨
                   ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x;
                   x ∉ ?X' i ⟧ ⟹
                 mem1' x = mem2' x"
        by (metis (erased, opaque_lifting) ‹i ≠ k› compat_different_vars i_le len_unchanged mems'_i_2 o_downgrade)

        have q: "⋀ x. ⟦ dma mem1' x = Low;
                   ?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨
                   ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x;
                   x ∉ ?X' i ⟧ ⟹
                 mem1' x = mem2' x"
          apply(case_tac "dma mem1 x")
           apply(blast intro: q_downgrade)
          by(blast intro: q')

        let ?Δ = "differing_vars (?mems1i [↦ σ']) (?mems1'i [↦ σ]) ∪
                  differing_vars (?mems2i [↦ σ']) (?mems2'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 (?mems1'i [↦ σ]) x = High
                   then Some (?mems1'i [↦ σ] x, ?mems2'i [↦ σ] x)
                   else if x ∈ ?X' i
                        then (case σ x of
                                Some v ⇒ Some (v, v)
                              | None ⇒ None)
                        else Some (mem1' x, mem1' 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

        (* FIXME: clean up *)
        have dma_eq: "dma (?mems1'i [↦ σ]) = dma mem1'"
          apply(rule dma_𝒞)
          apply(rule ballI)
          apply(case_tac "x ∈ ?X' i")
           apply(drule not_control[rotated])
            apply (metis i_le)
           apply blast
          apply(subst subst_not_in_dom)
           apply(simp add: domσ)
          apply(simp add: differing_vars_lists_def differing_vars_def)
          done

        (* FIXME: clean up *)
        have dma_eq'': "dma (?mems1i [↦ σ']) = dma mem1"
          apply(rule dma_𝒞)
          apply(rule ballI)
          apply(case_tac "x ∈ ?X i")
           using compat compat i_le len_unchanged apply fastforce
          apply(subst subst_not_in_dom)
           apply(simp add: ‹dom σ' = ?X i›)
          apply(simp add: differing_vars_lists_def differing_vars_def)
          done

        have dma_eq': "dma (subst ((to_partial mem2 |` differing_vars_lists mem1 mem2 mems k)) mem1') = dma mem1'"
          using compat b
          by(force intro!: dma_𝒞 subst_not_in_dom)

        have A_correct:
              "⋀ x.
               ?mems1i [↦ σ'] [∥1 A] x = ?mems1'i [↦ σ] x ∧
               ?mems2i [↦ σ'] [∥2 A] x = ?mems2'i [↦ σ] x"
        proof -
          fix x
          show "?thesis x"
            (is "?Eq1 ∧ ?Eq2")
          proof (cases "x ∈ ?Δ")
            assume "x ∈ ?Δ"
            hence diff:
              "?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨ ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x"
              by (auto simp: differing_vars_def)
            show ?thesis
            proof (cases "dma (?mems1'i [↦ σ]) x")
              assume "dma (?mems1'i [↦ σ]) x = High"
              from ‹dma (?mems1'i [↦ σ]) x = High› have A_simp [simp]:
                "A x = Some (?mems1'i [↦ σ] x, ?mems2'i [↦ σ] x)"
                unfolding A_def
                by (metis ‹x ∈ ?Δ›)
              from A_simp have ?Eq1 ?Eq2
                unfolding A_def apply_adaptation_def
                by auto
              thus ?thesis
                by auto
            next
              assume "dma (?mems1'i [↦ σ]) 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: "?mems1'i [↦ σ] x = v ∧ ?mems2'i [↦ σ] x = v"
                  unfolding subst_def
                  by auto
                moreover
                from ‹x ∈ ?X' i› and ‹dma (?mems1'i [↦ σ]) 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 ∈ ?Δ›)
                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 (mem1' x, mem1' x)"
                  unfolding A_def
                  using ‹x ∈ ?Δ› ‹x ∉ ?X' i› ‹dma (?mems1'i [↦ σ]) x = Low›
                  by auto

                from q have "mem1' x = mem2' x"
                  by (metis ‹dma (?mems1'i [↦ σ]) x = Low› diff ‹x ∉ ?X' i› dma_eq dma_eq'')

                from ‹x ∉ ?X' i› have
                  "?mems1'i [↦ σ] x = ?mems1'i x ∧ ?mems2'i [↦ σ] x = ?mems2'i x"
                  by (metis domσ subst_not_in_dom)
                moreover
                from ‹x ∉ ?X' i› have "?mems1'i x = mem1' x ∧ ?mems2'i x = mem2' x"
                  by (metis differing_vars_neg)
                ultimately show ?thesis
                  using ‹mem1' x = mem2' x›
                  by (auto simp: apply_adaptation_def)
              qed
            qed
          
          next
            assume "x ∉ ?Δ"
            hence "A x = None"
              by (metis domA domIff)
            from ‹A x = None› have "x ∉ dom A"
              by (metis domIff)
            from ‹x ∉ ?Δ› have "?mems1i [↦ σ'] [∥1 A] x = ?mems1'i [↦ σ] x ∧
                                 ?mems2i [↦ σ'] [∥2 A] x = ?mems2'i [↦ σ] x"
              using ‹A x = None›
              unfolding differing_vars_def apply_adaptation_def
              by auto

            thus ?thesis
              by auto
          qed
        qed
        hence adapt_eq: 
              "?mems1i [↦ σ'] [∥1 A] = ?mems1'i [↦ σ] ∧
               ?mems2i [↦ σ'] [∥2 A] = ?mems2'i [↦ σ]"
          by auto

        have "cms1' ! i = cms1 ! i"
          by (metis ‹i ≠ k› b nth_list_update_neq)

        have A_correct': "globally_consistent A (snd (cms1 ! i)) (?mems1i [↦ σ']) (?mems2i [↦ σ'])"
          (* FIXME: clean up *)
          apply(clarsimp simp: globally_consistent_def)
          apply(rule conjI)
           apply(split option.split)
           apply(intro allI conjI)
            apply simp
           apply(intro allI impI)
           apply(split prod.split)
           apply(intro allI impI)
           apply(simp only:)
           proof -
             fix x v v'
             assume A_updates_x1: "A x = Some (v, v')"
                and A_updates_x2:"subst σ' (fst (mems ! i)) x ≠ v ∨ subst σ' (snd (mems ! i)) x ≠ v'"
             hence "x ∈ dom A" by(blast)
             hence diff:
               "?mems1'i [↦ σ] x ≠ ?mems1i [↦ σ'] x ∨ ?mems2'i [↦ σ] x ≠ ?mems2i [↦ σ'] x"
                by (auto simp: differing_vars_def domA)
             show "¬ var_asm_not_written (snd (cms1 ! i)) x"
             proof (cases "x ∉ ?X' i ∨ ((dma mem1 x = Low ∨ dma mem1' x = High) ∧ dma mem1' x = dma mem1 x)")
               assume "x ∉ ?X' i ∨ ((dma mem1 x = Low ∨ dma mem1' x = High) ∧ (dma mem1' x = dma mem1 x))"
               from this p and diff show writable: "¬ var_asm_not_written (snd (cms1 ! i)) x"
                 by auto
             next
               assume "¬ (x ∉ ?X' i ∨ ((dma mem1 x = Low ∨ dma mem1' x = High) ∧ (dma mem1' x = dma mem1 x)))"
               hence "x ∈ ?X' i" "((dma mem1 x = High ∧ dma mem1' x = Low) ∨ (dma mem1' x ≠ dma mem1 x))"
                 by (metis Sec.exhaust)+

               thus ?thesis by(fastforce simp add: modifies_no_var_asm_not_written)
             qed
                      
          next
            
            have reclas: "(∀x. dma ((subst σ' (fst (mems ! i))) [∥1 A]) x ≠ dma (subst σ' (fst (mems ! i))) x ⟶
         ¬ var_asm_not_written (snd (cms1 ! i)) x)"
              apply(simp add: adapt_eq dma_eq dma_eq'')
              apply(simp add: modifies_no_var_asm_not_written)
              done

            have "snd (cms2 ! i) = snd (cms1 ! i)"
              by (metis ‹i < length cms1› equal_size modes_eq nth_map)

            hence low_mds_eq: "(subst σ' (fst (mems ! i))) =⇘snd (cms1 ! i)⇙l (subst σ' (snd (mems ! i)))"
              apply -
              apply(rule mm_equiv_low_eq[where c1="fst (cms1 ! i)" and c2="fst (cms2 ! i)"])
              using bisim
              by (metis prod.collapse)

            have "snd (cms2 ! k) = snd (cms1 ! k)"
              by (metis b equal_size modes_eq nth_map)

            hence low_mds_eqk: "(subst σ'k (fst (mems ! k))) =⇘snd (cms1 ! k)⇙l (subst σ'k (snd (mems ! k)))"
              apply -
              apply(rule mm_equiv_low_eq[where c1="fst (cms1 ! k)" and c2="fst (cms2 ! k)"])
              using bisimk
              by (metis prod.collapse)

            have eq: "∀x. dma ((subst σ' (fst (mems ! i))) [∥1 A]) x = Low ∧ (x ∈ (snd (cms1 ! i)) AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶
        (subst σ' (fst (mems ! i))) [∥1 A] x = (subst σ' (snd (mems ! i))) [∥2 A] x"
            (* FIXME: clean up *)
            apply(clarsimp simp: adapt_eq dma_eq)
            apply(case_tac "x ∈ dom σ")
             apply(force simp: subst_def)
            apply(simp add: subst_not_in_dom)
            apply(simp add: domσ)
            apply(clarsimp simp: differing_vars_lists_def differing_vars_def)
            apply(case_tac "i = k")
             apply(simp add: ‹i ≠ k›)
            apply(erule mems'_i_cases)
                apply(rule ‹i < length cms1'›[simplified len_unchanged])
               apply force
              apply fastforce
             apply clarsimp
            apply clarsimp

            apply(case_tac "x ∈ differing_vars_lists mem1 mem2 mems i")
             apply(force simp: differing_vars_lists_def differing_vars_def)

            apply(insert low_mds_eq)[1]
            apply(simp add: low_mds_eq_def)
            apply(drule_tac x=x in spec)

            apply(subst (asm) makes_compatible_dma_eq)
               apply(rule compat)
              apply(rule ‹i < length cms1›)
             apply(rule ‹dom σ' = differing_vars_lists mem1 mem2 mems i›)
            apply simp
            apply(subgoal_tac "x ∉ dom σ'")
             apply(simp add: subst_not_in_dom)
             apply force
            apply(simp add: ‹dom σ' = differing_vars_lists mem1 mem2 mems i›)+
            done
          from reclas eq
          show " (∀x. dma ((subst σ' (fst (mems ! i))) [∥1 A]) x ≠ dma (subst σ' (fst (mems ! i))) x ⟶
         ¬ var_asm_not_written (snd (cms1 ! i)) x) ∧
    (∀x. dma ((subst σ' (fst (mems ! i))) [∥1 A]) x = Low ∧ (x ∈ snd (cms1 ! i) AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶
         (subst σ' (fst (mems ! i))) [∥1 A] x = (subst σ' (snd (mems ! i))) [∥2 A] x)"
          by blast
        qed

        have "snd (cms1 ! i) = snd (cms2 ! i)"
          by (metis ‹i < length cms1› equal_size modes_eq nth_map)

        with bisim have "(cms1 ! i, ?mems1i [↦ σ'] [∥1 A]) ≈ (cms2 ! i, ?mems2i [↦ σ'] [∥2 A])"
          using A_correct'
          apply (subst surjective_pairing[of "cms1 ! i"])
          apply (subst surjective_pairing[of "cms2 ! i"])
          by (metis surjective_pairing globally_consistent_adapt_bisim)

        thus ?thesis using adapt_eq
          by (metis ‹i ≠ k› b cms2'_def nth_list_update_neq)
      qed
    next
      fix i x

      let ?mems1'i = "fst (mems' ! i)"
      let ?mems2'i = "snd (mems' ! i)"
      assume i_le: "i < length cms1'"
      assume mem_eq': "mem1' x = mem2' x ∨ dma mem1' x = High ∨ x ∈ 𝒞"
      show "x ∉ ?X' i"
      proof (cases "x ∈ 𝒞")
        assume "x ∈ 𝒞"
        thus ?thesis by(metis not_control i_le)
      next
        assume "x ∉ 𝒞"
        hence mem_eq: "mem1' x = mem2' x ∨ dma mem1' x = High" by(metis mem_eq')
        thus ?thesis
        proof (cases "i = k")
          assume "i = k"
          thus "x ∉ ?X' i"
            apply (cases "x ∉ ?X k")
             apply (metis differing_vars_neg_intro mems'_k_1 mems'_k_2)
            by(metis compat_different[OF compat] b mem_eq Sec.distinct(1) x_unchanged)
        next
          assume "i ≠ k"
          thus "x ∉ ?X' i"
          proof (rule mems'_i_cases)
            from b i_le show "i < length cms1"
              by (metis length_list_update)
          next
            assume "fst (mems' ! i) x = mem1' x"
              "snd (mems' ! i) x = mem2' x"
            thus "x ∉ ?X' i"
              by (metis differing_vars_neg_intro)
          next
            assume "mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x"
              "mem1' x ≠ mem2' x" and "dma mem1' 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
            (* FIXME: clean this up -- there is surely a more direct route.
                      Same must be true of mems'_i definition and o, o_downgrade,
                      p etc. lemmas above that are proved with surely lots of
                      overlapping cases *)
            assume case3: "mem1 x = mem1' x" "mem2 x = mem2' x" 
              "dma mem1 x = Low ∨ dma mem1' x = High"
              "fst (mems' ! i) x = fst (mems ! i) x"
              "snd (mems' ! i) x = snd (mems ! i) x"
            have "x ∈ ?X' i ⟹ mem1' x ≠ mem2' x ∧ dma mem1' 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 have "mem1' x ≠ mem2' x ∧ dma mem1 x = Low"
                by (metis b compat compat_different i_le length_list_update)
              with mem_eq have clases: "dma mem1 x = Low ∧ dma mem1' x = High" by auto
              have "fst (mems' ! i) x = mem1' x ∧ snd (mems' ! i) x = mem2' x"
                apply(rule mems'_i_5)
                     apply(rule ‹i ≠ k›)
                    using i_le len_unchanged apply(simp)
                   apply(simp add: case3)+
                 apply(simp add: clases)+
                done
              hence "x ∉ ?X' i" by (metis differing_vars_neg_intro)
              with ‹x ∈ ?X' i› show ?thesis by blast
            qed
            with ‹mem1' x = mem2' x ∨ dma mem1' x = High› show "x ∉ ?X' i"
              by auto
          next
            assume case4: "mem1 x = mem1' x" "mem2 x = mem2' x"
                   "dma mem1 x = High" "dma mem1' x = Low"
                   "fst (mems' ! i) x = mem1 x" "snd (mems' ! i) x = mem1 x"
            with mem_eq have "mem1' x = mem2' x" by auto
            with case4 show ?thesis by(auto simp: differing_vars_def differing_vars_lists_def)
          next
            assume "fst (mems' ! i) x = mem1' x"
                   "snd (mems' ! i) x = mem2' x" thus ?thesis by(metis differing_vars_neg_intro)
          qed
        qed
      qed
    next
      { fix x
        have "∃ i < length cms1. x ∉ ?X' i"
        proof (cases "mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x ∨ dma mem1' x ≠ dma mem1 x")
          assume var_changed: "mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x ∨ dma mem1' x ≠ dma mem1 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 "¬ (mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x ∨ dma mem1' x ≠ dma mem1 x)"
          hence assms: "mem1 x = mem1' x" "mem2 x = mem2' x" "dma mem1' x = dma mem1 x" by auto

          have "length cms1 ≠ 0"
            using b
            by (metis less_zeroE)
          then obtain i where i_prop: "i < length cms1 ∧ 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
            from i_prop have "x ∉ ?X i" by simp
            assume "i ≠ k"
            hence "x ∉ ?X' i"
              (* FIXME: clean up *)
              apply -
              apply(rule mems'_i_cases)
                    apply assumption
                   apply(simp add: i_prop)
                  apply(simp add: assms)+
               using ‹x ∉ ?X i› differing_vars_neg
               using ‹¬ (mem1 x ≠ mem1' x ∨ mem2 x ≠ mem2' x ∨ dma mem1' x ≠ dma mem1 x)› differing_vars_elim apply auto[1]
              by(metis differing_vars_neg_intro)
            with i_prop show ?thesis
              by auto
          qed
        qed
      }
      thus "(length cms1' = 0 ∧ mem1' =l mem2') ∨ (∀ x. ∃ i < length cms1'. x ∉ ?X' i)"
        by (metis cms2'_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 (cms1, mem1) (cms2, mem2) mems"
  assumes modes_eq: "map snd cms1 = map snd cms2"
  assumes x_low: "dma mem1 x = Low"
  assumes x_readable: "x ∈ 𝒞 ∨ (∀ i < length cms1. x ∉ snd (cms1 ! i) AsmNoReadOrWrite)"
  shows "mem1 x = mem2 x"
proof -
  let ?X = "λ i. differing_vars_lists mem1 mem2 mems i"
  from compat have "(length cms1 = 0 ∧ mem1 =l mem2) ∨
                    (∀ x. ∃ j. j < length cms1 ∧ x ∉ ?X j)"
    by auto
  thus "mem1 x = mem2 x"
  proof
    assume "length cms1 = 0 ∧ mem1 =l mem2"
    with x_low show ?thesis
      by (simp add: low_eq_def)
  next
    assume "∀ x. ∃ j. j < length cms1 ∧ x ∉ ?X j"
    then obtain j where j_prop: "j < length cms1 ∧ x ∉ ?X j"
      by auto
    let ?mems1j = "fst (mems ! j)" and
        ?mems2j = "snd (mems ! j)"

    obtain σ :: "'Var ⇀ 'Val" where domσ: "dom σ = ?X j"
      by (metis dom_restrict_total)

    from compat x_low makes_compatible_dma_eq j_prop ‹dom σ = ?X j›
    have x_low: "dma (?mems1j [↦ σ]) x = Low"
      by metis

    from domσ compat and j_prop have "(cms1 ! j, ?mems1j [↦ σ]) ≈ (cms2 ! j, ?mems2j [↦ σ])"
      by auto
    
    moreover
    have "snd (cms1 ! j) = snd (cms2 ! j)"
      using modes_eq
      by (metis j_prop length_map nth_map)

    ultimately have "?mems1j [↦ σ] =⇘snd (cms1 ! j)⇙l ?mems2j [↦ σ]"
      using modes_eq j_prop
      by (metis mm_equiv_low_eq prod.collapse)
    hence "?mems1j x = ?mems2j 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 meval_sched_one:
  "(cms, mem) ↝⇘k⇙ (cms', mem') ⟹
        (cms, mem) →⇘[k]⇙ (cms', mem')"
  apply(simp)
  done

lemma meval_sched_ConsI: 
  "(cms, mem) ↝⇘k⇙ (cms', mem') ⟹
   (cms', mem') →⇘sched⇙ (cms'', mem'') ⟹
   (cms, mem) →⇘(k#sched)⇙ (cms'', mem'')"
  by fastforce

lemma reachable_modes_subset:
  assumes eval: "(cms, mem) ↝⇘k⇙ (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 assms
    unfolding reachable_mode_states_def 
    by (blast intro: meval_sched_ConsI)
qed

lemma globally_sound_modes_invariant:
  assumes globally_sound: "globally_sound_mode_use (cms, mem)"
  assumes eval: "(cms, mem) ↝⇘k⇙ (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. var_asm_not_written mds x ⟶ mem1 x = mem2 x ∧ dma mem1 x = dma mem2 x"
  shows "⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem1⟩ ⟹ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c, mds, mem2⟩"
proof -
  let ?lc = "⟨c', mds', mem'⟩"
  assume "?lc ∈ loc_reach ⟨c, mds, mem1⟩"
  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. var_asm_not_written mds x ⟶ mem' x = mem x ∧ dma mem' x = dma 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) ↝⇘k⇙ (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 cmsk' where
    ev: "(cms ! k, mem) ↝ (cmsk', mem') ∧ k < length cms ∧ cms' = cms [k := cmsk']"
    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. var_asm_not_written (snd (cms ! i)) x ⟹ x ∈ snd (cms ! k) GuarNoWrite ∨ x ∈ snd (cms ! k) GuarNoReadOrWrite"
        unfolding compatible_modes_def
        by (metis (no_types) ‹i ≠ k› ‹length cms = length cms'› ev i_le length_map nth_map var_asm_not_written_def)
      hence "⋀ x. var_asm_not_written (snd (cms ! i)) x ⟶ doesnt_modify (fst (cms ! k)) x"
        using ev loc_sound
        unfolding locally_sound_mode_use_def
        by (metis loc_reach.refl surjective_pairing doesnt_read_or_modify_doesnt_modify)
      with ev have "⋀ x. var_asm_not_written (snd (cms ! i)) x ⟹ mem x = mem' x ∧ dma mem x = dma mem' x"
        unfolding doesnt_modify_def by (metis prod.collapse)
      with loc_reach_mem_diff_eq have "loc_reach (cms ! i, mem') = loc_reach (cms ! i, mem)"
         apply -
         by(case_tac "cms ! i", simp)
      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 app_Cons_rewrite:
  "ns @ (a # ms) = ((ns @ [a]) @ ms)"
  apply simp
  done

lemma meval_sched_app_iff:
  "(cms1, mem1) →⇘ns@ms⇙ (cms1', mem1') =
   (∃cms1'' mem1''. (cms1, mem1) →⇘ns⇙ (cms1'', mem1'') ∧ (cms1'', mem1'') →⇘ms⇙ (cms1', mem1'))"
  apply(induct ns arbitrary: ms cms1 mem1)
   apply simp
  apply force
  done

lemmas meval_sched_appD = meval_sched_app_iff[THEN iffD1]
lemmas meval_sched_appI = meval_sched_app_iff[THEN iffD2, OF exI, OF exI]

lemma meval_sched_snocD:
  "(cms1, mem1) →⇘ns@[n]⇙ (cms1', mem1') ⟹
   ∃cms1'' mem1''. (cms1, mem1) →⇘ns⇙ (cms1'', mem1'') ∧ (cms1'', mem1'') ↝⇘n⇙ (cms1', mem1')"
  apply(fastforce dest: meval_sched_appD)
  done

lemma meval_sched_snocI:
  "(cms1, mem1) →⇘ns⇙ (cms1'', mem1'') ∧ (cms1'', mem1'') ↝⇘n⇙ (cms1', mem1') ⟹
  (cms1, mem1) →⇘ns@[n]⇙ (cms1', mem1')"
  apply(fastforce intro: meval_sched_appI)
  done
  
lemma makes_compatible_eval_sched:
  assumes compat: "makes_compatible (cms1, mem1) (cms2, mem2) mems"
  assumes modes_eq: "map snd cms1 = map snd cms2"
  assumes sound_modes: "sound_mode_use (cms1, mem1)" "sound_mode_use (cms2, mem2)"
  assumes eval: "(cms1, mem1) →⇘sched⇙ (cms1', mem1')"
  shows "∃ cms2' mem2' mems'. sound_mode_use (cms1', mem1') ∧
                              sound_mode_use (cms2', mem2') ∧
                              map snd cms1' = map snd cms2' ∧
                              (cms2, mem2) →⇘sched⇙ (cms2', mem2') ∧
                              makes_compatible (cms1', mem1') (cms2', mem2') mems'"
proof -
  (* cms1' and mem1' need to be arbitrary so
     that the induction hypothesis is sufficiently general. *)
  from eval show ?thesis
  proof (induct "sched" arbitrary: cms1' mem1' rule: rev_induct)
    case Nil
    hence "cms1' = cms1 ∧ mem1' = mem1"
      by (simp add: Pair_inject meval_sched.simps(1))
    thus ?case
      by (metis compat meval_sched.simps(1) modes_eq sound_modes)
  next
    case (snoc n ns)
    then obtain cms1'' mem1'' where eval'':
      "(cms1, mem1) →⇘ns⇙ (cms1'', mem1'') ∧ (cms1'', mem1'') ↝⇘n⇙ (cms1', mem1')"
      by (metis meval_sched_snocD prod_cases3 snd_conv)
    hence "(cms1'', mem1'') ↝⇘n⇙ (cms1', mem1')" ..
    moreover
    from eval'' obtain cms2'' mem2'' mems'' where IH:
      "sound_mode_use (cms1'', mem1'') ∧
       sound_mode_use (cms2'', mem2'') ∧
       map snd cms1'' = map snd cms2'' ∧
       (cms2, mem2) →⇘ns⇙ (cms2'', mem2'') ∧
       makes_compatible (cms1'', mem1'') (cms2'', mem2'') mems''"
      using snoc
      by metis
    ultimately obtain cms2' mem2' mems' where
      "map snd cms1' = map snd cms2' ∧
       (cms2'', mem2'') ↝⇘n⇙ (cms2', mem2') ∧
       makes_compatible (cms1', mem1') (cms2', mem2') mems'"
      using makes_compatible_invariant
      by blast
    thus ?case
      using IH eval'' meval_sched_snocI sound_modes_invariant
      by metis
  qed
qed

lemma differing_vars_initially_empty:
  "i < n ⟹ x ∉ differing_vars_lists mem1 mem2 (zip (replicate n mem1) (replicate n mem2)) 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: "mem1 =l mem2"
  shows "makes_compatible (cmds, mem1)
                          (cmds, mem2)
                          (replicate (length cmds) (mem1, mem2))"
proof -
  let ?n = "length cmds"
  let ?mems = "replicate ?n (mem1, mem2)" and
      ?mdss = "map snd cmds"
  let ?X = "differing_vars_lists mem1 mem2 ?mems"
  have diff_empty: "∀ i < ?n. ?X i = {}"
    by (metis differing_vars_initially_empty ex_in_conv min.idem zip_replicate)

  show ?thesis
  proof
    show "length cmds = length cmds ∧ length cmds = length ?mems"
      by auto
  next
    fix i and σ :: "'Var ⇒ 'Val option"
    let ?mems1i = "fst (?mems ! i)" and ?mems2i = "snd (?mems ! i)"
    let ?mdssi = "?mdss ! i"
    assume i: "i < length cmds"
    assume domσ: "dom σ =
                  differing_vars_lists mem1 mem2
                                      (replicate (length cmds) (mem1, mem2)) i"
    from i have "?mems1i = mem1" "?mems2i = mem2"
      by auto

    with domσ have [simp]: "dom σ = {}" by(auto simp: differing_vars_lists_def differing_vars_def i)

    from i 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 "⋀ mem1 mem2. mem1 =⇘?mdssi⇙l mem2 ⟹
      (cmds ! i, mem1) ≈ (cmds ! i, mem2)"
      using com_sifum_secure_def low_indistinguishable_def
      by auto

    moreover
    have "⋀x. σ x = None" using ‹dom σ = {}›
      by (metis domIff empty_iff)
    hence [simp]: "⋀ mem. mem [↦ σ] = mem"
      by(simp add: subst_def)

    from i have "?mems1i = mem1" "?mems2i = mem2"
      by auto
    with low_eq have "?mems1i [↦ σ] =⇘?mdssi⇙l ?mems2i [↦ σ]"
      by (auto simp: low_mds_eq_def low_eq_def)

    ultimately show "(cmds ! i, ?mems1i [↦ σ]) ≈ (cmds ! i, ?mems2i [↦ σ])"
      by simp
  next
    fix i x
    assume "i < length cmds"
    with diff_empty show "x ∉ ?X i" by auto
  next
    show "(length cmds = 0 ∧ mem1 =l mem2) ∨ (∀ x. ∃ i < length cmds. 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_cont:
  assumes com_secure: "list_all com_sifum_secure cmds"
  assumes sound_modes: "∀ mem. INIT mem ⟶ sound_mode_use (cmds, mem)"
  shows "prog_sifum_secure_cont cmds"
  unfolding prog_sifum_secure_cont_def
  using assms
proof (clarify)
  fix mem1 mem2 :: "'Var ⇒ 'Val"
  fix sched cms1' mem1'
  let ?n = "length cmds"
  let ?mems = "zip (replicate ?n mem1) (replicate ?n mem2)"
  assume INIT1: "INIT mem1" and INIT2: "INIT mem2"
  assume low_eq: "mem1 =l mem2"
  with com_secure have compat:
    "makes_compatible (cmds, mem1) (cmds, mem2) ?mems"
    by (metis compatible_refl fst_conv length_replicate map_replicate snd_conv zip_eq_conv INIT1 INIT2)

  also assume eval: "(cmds, mem1) →⇘sched⇙ (cms1', mem1')"

  ultimately obtain cms2' mem2' mems'
    where p: "map snd cms1' = map snd cms2' ∧
             (cmds, mem2) →⇘sched⇙ (cms2', mem2') ∧
             makes_compatible (cms1', mem1') (cms2', mem2') mems'"
    using sound_modes makes_compatible_eval_sched INIT1 INIT2
    by blast

  thus "∃ cms2' mem2'. (cmds, mem2) →⇘sched⇙ (cms2', mem2') ∧
                        map snd cms1' = map snd cms2' ∧
                        length cms2' = length cms1' ∧
                        (∀ x. dma mem1' x = Low ∧ (x ∈ 𝒞 ∨ (∀ i < length cms1'. x ∉ snd (cms1' ! i) AsmNoReadOrWrite))
          ⟶ mem1' x = mem2' x)"
    using p compat_low_eq
    by (metis length_map)
qed

end

end