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 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)

(* 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 (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 x = High) 
             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 x = High   
          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 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 x = High)  x  differing_vars_lists mem1 mem2 mems i"
    by (simp add: Let_def, blast)
  with * show "dma x = Low"
    by (cases "dma 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 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 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 =mdsl 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)"
  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 (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 (fst (cms1 ! i)) x  doesnt_read (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 x = Low"
    by (metis compat_low)

  from compat ile x have b: "mem1 x  mem2 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 ! jl ?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) AsmNoRead"
  proof -
    { assume "x  (?mdss ! j) AsmNoRead"
      then have mems_eq: "?mems1j x = ?mems2j x"
        using dma x = Low low_eq subst_eq
        by (metis (full_types) low_mds_eq_def subst_eq)

      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) 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 (cms1 ! i)) x  doesnt_read (fst (cms2 ! 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 gX where IH: "change_respecting c, mds, mem c', mds', mem' X gX"
      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' [↦ gX σ'] (x := v))
         then (λ y :: 'Var.
                    if x = y
                    then σ y
                    else gX σ' y)
         else (λ y. gX σ' 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 evalX: "c, mds, mem [↦ X]  c', mds', mem' [↦ gX X]"
        using dom X = X
        unfolding change_respecting.simps
        by auto
      ultimately have
        noreadx:
        "( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX X] (x := v) ) 
        ( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX 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 noreadx show "g σ  σ"
        proof
          assume nowrite: " v. c, mds, mem [↦ X] (x := v) 
                 c', mds', mem' [↦ gX X] (x := v)"
          then have g_simp [simp]: "g σ = (λ y. if y = x then σ y else gX 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' [↦ gX X]"
          hence
            "¬ ( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX X] (x := v))"
            by (metis doesnt_read c x doesnt_read_mutually_exclusive evalX)
          hence g_simp [simp]: "g σ = gX X"
            unfolding g_def
            by (auto simp: Let_def)

          also from IH have "gX 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' [↦ gX X] (x := v)) 
            ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X] (x := v)))
           
           (( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX X]) 
            ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'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' [↦ gX (h |` X)] (x := v);
                         v. c, mds, mem [↦ h' |` X] (x := v) 
                             c', mds', mem' [↦ gX (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' [↦ gX (h |` X)] (x := v)"
            assume overwrite: " v. c, mds, mem [↦ h' |` X] (x := v) 
              c', mds', mem' [↦ gX (h' |` X)]"

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

            have "dom ?hX = 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 evalX': "c, mds, mem [↦ ?h'X]  c', mds', mem' [↦ gX ?h'X]"
              unfolding change_respecting.simps
              by auto
            with doesnt_read c x have noreadx':
             "( v. c, mds, mem [↦ ?h'X] (x := v)  c', mds', mem' [↦ gX ?h'X] (x := v)) 
              ( v. c, mds, mem [↦ ?h'X] (x := v)  c', mds', mem' [↦ gX ?h'X])"
              unfolding doesnt_read_def
              by auto

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

            obtain memv' where "c, mds, ?memv  c', mds', memv'"
              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 gv where
              IHv: "change_respecting c, mds, ?memv c', mds', memv' X gv"
              by (metis insert(3))

            hence evalv: "c, mds, ?memv [↦ ?hX]  c', mds', memv' [↦ gv ?hX]"
                         "c, mds, ?memv [↦ ?h'X]  c', mds', memv' [↦ gv ?h'X]"
              apply (metis dom (h |` X) = X change_respecting.simps)
              by (metis IHv dom (h' |` X) = X change_respecting.simps)

            from evalv(1) have "memv' x = v"
            proof -
              assume "c, mds, mem (x := v) [↦ ?hX]  c', mds', memv' [↦ gv ?hX]"
              have "?memv [↦ ?hX] = mem [↦ ?hX] (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 "memv' [↦ gv ?hX] = mem' [↦ gX ?hX] (x := v)"
                using deterministic
                by (erule_tac x = v in allE, auto, metis evalv(1))

              hence "memv' [↦ gv ?hX] x = v"
                by simp
              also have "x  dom (gv ?hX)"
                using IHv dom ?hX = X change_respecting_dom
                by (metis func_le_dom insert(2) rev_subsetD)
              ultimately show "memv' x = v"
                by (metis subst_not_in_dom)
            qed
            moreover
            from evalv(2) have "memv' x = mem' x"
            proof -
              assume "c, mds, ?memv [↦ ?h'X]  c', mds', memv' [↦ gv ?h'X]"
              moreover
              from overwrite have
                "c, mds, mem [↦ ?h'X] (x := v)  c', mds', mem' [↦ gX ?h'X]"
                by auto
              moreover
              have "?memv [↦ ?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' [↦ gX ?h'X] = memv' [↦ gv ?h'X]"
                using deterministic
                by auto
              also have "x  dom (gv ?h'X)"
                using IHv dom ?h'X = X change_respecting_dom
                by (metis func_le_dom insert(2) subsetD)
              ultimately show "memv' x = mem' x"
                using x  dom (gX ?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 evalX': "c, mds, mem [↦ ?σ'X]  c', mds', mem' [↦ gX ?σ'X]"
            unfolding change_respecting.simps
            by auto
          with doesnt_read c x have noreadx':
             "( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X] (x := v))
              
              ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X])"
            unfolding doesnt_read_def
            by auto

          ultimately show ?thesis
            using noreadx 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' [↦ gX X] (x := v)) 
            ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X] (x := v))"
          hence g_simp [simp]: "g σ = (λ y. if y = x then σ y else gX X y) 
                                g σ' = (λ y. if y = x then σ' y else gX ?σ'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' [↦ gX X]) 
            ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X])"
          hence
            "¬ ( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX X] (x := v))
            
            ¬ ( v. c, mds, mem [↦ ?σ'X] (x := v)  c', mds', mem' [↦ gX ?σ'X] (x := v))"
            by (metis doesnt_read c x doesnt_read_mutually_exclusive' fun_upd_triv)

          hence g_simp [simp]: "g σ = gX X  g σ' = gX ?σ'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 noreadx show "c, mds, mem [↦ σ]  c', mds', mem' [↦ g σ]"
      proof
        assume nowrite:
          " v. c, mds, mem[↦ X] (x := v)  c', mds', mem' [↦ gX X] (x := v)"
        then have g_simp [simp]: "g σ = (λ y. if y = x then σ y else gX 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' [↦ gX 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' [↦ gX 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' [↦ gX X]"
        hence
          "¬ ( v. c, mds, mem [↦ X] (x := v)  c', mds', mem' [↦ gX X] (x := v))"
          by (metis doesnt_read c x doesnt_read_mutually_exclusive' evalX)
        hence g_simp [simp]: "g σ = gX 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:
  " 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 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: "(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 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 (v1, v2)  if first then v1 else v2
             | None  mem x)"

abbreviation apply_adaptation1 ::
  "('Var, 'Val) Mem  ('Var, 'Val) adaptation  ('Var, 'Val) Mem"
  ("_ [∥1 _]" [900, 0] 1000)
  where "mem [∥1 A]  apply_adaptation True mem A"

abbreviation apply_adaptation2 ::
  "('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: "c1, mds, mem1  c2, mds, mem2"
  assumes globally_consistent: "globally_consistent A mds"
  shows "c1, mds, mem1 [∥1 A]  c2, mds, mem2 [∥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 "mem1 [∥1 A] = mem1" and "mem2 [∥2 A] = mem2"
      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': "c1, mds, mem1 [∥1 A']  c2, mds, mem2 [∥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 eq1: "mem1 [∥1 A'] (x := v) = mem1 [∥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 eq2: "mem2 [∥2 A'] (x := v') = mem2 [∥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 "c1, mds, mem1 [∥1 A'] (x := v)  c2, mds, mem2 [∥2 A'] (x := v')"
        using mm_equiv_glob_consistent
        unfolding closed_glob_consistent_def
        by (metis bisim' x  mds AsmNoWrite)
      thus ?case using eq1 eq2
        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
        "c1, mds, mem1 [∥1 A'] (x := v)  c2, mds, mem2 [∥2 A'] (x := v)"
        using mm_equiv_glob_consistent
        unfolding closed_glob_consistent_def
        by (metis dma x = Low bisim')
      ultimately show ?case using eq1 eq2
        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 (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)  (cms1', mem1')"
  obtains cms2' mem2' mems' where
      "map snd cms1' = map snd cms2' 
       (cms2, mem2)  (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 (fst (cms1 ! i)) x 
                                          doesnt_read (fst (cms2 ! i)) x"
    by (metis compatible_different_no_read)
  from eval obtain k where
    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 obtain g1 where
    c: "change_respecting (cms1 ! k, mem1) (cms1' ! k, mem1') (?X k) g1"
    using noread_exists_change_respecting b a
    by (metis surjective_pairing)

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

  with b and c have
    evalσ: " σ. dom σ = ?X k  (cms1 ! k, ?mems1k [↦ σ])  (cms1' ! k, mem1' [↦ g1 σ])"
    by auto

  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' [↦ g1 σ])   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' [↦ g1 h])   ch, ?mdsk', memh "
    using d
    by metis

  then obtain g2 where e:
    "change_respecting (cms2 ! k, ?mems2k [↦ h])  ch, ?mdsk', memh  (?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 
      (cms2 ! k, ?mems2k [↦ h] [↦ σ])   ch, ?mdsk', memh [↦ g2 σ] "
    unfolding change_respecting.simps
    by auto

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

  from d and f have g: " σ. dom σ = ?X k 
    (cms2 ! k, ?mems2k [↦ σ])   ch, ?mdsk', memh [↦ g2 σ]  
    (cms1' ! k, mem1' [↦ g1 σ])   ch, ?mdsk', memh [↦ g2 σ] "
    using h_prop
    by (metis deterministic)
  let ?σ_mem2 = "to_partial mem2 |` ?X k"
  define mem2' where "mem2' = memh [↦ g2 ?σ_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)  (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
  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 (cms1', mem1') (cms2', mem2') mems'"
  proof
    define mems'_k
      where "mems'_k x =
      (if x  ?X k
       then (mem1' x, mem2' x)
       else if (x  dom_g1)  (x  dom_g2)
       then (mem1' x, mem2' x)
       else (?mems1k x, ?mems2k 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  
      mem1 x = mem1' x  mem2 x = mem2' x"
    proof
      fix x
      assume "x  ?X k" and "x  dom_g1"
      thus "mem1 x = mem1' 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_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
      from x  dom_g2 dom_uniq e have g_eq: "g2 ?σ_mem2 x = Some (mem2 x)"
        unfolding change_respecting.simps func_le_def
        by (metis dom_restrict_total eq_mem2)
      hence "memh [↦ g2 ?σ_mem2] x = mem2 x"
        by (auto simp: subst_def)

      ultimately have "?mems2k [↦ h] [↦ ?σ_mem2] x = memh [↦ g2 ?σ_mem2] x"
        by auto
      thus "mem2 x = mem2' x"
        by (metis mem2 = ?mems2k [↦ ?σ_mem2] domσ_mem2 domh mem2'_def subst_overrides)
    qed

    define mems'_i
      where "mems'_i i x =
       (if ((mem1 x  mem1' x  mem2 x  mem2' x) 
          (mem1' x = mem2' x  dma x = High))
         then (mem1' x, mem2' x)
         else if ((mem1 x  mem1' x  mem2 x  mem2' x) 
                  (mem1' x  mem2' 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 cms1]"
    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 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; x  dom_g1  x  dom_g2  
      fst (mems' ! k) x = mem1' x  snd (mems' ! k) x = mem2' 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 = mem1' x;
           snd (mems' ! k) x = mem2' 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 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 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 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  
              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 cms1;
            mem1 x  mem1' x  mem2 x  mem2' x;
             mem1' x = mem2' x  dma 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 x = Low;
        fst (mems' ! i) x = some_val; snd (mems' ! i) x = some_val   P x;
       mem1 x = mem1' x; mem2 x = mem2' 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 mem1' mem2' mems' i"
    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 if (x  dom (g1 h))
                             then Some (?mems1'i x)
                             else if (x  dom (g2 h))
                                  then Some (?mems2'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 "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

        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 "?mems1'i x = mem1' x" "?mems2'i x = mem2' 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 "?mems1'i [↦ σ] = mem1' [↦ g1 σ']"
        proof (rule ext)
          fix x

          show "?mems1'i [↦ σ] x = mem1' [↦ 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 "?mems1'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 "mem1' [↦ 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 "?mems1'i [↦ σ] x = mem1' [↦ g1 σ'] 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 (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 (?mems1'i x)"
                unfolding σ'_def
                using domσ' domh
                by (metis g1 σ' x = σ' x x  dom (g1 σ') x  ?X' k domIff dom_uniq(1))

              hence "mem1' [↦ g1 σ'] x = ?mems1'i x"
                unfolding subst_def
                by (metis g1 σ' x = σ' x option.simps(5))
              thus ?thesis
                by (metis ?mems1'i [↦σ] x = ?mems1'i x)
            next
              assume "x  dom_g1"
              then have "mem1' [↦ g1 σ'] x = mem1' x"
                by (metis domσ' dom_uniq(1) 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 [↦ g2 σ']"
        proof (rule ext)
          fix x

          show "?mems2'i [↦ σ] x = memh [↦ 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 "?mems2'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 "mem2' [↦ 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) 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 (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 (?mems2'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 "mem1 x = mem1' x  mem2 x = mem2' 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
                    "?mems1'i x = ?mems1k x  ?mems2'i x = ?mems2k 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 "mem2' [↦ g2 σ'] x = ?mems2'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)
                  mem2'_def subst_not_in_dom subst_overrides)
            next
              assume "x  dom_g2"
              then have "memh [↦ g2 σ'] x = memh x"
                by (metis domσ' dom_uniq(2) subst_not_in_dom)
              moreover
              have "?mems2'i x = mem2' x"
                by (metis i = k x  dom_g2 mems'_k_1 mems'_k_2)

              hence "?mems2'i x = memh x"
                unfolding mem2'_def
                by (metis x  dom_g2 domσ_mem2 dom_uniq(2) subst_not_in_dom)
              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)
                  (mem1' x  mem1 x  mem2' x  mem2 x)"
        proof -
          fix x
          {
            assume eq_mem: "mem1' x = mem1 x  mem2' x = mem2 x"
            hence mems'_simp [simp]: "?mems1'i x = ?mems1i x  ?mems2'i x = ?mems2i 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"
              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
                apply (auto simp: subst_def)
                 apply (metis mems'_simp)
                by (metis mems'_simp)
            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

        from o have
          p: " x.  ?mems1'i [↦ σ] x  ?mems1i [↦ σ'] x 
                      ?mems2'i [↦ σ] x  ?mems2i [↦ σ'] x  
          x  snd (cms1 ! i) AsmNoWrite"
        proof
          fix x
          assume mems_neq:
            "?mems1'i [↦ σ] x  ?mems1i [↦ σ'] x  ?mems2'i [↦ σ] x  ?mems2i [↦ σ'] x"
          hence modified:
            "¬ (doesnt_modify (fst (cms1 ! k)) x)  ¬ (doesnt_modify (fst (cms2 ! 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 (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)"
            by (metis loc_reach.refl prod.collapse)
          hence guars:
                "x  snd (cms1 ! k) GuarNoWrite  doesnt_modify (fst (cms1 ! k)) x 
                 x  snd (cms2 ! k) GuarNoWrite  doesnt_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"
            using modified loc_modes locally_sound_mode_use_def
            by (metis snd (cms1 ! k) = snd (cms2 ! k) loc_reach.refl prod.collapse)
          moreover
          from sound_modes have "compatible_modes (map snd cms1)"
            by (metis globally_sound_modes_compatible sound_mode_use.simps)

          ultimately show "x  snd (cms1 ! 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;
                   ?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

        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 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

        have A_correct:
              " x.
               globally_consistent_var A (snd (cms1 ! i)) x 
               ?mems1i [↦ σ'] [∥1 A] x = ?mems1'i [↦ σ] x 
               ?mems2i [↦ σ'] [∥2 A] x = ?mems2'i [↦ σ] x"
        proof -
          fix x
          show "?thesis x"
            (is "?A  ?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)
            from p and diff have writable: "x  snd (cms1 ! 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 (?mems1'i [↦ σ] x, ?mems2'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 ?Eq1 ?Eq2
                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: "?mems1'i [↦ σ] x = v  ?mems2'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 (mem1' x, mem1' x)"
                  unfolding A_def
                  using x   dma x = Low
                  by auto
                from q have "mem1' x = mem2' 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
                  "?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)
            hence "globally_consistent_var A (snd (cms1 ! i)) x"
              by (auto simp: globally_consistent_var_def)
            moreover
            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

            ultimately show ?thesis
              by auto
          qed
        qed
        hence "?mems1i [↦ σ'] [∥1 A] = ?mems1'i [↦ σ] 
               ?mems2i [↦ σ'] [∥2 A] = ?mems2'i [↦ σ]"
          by auto
        moreover
        from A_correct have "globally_consistent A (snd (cms1 ! i))"
          by (metis Δ_finite globally_consistent_def domA)

        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 globally_consistent A (snd (cms1 ! i))
          apply (subst surjective_pairing[of "cms1 ! i"])
          apply (subst surjective_pairing[of "cms2 ! i"])
          by (metis surjective_pairing globally_consistent_adapt_bisim)

        ultimately show ?thesis
          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 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 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 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: "mem1 x = mem1' x" "mem2 x = mem2' x"
            "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 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 mem1' x = mem2' x  dma x = High show "x  ?X' i"
            by auto
        qed
      qed
    next
      { fix x
        have " i < length cms1. x  ?X' i"
        proof (cases "mem1 x  mem1' x  mem2 x  mem2' x")
          assume var_changed: "mem1 x  mem1' x  mem2 x  mem2' 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)"
          hence assms: "mem1 x = mem1' x" "mem2 x = mem2' 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
            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 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 x = Low"
  assumes x_readable: " i < length cms1. x  snd (cms1 ! i) AsmNoRead"
  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 σ = ?X j"
      by (metis dom_restrict_total)

    with 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 prod.collapse mm_equiv_low_eq)
    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 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  mem1 x = 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. 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 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. 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 (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) k(cms1', mem1')"
  shows " cms2' mem2' mems'. sound_mode_use (cms1', mem1') 
                              sound_mode_use (cms2', mem2') 
                              map snd cms1' = map snd cms2' 
                              (cms2, mem2) k(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 "k" arbitrary: cms1' mem1')
    case 0
    hence "cms1' = cms1  mem1' = mem1"
      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 cms1'' mem1'' where eval'':
      "(cms1, mem1) k(cms1'', mem1'')  (cms1'', mem1'')  (cms1', mem1')"
      by (metis meval_k.simps(2) prod_cases3 snd_conv)
    hence "(cms1'', mem1'')  (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) k(cms2'', mem2'') 
       makes_compatible (cms1'', mem1'') (cms2'', mem2'') mems''"
      using Suc
      by metis
    ultimately obtain cms2' mem2' mems' where
      "map snd cms1' = map snd cms2' 
       (cms2'', mem2'')  (cms2', mem2') 
       makes_compatible (cms1', mem1') (cms2', mem2') 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 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 (add_initial_modes cmds, mem1)
                          (add_initial_modes cmds, mem2)
                          (replicate (length cmds) (mem1, mem2))"
proof -
  let ?n = "length cmds"
  let ?mems = "replicate ?n (mem1, mem2)" and
      ?mdss = "replicate ?n mdss"
  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
    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 ?mems1i = "fst (?mems ! i)" and ?mems2i = "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 " mem1 mem2. mem1 =mdssl mem2 
      (zip cmds (replicate ?n mdss) ! i, mem1)  (zip cmds (replicate ?n mdss) ! i, mem2)"
      using com_sifum_secure_def low_indistinguishable_def
      by auto

    moreover
    from i have "?mems1i = mem1" "?mems2i = mem2"
      by auto
    with low_eq have "?mems1i [↦ σ] =mdssl ?mems2i [↦ σ]"
      by (auto simp: subst_def mdss_def low_mds_eq_def low_eq_def, case_tac "σ x", auto)

    ultimately show "(zip cmds ?mdss ! i, ?mems1i [↦ σ])  (zip cmds ?mdss ! i, ?mems2i [↦ σ])"
      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  mem1 =l mem2)  ( 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 mem1 mem2 :: "'Var  'Val"
  fix k cms1' mem1'
  let ?n = "length cmds"
  let ?mems = "zip (replicate ?n mem1) (replicate ?n mem2)"
  assume low_eq: "mem1 =l mem2"
  with com_secure have compat:
    "makes_compatible (add_initial_modes cmds, mem1) (add_initial_modes cmds, mem2) ?mems"
    by (metis compatible_refl fst_conv length_replicate map_replicate snd_conv zip_eq_conv)

  also assume eval: "(add_initial_modes cmds, mem1) k(cms1', mem1')"

  ultimately obtain cms2' mem2' mems'
    where p: "map snd cms1' = map snd cms2' 
             (add_initial_modes cmds, mem2) k(cms2', mem2') 
             makes_compatible (cms1', mem1') (cms2', mem2') mems'"
    using sound_modes makes_compatible_eval_k
    by blast

  thus " cms2' mem2'. (add_initial_modes cmds, mem2) k(cms2', mem2') 
                        map snd cms1' = map snd cms2' 
                        length cms2' = length cms1' 
                        ( x. dma x = Low  ( i < length cms1'. x  snd (cms1' ! i) AsmNoRead)
           mem1' x = mem2' x)"
    using p compat_low_eq
    by (metis length_map)
qed

end

end