[STATEMENT]
lemma differing_vars_neg: "x \<notin> differing_vars_lists mem1 mem2 mems i \<Longrightarrow>
  (fst (mems ! i) x = mem1 x \<and> snd (mems ! i) x = mem2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> differing_vars_lists mem1 mem2 mems i \<Longrightarrow> fst (mems ! i) x = mem1 x \<and> snd (mems ! i) x = mem2 x
[PROOF STEP]
by (simp add: differing_vars_lists_def differing_vars_def)


[STATEMENT]
lemma differing_vars_neg_intro:
  "\<lbrakk> mem\<^sub>1 x = fst (mems ! i) x;
  mem\<^sub>2 x = snd (mems ! i) x \<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mem\<^sub>1 x = fst (mems ! i) x; mem\<^sub>2 x = snd (mems ! i) x\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i
[PROOF STEP]
by (auto simp: differing_vars_lists_def differing_vars_def)


[STATEMENT]
lemma differing_vars_elim [elim]:
  "x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<Longrightarrow>
  (fst (mems ! i) x \<noteq> mem\<^sub>1 x) \<or> (snd (mems ! i) x \<noteq> mem\<^sub>2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> differing_vars_lists mem\<^sub>1 mem\<^sub>2 mems i \<Longrightarrow> fst (mems ! i) x \<noteq> mem\<^sub>1 x \<or> snd (mems ! i) x \<noteq> mem\<^sub>2 x
[PROOF STEP]
by (auto simp: differing_vars_lists_def differing_vars_def)


[STATEMENT]
lemma subst_overrides: "dom \<sigma> = dom \<tau> \<Longrightarrow> mem [\<mapsto> \<tau>] [\<mapsto> \<sigma>] = mem [\<mapsto> \<sigma>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom \<sigma> = dom \<tau> \<Longrightarrow> subst \<sigma> (subst \<tau> mem) = subst \<sigma> mem
[PROOF STEP]
unfolding subst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom \<sigma> = dom \<tau> \<Longrightarrow> (\<lambda>x. case \<sigma> x of None \<Rightarrow> case \<tau> x of None \<Rightarrow> mem x | Some v \<Rightarrow> v | Some v \<Rightarrow> v) = (\<lambda>x. case \<sigma> x of None \<Rightarrow> mem x | Some v \<Rightarrow> v)
[PROOF STEP]
by (metis domIff option.exhaust option.simps(4) option.simps(5))


[STATEMENT]
lemma dom_restrict_total: "dom (to_partial f |` X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (to_partial f |` X) = X
[PROOF STEP]
unfolding to_partial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom ((\<lambda>x. Some (f x)) |` X) = X
[PROOF STEP]
by (metis Int_UNIV_left dom_const dom_restrict)


[STATEMENT]
lemma update_nth_eq:
  "\<lbrakk> xs = ys; n < length xs \<rbrakk> \<Longrightarrow> xs = ys [n := xs ! n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = ys; n \<sqsubset> length xs\<rbrakk> \<Longrightarrow> xs = ys[n := xs ! n]
[PROOF STEP]
by (metis list_update_id)


[STATEMENT]
lemma mm_equiv_step:
  assumes bisim: "(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2)"
  assumes modes_eq: "snd cms\<^sub>1 = snd cms\<^sub>2"
  assumes step: "(cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1')"
  shows "\<exists> c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle> c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2' \<rangle> \<and>
  (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle> c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2' \<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
using assms mm_equiv_strong_low_bisim
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2)
snd cms\<^sub>1 = snd cms\<^sub>2
(cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1')
strong_low_bisim_mm mm_equiv

goal (1 subgoal):
 1. \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
unfolding strong_low_bisim_mm_def
[PROOF STATE]
proof (prove)
using this:
(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2)
snd cms\<^sub>1 = snd cms\<^sub>2
(cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1')
sym mm_equiv \<and> closed_glob_consistent mm_equiv \<and> (\<forall>c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<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 \<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> \<approx> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle>)))

goal (1 subgoal):
 1. \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2); snd cms\<^sub>1 = snd cms\<^sub>2; (cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1'); sym mm_equiv; closed_glob_consistent mm_equiv; \<forall>c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<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 \<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> \<approx> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle>))\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
apply (erule_tac x = "fst cms\<^sub>1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2); snd cms\<^sub>1 = snd cms\<^sub>2; (cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1'); sym mm_equiv; closed_glob_consistent mm_equiv; \<forall>mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<langle>fst cms\<^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 \<and> (\<forall>c\<^sub>1' mds' mem\<^sub>1'. \<langle>fst cms\<^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> \<approx> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle>))\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
apply (erule_tac x = "snd cms\<^sub>1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cms\<^sub>1, mem\<^sub>1) \<approx> (cms\<^sub>2, mem\<^sub>2); snd cms\<^sub>1 = snd cms\<^sub>2; (cms\<^sub>1, mem\<^sub>1) \<leadsto> (cms\<^sub>1', mem\<^sub>1'); sym mm_equiv; closed_glob_consistent mm_equiv; \<forall>mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<langle>fst cms\<^sub>1, snd cms\<^sub>1, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, snd cms\<^sub>1, mem\<^sub>2\<rangle> \<longrightarrow> mem\<^sub>1 =\<^bsub>snd cms\<^sub>1\<^esub>\<^sup>l mem\<^sub>2 \<and> (\<forall>c\<^sub>1' mds' mem\<^sub>1'. \<langle>fst cms\<^sub>1, snd cms\<^sub>1, 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, snd cms\<^sub>1, mem\<^sub>2\<rangle> \<leadsto> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle> \<and> \<langle>c\<^sub>1', mds', mem\<^sub>1'\<rangle> \<approx> \<langle>c\<^sub>2', mds', mem\<^sub>2'\<rangle>))\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>2' mem\<^sub>2'. (cms\<^sub>2, mem\<^sub>2) \<leadsto> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle> \<and> (cms\<^sub>1', mem\<^sub>1') \<approx> \<langle>c\<^sub>2', snd cms\<^sub>1', mem\<^sub>2'\<rangle>
[PROOF STEP]
by (metis surjective_pairing)


[STATEMENT]
lemma change_respecting_doesnt_modify:
  assumes cr: "change_respecting (cms, mem) (cms', mem') X g"
  assumes eval: "(cms, mem) \<leadsto> (cms', mem')"
  assumes domf: "dom f = X"
  assumes x_in_dom: "x \<in> dom (g f)"
  assumes noread: "doesnt_read (fst cms) x"
  shows "mem x = mem' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
let ?f' = "to_partial mem |` X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
have domf': "dom ?f' = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (to_partial mem |` X) = X
[PROOF STEP]
by (metis dom_restrict_total)
[PROOF STATE]
proof (state)
this:
dom (to_partial mem |` X) = X

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
from cr and eval
[PROOF STATE]
proof (chain)
picking this:
change_respecting (cms, mem) (cms', mem') X g
(cms, mem) \<leadsto> (cms', mem')
[PROOF STEP]
have "\<forall> f. dom f = X \<longrightarrow> (cms, mem [\<mapsto> f]) \<leadsto> (cms', mem' [\<mapsto> g f])"
[PROOF STATE]
proof (prove)
using this:
change_respecting (cms, mem) (cms', mem') X g
(cms, mem) \<leadsto> (cms', mem')

goal (1 subgoal):
 1. \<forall>f. dom f = X \<longrightarrow> (cms, subst f mem) \<leadsto> (cms', subst (g f) mem')
[PROOF STEP]
unfolding change_respecting.simps
[PROOF STATE]
proof (prove)
using this:
(cms, mem) \<leadsto> (cms', mem') \<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> (cms, subst \<sigma> mem) \<leadsto> (cms', subst (g \<sigma>) mem'))
(cms, mem) \<leadsto> (cms', mem')

goal (1 subgoal):
 1. \<forall>f. dom f = X \<longrightarrow> (cms, subst f mem) \<leadsto> (cms', subst (g f) mem')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>f. dom f = X \<longrightarrow> (cms, subst f mem) \<leadsto> (cms', subst (g f) mem')

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
hence eval': "(cms, mem [\<mapsto> ?f']) \<leadsto> (cms', mem' [\<mapsto> g ?f'])"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. dom f = X \<longrightarrow> (cms, subst f mem) \<leadsto> (cms', subst (g f) mem')

goal (1 subgoal):
 1. (cms, subst (to_partial mem |` X) mem) \<leadsto> (cms', subst (g (to_partial mem |` X)) mem')
[PROOF STEP]
by (metis domf')
[PROOF STATE]
proof (state)
this:
(cms, subst (to_partial mem |` X) mem) \<leadsto> (cms', subst (g (to_partial mem |` X)) mem')

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
have mem_eq: "mem [\<mapsto> ?f'] = mem"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (to_partial mem |` X) mem = mem
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subst (to_partial mem |` X) mem x = mem x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. subst (to_partial mem |` X) mem x = mem x
[PROOF STEP]
show "mem [\<mapsto> ?f'] x = mem x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (to_partial mem |` X) mem x = mem x
[PROOF STEP]
unfolding subst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (to_partial mem |` X) x of None \<Rightarrow> mem x | Some v \<Rightarrow> v) = mem x
[PROOF STEP]
apply (cases "x \<in> X")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> X \<Longrightarrow> (case (to_partial mem |` X) x of None \<Rightarrow> mem x | Some v \<Rightarrow> v) = mem x
 2. x \<notin> X \<Longrightarrow> (case (to_partial mem |` X) x of None \<Rightarrow> mem x | Some v \<Rightarrow> v) = mem x
[PROOF STEP]
apply (metis option.simps(5) restrict_in to_partial_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> X \<Longrightarrow> (case (to_partial mem |` X) x of None \<Rightarrow> mem x | Some v \<Rightarrow> v) = mem x
[PROOF STEP]
by (metis domf' subst_def subst_not_in_dom)
[PROOF STATE]
proof (state)
this:
subst (to_partial mem |` X) mem x = mem x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst (to_partial mem |` X) mem = mem

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
subst (to_partial mem |` X) mem = mem
[PROOF STEP]
have mem'_eq: "mem' [\<mapsto> g ?f'] = mem'"
[PROOF STATE]
proof (prove)
using this:
subst (to_partial mem |` X) mem = mem

goal (1 subgoal):
 1. subst (g (to_partial mem |` X)) mem' = mem'
[PROOF STEP]
using eval eval' deterministic
[PROOF STATE]
proof (prove)
using this:
subst (to_partial mem |` X) mem = mem
(cms, mem) \<leadsto> (cms', mem')
(cms, subst (to_partial mem |` X) mem) \<leadsto> (cms', subst (g (to_partial mem |` X)) mem')
\<lbrakk>?lc \<leadsto> ?lc'; ?lc \<leadsto> ?lc''\<rbrakk> \<Longrightarrow> ?lc' = ?lc''

goal (1 subgoal):
 1. subst (g (to_partial mem |` X)) mem' = mem'
[PROOF STEP]
by (metis Pair_inject)
[PROOF STATE]
proof (state)
this:
subst (g (to_partial mem |` X)) mem' = mem'

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subst (g (to_partial mem |` X)) mem' = mem'

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
have "dom (g ?f') = dom (g f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (g (to_partial mem |` X)) = dom (g f)
[PROOF STEP]
by (metis change_respecting.simps cr domf domf')
[PROOF STATE]
proof (state)
this:
dom (g (to_partial mem |` X)) = dom (g f)

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
hence x_in_dom': "x \<in> dom (g ?f')"
[PROOF STATE]
proof (prove)
using this:
dom (g (to_partial mem |` X)) = dom (g f)

goal (1 subgoal):
 1. x \<in> dom (g (to_partial mem |` X))
[PROOF STEP]
by (metis x_in_dom)
[PROOF STATE]
proof (state)
this:
x \<in> dom (g (to_partial mem |` X))

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
have "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X
[PROOF STEP]
by (metis change_respecting.simps cr domf func_le_dom in_mono x_in_dom)
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
hence "?f' x = Some (mem x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. (to_partial mem |` X) x = Some (mem x)
[PROOF STEP]
by (metis restrict_in to_partial_def)
[PROOF STATE]
proof (state)
this:
(to_partial mem |` X) x = Some (mem x)

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
hence "g ?f' x = Some (mem x)"
[PROOF STATE]
proof (prove)
using this:
(to_partial mem |` X) x = Some (mem x)

goal (1 subgoal):
 1. g (to_partial mem |` X) x = Some (mem x)
[PROOF STEP]
using cr func_le_def
[PROOF STATE]
proof (prove)
using this:
(to_partial mem |` X) x = Some (mem x)
change_respecting (cms, mem) (cms', mem') X g
?f \<preceq> ?g = (\<forall>x\<in>dom ?f. ?f x = ?g x)

goal (1 subgoal):
 1. g (to_partial mem |` X) x = Some (mem x)
[PROOF STEP]
by (metis change_respecting.simps domf' x_in_dom')
[PROOF STATE]
proof (state)
this:
g (to_partial mem |` X) x = Some (mem x)

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
hence "mem' [\<mapsto> g ?f'] x = mem x"
[PROOF STATE]
proof (prove)
using this:
g (to_partial mem |` X) x = Some (mem x)

goal (1 subgoal):
 1. subst (g (to_partial mem |` X)) mem' x = mem x
[PROOF STEP]
using subst_def x_in_dom'
[PROOF STATE]
proof (prove)
using this:
g (to_partial mem |` X) x = Some (mem x)
subst ?f ?mem = (\<lambda>x. case ?f x of None \<Rightarrow> ?mem x | Some v \<Rightarrow> v)
x \<in> dom (g (to_partial mem |` X))

goal (1 subgoal):
 1. subst (g (to_partial mem |` X)) mem' x = mem x
[PROOF STEP]
by (metis option.simps(5))
[PROOF STATE]
proof (state)
this:
subst (g (to_partial mem |` X)) mem' x = mem x

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
thus "mem x = mem' x"
[PROOF STATE]
proof (prove)
using this:
subst (g (to_partial mem |` X)) mem' x = mem x

goal (1 subgoal):
 1. mem x = mem' x
[PROOF STEP]
by (metis mem'_eq)
[PROOF STATE]
proof (state)
this:
mem x = mem' x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma differing_empty_eq:
  "\<lbrakk> differing_vars mem mem' = {} \<rbrakk> \<Longrightarrow> mem = mem'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. differing_vars mem mem' = {} \<Longrightarrow> mem = mem'
[PROOF STEP]
unfolding differing_vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. mem x \<noteq> mem' x} = {} \<Longrightarrow> mem = mem'
[PROOF STEP]
by auto


[STATEMENT]
lemma globally_consistent_dom:
  "\<lbrakk> globally_consistent A mds; X \<subseteq> dom A \<rbrakk> \<Longrightarrow> globally_consistent (A |` X) mds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globally_consistent A mds; X \<subseteq> dom A\<rbrakk> \<Longrightarrow> globally_consistent (A |` X) mds
[PROOF STEP]
unfolding globally_consistent_def globally_consistent_var_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite (dom A) \<and> (\<forall>x\<in>dom A. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v')); X \<subseteq> dom A\<rbrakk> \<Longrightarrow> finite (dom (A |` X)) \<and> (\<forall>x\<in>dom (A |` X). case (A |` X) x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v'))
[PROOF STEP]
by (metis (no_types) IntE dom_restrict inf_absorb2 restrict_in rev_finite_subset)


[STATEMENT]
lemma globally_consistent_writable:
  "\<lbrakk> x \<in> dom A; globally_consistent A mds \<rbrakk> \<Longrightarrow> x \<notin> mds AsmNoWrite"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> x \<notin> mds AsmNoWrite
[PROOF STEP]
unfolding globally_consistent_def globally_consistent_var_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom A; finite (dom A) \<and> (\<forall>x\<in>dom A. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v'))\<rbrakk> \<Longrightarrow> x \<notin> mds AsmNoWrite
[PROOF STEP]
by (metis (no_types) domD option.simps(5) split_part)


[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. v = v'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = v'
[PROOF STEP]
from some
[PROOF STATE]
proof (chain)
picking this:
A x = Some (v, v')
[PROOF STEP]
have "x \<in> dom A"
[PROOF STATE]
proof (prove)
using this:
A x = Some (v, v')

goal (1 subgoal):
 1. x \<in> dom A
[PROOF STEP]
by (metis domI)
[PROOF STATE]
proof (state)
this:
x \<in> dom A

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
hence "case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> (dma x = Low \<longrightarrow> v = v')"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom A

goal (1 subgoal):
 1. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'
[PROOF STEP]
using globally_consistent
[PROOF STATE]
proof (prove)
using this:
x \<in> dom A
globally_consistent A mds

goal (1 subgoal):
 1. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'
[PROOF STEP]
unfolding globally_consistent_def globally_consistent_var_def
[PROOF STATE]
proof (prove)
using this:
x \<in> dom A
finite (dom A) \<and> (\<forall>x\<in>dom A. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v'))

goal (1 subgoal):
 1. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'
[PROOF STEP]
by (metis option.simps(5) some split_part)
[PROOF STATE]
proof (state)
this:
case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
with \<open>dma x = Low\<close>
[PROOF STATE]
proof (chain)
picking this:
dma x = Low
case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dma x = Low
case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
unfolding some
[PROOF STATE]
proof (prove)
using this:
dma x = Low
case Some (v, v') of None \<Rightarrow> True | Some (v, v') \<Rightarrow> dma x = Low \<longrightarrow> v = v'

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma globally_consistent_adapt_bisim:
  assumes bisim: "\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>"
  assumes globally_consistent: "globally_consistent A mds"
  shows "\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
from globally_consistent
[PROOF STATE]
proof (chain)
picking this:
globally_consistent A mds
[PROOF STEP]
have "finite (dom A)"
[PROOF STATE]
proof (prove)
using this:
globally_consistent A mds

goal (1 subgoal):
 1. finite (dom A)
[PROOF STEP]
by (auto simp: globally_consistent_def)
[PROOF STATE]
proof (state)
this:
finite (dom A)

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (dom A)

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
using globally_consistent
[PROOF STATE]
proof (prove)
using this:
finite (dom A)
globally_consistent A mds

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
proof (induct "dom A" arbitrary: A rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} = dom A
globally_consistent A mds

goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
hence "\<And> x. A x = None"
[PROOF STATE]
proof (prove)
using this:
{} = dom A
globally_consistent A mds

goal (1 subgoal):
 1. \<And>x. A x = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A ?x5 = None

goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
hence "mem\<^sub>1 [\<parallel>\<^sub>1 A] = mem\<^sub>1" and "mem\<^sub>2 [\<parallel>\<^sub>2 A] = mem\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
A ?x5 = None

goal (1 subgoal):
 1. mem\<^sub>1 [\<parallel>\<^sub>1 A] = mem\<^sub>1 &&& mem\<^sub>2 [\<parallel>\<^sub>2 A] = mem\<^sub>2
[PROOF STEP]
unfolding apply_adaptation_def
[PROOF STATE]
proof (prove)
using this:
A ?x5 = None

goal (1 subgoal):
 1. (\<lambda>x. case A x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb) = mem\<^sub>1 &&& (\<lambda>x. case A x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb) = mem\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 [\<parallel>\<^sub>1 A] = mem\<^sub>1
mem\<^sub>2 [\<parallel>\<^sub>2 A] = mem\<^sub>2

goal (2 subgoals):
 1. \<And>A. \<lbrakk>{} = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
with bisim
[PROOF STATE]
proof (chain)
picking this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>
mem\<^sub>1 [\<parallel>\<^sub>1 A] = mem\<^sub>1
mem\<^sub>2 [\<parallel>\<^sub>2 A] = mem\<^sub>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>
mem\<^sub>1 [\<parallel>\<^sub>1 A] = mem\<^sub>1
mem\<^sub>2 [\<parallel>\<^sub>2 A] = mem\<^sub>2

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
case (insert x X)
[PROOF STATE]
proof (state)
this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
define A' where "A' = A |` X"
[PROOF STATE]
proof (state)
this:
A' = A |` X

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
hence "dom A' = X"
[PROOF STATE]
proof (prove)
using this:
A' = A |` X

goal (1 subgoal):
 1. dom A' = X
[PROOF STEP]
by (metis Int_insert_left_if0 dom_restrict inf_absorb2 insert(2) insert(4) order_refl)
[PROOF STATE]
proof (state)
this:
dom A' = X

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom A' = X

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds
[PROOF STEP]
have "globally_consistent A' mds"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds

goal (1 subgoal):
 1. globally_consistent A' mds
[PROOF STEP]
by (metis A'_def globally_consistent_dom subset_insertI)
[PROOF STATE]
proof (state)
this:
globally_consistent A' mds

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dom A' = X
globally_consistent A' mds
[PROOF STEP]
have bisim': "\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>"
[PROOF STATE]
proof (prove)
using this:
dom A' = X
globally_consistent A' mds

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
dom A' = X
globally_consistent A' mds
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
with insert
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>
[PROOF STEP]
have writable: "x \<notin> mds AsmNoWrite"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A']\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A']\<rangle>

goal (1 subgoal):
 1. x \<notin> mds AsmNoWrite
[PROOF STEP]
by (metis globally_consistent_writable insertI1)
[PROOF STATE]
proof (state)
this:
x \<notin> mds AsmNoWrite

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds
[PROOF STEP]
obtain v v' where "A x = Some (v, v')"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; globally_consistent ?A5 mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
globally_consistent A mds

goal (1 subgoal):
 1. (\<And>v v'. A x = Some (v, v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding globally_consistent_def globally_consistent_var_def
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X = dom ?A5; finite (dom ?A5) \<and> (\<forall>x\<in>dom ?A5. case ?A5 x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v'))\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 ?A5]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 ?A5]\<rangle>
insert x X = dom A
finite (dom A) \<and> (\<forall>x\<in>dom A. case A x of None \<Rightarrow> True | Some (v, v') \<Rightarrow> x \<notin> mds AsmNoWrite \<and> (dma x = Low \<longrightarrow> v = v'))

goal (1 subgoal):
 1. (\<And>v v'. A x = Some (v, v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types) domD insert_iff option.simps(5) case_prodE)
[PROOF STATE]
proof (state)
this:
A x = Some (v, v')

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
have A_A': "\<And> y. y \<noteq> x \<Longrightarrow> A y = A' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<noteq> x \<Longrightarrow> A y = A' y
[PROOF STEP]
unfolding A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<noteq> x \<Longrightarrow> A y = (A |` X) y
[PROOF STEP]
by (metis domIff insert(4) insert_iff restrict_in restrict_out)
[PROOF STATE]
proof (state)
this:
?y5 \<noteq> x \<Longrightarrow> A ?y5 = A' ?y5

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
(* The following equalities may have more elegant proofs, but
        this should suffice, since the propositions are
        quite obvious. *)
[PROOF STATE]
proof (state)
this:
?y5 \<noteq> x \<Longrightarrow> A ?y5 = A' ?y5

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
have eq\<^sub>1: "mem\<^sub>1 [\<parallel>\<^sub>1 A'] (x := v) = mem\<^sub>1 [\<parallel>\<^sub>1 A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v) = mem\<^sub>1 [\<parallel>\<^sub>1 A]
[PROOF STEP]
unfolding apply_adaptation_def A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)(x := v) = (\<lambda>x. case A x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)
[PROOF STEP]
apply (rule ext, rename_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)(x := v)) y = (case A y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb)
[PROOF STEP]
apply (case_tac "x = y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. x = y \<Longrightarrow> ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)(x := v)) y = (case A y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb)
 2. \<And>y. x \<noteq> y \<Longrightarrow> ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)(x := v)) y = (case A y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. v = (case A x of None \<Rightarrow> mem\<^sub>1 x | Some (xa, xb) \<Rightarrow> if True then xa else xb)
 2. \<And>y. x \<noteq> y \<Longrightarrow> (case (A |` X) y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb) = (case A y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb)
[PROOF STEP]
apply (metis \<open>A x = Some (v, v')\<close> option.simps(5) split_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. x \<noteq> y \<Longrightarrow> (case (A |` X) y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb) = (case A y of None \<Rightarrow> mem\<^sub>1 y | Some (xa, xb) \<Rightarrow> if True then xa else xb)
[PROOF STEP]
by (metis A'_def A_A')
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v) = mem\<^sub>1 [\<parallel>\<^sub>1 A]

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
have eq\<^sub>2: "mem\<^sub>2 [\<parallel>\<^sub>2 A'] (x := v') = mem\<^sub>2 [\<parallel>\<^sub>2 A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v') = mem\<^sub>2 [\<parallel>\<^sub>2 A]
[PROOF STEP]
unfolding apply_adaptation_def A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)(x := v') = (\<lambda>x. case A x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)
[PROOF STEP]
apply (rule ext, rename_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)(x := v')) y = (case A y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb)
[PROOF STEP]
apply (case_tac "x = y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. x = y \<Longrightarrow> ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)(x := v')) y = (case A y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb)
 2. \<And>y. x \<noteq> y \<Longrightarrow> ((\<lambda>x. case (A |` X) x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)(x := v')) y = (case A y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. v' = (case A x of None \<Rightarrow> mem\<^sub>2 x | Some (xa, xb) \<Rightarrow> if False then xa else xb)
 2. \<And>y. x \<noteq> y \<Longrightarrow> (case (A |` X) y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb) = (case A y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb)
[PROOF STEP]
apply (metis \<open>A x = Some (v, v')\<close> option.simps(5) split_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. x \<noteq> y \<Longrightarrow> (case (A |` X) y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb) = (case A y of None \<Rightarrow> mem\<^sub>2 y | Some (xa, xb) \<Rightarrow> if False then xa else xb)
[PROOF STEP]
by (metis A'_def A_A')
[PROOF STATE]
proof (state)
this:
mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v') = mem\<^sub>2 [\<parallel>\<^sub>2 A]

goal (1 subgoal):
 1. \<And>x F A. \<lbrakk>finite F; x \<notin> F; \<And>A. \<lbrakk>F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>; insert x F = dom A; globally_consistent A mds\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
proof (cases "dma x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dma x = High \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
assume "dma x = High"
[PROOF STATE]
proof (state)
this:
dma x = High

goal (2 subgoals):
 1. dma x = High \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
hence "\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'] (x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'] (x := v')\<rangle>"
[PROOF STATE]
proof (prove)
using this:
dma x = High

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>
[PROOF STEP]
using mm_equiv_glob_consistent
[PROOF STATE]
proof (prove)
using this:
dma x = High
closed_glob_consistent mm_equiv

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>
[PROOF STEP]
unfolding closed_glob_consistent_def
[PROOF STATE]
proof (prove)
using this:
dma x = High
\<forall>c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<longrightarrow> (\<forall>x. (dma x = High \<and> x \<notin> mds AsmNoWrite \<longrightarrow> (\<forall>v\<^sub>1 v\<^sub>2. \<langle>c\<^sub>1, mds, mem\<^sub>1(x := v\<^sub>1)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2(x := v\<^sub>2)\<rangle>)) \<and> (dma x = Low \<and> x \<notin> mds AsmNoWrite \<longrightarrow> (\<forall>v. \<langle>c\<^sub>1, mds, mem\<^sub>1(x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2(x := v)\<rangle>)))

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>
[PROOF STEP]
by (metis bisim' \<open>x \<notin> mds AsmNoWrite\<close>)
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>

goal (2 subgoals):
 1. dma x = High \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
 2. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
using eq\<^sub>1 eq\<^sub>2
[PROOF STATE]
proof (prove)
using this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v')\<rangle>
mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v) = mem\<^sub>1 [\<parallel>\<^sub>1 A]
mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v') = mem\<^sub>2 [\<parallel>\<^sub>2 A]

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>

goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
assume "dma x = Low"
[PROOF STATE]
proof (state)
this:
dma x = Low

goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
hence "v = v'"
[PROOF STATE]
proof (prove)
using this:
dma x = Low

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
by (metis \<open>A x = Some (v, v')\<close> globally_consistent_loweq insert.prems)
[PROOF STATE]
proof (state)
this:
v = v'

goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v = v'

goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
from writable and bisim
[PROOF STATE]
proof (chain)
picking this:
x \<notin> mds AsmNoWrite
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>
[PROOF STEP]
have
        "\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'] (x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'] (x := v)\<rangle>"
[PROOF STATE]
proof (prove)
using this:
x \<notin> mds AsmNoWrite
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>
[PROOF STEP]
using mm_equiv_glob_consistent
[PROOF STATE]
proof (prove)
using this:
x \<notin> mds AsmNoWrite
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>
closed_glob_consistent mm_equiv

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>
[PROOF STEP]
unfolding closed_glob_consistent_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> mds AsmNoWrite
\<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle>
\<forall>c\<^sub>1 mds mem\<^sub>1 c\<^sub>2 mem\<^sub>2. \<langle>c\<^sub>1, mds, mem\<^sub>1\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2\<rangle> \<longrightarrow> (\<forall>x. (dma x = High \<and> x \<notin> mds AsmNoWrite \<longrightarrow> (\<forall>v\<^sub>1 v\<^sub>2. \<langle>c\<^sub>1, mds, mem\<^sub>1(x := v\<^sub>1)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2(x := v\<^sub>2)\<rangle>)) \<and> (dma x = Low \<and> x \<notin> mds AsmNoWrite \<longrightarrow> (\<forall>v. \<langle>c\<^sub>1, mds, mem\<^sub>1(x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2(x := v)\<rangle>)))

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>
[PROOF STEP]
by (metis \<open>dma x = Low\<close> bisim')
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>

goal (1 subgoal):
 1. dma x = Low \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v = v'
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v = v'
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
using eq\<^sub>1 eq\<^sub>2
[PROOF STATE]
proof (prove)
using this:
v = v'
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v)\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v)\<rangle>
mem\<^sub>1 [\<parallel>\<^sub>1 A'](x := v) = mem\<^sub>1 [\<parallel>\<^sub>1 A]
mem\<^sub>2 [\<parallel>\<^sub>2 A'](x := v') = mem\<^sub>2 [\<parallel>\<^sub>2 A]

goal (1 subgoal):
 1. \<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>c\<^sub>1, mds, mem\<^sub>1 [\<parallel>\<^sub>1 A]\<rangle> \<approx> \<langle>c\<^sub>2, mds, mem\<^sub>2 [\<parallel>\<^sub>2 A]\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed