[STATEMENT]
lemma eq_upto_seq_inconsist_appendI:
  "\<lbrakk> eq_upto_seq_inconsist P obs OBS vs;
     \<lbrakk> ta_seq_consist P vs (llist_of obs) \<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS) \<rbrakk>
  \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_upto_seq_inconsist P obs OBS vs; ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs
[PROOF STEP]
apply(induct obs arbitrary: vs OBS)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>vs OBS. \<lbrakk>eq_upto_seq_inconsist P [] OBS vs; ta_seq_consist P vs (llist_of []) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P ([] @ obs') (OBS @ OBS') vs
 2. \<And>a obs vs OBS. \<lbrakk>\<And>vs OBS. \<lbrakk>eq_upto_seq_inconsist P obs OBS vs; ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs; eq_upto_seq_inconsist P (a # obs) OBS vs; ta_seq_consist P vs (llist_of (a # obs)) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P ((a # obs) @ obs') (OBS @ OBS') vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a obs vs OBS. \<lbrakk>\<And>vs OBS. \<lbrakk>eq_upto_seq_inconsist P obs OBS vs; ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs; eq_upto_seq_inconsist P (a # obs) OBS vs; ta_seq_consist P vs (llist_of (a # obs)) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P ((a # obs) @ obs') (OBS @ OBS') vs
[PROOF STEP]
apply(auto simp add: eq_upto_seq_inconsist_Cons1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a obs vs ob' obs''. \<lbrakk>\<And>vs OBS. \<lbrakk>eq_upto_seq_inconsist P obs OBS vs; ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs; (case a of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ta_seq_consist P (mrw_value P vs a) (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P (mrw_value P vs ob') obs''); case a of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a) else a \<approx> ob' | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a)\<rbrakk> \<Longrightarrow> case a of NormalAction (ReadMem ad al v) \<Rightarrow> ((\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> ob' = a \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') (mrw_value P vs a)) \<and> ((\<nexists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> a \<approx> ob') | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') (mrw_value P vs a)
[PROOF STEP]
apply(simp split: action.split obs_event.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a obs vs ob' obs''. \<lbrakk>\<And>vs OBS. \<lbrakk>eq_upto_seq_inconsist P obs OBS vs; ta_seq_consist P vs (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P vs OBS)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (obs @ obs') (OBS @ OBS') vs; (case a of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<and> ta_seq_consist P (mrw_value P vs a) (llist_of obs) \<Longrightarrow> eq_upto_seq_inconsist P obs' OBS' (mrw_values P (mrw_value P vs ob') obs''); case a of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a) else a \<approx> ob' | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs'' (mrw_value P vs a)\<rbrakk> \<Longrightarrow> (\<forall>x1. (\<forall>x11 x12 x13 x14. x1 = ExternalCall x11 x12 x13 x14 \<longrightarrow> a = NormalAction (ExternalCall x11 x12 x13 x14) \<longrightarrow> ob' = NormalAction (ExternalCall x11 x12 x13 x14) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x21 x22 x23. x1 = ReadMem x21 x22 x23 \<longrightarrow> a = NormalAction (ReadMem x21 x22 x23) \<longrightarrow> ((\<exists>b. vs (x21, x22) = \<lfloor>(x23, b)\<rfloor>) \<longrightarrow> ob' = NormalAction (ReadMem x21 x22 x23) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> ((\<forall>b. vs (x21, x22) \<noteq> \<lfloor>(x23, b)\<rfloor>) \<longrightarrow> (\<exists>v'. ob' = NormalAction (ReadMem x21 x22 v')))) \<and> (\<forall>x31 x32 x33. x1 = WriteMem x31 x32 x33 \<longrightarrow> a = NormalAction (WriteMem x31 x32 x33) \<longrightarrow> ob' = NormalAction (WriteMem x31 x32 x33) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') (vs((x31, x32) \<mapsto> (x33, True)))) \<and> (\<forall>x41 x42. x1 = NewHeapElem x41 x42 \<longrightarrow> a = NormalAction (NewHeapElem x41 x42) \<longrightarrow> ob' = NormalAction (NewHeapElem x41 x42) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') (\<lambda>(ad', al). if x41 = ad' \<and> al \<in> addr_locs P x42 \<and> (case vs (x41, al) of None \<Rightarrow> True | \<lfloor>(v, xa)\<rfloor> \<Rightarrow> \<not> xa) then \<lfloor>(addr_loc_default P x42 al, False)\<rfloor> else vs (ad', al))) \<and> (\<forall>x5. x1 = ThreadStart x5 \<longrightarrow> a = NormalAction (ThreadStart x5) \<longrightarrow> ob' = NormalAction (ThreadStart x5) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x6. x1 = ThreadJoin x6 \<longrightarrow> a = NormalAction (ThreadJoin x6) \<longrightarrow> ob' = NormalAction (ThreadJoin x6) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x7. x1 = SyncLock x7 \<longrightarrow> a = NormalAction (SyncLock x7) \<longrightarrow> ob' = NormalAction (SyncLock x7) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x8. x1 = SyncUnlock x8 \<longrightarrow> a = NormalAction (SyncUnlock x8) \<longrightarrow> ob' = NormalAction (SyncUnlock x8) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x9. x1 = ObsInterrupt x9 \<longrightarrow> a = NormalAction (ObsInterrupt x9) \<longrightarrow> ob' = NormalAction (ObsInterrupt x9) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (\<forall>x10. x1 = ObsInterrupted x10 \<longrightarrow> a = NormalAction (ObsInterrupted x10) \<longrightarrow> ob' = NormalAction (ObsInterrupted x10) \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs)) \<and> (a = InitialThreadAction \<longrightarrow> ob' = InitialThreadAction \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs) \<and> (a = ThreadFinishAction \<longrightarrow> ob' = ThreadFinishAction \<and> eq_upto_seq_inconsist P (obs @ obs') (obs'' @ OBS') vs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eq_upto_seq_inconsist_trans:
  "\<lbrakk> eq_upto_seq_inconsist P obs obs' vs; eq_upto_seq_inconsist P obs' obs'' vs \<rbrakk>
  \<Longrightarrow> eq_upto_seq_inconsist P obs obs'' vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; eq_upto_seq_inconsist P obs' obs'' vs\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs obs'' vs
[PROOF STEP]
apply(induction obs arbitrary: obs' obs'' vs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>obs' obs'' vs. \<lbrakk>eq_upto_seq_inconsist P [] obs' vs; eq_upto_seq_inconsist P obs' obs'' vs\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P [] obs'' vs
 2. \<And>a obs obs' obs'' vs. \<lbrakk>\<And>obs' obs'' vs. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; eq_upto_seq_inconsist P obs' obs'' vs\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs obs'' vs; eq_upto_seq_inconsist P (a # obs) obs' vs; eq_upto_seq_inconsist P obs' obs'' vs\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (a # obs) obs'' vs
[PROOF STEP]
apply(clarsimp simp add: eq_upto_seq_inconsist_Cons1)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a obs vs ob' obs''a ob'a obs''b. \<lbrakk>\<And>obs' obs'' vs. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; eq_upto_seq_inconsist P obs' obs'' vs\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs obs'' vs; case a of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a) else a \<approx> ob' | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a); case ob' of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob'a = ob' \<and> eq_upto_seq_inconsist P obs''a obs''b (mrw_value P vs ob') else ob' \<approx> ob'a | NormalAction _ \<Rightarrow> ob'a = ob' \<and> eq_upto_seq_inconsist P obs''a obs''b (mrw_value P vs ob') | _ \<Rightarrow> ob'a = ob' \<and> eq_upto_seq_inconsist P obs''a obs''b (mrw_value P vs ob')\<rbrakk> \<Longrightarrow> case a of NormalAction (ReadMem ad al v) \<Rightarrow> ((\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> ob'a = a \<and> eq_upto_seq_inconsist P obs obs''b (mrw_value P vs a)) \<and> ((\<nexists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> a \<approx> ob'a) | NormalAction _ \<Rightarrow> ob'a = a \<and> eq_upto_seq_inconsist P obs obs''b (mrw_value P vs a) | _ \<Rightarrow> ob'a = a \<and> eq_upto_seq_inconsist P obs obs''b (mrw_value P vs a)
[PROOF STEP]
apply(auto split!: action.split obs_event.split if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eq_upto_seq_inconsist_append2:
  "\<lbrakk> eq_upto_seq_inconsist P obs obs' vs; \<not> ta_seq_consist P vs (llist_of obs) \<rbrakk>
  \<Longrightarrow> eq_upto_seq_inconsist P obs (obs' @ obs'') vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; \<not> ta_seq_consist P vs (llist_of obs)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs (obs' @ obs'') vs
[PROOF STEP]
apply(induction obs arbitrary: obs' vs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>obs' vs. \<lbrakk>eq_upto_seq_inconsist P [] obs' vs; \<not> ta_seq_consist P vs (llist_of [])\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P [] (obs' @ obs'') vs
 2. \<And>a obs obs' vs. \<lbrakk>\<And>obs' vs. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; \<not> ta_seq_consist P vs (llist_of obs)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs (obs' @ obs'') vs; eq_upto_seq_inconsist P (a # obs) obs' vs; \<not> ta_seq_consist P vs (llist_of (a # obs))\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P (a # obs) (obs' @ obs'') vs
[PROOF STEP]
apply(clarsimp simp add: eq_upto_seq_inconsist_Cons1)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a obs vs ob' obs''a. \<lbrakk>\<And>obs' vs. \<lbrakk>eq_upto_seq_inconsist P obs obs' vs; \<not> ta_seq_consist P vs (llist_of obs)\<rbrakk> \<Longrightarrow> eq_upto_seq_inconsist P obs (obs' @ obs'') vs; (case a of NormalAction (ReadMem ad al v) \<Rightarrow> \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> | NormalAction _ \<Rightarrow> True | _ \<Rightarrow> True) \<longrightarrow> \<not> ta_seq_consist P (mrw_value P vs a) (llist_of obs); case a of NormalAction (ReadMem ad al v) \<Rightarrow> if \<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor> then ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a) else a \<approx> ob' | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs obs''a (mrw_value P vs a)\<rbrakk> \<Longrightarrow> case a of NormalAction (ReadMem ad al v) \<Rightarrow> ((\<exists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs (obs''a @ obs'') (mrw_value P vs a)) \<and> ((\<nexists>b. vs (ad, al) = \<lfloor>(v, b)\<rfloor>) \<longrightarrow> a \<approx> ob') | NormalAction _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs (obs''a @ obs'') (mrw_value P vs a) | _ \<Rightarrow> ob' = a \<and> eq_upto_seq_inconsist P obs (obs''a @ obs'') (mrw_value P vs a)
[PROOF STEP]
apply(auto split!: action.split obs_event.split if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ta_seq_consist_mrwI:
  assumes E: "E \<in> \<E>"
  and wf: "P \<turnstile> (E, ws) \<surd>"
  and mrw: "\<And>a. \<lbrakk> enat a < r; a \<in> read_actions E \<rbrakk> \<Longrightarrow> P,E \<turnstile> a \<leadsto>mrw ws a"
  shows "ta_seq_consist P Map.empty (lmap snd (ltake r E))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_seq_consist P Map.empty (lmap snd (ltake r E))
[PROOF STEP]
proof(rule ta_seq_consist_nthI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
fix i ad al v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
assume i_len: "enat i < llength (lmap snd (ltake r E))"
    and E_i: "lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v)"
    and sc: "ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))"
[PROOF STATE]
proof (state)
this:
enat i < llength (lmap snd (ltake r E))
lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v)
ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from i_len
[PROOF STATE]
proof (chain)
picking this:
enat i < llength (lmap snd (ltake r E))
[PROOF STEP]
have "enat i < r"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. enat i < r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat i < r

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
with sc
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))
enat i < r
[PROOF STEP]
have "ta_seq_consist P Map.empty (ltake (enat i) (lmap snd E))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))
enat i < r

goal (1 subgoal):
 1. ta_seq_consist P Map.empty (ltake (enat i) (lmap snd E))
[PROOF STEP]
by(simp add: min_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P Map.empty (ltake (enat i) (lmap snd E))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
hence ns: "non_speculative P (\<lambda>_. {}) (ltake (enat i) (lmap snd E))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P Map.empty (ltake (enat i) (lmap snd E))

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

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from i_len
[PROOF STATE]
proof (chain)
picking this:
enat i < llength (lmap snd (ltake r E))
[PROOF STEP]
have "i \<in> actions E"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lmap snd (ltake r E))

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

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in> actions E

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from E_i i_len
[PROOF STATE]
proof (chain)
picking this:
lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v)
enat i < llength (lmap snd (ltake r E))
[PROOF STEP]
have obs_i: "action_obs E i = NormalAction (ReadMem ad al v)"
[PROOF STATE]
proof (prove)
using this:
lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v)
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. action_obs E i = NormalAction (ReadMem ad al v)
[PROOF STEP]
by(simp add: action_obs_def lnth_ltake)
[PROOF STATE]
proof (state)
this:
action_obs E i = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<in> actions E
action_obs E i = NormalAction (ReadMem ad al v)
[PROOF STEP]
have read: "i \<in> read_actions E"
[PROOF STATE]
proof (prove)
using this:
i \<in> actions E
action_obs E i = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. i \<in> read_actions E
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i \<in> read_actions E

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
with i_len
[PROOF STATE]
proof (chain)
picking this:
enat i < llength (lmap snd (ltake r E))
i \<in> read_actions E
[PROOF STEP]
have mrw_i: "P,E \<turnstile> i \<leadsto>mrw ws i"
[PROOF STATE]
proof (prove)
using this:
enat i < llength (lmap snd (ltake r E))
i \<in> read_actions E

goal (1 subgoal):
 1. P,E \<turnstile> i \<leadsto>mrw ws i
[PROOF STEP]
by(auto intro: mrw)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> i \<leadsto>mrw ws i

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
with E
[PROOF STATE]
proof (chain)
picking this:
E \<in> \<E>
P,E \<turnstile> i \<leadsto>mrw ws i
[PROOF STEP]
have "ws i < i"
[PROOF STATE]
proof (prove)
using this:
E \<in> \<E>
P,E \<turnstile> i \<leadsto>mrw ws i

goal (1 subgoal):
 1. ws i < i
[PROOF STEP]
using ns
[PROOF STATE]
proof (prove)
using this:
E \<in> \<E>
P,E \<turnstile> i \<leadsto>mrw ws i
non_speculative P (\<lambda>_. {}) (ltake (enat i) (lmap snd E))

goal (1 subgoal):
 1. ws i < i
[PROOF STEP]
by(rule mrw_before)
[PROOF STATE]
proof (state)
this:
ws i < i

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from mrw_i obs_i
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> i \<leadsto>mrw ws i
action_obs E i = NormalAction (ReadMem ad al v)
[PROOF STEP]
obtain adal_w: "(ad, al) \<in> action_loc P E (ws i)"
    and adal_r: "(ad, al) \<in> action_loc P E i"
    and "write": "ws i \<in> write_actions E"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> i \<leadsto>mrw ws i
action_obs E i = NormalAction (ReadMem ad al v)

goal (1 subgoal):
 1. (\<lbrakk>(ad, al) \<in> action_loc P E (ws i); (ad, al) \<in> action_loc P E i; ws i \<in> write_actions E\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc P E (ws i)
(ad, al) \<in> action_loc P E i
ws i \<in> write_actions E

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> (E, ws) \<surd>
[PROOF STEP]
have "is_write_seen P E ws"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> (E, ws) \<surd>

goal (1 subgoal):
 1. is_write_seen P E ws
[PROOF STEP]
by(rule wf_exec_is_write_seenD)
[PROOF STATE]
proof (state)
this:
is_write_seen P E ws

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from is_write_seenD[OF this read obs_i]
[PROOF STATE]
proof (chain)
picking this:
ws i \<in> write_actions E \<and> (ad, al) \<in> action_loc P E (ws i) \<and> value_written P E (ws i) (ad, al) = v \<and> \<not> P,E \<turnstile> i \<le>hb ws i \<and> (is_volatile P al \<longrightarrow> \<not> P,E \<turnstile> i \<le>so ws i) \<and> (\<forall>a'\<in>write_actions E. (ad, al) \<in> action_loc P E a' \<and> (P,E \<turnstile> ws i \<le>hb a' \<and> P,E \<turnstile> a' \<le>hb i \<or> is_volatile P al \<and> P,E \<turnstile> ws i \<le>so a' \<and> P,E \<turnstile> a' \<le>so i) \<longrightarrow> a' = ws i)
[PROOF STEP]
have vw_v: "value_written P E (ws i) (ad, al) = v"
[PROOF STATE]
proof (prove)
using this:
ws i \<in> write_actions E \<and> (ad, al) \<in> action_loc P E (ws i) \<and> value_written P E (ws i) (ad, al) = v \<and> \<not> P,E \<turnstile> i \<le>hb ws i \<and> (is_volatile P al \<longrightarrow> \<not> P,E \<turnstile> i \<le>so ws i) \<and> (\<forall>a'\<in>write_actions E. (ad, al) \<in> action_loc P E a' \<and> (P,E \<turnstile> ws i \<le>hb a' \<and> P,E \<turnstile> a' \<le>hb i \<or> is_volatile P al \<and> P,E \<turnstile> ws i \<le>so a' \<and> P,E \<turnstile> a' \<le>so i) \<longrightarrow> a' = ws i)

goal (1 subgoal):
 1. value_written P E (ws i) (ad, al) = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
value_written P E (ws i) (ad, al) = v

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
let ?vs = "mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from \<open>ws i < i\<close> i_len
[PROOF STATE]
proof (chain)
picking this:
ws i < i
enat i < llength (lmap snd (ltake r E))
[PROOF STEP]
have "enat (ws i) < llength (ltake (enat i) E)"
[PROOF STATE]
proof (prove)
using this:
ws i < i
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. enat (ws i) < llength (ltake (enat i) E)
[PROOF STEP]
by(simp add: less_trans[where y="enat i"])
[PROOF STATE]
proof (state)
this:
enat (ws i) < llength (ltake (enat i) E)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
hence "ltake (enat i) E = lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))"
[PROOF STATE]
proof (prove)
using this:
enat (ws i) < llength (ltake (enat i) E)

goal (1 subgoal):
 1. ltake (enat i) E = lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))
[PROOF STEP]
by(simp only: ldropn_Suc_conv_ldropn lappend_ltake_enat_ldropn)
[PROOF STATE]
proof (state)
this:
ltake (enat i) E = lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ltake (enat i) E = lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
have "\<dots> = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E))) = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))
[PROOF STEP]
using \<open>ws i < i\<close> i_len \<open>enat (ws i) < llength (ltake (enat i) E)\<close>
[PROOF STATE]
proof (prove)
using this:
ws i < i
enat i < llength (lmap snd (ltake r E))
enat (ws i) < llength (ltake (enat i) E)

goal (1 subgoal):
 1. lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E))) = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))
[PROOF STEP]
by (simp add: lnth_ltake)
[PROOF STATE]
proof (state)
this:
lappend (ltake (enat (ws i)) (ltake (enat i) E)) (LCons (lnth (ltake (enat i) E) (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E))) = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ltake (enat i) E = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))
[PROOF STEP]
have r_E: "ltake (enat i) E = \<dots>"
[PROOF STATE]
proof (prove)
using this:
ltake (enat i) E = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))

goal (1 subgoal):
 1. ltake (enat i) E = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ltake (enat i) E = lappend (ltake (enat (ws i)) E) (LCons (lnth E (ws i)) (ldropn (Suc (ws i)) (ltake (enat i) E)))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
have "mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al)
    = mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)
[PROOF STEP]
using \<open>enat i < r\<close>
[PROOF STATE]
proof (prove)
using this:
enat i < r

goal (1 subgoal):
 1. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)
[PROOF STEP]
by(auto simp add: min_def)
[PROOF STATE]
proof (state)
this:
mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
have "\<dots> = mrw_values P (mrw_value P ?vs (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al) = mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al)
[PROOF STEP]
by(subst r_E)(simp add: list_of_lappend)
[PROOF STATE]
proof (state)
this:
mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al) = mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mrw_values P Map.empty (map snd (list_of (ltake (enat i) E))) (ad, al) = mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
have "\<dots> = mrw_value P ?vs (snd (lnth E (ws i))) (ad, al)"
[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 (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al) = mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al)
[PROOF STEP]
proof(rule mrw_values_no_write_unchanged)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
fix wa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
assume wa: "wa \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))"
      and "is_write_action wa" "(ad, al) \<in> action_loc_aux P wa"
[PROOF STATE]
proof (state)
this:
wa \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from wa
[PROOF STATE]
proof (chain)
picking this:
wa \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
[PROOF STEP]
obtain w where "w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))"
      and "map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa"
[PROOF STATE]
proof (prove)
using this:
wa \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
\<exists>ia<length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))). map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! ia = wa

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
hence "Suc (ws i + w) < i" (is "?w < _")
[PROOF STATE]
proof (prove)
using this:
w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa

goal (1 subgoal):
 1. Suc (ws i + w) < i
[PROOF STEP]
using i_len
[PROOF STATE]
proof (prove)
using this:
w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. Suc (ws i + w) < i
[PROOF STEP]
by(cases "llength E")(simp_all add: length_list_of_conv_the_enat)
[PROOF STATE]
proof (state)
this:
Suc (ws i + w) < i

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

goal (1 subgoal):
 1. action_obs E (Suc (ws i + w)) = wa
[PROOF STEP]
using i_len
[PROOF STATE]
proof (prove)
using this:
w < length (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))))
map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E))) ! w = wa
Suc (ws i + w) < i
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. action_obs E (Suc (ws i + w)) = wa
[PROOF STEP]
by(simp add: action_obs_def lnth_ltake less_trans[where y="enat i"] ac_simps)
[PROOF STATE]
proof (state)
this:
action_obs E (Suc (ws i + w)) = wa

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from \<open>?w < i\<close> i_len
[PROOF STATE]
proof (chain)
picking this:
Suc (ws i + w) < i
enat i < llength (lmap snd (ltake r E))
[PROOF STEP]
have "?w \<in> actions E"
[PROOF STATE]
proof (prove)
using this:
Suc (ws i + w) < i
enat i < llength (lmap snd (ltake r E))

goal (1 subgoal):
 1. Suc (ws i + w) \<in> actions E
[PROOF STEP]
by(simp add: actions_def less_trans[where y="enat i"])
[PROOF STATE]
proof (state)
this:
Suc (ws i + w) \<in> actions E

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
with \<open>is_write_action wa\<close> obs_w' \<open>(ad, al) \<in> action_loc_aux P wa\<close>
[PROOF STATE]
proof (chain)
picking this:
is_write_action wa
action_obs E (Suc (ws i + w)) = wa
(ad, al) \<in> action_loc_aux P wa
Suc (ws i + w) \<in> actions E
[PROOF STEP]
have write': "?w \<in> write_actions E"
      and adal': "(ad, al) \<in> action_loc P E ?w"
[PROOF STATE]
proof (prove)
using this:
is_write_action wa
action_obs E (Suc (ws i + w)) = wa
(ad, al) \<in> action_loc_aux P wa
Suc (ws i + w) \<in> actions E

goal (1 subgoal):
 1. Suc (ws i + w) \<in> write_actions E &&& (ad, al) \<in> action_loc P E (Suc (ws i + w))
[PROOF STEP]
by(auto intro: write_actions.intros)
[PROOF STATE]
proof (state)
this:
Suc (ws i + w) \<in> write_actions E
(ad, al) \<in> action_loc P E (Suc (ws i + w))

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from \<open>?w < i\<close> \<open>i \<in> read_actions E\<close> \<open>?w \<in> actions E\<close>
[PROOF STATE]
proof (chain)
picking this:
Suc (ws i + w) < i
i \<in> read_actions E
Suc (ws i + w) \<in> actions E
[PROOF STEP]
have "E \<turnstile> ?w \<le>a i"
[PROOF STATE]
proof (prove)
using this:
Suc (ws i + w) < i
i \<in> read_actions E
Suc (ws i + w) \<in> actions E

goal (1 subgoal):
 1. E \<turnstile> Suc (ws i + w) \<le>a i
[PROOF STEP]
by(auto simp add: action_order_def elim: read_actions.cases)
[PROOF STATE]
proof (state)
this:
E \<turnstile> Suc (ws i + w) \<le>a i

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from mrw_i adal_r write' adal'
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> i \<leadsto>mrw ws i
(ad, al) \<in> action_loc P E i
Suc (ws i + w) \<in> write_actions E
(ad, al) \<in> action_loc P E (Suc (ws i + w))
[PROOF STEP]
have "E \<turnstile> ?w \<le>a ws i \<or> E \<turnstile> i \<le>a ?w"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> i \<leadsto>mrw ws i
(ad, al) \<in> action_loc P E i
Suc (ws i + w) \<in> write_actions E
(ad, al) \<in> action_loc P E (Suc (ws i + w))

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

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

goal (1 subgoal):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
 2. E \<turnstile> i \<le>a Suc (ws i + w) \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
assume "E \<turnstile> i \<le>a ?w"
[PROOF STATE]
proof (state)
this:
E \<turnstile> i \<le>a Suc (ws i + w)

goal (2 subgoals):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
 2. E \<turnstile> i \<le>a Suc (ws i + w) \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
with \<open>E \<turnstile> ?w \<le>a i\<close>
[PROOF STATE]
proof (chain)
picking this:
E \<turnstile> Suc (ws i + w) \<le>a i
E \<turnstile> i \<le>a Suc (ws i + w)
[PROOF STEP]
have "?w = i"
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> Suc (ws i + w) \<le>a i
E \<turnstile> i \<le>a Suc (ws i + w)

goal (1 subgoal):
 1. Suc (ws i + w) = i
[PROOF STEP]
by(rule antisymPD[OF antisym_action_order])
[PROOF STATE]
proof (state)
this:
Suc (ws i + w) = i

goal (2 subgoals):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
 2. E \<turnstile> i \<le>a Suc (ws i + w) \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
with write' read
[PROOF STATE]
proof (chain)
picking this:
Suc (ws i + w) \<in> write_actions E
i \<in> read_actions E
Suc (ws i + w) = i
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
Suc (ws i + w) \<in> write_actions E
i \<in> read_actions E
Suc (ws i + w) = i

goal (1 subgoal):
 1. False
[PROOF STEP]
by(auto dest: read_actions_not_write_actions)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
 2. E \<turnstile> i \<le>a Suc (ws i + w) \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. E \<turnstile> Suc (ws i + w) \<le>a ws i \<Longrightarrow> E \<turnstile> Suc (ws i + w) \<le>a ws i
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E \<turnstile> Suc (ws i + w) \<le>a ws i

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from adal_w "write"
[PROOF STATE]
proof (chain)
picking this:
(ad, al) \<in> action_loc P E (ws i)
ws i \<in> write_actions E
[PROOF STEP]
have "mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
(ad, al) \<in> action_loc P E (ws i)
ws i \<in> write_actions E

goal (1 subgoal):
 1. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) \<noteq> None
[PROOF STEP]
by(cases "snd (lnth E (ws i))" rule: mrw_value_cases)
        (auto simp add: action_obs_def split: if_split_asm elim: write_actions.cases)
[PROOF STATE]
proof (state)
this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) \<noteq> None

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) \<noteq> None
[PROOF STEP]
obtain b v where vb: "mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) = Some (v, b)"
[PROOF STATE]
proof (prove)
using this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) \<noteq> None

goal (1 subgoal):
 1. (\<And>v b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from \<open>E \<turnstile> ?w \<le>a ws i\<close> obs_w'
[PROOF STATE]
proof (chain)
picking this:
E \<turnstile> Suc (ws i + w) \<le>a ws i
action_obs E (Suc (ws i + w)) = wa
[PROOF STEP]
have "is_new_action wa" "\<not> is_new_action (action_obs E (ws i))"
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> Suc (ws i + w) \<le>a ws i
action_obs E (Suc (ws i + w)) = wa

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
from \<open>\<not> is_new_action (action_obs E (ws i))\<close> "write" adal_w
[PROOF STATE]
proof (chain)
picking this:
\<not> is_new_action (action_obs E (ws i))
ws i \<in> write_actions E
(ad, al) \<in> action_loc P E (ws i)
[PROOF STEP]
obtain v' where "action_obs E (ws i) = NormalAction (WriteMem ad al v')"
[PROOF STATE]
proof (prove)
using this:
\<not> is_new_action (action_obs E (ws i))
ws i \<in> write_actions E
(ad, al) \<in> action_loc P E (ws i)

goal (1 subgoal):
 1. (\<And>v'. action_obs E (ws i) = NormalAction (WriteMem ad al v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!: write_actions.cases is_write_action.cases)
[PROOF STATE]
proof (state)
this:
action_obs E (ws i) = NormalAction (WriteMem ad al v')

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
with vb
[PROOF STATE]
proof (chain)
picking this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>
action_obs E (ws i) = NormalAction (WriteMem ad al v')
[PROOF STEP]
have b
[PROOF STATE]
proof (prove)
using this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>
action_obs E (ws i) = NormalAction (WriteMem ad al v')

goal (1 subgoal):
 1. b
[PROOF STEP]
by(simp add: action_obs_def)
[PROOF STATE]
proof (state)
this:
b

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> set (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))); is_write_action w; (ad, al) \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action w
[PROOF STEP]
with \<open>is_new_action wa\<close> vb
[PROOF STATE]
proof (chain)
picking this:
is_new_action wa
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>
b
[PROOF STEP]
show "case mrw_value P ?vs (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa"
[PROOF STATE]
proof (prove)
using this:
is_new_action wa
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>
b

goal (1 subgoal):
 1. case mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) 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 (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) of None \<Rightarrow> False | \<lfloor>(v, b)\<rfloor> \<Rightarrow> b \<and> is_new_action wa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al) = mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al) = mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mrw_values P (mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i)))) (map snd (list_of (ldropn (Suc (ws i)) (ltake (enat i) E)))) (ad, al) = mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
assume "?vs (ad, al) = Some (v, True)"
      and "is_new_action (action_obs E (ws i))"
[PROOF STATE]
proof (state)
this:
mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(v, True)\<rfloor>
is_new_action (action_obs E (ws i))

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
from mrw_values_eq_SomeD[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
(None = \<lfloor>(v, True)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd (list_of (ltake (enat (ws i)) 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 (ws i)) 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 wa where "wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))"
      and "is_write_action wa"
      and "(ad, al) \<in> action_loc_aux P wa"
      and "\<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 (ws i)) 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 (ws i)) 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>wa. \<lbrakk>wa \<in> set (map snd (list_of (ltake (enat (ws i)) E))); 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(fastforce simp del: set_map)
[PROOF STATE]
proof (state)
this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa
[PROOF STEP]
obtain w where w: "w < ws i"  and wa: "wa = snd (lnth E w)"
[PROOF STATE]
proof (prove)
using this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w < ws i; wa = snd (lnth E w)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
\<exists>ia<length (map snd (list_of (ltake (enat (ws i)) E))). map snd (list_of (ltake (enat (ws i)) E)) ! ia = wa
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w < ws i; wa = snd (lnth E w)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "llength E")(auto simp add: lnth_ltake length_list_of_conv_the_enat)
[PROOF STATE]
proof (state)
this:
w < ws i
wa = snd (lnth E w)

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa
w < ws i
wa = snd (lnth E w)
[PROOF STEP]
have "w \<in> write_actions E" "action_obs E w = wa" "(ad, al) \<in> action_loc P E w"
[PROOF STATE]
proof (prove)
using this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa
w < ws i
wa = snd (lnth E w)

goal (1 subgoal):
 1. w \<in> write_actions E &&& action_obs E w = wa &&& (ad, al) \<in> action_loc P E w
[PROOF STEP]
using \<open>ws i \<in> write_actions E\<close>
[PROOF STATE]
proof (prove)
using this:
wa \<in> set (map snd (list_of (ltake (enat (ws i)) E)))
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
\<not> is_new_action wa
w < ws i
wa = snd (lnth E w)
ws i \<in> write_actions E

goal (1 subgoal):
 1. w \<in> write_actions E &&& action_obs E w = wa &&& (ad, al) \<in> action_loc P E w
[PROOF STEP]
by(auto intro!: write_actions.intros simp add: actions_def less_trans[where y="enat (ws i)"] action_obs_def elim!: write_actions.cases)
[PROOF STATE]
proof (state)
this:
w \<in> write_actions E
action_obs E w = wa
(ad, al) \<in> action_loc P E w

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
with mrw_i adal_r
[PROOF STATE]
proof (chain)
picking this:
P,E \<turnstile> i \<leadsto>mrw ws i
(ad, al) \<in> action_loc P E i
w \<in> write_actions E
action_obs E w = wa
(ad, al) \<in> action_loc P E w
[PROOF STEP]
have "E \<turnstile> w \<le>a ws i \<or> E \<turnstile> i \<le>a w"
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> i \<leadsto>mrw ws i
(ad, al) \<in> action_loc P E i
w \<in> write_actions E
action_obs E w = wa
(ad, al) \<in> action_loc P E w

goal (1 subgoal):
 1. E \<turnstile> w \<le>a ws i \<or> E \<turnstile> i \<le>a w
[PROOF STEP]
by -(rule most_recent_write_recent)
[PROOF STATE]
proof (state)
this:
E \<turnstile> w \<le>a ws i \<or> E \<turnstile> i \<le>a w

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> w \<le>a ws i \<or> E \<turnstile> i \<le>a w

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. E \<turnstile> w \<le>a ws i \<Longrightarrow> False
 2. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
assume "E \<turnstile> w \<le>a ws i"
[PROOF STATE]
proof (state)
this:
E \<turnstile> w \<le>a ws i

goal (2 subgoals):
 1. E \<turnstile> w \<le>a ws i \<Longrightarrow> False
 2. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
E \<turnstile> w \<le>a ws i

goal (2 subgoals):
 1. E \<turnstile> w \<le>a ws i \<Longrightarrow> False
 2. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
from \<open>\<not> is_new_action wa\<close> \<open>is_new_action (action_obs E (ws i))\<close> "write" w wa \<open>w \<in> write_actions E\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> is_new_action wa
is_new_action (action_obs E (ws i))
ws i \<in> write_actions E
w < ws i
wa = snd (lnth E w)
w \<in> write_actions E
[PROOF STEP]
have "E \<turnstile> ws i \<le>a w"
[PROOF STATE]
proof (prove)
using this:
\<not> is_new_action wa
is_new_action (action_obs E (ws i))
ws i \<in> write_actions E
w < ws i
wa = snd (lnth E w)
w \<in> write_actions E

goal (1 subgoal):
 1. E \<turnstile> ws i \<le>a w
[PROOF STEP]
by(auto simp add: action_order_def action_obs_def)
[PROOF STATE]
proof (state)
this:
E \<turnstile> ws i \<le>a w

goal (2 subgoals):
 1. E \<turnstile> w \<le>a ws i \<Longrightarrow> False
 2. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
E \<turnstile> w \<le>a ws i
E \<turnstile> ws i \<le>a w
[PROOF STEP]
have "w = ws i"
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> w \<le>a ws i
E \<turnstile> ws i \<le>a w

goal (1 subgoal):
 1. w = ws i
[PROOF STEP]
by(rule antisymPD[OF antisym_action_order])
[PROOF STATE]
proof (state)
this:
w = ws i

goal (2 subgoals):
 1. E \<turnstile> w \<le>a ws i \<Longrightarrow> False
 2. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
with \<open>w < ws i\<close>
[PROOF STATE]
proof (chain)
picking this:
w < ws i
w = ws i
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
w < ws i
w = ws i

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

goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
assume "E \<turnstile> i \<le>a w"
[PROOF STATE]
proof (state)
this:
E \<turnstile> i \<le>a w

goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
E \<turnstile> i \<le>a w

goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
from \<open>w \<in> write_actions E\<close> \<open>w < ws i\<close> \<open>ws i < i\<close> read
[PROOF STATE]
proof (chain)
picking this:
w \<in> write_actions E
w < ws i
ws i < i
i \<in> read_actions E
[PROOF STEP]
have "E \<turnstile> w \<le>a i"
[PROOF STATE]
proof (prove)
using this:
w \<in> write_actions E
w < ws i
ws i < i
i \<in> read_actions E

goal (1 subgoal):
 1. E \<turnstile> w \<le>a i
[PROOF STEP]
by(auto simp add: action_order_def elim: read_actions.cases)
[PROOF STATE]
proof (state)
this:
E \<turnstile> w \<le>a i

goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
E \<turnstile> i \<le>a w
E \<turnstile> w \<le>a i
[PROOF STEP]
have "i = w"
[PROOF STATE]
proof (prove)
using this:
E \<turnstile> i \<le>a w
E \<turnstile> w \<le>a i

goal (1 subgoal):
 1. i = w
[PROOF STEP]
by(rule antisymPD[OF antisym_action_order])
[PROOF STATE]
proof (state)
this:
i = w

goal (1 subgoal):
 1. E \<turnstile> i \<le>a w \<Longrightarrow> False
[PROOF STEP]
with \<open>w < ws i\<close> \<open>ws i < i\<close>
[PROOF STATE]
proof (chain)
picking this:
w < ws i
ws i < i
i = w
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
w < ws i
ws i < i
i = w

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(?va2, True)\<rfloor>; is_new_action (action_obs E (ws i))\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(?va2, True)\<rfloor>; is_new_action (action_obs E (ws i))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain b where "\<dots> = Some (v, b)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(?va2, True)\<rfloor>; is_new_action (action_obs E (ws i))\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (\<And>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vw_v "write" adal_w
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(?va2, True)\<rfloor>; is_new_action (action_obs E (ws i))\<rbrakk> \<Longrightarrow> False
value_written P E (ws i) (ad, al) = v
ws i \<in> write_actions E
(ad, al) \<in> action_loc P E (ws i)

goal (1 subgoal):
 1. (\<And>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(atomize_elim)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>va. \<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(va, True)\<rfloor>; is_new_action (action_obs E (ws i))\<rbrakk> \<Longrightarrow> False; value_written P E (ws i) (ad, al) = v; ws i \<in> write_actions E; (ad, al) \<in> action_loc P E (ws i)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(auto simp add: action_obs_def value_written_def write_actions_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>va. \<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(va, True)\<rfloor>; is_new_action (snd (lnth E (ws i)))\<rbrakk> \<Longrightarrow> False; (ad, al) \<in> action_loc_aux P (snd (lnth E (ws i))); v = value_written_aux P (snd (lnth E (ws i))) al; ws i \<in> actions E; is_write_action (snd (lnth E (ws i)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(value_written_aux P (snd (lnth E (ws i))) al, b)\<rfloor>
[PROOF STEP]
apply(erule is_write_action.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ada hT. \<lbrakk>\<And>va. \<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(va, True)\<rfloor>; is_new_action (snd (lnth E (ws i)))\<rbrakk> \<Longrightarrow> False; (ad, al) \<in> action_loc_aux P (snd (lnth E (ws i))); v = value_written_aux P (snd (lnth E (ws i))) al; ws i \<in> actions E; snd (lnth E (ws i)) = NormalAction (NewHeapElem ada hT)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(value_written_aux P (snd (lnth E (ws i))) al, b)\<rfloor>
 2. \<And>ada ala va. \<lbrakk>\<And>va. \<lbrakk>mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E))) (ad, al) = \<lfloor>(va, True)\<rfloor>; is_new_action (snd (lnth E (ws i)))\<rbrakk> \<Longrightarrow> False; (ad, al) \<in> action_loc_aux P (snd (lnth E (ws i))); v = value_written_aux P (snd (lnth E (ws i))) al; ws i \<in> actions E; snd (lnth E (ws i)) = NormalAction (WriteMem ada ala va)\<rbrakk> \<Longrightarrow> \<exists>b. mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(value_written_aux P (snd (lnth E (ws i))) al, b)\<rfloor>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mrw_value P (mrw_values P Map.empty (map snd (list_of (ltake (enat (ws i)) E)))) (snd (lnth E (ws i))) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<And>i ad al v. \<lbrakk>enat i < llength (lmap snd (ltake r E)); lnth (lmap snd (ltake r E)) i = NormalAction (ReadMem ad al v); ta_seq_consist P Map.empty (ltake (enat i) (lmap snd (ltake r E)))\<rbrakk> \<Longrightarrow> \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
show "\<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. mrw_values P Map.empty (list_of (ltake (enat i) (lmap snd (ltake r E)))) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sc_completionD:
  "\<lbrakk> sc_completion s vs; s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)));
     thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> (x, shr s') -ta\<rightarrow> (x', m'); actions_ok s' t ta \<rbrakk>
  \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> (x, shr s') -ta'\<rightarrow> (x'', m'') \<and> actions_ok s' t ta' \<and>
                   ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sc_completion s vs; s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
unfolding sc_completion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ttas s' t x ta x' m'. s -\<triangleright>ttas\<rightarrow>* s' \<longrightarrow> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<longrightarrow> thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor> \<longrightarrow> t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle> \<longrightarrow> actions_ok s' t ta \<longrightarrow> (\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)); s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
by blast


[STATEMENT]
lemma sc_completionI:
  "(\<And>ttas s' t x ta x' m'.
     \<lbrakk> s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)));
       thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> (x, shr s') -ta\<rightarrow> (x', m'); actions_ok s' t ta \<rbrakk>
     \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> (x, shr s') -ta'\<rightarrow> (x'', m'') \<and> actions_ok s' t ta' \<and>
                   ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
  \<Longrightarrow> sc_completion s vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ttas s' t x ta x' m'. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) \<Longrightarrow> sc_completion s vs
[PROOF STEP]
unfolding sc_completion_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ttas s' t x ta x' m'. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)) \<Longrightarrow> \<forall>ttas s' t x ta x' m'. s -\<triangleright>ttas\<rightarrow>* s' \<longrightarrow> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<longrightarrow> thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor> \<longrightarrow> t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle> \<longrightarrow> actions_ok s' t ta \<longrightarrow> (\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>))
[PROOF STEP]
by blast


[STATEMENT]
lemma sc_completion_shift:
  assumes sc_c: "sc_completion s vs"
  and \<tau>Red: "s -\<triangleright>ttas\<rightarrow>* s'"
  and sc: "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of ttas)))"
  shows "sc_completion s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc_completion s' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
proof(rule sc_completionI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
fix ttas' s'' t x ta x' m'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
assume \<tau>Red': "s' -\<triangleright>ttas'\<rightarrow>* s''"
    and sc': "ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))"
    and red: "thr s'' t = \<lfloor>(x, no_wait_locks)\<rfloor>" "t \<turnstile> \<langle>x, shr s''\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>" "actions_ok s'' t ta"
[PROOF STATE]
proof (state)
this:
s' -\<triangleright>ttas'\<rightarrow>* s''
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))
thr s'' t = \<lfloor>(x, no_wait_locks)\<rfloor>
t \<turnstile> \<langle>x, shr s''\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>
actions_ok s'' t ta

goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
from \<tau>Red \<tau>Red'
[PROOF STATE]
proof (chain)
picking this:
s -\<triangleright>ttas\<rightarrow>* s'
s' -\<triangleright>ttas'\<rightarrow>* s''
[PROOF STEP]
have "s -\<triangleright>ttas @ ttas'\<rightarrow>* s''"
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas\<rightarrow>* s'
s' -\<triangleright>ttas'\<rightarrow>* s''

goal (1 subgoal):
 1. s -\<triangleright>ttas @ ttas'\<rightarrow>* s''
[PROOF STEP]
unfolding RedT_def
[PROOF STATE]
proof (prove)
using this:
mthr.Trsys s ttas s'
mthr.Trsys s' ttas' s''

goal (1 subgoal):
 1. mthr.Trsys s (ttas @ ttas') s''
[PROOF STEP]
by(rule rtrancl3p_trans)
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''

goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''

goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
from sc sc'
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of ttas)))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))
[PROOF STEP]
have "ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of ttas)))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))

goal (1 subgoal):
 1. ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))
[PROOF STEP]
apply(simp add: lappend_llist_of_llist_of[symmetric] ta_seq_consist_lappend del: lappend_llist_of_llist_of)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ta_seq_consist P vs (lconcat (llist_of (map (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas')))\<rbrakk> \<Longrightarrow> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
apply(simp add: lconcat_llist_of[symmetric] lmap_llist_of[symmetric] llist.map_comp o_def split_def del: lmap_llist_of)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))

goal (1 subgoal):
 1. \<And>ttasa s'a t x ta x' m'. \<lbrakk>s' -\<triangleright>ttasa\<rightarrow>* s'a; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))); thr s'a t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'a\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s'a t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'a\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'a t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))
[PROOF STEP]
show "\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s''\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'' t ta' \<and>
         ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))

goal (1 subgoal):
 1. \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s''\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'' t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
using red
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))
thr s'' t = \<lfloor>(x, no_wait_locks)\<rfloor>
t \<turnstile> \<langle>x, shr s''\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>
actions_ok s'' t ta

goal (1 subgoal):
 1. \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s''\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'' t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
unfolding foldl_append[symmetric] concat_append[symmetric] map_append[symmetric]
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas @ ttas'\<rightarrow>* s''
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas'))))
thr s'' t = \<lfloor>(x, no_wait_locks)\<rfloor>
t \<turnstile> \<langle>x, shr s''\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>
actions_ok s'' t ta

goal (1 subgoal):
 1. \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s''\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) (ttas @ ttas')))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
by(rule sc_completionD[OF sc_c])
[PROOF STATE]
proof (state)
this:
\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s''\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s'' t ta' \<and> ta_seq_consist P (mrw_values P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)

goal:
No subgoals!
[PROOF STEP]
qed