[STATEMENT]
lemma ta_seq_consist_imp_sequentially_consistent:
  assumes tsa_ok: "thread_start_actions_ok E"
  and new_actions_for_fun: "\<And>adal a a'. \<lbrakk> a \<in> new_actions_for P E adal; a' \<in> new_actions_for P E adal \<rbrakk> \<Longrightarrow> a = a'"
  and seq: "ta_seq_consist P Map.empty (lmap snd E)"
  shows "\<exists>ws. sequentially_consistent P (E, ws) \<and> P \<turnstile> (E, ws) \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ws. sequentially_consistent P (E, ws) \<and> P \<turnstile> (E, ws) \<surd>
[PROOF STEP]
proof(intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sequentially_consistent P (E, ?ws)
 2. P \<turnstile> (E, ?ws) \<surd>
[PROOF STEP]
define ws where "ws i = (THE w. P,E \<turnstile> i \<leadsto>mrw w)" for i
[PROOF STATE]
proof (state)
this:
ws ?i = (THE w. P,E \<turnstile> ?i \<leadsto>mrw w)

goal (2 subgoals):
 1. sequentially_consistent P (E, ?ws)
 2. P \<turnstile> (E, ?ws) \<surd>
[PROOF STEP]
from seq
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
[PROOF STEP]
have ns: "non_speculative P (\<lambda>_. {}) (lmap snd E)"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)

goal (1 subgoal):
 1. non_speculative P (\<lambda>_. {}) (lmap snd E)
[PROOF STEP]
by(rule ta_seq_consist_into_non_speculative) simp
[PROOF STATE]
proof (state)
this:
non_speculative P (\<lambda>_. {}) (lmap snd E)

goal (2 subgoals):
 1. sequentially_consistent P (E, ?ws)
 2. P \<turnstile> (E, ?ws) \<surd>
[PROOF STEP]
show "sequentially_consistent P (E, ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequentially_consistent P (E, ws)
[PROOF STEP]
unfolding ws_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequentially_consistent P (E, \<lambda>i. The (most_recent_write_for P E i))
[PROOF STEP]
proof(rule sequentially_consistentI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> read_actions E \<Longrightarrow> P,E \<turnstile> r \<leadsto>mrw The (most_recent_write_for P E r)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. r \<in> read_actions E \<Longrightarrow> P,E \<turnstile> r \<leadsto>mrw The (most_recent_write_for P E r)
[PROOF STEP]
assume "r \<in> read_actions E"
[PROOF STATE]
proof (state)
this:
r \<in> read_actions E

goal (1 subgoal):
 1. \<And>r. r \<in> read_actions E \<Longrightarrow> P,E \<turnstile> r \<leadsto>mrw The (most_recent_write_for P E r)
[PROOF STEP]
with seq new_actions_for_fun
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'
r \<in> read_actions E
[PROOF STEP]
obtain w where "P,E \<turnstile> r \<leadsto>mrw w"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'
r \<in> read_actions E

goal (1 subgoal):
 1. (\<And>w. P,E \<turnstile> r \<leadsto>mrw w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: ta_seq_consist_most_recent_write_for)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> r \<leadsto>mrw w

goal (1 subgoal):
 1. \<And>r. r \<in> read_actions E \<Longrightarrow> P,E \<turnstile> r \<leadsto>mrw The (most_recent_write_for P E r)
[PROOF STEP]
thus "P,E \<turnstile> r \<leadsto>mrw THE w. P,E \<turnstile> r \<leadsto>mrw w"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> r \<leadsto>mrw w

goal (1 subgoal):
 1. P,E \<turnstile> r \<leadsto>mrw THE w. P,E \<turnstile> r \<leadsto>mrw w
[PROOF STEP]
by(simp add: THE_most_recent_writeI)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> r \<leadsto>mrw THE w. P,E \<turnstile> r \<leadsto>mrw w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sequentially_consistent P (E, ws)

goal (1 subgoal):
 1. P \<turnstile> (E, \<lambda>i. The (most_recent_write_for P E i)) \<surd>
[PROOF STEP]
show "P \<turnstile> (E, ws) \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> (E, ws) \<surd>
[PROOF STEP]
proof(rule wf_execI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_write_seen P E ws
 2. thread_start_actions_ok E
[PROOF STEP]
show "is_write_seen P E ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_write_seen P E ws
[PROOF STEP]
proof(rule is_write_seenI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
fix a ad al v
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
assume a: "a \<in> read_actions E"
        and adal: "action_obs E a = NormalAction (ReadMem ad al v)"
[PROOF STATE]
proof (state)
this:
a \<in> read_actions E
action_obs E a = NormalAction (ReadMem ad al v)

goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from ns
[PROOF STATE]
proof (chain)
picking this:
non_speculative P (\<lambda>_. {}) (lmap snd E)
[PROOF STEP]
have seq': "non_speculative P (\<lambda>_. {}) (ltake (enat a) (lmap snd E))"
[PROOF STATE]
proof (prove)
using this:
non_speculative P (\<lambda>_. {}) (lmap snd E)

goal (1 subgoal):
 1. non_speculative P (\<lambda>_. {}) (ltake (enat a) (lmap snd E))
[PROOF STEP]
by(rule non_speculative_ltake)
[PROOF STATE]
proof (state)
this:
non_speculative P (\<lambda>_. {}) (ltake (enat a) (lmap snd E))

goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from seq a seq new_actions_for_fun
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
a \<in> read_actions E
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'
[PROOF STEP]
obtain w where mrw: "P,E \<turnstile> a \<leadsto>mrw w"
        and "w < a"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)
a \<in> read_actions E
ta_seq_consist P Map.empty (lmap snd E)
\<lbrakk>?a \<in> new_actions_for P E ?adal; ?a' \<in> new_actions_for P E ?adal\<rbrakk> \<Longrightarrow> ?a = ?a'

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>P,E \<turnstile> a \<leadsto>mrw w; w < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: ta_seq_consist_most_recent_write_for)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> a \<leadsto>mrw w
w < a

goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence w: "ws a = w"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> a \<leadsto>mrw w
w < a

goal (1 subgoal):
 1. ws a = w
[PROOF STEP]
by(simp add: ws_def THE_most_recent_writeI)
[PROOF STATE]
proof (state)
this:
ws a = w

goal (7 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> ws a \<in> write_actions E
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> (ad, al) \<in> action_loc P E (ws a)
 3. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 4. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>hb ws a
 5. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 6. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 7. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
with mrw adal
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> a \<leadsto>mrw w
action_obs E a = NormalAction (ReadMem ad al v)
ws a = w
[PROOF STEP]
show "ws a \<in> write_actions E"
        and "(ad, al) \<in> action_loc P E (ws a)"
        and "\<not> P,E \<turnstile> a \<le>hb ws a"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> a \<leadsto>mrw w
action_obs E a = NormalAction (ReadMem ad al v)
ws a = w

goal (1 subgoal):
 1. ws a \<in> write_actions E &&& (ad, al) \<in> action_loc P E (ws a) &&& \<not> P,E \<turnstile> a \<le>hb ws a
[PROOF STEP]
by(fastforce elim!: most_recent_write_for.cases dest: happens_before_into_action_order antisymPD[OF antisym_action_order] read_actions_not_write_actions)+
[PROOF STATE]
proof (state)
this:
ws a \<in> write_actions E
(ad, al) \<in> action_loc P E (ws a)
\<not> P,E \<turnstile> a \<le>hb ws a

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
let ?between = "ltake (enat (a - Suc w)) (ldropn (Suc w) E)"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
let ?prefix = "ltake (enat w) E"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
let ?vs_prefix = "mrw_values P Map.empty (map snd (list_of ?prefix))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
fix v'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
assume new: "is_new_action (action_obs E w)"
          and vs': "?vs_prefix (ad, al) = \<lfloor>(v', True)\<rfloor>"
[PROOF STATE]
proof (state)
this:
is_new_action (action_obs E w)
mrw_values P Map.empty (map snd (list_of (ltake (enat w) E))) (ad, al) = \<lfloor>(v', True)\<rfloor>

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from mrw_values_eq_SomeD[OF vs']
[PROOF STATE]
proof (chain)
picking this:
(None = \<lfloor>(v', True)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd (list_of (ltake (enat w) E))) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (True \<longrightarrow> \<not> is_new_action wa)) \<Longrightarrow> \<exists>obs' wa obs''. map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs'' \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> value_written_aux P wa al = v' \<and> is_new_action wa = (\<not> True) \<and> (\<forall>ob\<in>set obs''. is_write_action ob \<longrightarrow> (ad, al) \<in> action_loc_aux P ob \<longrightarrow> is_new_action ob \<and> True)
[PROOF STEP]
obtain obs' wa obs'' where split: "map snd (list_of ?prefix) = obs' @ wa # obs''"
          and wa: "is_write_action wa"
          and adal': "(ad, al) \<in> action_loc_aux P wa"
          and new_wa: "\<not> is_new_action wa"
[PROOF STATE]
proof (prove)
using this:
(None = \<lfloor>(v', True)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd (list_of (ltake (enat w) E))) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (True \<longrightarrow> \<not> is_new_action wa)) \<Longrightarrow> \<exists>obs' wa obs''. map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs'' \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> value_written_aux P wa al = v' \<and> is_new_action wa = (\<not> True) \<and> (\<forall>ob\<in>set obs''. is_write_action ob \<longrightarrow> (ad, al) \<in> action_loc_aux P ob \<longrightarrow> is_new_action ob \<and> True)

goal (1 subgoal):
 1. (\<And>obs' wa obs''. \<lbrakk>map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''; is_write_action wa; (ad, al) \<in> action_loc_aux P wa; \<not> is_new_action wa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''
[PROOF STEP]
have "length (map snd (list_of ?prefix)) = Suc (length obs' + length obs'')"
[PROOF STATE]
proof (prove)
using this:
map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''

goal (1 subgoal):
 1. length (map snd (list_of (ltake (enat w) E))) = Suc (length obs' + length obs'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (map snd (list_of (ltake (enat w) E))) = Suc (length obs' + length obs'')

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence len_prefix: "llength ?prefix = enat \<dots>"
[PROOF STATE]
proof (prove)
using this:
length (map snd (list_of (ltake (enat w) E))) = Suc (length obs' + length obs'')

goal (1 subgoal):
 1. llength (ltake (enat w) E) = enat (Suc (length obs' + length obs''))
[PROOF STEP]
by(simp add: length_list_of_conv_the_enat min_enat1_conv_enat)
[PROOF STATE]
proof (state)
this:
llength (ltake (enat w) E) = enat (Suc (length obs' + length obs''))

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
with split
[PROOF STATE]
proof (chain)
picking this:
map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''
llength (ltake (enat w) E) = enat (Suc (length obs' + length obs''))
[PROOF STEP]
have "nth (map snd (list_of ?prefix)) (length obs') = wa"
          and "enat (length obs') < llength ?prefix"
[PROOF STATE]
proof (prove)
using this:
map snd (list_of (ltake (enat w) E)) = obs' @ wa # obs''
llength (ltake (enat w) E) = enat (Suc (length obs' + length obs''))

goal (1 subgoal):
 1. map snd (list_of (ltake (enat w) E)) ! length obs' = wa &&& enat (length obs') < llength (ltake (enat w) E)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
map snd (list_of (ltake (enat w) E)) ! length obs' = wa
enat (length obs') < llength (ltake (enat w) E)

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence "snd (lnth ?prefix (length obs')) = wa"
[PROOF STATE]
proof (prove)
using this:
map snd (list_of (ltake (enat w) E)) ! length obs' = wa
enat (length obs') < llength (ltake (enat w) E)

goal (1 subgoal):
 1. snd (lnth (ltake (enat w) E) (length obs')) = wa
[PROOF STEP]
by(simp add: list_of_lmap[symmetric] del: list_of_lmap)
[PROOF STATE]
proof (state)
this:
snd (lnth (ltake (enat w) E) (length obs')) = wa

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence wa': "action_obs E (length obs') = wa" and "enat (length obs') < llength E"
[PROOF STATE]
proof (prove)
using this:
snd (lnth (ltake (enat w) E) (length obs')) = wa

goal (1 subgoal):
 1. action_obs E (length obs') = wa &&& enat (length obs') < llength E
[PROOF STEP]
using \<open>enat (length obs') < llength ?prefix\<close>
[PROOF STATE]
proof (prove)
using this:
snd (lnth (ltake (enat w) E) (length obs')) = wa
enat (length obs') < llength (ltake (enat w) E)

goal (1 subgoal):
 1. action_obs E (length obs') = wa &&& enat (length obs') < llength E
[PROOF STEP]
by(auto simp add: action_obs_def lnth_ltake)
[PROOF STATE]
proof (state)
this:
action_obs E (length obs') = wa
enat (length obs') < llength E

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
with wa
[PROOF STATE]
proof (chain)
picking this:
is_write_action wa
action_obs E (length obs') = wa
enat (length obs') < llength E
[PROOF STEP]
have "length obs' \<in> write_actions E"
[PROOF STATE]
proof (prove)
using this:
is_write_action wa
action_obs E (length obs') = wa
enat (length obs') < llength E

goal (1 subgoal):
 1. length obs' \<in> write_actions E
[PROOF STEP]
by(auto intro: write_actions.intros simp add: actions_def)
[PROOF STATE]
proof (state)
this:
length obs' \<in> write_actions E

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from most_recent_write_recent[OF mrw _ this, of "(ad, al)"] adal adal' wa'
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(ad, al) \<in> action_loc P E a; (ad, al) \<in> action_loc P E (length obs')\<rbrakk> \<Longrightarrow> E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'
action_obs E a = NormalAction (ReadMem ad al v)
(ad, al) \<in> action_loc_aux P wa
action_obs E (length obs') = wa
[PROOF STEP]
have "E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(ad, al) \<in> action_loc P E a; (ad, al) \<in> action_loc P E (length obs')\<rbrakk> \<Longrightarrow> E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'
action_obs E a = NormalAction (ReadMem ad al v)
(ad, al) \<in> action_loc_aux P wa
action_obs E (length obs') = wa

goal (1 subgoal):
 1. E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'

goal (1 subgoal):
 1. False
[PROOF STEP]
using new_wa new wa' adal len_prefix \<open>w < a\<close>
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> length obs' \<le>a w \<or> E \<turnstile> a \<le>a length obs'
\<not> is_new_action wa
is_new_action (action_obs E w)
action_obs E (length obs') = wa
action_obs E a = NormalAction (ReadMem ad al v)
llength (ltake (enat w) E) = enat (Suc (length obs' + length obs''))
w < a

goal (1 subgoal):
 1. False
[PROOF STEP]
by(auto elim!: action_orderE simp add: min_enat1_conv_enat split: enat.split_asm)
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_new_action (action_obs E w); mrw_values P Map.empty (map snd (list_of (ltake (enat w) E))) (ad, al) = \<lfloor>(?v'2, True)\<rfloor>\<rbrakk> \<Longrightarrow> False

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence mrw_value_w: "mrw_value P ?vs_prefix (snd (lnth E w)) (ad, al) =
                          \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_new_action (action_obs E w); mrw_values P Map.empty (map snd (list_of (ltake (enat w) E))) (ad, al) = \<lfloor>(?v'2, True)\<rfloor>\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
using \<open>ws a \<in> write_actions E\<close> \<open>(ad, al) \<in> action_loc P E (ws a)\<close> w
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_new_action (action_obs E w); mrw_values P Map.empty (map snd (list_of (ltake (enat w) E))) (ad, al) = \<lfloor>(?v'2, True)\<rfloor>\<rbrakk> \<Longrightarrow> False
ws a \<in> write_actions E
(ad, al) \<in> action_loc P E (ws a)
ws a = w

goal (1 subgoal):
 1. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
by(cases "snd (lnth E w)" rule: mrw_value_cases)(fastforce elim: write_actions.cases simp add: value_written_def action_obs_def)+
[PROOF STATE]
proof (state)
this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
have "mrw_values P (mrw_value P ?vs_prefix (snd (lnth E w))) (list_of (lmap snd ?between)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
proof(subst mrw_values_no_write_unchanged)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
fix wa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
assume "wa \<in> set (list_of (lmap snd ?between))"
          and write_wa: "is_write_action wa"
          and adal_wa: "(ad, al) \<in> action_loc_aux P wa"
[PROOF STATE]
proof (state)
this:
wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
hence wa: "wa \<in> lset (lmap snd ?between)"
[PROOF STATE]
proof (prove)
using this:
wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa

goal (1 subgoal):
 1. wa \<in> lset (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wa \<in> lset (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
from wa
[PROOF STATE]
proof (chain)
picking this:
wa \<in> lset (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))
[PROOF STEP]
obtain i_wa where "wa = lnth (lmap snd ?between) i_wa"
          and i_wa: "enat i_wa < llength (lmap snd ?between)"
[PROOF STATE]
proof (prove)
using this:
wa \<in> lset (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))

goal (1 subgoal):
 1. (\<And>i_wa. \<lbrakk>wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa; enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lset_conv_lnth
[PROOF STATE]
proof (prove)
using this:
wa \<in> {lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) n |n. enat n < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))}

goal (1 subgoal):
 1. (\<And>i_wa. \<lbrakk>wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa; enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
hence i_wa_len: "enat (Suc (w + i_wa)) < llength E"
[PROOF STATE]
proof (prove)
using this:
wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))

goal (1 subgoal):
 1. enat (Suc (w + i_wa)) < llength E
[PROOF STEP]
by(cases "llength E") auto
[PROOF STATE]
proof (state)
this:
enat (Suc (w + i_wa)) < llength E

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))
enat (Suc (w + i_wa)) < llength E
[PROOF STEP]
have wa': "wa = action_obs E (Suc (w + i_wa))"
[PROOF STATE]
proof (prove)
using this:
wa = lnth (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))) i_wa
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))
enat (Suc (w + i_wa)) < llength E

goal (1 subgoal):
 1. wa = action_obs E (Suc (w + i_wa))
[PROOF STEP]
by(simp_all add: lnth_ltake action_obs_def ac_simps)
[PROOF STATE]
proof (state)
this:
wa = action_obs E (Suc (w + i_wa))

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
with write_wa i_wa_len
[PROOF STATE]
proof (chain)
picking this:
is_write_action wa
enat (Suc (w + i_wa)) < llength E
wa = action_obs E (Suc (w + i_wa))
[PROOF STEP]
have "Suc (w + i_wa) \<in> write_actions E"
[PROOF STATE]
proof (prove)
using this:
is_write_action wa
enat (Suc (w + i_wa)) < llength E
wa = action_obs E (Suc (w + i_wa))

goal (1 subgoal):
 1. Suc (w + i_wa) \<in> write_actions E
[PROOF STEP]
by(auto intro: write_actions.intros simp add: actions_def)
[PROOF STATE]
proof (state)
this:
Suc (w + i_wa) \<in> write_actions E

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
from most_recent_write_recent[OF mrw _ this, of "(ad, al)"] adal adal_wa wa'
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(ad, al) \<in> action_loc P E a; (ad, al) \<in> action_loc P E (Suc (w + i_wa))\<rbrakk> \<Longrightarrow> E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)
action_obs E a = NormalAction (ReadMem ad al v)
(ad, al) \<in> action_loc_aux P wa
wa = action_obs E (Suc (w + i_wa))
[PROOF STEP]
have "E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(ad, al) \<in> action_loc P E a; (ad, al) \<in> action_loc P E (Suc (w + i_wa))\<rbrakk> \<Longrightarrow> E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)
action_obs E a = NormalAction (ReadMem ad al v)
(ad, al) \<in> action_loc_aux P wa
wa = action_obs E (Suc (w + i_wa))

goal (1 subgoal):
 1. E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
hence "is_new_action wa \<and> \<not> is_new_action (action_obs E w)"
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)

goal (1 subgoal):
 1. is_new_action wa \<and> \<not> is_new_action (action_obs E w)
[PROOF STEP]
using adal i_wa wa'
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> Suc (w + i_wa) \<le>a w \<or> E \<turnstile> a \<le>a Suc (w + i_wa)
action_obs E a = NormalAction (ReadMem ad al v)
enat i_wa < llength (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))
wa = action_obs E (Suc (w + i_wa))

goal (1 subgoal):
 1. is_new_action wa \<and> \<not> is_new_action (action_obs E w)
[PROOF STEP]
by(auto elim: action_orderE)
[PROOF STATE]
proof (state)
this:
is_new_action wa \<and> \<not> is_new_action (action_obs E w)

goal (2 subgoals):
 1. \<And>wa. \<lbrakk>wa \<in> set (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))); is_write_action wa; (ad, al) \<in> action_loc_aux P wa\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
 2. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
thus "case (mrw_value P ?vs_prefix (snd (lnth E w)) (ad, al)) of None \<Rightarrow> False | Some (v, b) \<Rightarrow> b \<and> is_new_action wa"
[PROOF STATE]
proof (prove)
using this:
is_new_action wa \<and> \<not> is_new_action (action_obs E w)

goal (1 subgoal):
 1. case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
[PROOF STEP]
unfolding mrw_value_w
[PROOF STATE]
proof (prove)
using this:
is_new_action wa \<and> \<not> is_new_action (action_obs E w)

goal (1 subgoal):
 1. case \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor> of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa

goal (1 subgoal):
 1. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w)) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
[PROOF STEP]
qed(simp add: mrw_value_w)
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a \<in> read_actions E
[PROOF STEP]
have "a \<in> actions E"
[PROOF STATE]
proof (prove)
using this:
a \<in> read_actions E

goal (1 subgoal):
 1. a \<in> actions E
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<in> actions E

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence "enat a < llength E"
[PROOF STATE]
proof (prove)
using this:
a \<in> actions E

goal (1 subgoal):
 1. enat a < llength E
[PROOF STEP]
by(rule actionsE)
[PROOF STATE]
proof (state)
this:
enat a < llength E

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
with \<open>w < a\<close>
[PROOF STATE]
proof (chain)
picking this:
w < a
enat a < llength E
[PROOF STEP]
have "enat (a - Suc w) < llength E - enat (Suc w)"
[PROOF STATE]
proof (prove)
using this:
w < a
enat a < llength E

goal (1 subgoal):
 1. enat (a - Suc w) < llength E - enat (Suc w)
[PROOF STEP]
by(cases "llength E") simp_all
[PROOF STATE]
proof (state)
this:
enat (a - Suc w) < llength E - enat (Suc w)

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence "E = lappend (lappend ?prefix (LCons (lnth E w) ?between)) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))"
[PROOF STATE]
proof (prove)
using this:
enat (a - Suc w) < llength E - enat (Suc w)

goal (1 subgoal):
 1. E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))
[PROOF STEP]
using \<open>w < a\<close> \<open>enat a < llength E\<close>
[PROOF STATE]
proof (prove)
using this:
enat (a - Suc w) < llength E - enat (Suc w)
w < a
enat a < llength E

goal (1 subgoal):
 1. E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))
[PROOF STEP]
unfolding lappend_assoc lappend_code
[PROOF STATE]
proof (prove)
using this:
enat (a - Suc w) < llength E - enat (Suc w)
w < a
enat a < llength E

goal (1 subgoal):
 1. E = lappend (ltake (enat w) E) (LCons (lnth E w) (lappend (ltake (enat (a - Suc w)) (ldropn (Suc w) E)) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))))
[PROOF STEP]
apply(subst ldropn_Suc_conv_ldropn, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat (a - Suc w) < llength E - enat (Suc w); w < a; enat a < llength E\<rbrakk> \<Longrightarrow> E = lappend (ltake (enat w) E) (LCons (lnth E w) (lappend (ltake (enat (a - Suc w)) (ldropn (Suc w) E)) (ldropn (a - Suc w) (ldropn (Suc w) E))))
[PROOF STEP]
apply(subst lappend_ltake_enat_ldropn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat (a - Suc w) < llength E - enat (Suc w); w < a; enat a < llength E\<rbrakk> \<Longrightarrow> E = lappend (ltake (enat w) E) (LCons (lnth E w) (ldropn (Suc w) E))
[PROOF STEP]
apply(subst ldropn_Suc_conv_ldropn, simp add: less_trans[where y="enat a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>enat (a - Suc w) < llength E - enat (Suc w); w < a; enat a < llength E\<rbrakk> \<Longrightarrow> E = lappend (ltake (enat w) E) (ldropn w E)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
hence E': "E = lappend (lappend ?prefix (LCons (lnth E w) ?between)) (LCons (lnth E a) (ldropn (Suc a) E))"
[PROOF STATE]
proof (prove)
using this:
E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))

goal (1 subgoal):
 1. E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth E a) (ldropn (Suc a) E))
[PROOF STEP]
using \<open>w < a\<close> \<open>enat a < llength E\<close>
[PROOF STATE]
proof (prove)
using this:
E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth (ldropn (Suc w) E) (a - Suc w)) (ldropn (Suc (a - Suc w)) (ldropn (Suc w) E)))
w < a
enat a < llength E

goal (1 subgoal):
 1. E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth E a) (ldropn (Suc a) E))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E = lappend (lappend (ltake (enat w) E) (LCons (lnth E w) (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (LCons (lnth E a) (ldropn (Suc a) E))

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
from seq
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (lmap snd E)
[PROOF STEP]
have "ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd ?prefix) (LCons (snd (lnth E w)) (lmap snd ?between))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (lmap snd E)

goal (1 subgoal):
 1. ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd (ltake (enat w) E)) (LCons (snd (lnth E w)) (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))
[PROOF STEP]
by(subst (asm) E')(simp add: lmap_lappend_distrib ta_seq_consist_lappend)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd (ltake (enat w) E)) (LCons (snd (lnth E w)) (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))

goal (4 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v)\<rbrakk> \<Longrightarrow> value_written P E (ws a) (ad, al) = v
 2. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd (ltake (enat w) E)) (LCons (snd (lnth E w)) (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))
[PROOF STEP]
show "value_written P E (ws a) (ad, al) = v"
[PROOF STATE]
proof (prove)
using this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd (ltake (enat w) E)) (LCons (snd (lnth E w)) (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))

goal (1 subgoal):
 1. value_written P E (ws a) (ad, al) = v
[PROOF STEP]
using adal w
[PROOF STATE]
proof (prove)
using this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat w) E)))) (snd (lnth E w))) (list_of (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E)))) (ad, al) = \<lfloor>(value_written P E w (ad, al), \<not> is_new_action (action_obs E w))\<rfloor>
ta_seq_consist P (mrw_values P Map.empty (list_of (lappend (lmap snd (ltake (enat w) E)) (LCons (snd (lnth E w)) (lmap snd (ltake (enat (a - Suc w)) (ldropn (Suc w) E))))))) (lmap snd (LCons (lnth E a) (ldropn (Suc a) E)))
action_obs E a = NormalAction (ReadMem ad al v)
ws a = w

goal (1 subgoal):
 1. value_written P E (ws a) (ad, al) = v
[PROOF STEP]
by(clarsimp simp add: action_obs_def list_of_lappend list_of_LCons)
[PROOF STATE]
proof (state)
this:
value_written P E (ws a) (ad, al) = v

goal (3 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
(* assume "is_volatile P al" *)
[PROOF STATE]
proof (state)
this:
value_written P E (ws a) (ad, al) = v

goal (3 subgoals):
 1. \<And>a ad al v. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); is_volatile P al\<rbrakk> \<Longrightarrow> \<not> P,E \<turnstile> a \<le>so ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
show "\<not> P,E \<turnstile> a \<le>so ws a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P,E \<turnstile> a \<le>so ws a
[PROOF STEP]
using \<open>w < a\<close> w adal
[PROOF STATE]
proof (prove)
using this:
w < a
ws a = w
action_obs E a = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. \<not> P,E \<turnstile> a \<le>so ws a
[PROOF STEP]
by(auto elim!: action_orderE sync_orderE)
[PROOF STATE]
proof (state)
this:
\<not> P,E \<turnstile> a \<le>so ws a

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
assume a': "a' \<in> write_actions E" "(ad, al) \<in> action_loc P E a'"
[PROOF STATE]
proof (state)
this:
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
presume "E \<turnstile> ws a \<le>a a'" "E \<turnstile> a' \<le>a a"
[PROOF STATE]
proof (state)
this:
E \<turnstile> ws a \<le>a a'
E \<turnstile> a' \<le>a a

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
with mrw adal a'
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> a \<leadsto>mrw w
action_obs E a = NormalAction (ReadMem ad al v)
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'
E \<turnstile> ws a \<le>a a'
E \<turnstile> a' \<le>a a
[PROOF STEP]
have "a' = ws a"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> a \<leadsto>mrw w
action_obs E a = NormalAction (ReadMem ad al v)
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'
E \<turnstile> ws a \<le>a a'
E \<turnstile> a' \<le>a a

goal (1 subgoal):
 1. a' = ws a
[PROOF STEP]
unfolding w
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> a \<leadsto>mrw w
action_obs E a = NormalAction (ReadMem ad al v)
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'
E \<turnstile> w \<le>a a'
E \<turnstile> a' \<le>a a

goal (1 subgoal):
 1. a' = w
[PROOF STEP]
by cases(fastforce dest: antisymPD[OF antisym_action_order] read_actions_not_write_actions elim!: meta_allE[where x=a'])
[PROOF STATE]
proof (state)
this:
a' = ws a

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> a' = ws a
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> a' = ws a
[PROOF STEP]
thus "a' = ws a" "a' = ws a"
[PROOF STATE]
proof (prove)
using this:
a' = ws a

goal (1 subgoal):
 1. a' = ws a &&& a' = ws a
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
a' = ws a
a' = ws a

goal (4 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
assume "P,E \<turnstile> ws a \<le>hb a'" "P,E \<turnstile> a' \<le>hb a"
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> ws a \<le>hb a'
P,E \<turnstile> a' \<le>hb a

goal (4 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; P,E \<turnstile> ws a \<le>hb a'; P,E \<turnstile> a' \<le>hb a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
 3. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 4. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
thus "E \<turnstile> ws a \<le>a a'" "E \<turnstile> a' \<le>a a"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> ws a \<le>hb a'
P,E \<turnstile> a' \<le>hb a

goal (1 subgoal):
 1. E \<turnstile> ws a \<le>a a' &&& E \<turnstile> a' \<le>a a
[PROOF STEP]
using a'
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> ws a \<le>hb a'
P,E \<turnstile> a' \<le>hb a
a' \<in> write_actions E
(ad, al) \<in> action_loc P E a'

goal (1 subgoal):
 1. E \<turnstile> ws a \<le>a a' &&& E \<turnstile> a' \<le>a a
[PROOF STEP]
by(blast intro: happens_before_into_action_order)+
[PROOF STATE]
proof (state)
this:
E \<turnstile> ws a \<le>a a'
E \<turnstile> a' \<le>a a

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
assume "is_volatile P al" "P,E \<turnstile> ws a \<le>so a'" "P,E \<turnstile> a' \<le>so a"
[PROOF STATE]
proof (state)
this:
is_volatile P al
P,E \<turnstile> ws a \<le>so a'
P,E \<turnstile> a' \<le>so a

goal (2 subgoals):
 1. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
 2. \<And>a ad al v a'. \<lbrakk>a \<in> read_actions E; action_obs E a = NormalAction (ReadMem ad al v); a' \<in> write_actions E; (ad, al) \<in> action_loc P E a'; is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a
[PROOF STEP]
thus "E \<turnstile> ws a \<le>a a'" "E \<turnstile> a' \<le>a a"
[PROOF STATE]
proof (prove)
using this:
is_volatile P al
P,E \<turnstile> ws a \<le>so a'
P,E \<turnstile> a' \<le>so a

goal (1 subgoal):
 1. E \<turnstile> ws a \<le>a a' &&& E \<turnstile> a' \<le>a a
[PROOF STEP]
by(auto elim: sync_orderE)
[PROOF STATE]
proof (state)
this:
E \<turnstile> ws a \<le>a a'
E \<turnstile> a' \<le>a a

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> ws a \<le>a a'
\<lbrakk>is_volatile P al; P,E \<turnstile> ws a \<le>so a'; P,E \<turnstile> a' \<le>so a\<rbrakk> \<Longrightarrow> E \<turnstile> a' \<le>a a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_write_seen P E ws

goal (1 subgoal):
 1. thread_start_actions_ok E
[PROOF STEP]
qed(rule tsa_ok)
[PROOF STATE]
proof (state)
this:
P \<turnstile> (E, ws) \<surd>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_upto_seq_inconsist_simps:
  "eq_upto_seq_inconsist P [] obs' vs \<longleftrightarrow> obs' = []"
  "eq_upto_seq_inconsist P obs [] vs \<longleftrightarrow> obs = []"
  "eq_upto_seq_inconsist P (ob # obs) (ob' # obs') vs \<longleftrightarrow>
   (case ob of NormalAction (ReadMem ad al v) \<Rightarrow>
      if (\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>)
      then ob = ob' \<and> eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob)
      else ob \<approx> ob'
    | _ \<Rightarrow> ob = ob' \<and> eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_upto_seq_inconsist P [] obs' vs = (obs' = []) &&& eq_upto_seq_inconsist P obs [] vs = (obs = []) &&& eq_upto_seq_inconsist P (ob # obs) (ob' # obs') vs = (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob = ob' \<and> eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob) else ob \<approx> ob' | NormalAction _ \<Rightarrow> ob = ob' \<and> eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob) | _ \<Rightarrow> ob = ob' \<and> eq_upto_seq_inconsist P obs obs' (mrw_value P vs ob))
[PROOF STEP]
by(auto simp add: eq_upto_seq_inconsist_def split: action.split obs_event.split)


[STATEMENT]
lemma eq_upto_seq_inconsist_Cons1:
  "eq_upto_seq_inconsist P (ob # obs) obs' vs \<longleftrightarrow>
   (\<exists>ob' obs''. obs' = ob' # obs'' \<and>
      (case ob of NormalAction (ReadMem ad al v) \<Rightarrow>
         if (\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>)
         then ob' = ob \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob)
         else ob \<approx> ob'
       | _ \<Rightarrow> ob' = ob \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_upto_seq_inconsist P (ob # obs) obs' vs = (\<exists>ob' obs''. obs' = ob' # obs'' \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = ob \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob) else ob \<approx> ob' | NormalAction _ \<Rightarrow> ob' = ob \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob) | _ \<Rightarrow> ob' = ob \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs ob)))
[PROOF STEP]
unfolding eq_upto_seq_inconsist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl_list_all2 (\<lambda>ob ob' vs. mrw_value P vs ob) (\<lambda>ob ob' vs. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) (\<lambda>ob ob' vs. if case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True then ob = ob' else ob \<approx> ob') (ob # obs) obs' vs = (\<exists>ob' obs''. obs' = ob' # obs'' \<and> (case ob of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = ob \<and> foldl_list_all2 (\<lambda>ob ob' vs. mrw_value P vs ob) (\<lambda>ob ob' vs. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) (\<lambda>ob ob' vs. if case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True then ob = ob' else ob \<approx> ob') obs obs'' (mrw_value P vs ob) else ob \<approx> ob' | NormalAction _ \<Rightarrow> ob' = ob \<and> foldl_list_all2 (\<lambda>ob ob' vs. mrw_value P vs ob) (\<lambda>ob ob' vs. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) (\<lambda>ob ob' vs. if case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True then ob = ob' else ob \<approx> ob') obs obs'' (mrw_value P vs ob) | _ \<Rightarrow> ob' = ob \<and> foldl_list_all2 (\<lambda>ob ob' vs. mrw_value P vs ob) (\<lambda>ob ob' vs. case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) (\<lambda>ob ob' vs. if case ob of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True then ob = ob' else ob \<approx> ob') obs obs'' (mrw_value P vs ob)))
[PROOF STEP]
by(auto split: obs_event.split action.split simp add: foldl_list_all2_Cons1)


[STATEMENT]
lemma eq_upto_seq_inconsist_appendD:
  assumes "eq_upto_seq_inconsist P (obs @ obs') obs'' vs"
  and "ta_seq_consist P vs (llist_of obs)"
  shows "length obs \<le> length obs''" (is ?thesis1)
  and "take (length obs) obs'' = obs" (is ?thesis2)
  and "eq_upto_seq_inconsist P obs' (drop (length obs) obs'') (mrw_values P vs obs)" (is ?thesis3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length obs \<le> length obs'' &&& take (length obs) obs'' = obs &&& eq_upto_seq_inconsist P obs' (drop (length obs) obs'') (mrw_values P vs obs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eq_upto_seq_inconsist P (obs @ obs') obs'' vs
ta_seq_consist P vs (llist_of obs)

goal (1 subgoal):
 1. length obs \<le> length obs'' &&& take (length obs) obs'' = obs &&& eq_upto_seq_inconsist P obs' (drop (length obs) obs'') (mrw_values P vs obs)
[PROOF STEP]
by(induct obs arbitrary: obs'' vs)(auto split: action.split_asm obs_event.split_asm simp add: eq_upto_seq_inconsist_Cons1)


[STATEMENT]
lemma ta_seq_consist_imp_eq_upto_seq_inconsist_refl:
  "ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs obs vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs obs vs
[PROOF STEP]
apply(induct obs arbitrary: vs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>vs. ta_seq_consist P vs (llist_of []) \<Longrightarrow> eq_upto_seq_inconsist P [] [] vs
 2. \<And>a obs vs. \<lbrakk>\<And>vs. ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs obs vs; ta_seq_consist P vs (llist_of (a # obs))\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (a # obs) (a # obs) vs
[PROOF STEP]
apply(auto simp add: eq_upto_seq_inconsist_simps split: action.split obs_event.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done