[STATEMENT]
lemma differing_finite: "finite (differing_vars mem\<^sub>1 mem\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (differing_vars mem\<^sub>1 mem\<^sub>2)
[PROOF STEP]
by (metis UNIV_def Un_UNIV_left finite_Un finite_memory)


[STATEMENT]
lemma differing_lists_finite: "finite (differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i)
[PROOF STEP]
by (simp add: differing_finite differing_vars_lists_def)


[STATEMENT]
lemma subst_not_in_dom : "\<lbrakk> x \<notin> dom \<sigma> \<rbrakk> \<Longrightarrow> mem [\<mapsto> \<sigma>] x = mem x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom \<sigma> \<Longrightarrow> subst \<sigma> mem x = mem x
[PROOF STEP]
by (simp add: domIff subst_def)


[STATEMENT]
lemma makes_compatible_intro [intro]:
  "\<lbrakk> length cms\<^sub>1 = length cms\<^sub>2 \<and> length cms\<^sub>1 = length mems;
     (\<And> i \<sigma>. \<lbrakk> i < length cms\<^sub>1; dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<rbrakk> \<Longrightarrow>
          (cms\<^sub>1 ! i, (fst (mems ! i)) [\<mapsto> \<sigma>]) \<approx> (cms\<^sub>2 ! i, (snd (mems ! i)) [\<mapsto> \<sigma>]));
     (\<And> i x. \<lbrakk> i < length cms\<^sub>1; mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High \<rbrakk> \<Longrightarrow>
          x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i);
     (length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2) \<or>
     (\<forall> x. \<exists> i. i < length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i) \<rbrakk> \<Longrightarrow>
  makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length cms\<^sub>1 = length cms\<^sub>2 \<and> length cms\<^sub>1 = length mems; \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length cms\<^sub>1; dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> (cms\<^sub>1 ! i, subst \<sigma> (fst (mems ! i))) \<approx> (cms\<^sub>2 ! i, subst \<sigma> (snd (mems ! i))); \<And>i x. \<lbrakk>i \<sqsubset> length cms\<^sub>1; mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i; length cms\<^sub>1 = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length cms\<^sub>1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i)\<rbrakk> \<Longrightarrow> makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
[PROOF STEP]
by auto


[STATEMENT]
lemma compat_low:
  "\<lbrakk> makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems;
     i < length cms\<^sub>1;
     x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<rbrakk> \<Longrightarrow> dma x = Low"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems; i \<sqsubset> length cms\<^sub>1; x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> dma x = Low
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems; i \<sqsubset> length cms\<^sub>1; x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> dma x = Low
[PROOF STEP]
assume "i < length cms\<^sub>1" and *: "x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i" and
    "makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems"
[PROOF STATE]
proof (state)
this:
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems

goal (1 subgoal):
 1. \<lbrakk>makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems; i \<sqsubset> length cms\<^sub>1; x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> dma x = Low
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
[PROOF STEP]
have
    "(mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High) \<longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
[PROOF STATE]
proof (prove)
using this:
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High \<longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
[PROOF STEP]
by (simp add: Let_def, blast)
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High \<longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. \<lbrakk>makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems; i \<sqsubset> length cms\<^sub>1; x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> dma x = Low
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High \<longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
[PROOF STEP]
show "dma x = Low"
[PROOF STATE]
proof (prove)
using this:
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High \<longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. dma x = Low
[PROOF STEP]
by (cases "dma x") blast
[PROOF STATE]
proof (state)
this:
dma x = Low

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compat_different:
  "\<lbrakk> makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems;
     i < length cms\<^sub>1;
     x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<rbrakk> \<Longrightarrow> mem\<^sub>1 x \<noteq> mem\<^sub>2 x \<and> dma x = Low"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems; i \<sqsubset> length cms\<^sub>1; x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x \<noteq> mem\<^sub>2 x \<and> dma x = Low
[PROOF STEP]
by (cases "dma x", auto)


[STATEMENT]
lemma sound_modes_no_read :
  "\<lbrakk> sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i < length cms \<rbrakk> \<Longrightarrow>
  doesnt_read (fst (cms ! i)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
fix cms mem x i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
assume sound_modes: "sound_mode_use (cms, mem)" and "i < length cms"
[PROOF STATE]
proof (state)
this:
sound_mode_use (cms, mem)
i \<sqsubset> length cms

goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
hence "locally_sound_mode_use (cms ! i, mem)"
[PROOF STATE]
proof (prove)
using this:
sound_mode_use (cms, mem)
i \<sqsubset> length cms

goal (1 subgoal):
 1. locally_sound_mode_use (cms ! i, mem)
[PROOF STEP]
by (auto simp: sound_mode_use_def list_all_length)
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use (cms ! i, mem)

goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
locally_sound_mode_use (cms ! i, mem)

goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
assume "x \<in> (map snd cms ! i) GuarNoRead"
[PROOF STATE]
proof (state)
this:
x \<in> (map snd cms ! i) GuarNoRead

goal (1 subgoal):
 1. \<lbrakk>sound_mode_use (cms, mem); x \<in> (map snd cms ! i) GuarNoRead; i \<sqsubset> length cms\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
locally_sound_mode_use (cms ! i, mem)
x \<in> (map snd cms ! i) GuarNoRead
[PROOF STEP]
show "doesnt_read (fst (cms !i)) x"
[PROOF STATE]
proof (prove)
using this:
locally_sound_mode_use (cms ! i, mem)
x \<in> (map snd cms ! i) GuarNoRead

goal (1 subgoal):
 1. doesnt_read (fst (cms ! i)) x
[PROOF STEP]
apply (simp add: locally_sound_mode_use_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c' mds'. (\<exists>mem'. \<langle>c', mds', mem'\<rangle> \<in> loc_reach (cms ! i, mem)) \<longrightarrow> (\<forall>x. (x \<in> mds' GuarNoRead \<longrightarrow> doesnt_read c' x) \<and> (x \<in> mds' GuarNoWrite \<longrightarrow> doesnt_modify c' x)); x \<in> (map snd cms ! i) GuarNoRead\<rbrakk> \<Longrightarrow> doesnt_read (fst (cms ! i)) x
[PROOF STEP]
by (metis prod.exhaust \<open>i < length cms\<close> fst_conv loc_reach.refl nth_map snd_conv)
[PROOF STATE]
proof (state)
this:
doesnt_read (fst (cms ! i)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compat_different_vars:
  "\<lbrakk> fst (mems ! i) x = snd (mems ! i) x;
     x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<rbrakk> \<Longrightarrow>
    mem\<^sub>1 x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
assume "x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
[PROOF STATE]
proof (state)
this:
x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
hence "fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x
[PROOF STEP]
by (simp add: differing_vars_lists_def differing_vars_def)
[PROOF STATE]
proof (state)
this:
fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x

goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x

goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
assume "fst (mems ! i) x = snd (mems ! i) x"
[PROOF STATE]
proof (state)
this:
fst (mems ! i) x = snd (mems ! i) x

goal (1 subgoal):
 1. \<lbrakk>fst (mems ! i) x = snd (mems ! i) x; x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i\<rbrakk> \<Longrightarrow> mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x
fst (mems ! i) x = snd (mems ! i) x
[PROOF STEP]
show "mem\<^sub>1 x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
fst (mems ! i) x = mem\<^sub>1 x \<and> snd (mems ! i) x = mem\<^sub>2 x
fst (mems ! i) x = snd (mems ! i) x

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma differing_vars_subst [rule_format]:
  assumes dom\<sigma>: "dom \<sigma> \<supseteq> differing_vars mem\<^sub>1 mem\<^sub>2"
  shows "mem\<^sub>1 [\<mapsto> \<sigma>] = mem\<^sub>2 [\<mapsto> \<sigma>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst \<sigma> mem\<^sub>1 = subst \<sigma> mem\<^sub>2
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subst \<sigma> mem\<^sub>1 x = subst \<sigma> mem\<^sub>2 x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subst \<sigma> mem\<^sub>1 x = subst \<sigma> mem\<^sub>2 x
[PROOF STEP]
from dom\<sigma>
[PROOF STATE]
proof (chain)
picking this:
differing_vars mem\<^sub>1 mem\<^sub>2 \<subseteq> dom \<sigma>
[PROOF STEP]
show "mem\<^sub>1 [\<mapsto> \<sigma>] x = mem\<^sub>2 [\<mapsto> \<sigma>] x"
[PROOF STATE]
proof (prove)
using this:
differing_vars mem\<^sub>1 mem\<^sub>2 \<subseteq> dom \<sigma>

goal (1 subgoal):
 1. subst \<sigma> mem\<^sub>1 x = subst \<sigma> mem\<^sub>2 x
[PROOF STEP]
unfolding subst_def differing_vars_def
[PROOF STATE]
proof (prove)
using this:
{x. mem\<^sub>1 x \<noteq> mem\<^sub>2 x} \<subseteq> dom \<sigma>

goal (1 subgoal):
 1. (case \<sigma> x of None \<Rightarrow> mem\<^sub>1 x | Some v \<Rightarrow> v) = (case \<sigma> x of None \<Rightarrow> mem\<^sub>2 x | Some v \<Rightarrow> v)
[PROOF STEP]
by (cases "\<sigma> x", auto)
[PROOF STATE]
proof (state)
this:
subst \<sigma> mem\<^sub>1 x = subst \<sigma> mem\<^sub>2 x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mm_equiv_low_eq:
  "\<lbrakk> \<langle> c\<^sub>1, mds, mem\<^sub>1 \<rangle> \<approx> \<langle> c\<^sub>2, mds, mem\<^sub>2 \<rangle> \<rbrakk> \<Longrightarrow> mem\<^sub>1 =\<^bsub>mds\<^esub>\<^sup>l mem\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<Longrightarrow> mem\<^sub>1 =\<^bsub>mds\<^esub>\<^sup>l mem\<^sub>2
[PROOF STEP]
unfolding mm_equiv.simps strong_low_bisim_mm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<R> lc\<^sub>1 lc\<^sub>2. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> = lc\<^sub>1 \<and> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> = lc\<^sub>2 \<and> (sym \<R> \<and> closed_glob_consistent \<R> \<and> (\<forall>c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. (\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle>, \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>) \<in> \<R> \<longrightarrow> mem\<^sub>1 =\<^bsub>mds\<^esub>\<^sup>l mem\<^sub>2 \<and> (\<forall>c\<^sub>1' mds' mem\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<leadsto> \<langle>c\<^sub>1', mds', mem\<^sub>1'\<rangle> \<longrightarrow> (\<exists>c\<^sub>2' mem\<^sub>2'. \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<leadsto> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle> \<and> (\<langle>c\<^sub>1', mds', mem\<^sub>1'\<rangle>, \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle>) \<in> \<R>)))) \<and> (lc\<^sub>1, lc\<^sub>2) \<in> \<R> \<Longrightarrow> mem\<^sub>1 =\<^bsub>mds\<^esub>\<^sup>l mem\<^sub>2
[PROOF STEP]
by fast


[STATEMENT]
lemma globally_sound_modes_compatible:
  "\<lbrakk> globally_sound_mode_use (cms, mem) \<rbrakk> \<Longrightarrow> compatible_modes (map snd cms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. globally_sound_mode_use (cms, mem) \<Longrightarrow> compatible_modes (map snd cms)
[PROOF STEP]
by (simp add: globally_sound_mode_use_def reachable_mode_states_def, auto)


[STATEMENT]
lemma compatible_different_no_read :
  assumes sound_modes: "sound_mode_use (cms\<^sub>1, mem\<^sub>1)"
                       "sound_mode_use (cms\<^sub>2, mem\<^sub>2)"
  assumes compat: "makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems"
  assumes modes_eq: "map snd cms\<^sub>1 = map snd cms\<^sub>2"
  assumes ile: "i < length cms\<^sub>1"
  assumes x: "x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
  shows "doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
from compat
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
[PROOF STEP]
have len: "length cms\<^sub>1 = length cms\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems

goal (1 subgoal):
 1. length cms\<^sub>1 = length cms\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length cms\<^sub>1 = length cms\<^sub>2

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
let ?X\<^sub>i = "differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
from compat ile x
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
[PROOF STEP]
have a: "dma x = Low"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. dma x = Low
[PROOF STEP]
by (metis compat_low)
[PROOF STATE]
proof (state)
this:
dma x = Low

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
from compat ile x
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
[PROOF STEP]
have b: "mem\<^sub>1 x \<noteq> mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i

goal (1 subgoal):
 1. mem\<^sub>1 x \<noteq> mem\<^sub>2 x
[PROOF STEP]
by (metis compat_different)
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x \<noteq> mem\<^sub>2 x

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
with a and compat ile x
[PROOF STATE]
proof (chain)
picking this:
dma x = Low
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
mem\<^sub>1 x \<noteq> mem\<^sub>2 x
[PROOF STEP]
obtain j where
    jprop: "j < length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j"
[PROOF STATE]
proof (prove)
using this:
dma x = Low
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
i \<sqsubset> length cms\<^sub>1
x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
mem\<^sub>1 x \<noteq> mem\<^sub>2 x

goal (1 subgoal):
 1. (\<And>j. j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
let ?X\<^sub>j = "differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
obtain \<sigma> :: "'Var \<rightharpoonup> 'Val" where dom\<sigma>: "dom \<sigma> = ?X\<^sub>j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<sigma>. dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<sigma>. dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> dom ?\<sigma>12 = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
let ?\<sigma> = "\<lambda> x. if (x \<in> ?X\<^sub>j) then Some some_val else None"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<sigma>. dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j \<Longrightarrow> thesis) \<Longrightarrow> dom ?\<sigma>12 = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
show "dom ?\<sigma> = ?X\<^sub>j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j then Some some_val else None) = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
unfolding dom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. (if a \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j then Some some_val else None) \<noteq> None} = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom (\<lambda>x. if x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j then Some some_val else None) = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
let ?mdss = "map snd cms\<^sub>1" and
      ?mems\<^sub>1j = "fst (mems ! j)" and
      ?mems\<^sub>2j = "snd (mems ! j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
from jprop dom\<sigma>
[PROOF STATE]
proof (chain)
picking this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
have subst_eq:
  "?mems\<^sub>1j [\<mapsto> \<sigma>] x = ?mems\<^sub>1j x \<and> ?mems\<^sub>2j [\<mapsto> \<sigma>] x = ?mems\<^sub>2j x"
[PROOF STATE]
proof (prove)
using this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. subst \<sigma> (fst (mems ! j)) x = fst (mems ! j) x \<and> subst \<sigma> (snd (mems ! j)) x = snd (mems ! j) x
[PROOF STEP]
by (metis subst_not_in_dom)
[PROOF STATE]
proof (state)
this:
subst \<sigma> (fst (mems ! j)) x = fst (mems ! j) x \<and> subst \<sigma> (snd (mems ! j)) x = snd (mems ! j) x

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
from compat jprop dom\<sigma>
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
[PROOF STEP]
have "(cms\<^sub>1 ! j, ?mems\<^sub>1j [\<mapsto> \<sigma>]) \<approx> (cms\<^sub>2 ! j, ?mems\<^sub>2j [\<mapsto> \<sigma>])"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (cms\<^sub>1, mem\<^sub>1) (cms\<^sub>2, mem\<^sub>2) mems
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. (cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
hence low_eq: "?mems\<^sub>1j [\<mapsto> \<sigma>] =\<^bsub>?mdss ! j\<^esub>\<^sup>l ?mems\<^sub>2j [\<mapsto> \<sigma>]"
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))

goal (1 subgoal):
 1. subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
[PROOF STEP]
using modes_eq
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1 ! j, subst \<sigma> (fst (mems ! j))) \<approx> (cms\<^sub>2 ! j, subst \<sigma> (snd (mems ! j)))
map snd cms\<^sub>1 = map snd cms\<^sub>2

goal (1 subgoal):
 1. subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
[PROOF STEP]
by (metis (no_types) jprop len mm_equiv_low_eq nth_map surjective_pairing)
[PROOF STATE]
proof (state)
this:
subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
with jprop and b
[PROOF STATE]
proof (chain)
picking this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
mem\<^sub>1 x \<noteq> mem\<^sub>2 x
subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
[PROOF STEP]
have "x \<in> (?mdss ! j) AsmNoRead"
[PROOF STATE]
proof (prove)
using this:
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j
mem\<^sub>1 x \<noteq> mem\<^sub>2 x
subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))

goal (1 subgoal):
 1. x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
assume "x \<notin> (?mdss ! j) AsmNoRead"
[PROOF STATE]
proof (state)
this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead

goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
have mems_eq: "?mems\<^sub>1j x = ?mems\<^sub>2j x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead

goal (1 subgoal):
 1. fst (mems ! j) x = snd (mems ! j) x
[PROOF STEP]
using \<open>dma x = Low\<close> low_eq subst_eq
[PROOF STATE]
proof (prove)
using this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead
dma x = Low
subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))
subst \<sigma> (fst (mems ! j)) x = fst (mems ! j) x \<and> subst \<sigma> (snd (mems ! j)) x = snd (mems ! j) x

goal (1 subgoal):
 1. fst (mems ! j) x = snd (mems ! j) x
[PROOF STEP]
by (metis (full_types) low_mds_eq_def subst_eq)
[PROOF STATE]
proof (state)
this:
fst (mems ! j) x = snd (mems ! j) x

goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
hence "mem\<^sub>1 x = mem\<^sub>2 x"
[PROOF STATE]
proof (prove)
using this:
fst (mems ! j) x = snd (mems ! j) x

goal (1 subgoal):
 1. mem\<^sub>1 x = mem\<^sub>2 x
[PROOF STEP]
by (metis compat_different_vars jprop)
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 x = mem\<^sub>2 x

goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
mem\<^sub>1 x = mem\<^sub>2 x

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis b)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead \<Longrightarrow> False

goal (1 subgoal):
 1. \<lbrakk>j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j; mem\<^sub>1 x \<noteq> mem\<^sub>2 x; subst \<sigma> (fst (mems ! j)) =\<^bsub>map snd cms\<^sub>1 ! j\<^esub>\<^sup>l subst \<sigma> (snd (mems ! j))\<rbrakk> \<Longrightarrow> x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> (map snd cms\<^sub>1 ! j) AsmNoRead \<Longrightarrow> False

goal (1 subgoal):
 1. x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
hence "x \<in> (?mdss ! i) GuarNoRead"
[PROOF STATE]
proof (prove)
using this:
x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead

goal (1 subgoal):
 1. x \<in> (map snd cms\<^sub>1 ! i) GuarNoRead
[PROOF STEP]
using sound_modes jprop
[PROOF STATE]
proof (prove)
using this:
x \<in> (map snd cms\<^sub>1 ! j) AsmNoRead
sound_mode_use (cms\<^sub>1, mem\<^sub>1)
sound_mode_use (cms\<^sub>2, mem\<^sub>2)
j \<sqsubset> length cms\<^sub>1 \<and> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems j

goal (1 subgoal):
 1. x \<in> (map snd cms\<^sub>1 ! i) GuarNoRead
[PROOF STEP]
by (metis compatible_modes_def globally_sound_modes_compatible
      length_map sound_mode_use.simps x ile)
[PROOF STATE]
proof (state)
this:
x \<in> (map snd cms\<^sub>1 ! i) GuarNoRead

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
thus "doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x"
[PROOF STATE]
proof (prove)
using this:
x \<in> (map snd cms\<^sub>1 ! i) GuarNoRead

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
using sound_modes ile
[PROOF STATE]
proof (prove)
using this:
x \<in> (map snd cms\<^sub>1 ! i) GuarNoRead
sound_mode_use (cms\<^sub>1, mem\<^sub>1)
sound_mode_use (cms\<^sub>2, mem\<^sub>2)
i \<sqsubset> length cms\<^sub>1

goal (1 subgoal):
 1. doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x
[PROOF STEP]
by (metis len modes_eq sound_modes_no_read)
[PROOF STATE]
proof (state)
this:
doesnt_read (fst (cms\<^sub>1 ! i)) x \<and> doesnt_read (fst (cms\<^sub>2 ! i)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma change_respecting_dom_unique:
  "\<lbrakk> change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> X g \<rbrakk> \<Longrightarrow>
   \<exists> d. \<forall> f. dom f = X \<longrightarrow> d = dom (g f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> X g \<Longrightarrow> \<exists>d. \<forall>f. dom f = X \<longrightarrow> d = dom (g f)
[PROOF STEP]
by (metis change_respecting.simps)


[STATEMENT]
lemma func_le_restrict: "\<lbrakk> f \<preceq> g; X \<subseteq> dom f \<rbrakk> \<Longrightarrow> f |` X \<preceq> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<preceq> g; X \<subseteq> dom f\<rbrakk> \<Longrightarrow> f |` X \<preceq> g
[PROOF STEP]
by (auto simp: func_le_def)


[STATEMENT]
lemma func_le_dom: "f \<preceq> g \<Longrightarrow> dom f \<subseteq> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<preceq> g \<Longrightarrow> dom f \<subseteq> dom g
[PROOF STEP]
by (auto simp add: func_le_def, metis domIff option.simps(2))


[STATEMENT]
lemma doesnt_read_mutually_exclusive:
  assumes noread: "doesnt_read c x"
  assumes eval: "\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>"
  assumes unchanged: "\<forall> v. \<langle>c, mds, mem (x := v)\<rangle> \<leadsto> \<langle>c', mds', mem' (x := v)\<rangle>"
  shows "\<not> (\<forall> v. \<langle>c, mds, mem (x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
doesnt_read c x
\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>
\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'(x := v)\<rangle>

goal (1 subgoal):
 1. \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)
[PROOF STEP]
apply (case_tac "mem' x = some_val")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>doesnt_read c x; \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>; \<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'(x := v)\<rangle>; mem' x = some_val\<rbrakk> \<Longrightarrow> \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)
 2. \<lbrakk>doesnt_read c x; \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>; \<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'(x := v)\<rangle>; mem' x \<noteq> some_val\<rbrakk> \<Longrightarrow> \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)
[PROOF STEP]
apply (metis (full_types) prod.inject deterministic different_values fun_upd_same)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>doesnt_read c x; \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>; \<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'(x := v)\<rangle>; mem' x \<noteq> some_val\<rbrakk> \<Longrightarrow> \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>)
[PROOF STEP]
by (metis (full_types) prod.inject deterministic fun_upd_same)


[STATEMENT]
lemma doesnt_read_mutually_exclusive':
  assumes noread: "doesnt_read c x"
  assumes eval: "\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>"
  assumes overwrite: "\<forall> v. \<langle>c, mds, mem (x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>"
  shows "\<not> (\<forall> v. \<langle>c, mds, mem (x := v)\<rangle> \<leadsto> \<langle>c', mds', mem' (x := v)\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>v. \<langle>c, mds, mem(x := v)\<rangle> \<leadsto> \<langle>c', mds', mem'(x := v)\<rangle>)
[PROOF STEP]
by (metis assms doesnt_read_mutually_exclusive)


[STATEMENT]
lemma change_respecting_dom:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X g"
  assumes dom\<sigma>: "dom \<sigma> = X"
  shows "dom (g \<sigma>) \<subseteq> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (g \<sigma>) \<subseteq> X
[PROOF STEP]
by (metis assms change_respecting.simps func_le_dom)


[STATEMENT]
lemma change_respecting_intro [iff]:
  "\<lbrakk> \<langle> c, mds, mem \<rangle> \<leadsto> \<langle> c', mds', mem' \<rangle>;
     \<And> f. dom f = X \<Longrightarrow>
           g f \<preceq> f \<and>
           (\<forall> f'. dom f' = X \<longrightarrow> dom (g f) = dom (g f')) \<and>
           (\<langle> c, mds, mem [\<mapsto> f] \<rangle> \<leadsto> \<langle> c', mds', mem' [\<mapsto> g f] \<rangle>) \<rbrakk>
  \<Longrightarrow> change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> X g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>; \<And>f. dom f = X \<Longrightarrow> g f \<preceq> f \<and> (\<forall>f'. dom f' = X \<longrightarrow> dom (g f) = dom (g f')) \<and> \<langle>c, mds, subst f mem\<rangle> \<leadsto> \<langle>c', mds', subst (g f) mem'\<rangle>\<rbrakk> \<Longrightarrow> change_respecting \<langle>c, mds, mem\<rangle> \<langle>c', mds', mem'\<rangle> X g
[PROOF STEP]
unfolding change_respecting.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle>; \<And>f. dom f = X \<Longrightarrow> g f \<preceq> f \<and> (\<forall>f'. dom f' = X \<longrightarrow> dom (g f) = dom (g f')) \<and> \<langle>c, mds, subst f mem\<rangle> \<leadsto> \<langle>c', mds', subst (g f) mem'\<rangle>\<rbrakk> \<Longrightarrow> \<langle>c, mds, mem\<rangle> \<leadsto> \<langle>c', mds', mem'\<rangle> \<and> (\<forall>\<sigma>. dom \<sigma> = X \<longrightarrow> g \<sigma> \<preceq> \<sigma>) \<and> (\<forall>\<sigma> \<sigma>'. dom \<sigma> = X \<and> dom \<sigma>' = X \<longrightarrow> dom (g \<sigma>) = dom (g \<sigma>')) \<and> (\<forall>\<sigma>. dom \<sigma> = X \<longrightarrow> \<langle>c, mds, subst \<sigma> mem\<rangle> \<leadsto> \<langle>c', mds', subst (g \<sigma>) mem'\<rangle>)
[PROOF STEP]
by blast


[STATEMENT]
lemma conjI3: "\<lbrakk> A; B; C \<rbrakk> \<Longrightarrow> A \<and> B \<and> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A \<and> B \<and> C
[PROOF STEP]
by simp