[STATEMENT]
lemma mrw_value_cases:
  obtains ad al v where "x = NormalAction (WriteMem ad al v)"
  | ad hT where "x = NormalAction (NewHeapElem ad hT)"
  | ad M vs v where "x = NormalAction (ExternalCall ad M vs v)"
  | ad al v where "x = NormalAction (ReadMem ad al v)"
  | t where "x = NormalAction (ThreadStart t)"
  | t where "x = NormalAction (ThreadJoin t)"
  | ad where "x = NormalAction (SyncLock ad)"
  | ad where "x = NormalAction (SyncUnlock ad)"
  | t where "x = NormalAction (ObsInterrupt t)"
  | t where "x = NormalAction (ObsInterrupted t)"
  | "x = InitialThreadAction"
  | "x = ThreadFinishAction"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ad al v. x = NormalAction (WriteMem ad al v) \<Longrightarrow> thesis; \<And>ad hT. x = NormalAction (NewHeapElem ad hT) \<Longrightarrow> thesis; \<And>ad M vs v. x = NormalAction (ExternalCall ad M vs v) \<Longrightarrow> thesis; \<And>ad al v. x = NormalAction (ReadMem ad al v) \<Longrightarrow> thesis; \<And>t. x = NormalAction (ThreadStart t) \<Longrightarrow> thesis; \<And>t. x = NormalAction (ThreadJoin t) \<Longrightarrow> thesis; \<And>ad. x = NormalAction (SyncLock ad) \<Longrightarrow> thesis; \<And>ad. x = NormalAction (SyncUnlock ad) \<Longrightarrow> thesis; \<And>t. x = NormalAction (ObsInterrupt t) \<Longrightarrow> thesis; \<And>t. x = NormalAction (ObsInterrupted t) \<Longrightarrow> thesis; x = InitialThreadAction \<Longrightarrow> thesis; x = ThreadFinishAction \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by pat_completeness


[STATEMENT]
lemma mrw_values_eq_SomeD:
  assumes mrw: "mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>"
  and "vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)"
  shows "\<exists>obs' wa obs''. obs = 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 \<longleftrightarrow> \<not> b) \<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> b)"
  (is "?concl obs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs = 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> b) \<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> b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs = 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> b) \<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> b)
[PROOF STEP]
proof(induct obs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>mrw_values P vs0 [] (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set [] \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. [] = 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> b) \<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> b)
 2. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
mrw_values P vs0 [] (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set [] \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (2 subgoals):
 1. \<lbrakk>mrw_values P vs0 [] (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set [] \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. [] = 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> b) \<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> b)
 2. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mrw_values P vs0 [] (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set [] \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<exists>obs' wa obs''. [] = 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> b) \<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> b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>obs' wa obs''. [] = 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> b) \<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> b)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
case (snoc ob obs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. obs = 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> b) \<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> b)
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
note mrw = \<open>mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>\<close>
[PROOF STATE]
proof (state)
this:
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>mrw_values P vs0 xs (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set xs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs = 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> b) \<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> b); mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, b)\<rfloor>; vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (xs @ [x]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)\<rbrakk> \<Longrightarrow> \<exists>obs' wa obs''. xs @ [x] = 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> b) \<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> b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
proof(cases "is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
 2. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)

goal (2 subgoals):
 1. is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
 2. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
using mrw
[PROOF STATE]
proof (prove)
using this:
is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
by(fastforce elim!: is_write_action.cases intro: action_loc_aux_intros split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
with mrw
[PROOF STATE]
proof (chain)
picking this:
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))
[PROOF STEP]
have "mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))

goal (1 subgoal):
 1. mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
by(cases "ob" rule: mrw_value_cases)(auto split: if_split_asm simp add: addr_locs_def split: htype.split_asm)
[PROOF STATE]
proof (state)
this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
assume "vs0 (ad, al) = \<lfloor>(v, b)\<rfloor>"
[PROOF STATE]
proof (state)
this:
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
hence "\<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)"
[PROOF STATE]
proof (prove)
using this:
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)
[PROOF STEP]
by(rule snoc)
[PROOF STATE]
proof (state)
this:
\<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))
\<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)
[PROOF STEP]
have "\<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)"
[PROOF STATE]
proof (prove)
using this:
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))
\<exists>wa. wa \<in> set (obs @ [ob]) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)
[PROOF STEP]
have "?concl obs"
[PROOF STATE]
proof (prove)
using this:
mrw_values P vs0 obs (ad, al) = \<lfloor>(v, b)\<rfloor>
vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set obs \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs = 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> b) \<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> b)
[PROOF STEP]
by(rule snoc)
[PROOF STATE]
proof (state)
this:
\<exists>obs' wa obs''. obs = 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> b) \<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> b)

goal (1 subgoal):
 1. \<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b)) \<Longrightarrow> \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' wa obs''. obs = 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> b) \<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> b)

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
using False mrw
[PROOF STATE]
proof (prove)
using this:
\<exists>obs' wa obs''. obs = 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> b) \<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> b)
\<not> (is_write_action ob \<and> (ad, al) \<in> action_loc_aux P ob \<and> (is_new_action ob \<longrightarrow> \<not> b))
mrw_values P vs0 (obs @ [ob]) (ad, al) = \<lfloor>(v, b)\<rfloor>

goal (1 subgoal):
 1. \<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>obs' wa obs''. obs @ [ob] = 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> b) \<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> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mrw_values_WriteMemD:
  assumes "NormalAction (WriteMem ad al v') \<in> set obs"
  shows "\<exists>v. mrw_values P vs0 obs (ad, al) = Some (v, True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. mrw_values P vs0 obs (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NormalAction (WriteMem ad al v') \<in> set obs

goal (1 subgoal):
 1. \<exists>v. mrw_values P vs0 obs (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply(induct obs rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. NormalAction (WriteMem ad al v') \<in> set [] \<Longrightarrow> \<exists>v. mrw_values P vs0 [] (ad, al) = \<lfloor>(v, True)\<rfloor>
 2. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>v. mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') \<in> set (xs @ [x])\<rbrakk> \<Longrightarrow> \<exists>v. mrw_values P vs0 (xs @ [x]) (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') = x \<or> NormalAction (WriteMem ad al v') \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') = x\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 2. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs \<Longrightarrow> \<exists>v. mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; NormalAction (WriteMem ad al v') \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs v. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
[PROOF STEP]
apply(case_tac x rule: mrw_value_cases)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>x xs v ada ala va. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (WriteMem ada ala va)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 2. \<And>x xs v ada hT. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (NewHeapElem ada hT)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 3. \<And>x xs v ada M vs va. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ExternalCall ada M vs va)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 4. \<And>x xs v ada ala va. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ReadMem ada ala va)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 5. \<And>x xs v t. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ThreadStart t)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 6. \<And>x xs v t. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ThreadJoin t)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 7. \<And>x xs v ada. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (SyncLock ada)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 8. \<And>x xs v ada. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (SyncUnlock ada)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 9. \<And>x xs v t. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ObsInterrupt t)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
 10. \<And>x xs v t. \<lbrakk>NormalAction (WriteMem ad al v') \<in> set xs; mrw_values P vs0 xs (ad, al) = \<lfloor>(v, True)\<rfloor>; x = NormalAction (ObsInterrupted t)\<rbrakk> \<Longrightarrow> \<exists>v. mrw_value P (mrw_values P vs0 xs) x (ad, al) = \<lfloor>(v, True)\<rfloor>
A total of 12 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mrw_values_new_actionD:
  assumes "w \<in> set obs" "is_new_action w" "adal \<in> action_loc_aux P w"
  shows "\<exists>v b. mrw_values P vs0 obs adal = Some (v, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v b. mrw_values P vs0 obs adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<in> set obs
is_new_action w
adal \<in> action_loc_aux P w

goal (1 subgoal):
 1. \<exists>v b. mrw_values P vs0 obs adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(induct obs rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w \<in> set []; is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_values P vs0 [] adal = \<lfloor>(v, b)\<rfloor>
 2. \<And>x xs. \<lbrakk>\<lbrakk>w \<in> set xs; is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; w \<in> set (xs @ [x]); is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_values P vs0 (xs @ [x]) adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>w \<in> set xs; is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; w \<in> set (xs @ [x]); is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_values P vs0 (xs @ [x]) adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>w \<in> set xs \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; w = x \<or> w \<in> set xs; is_new_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 xs) x adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>w \<in> set xs \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; is_new_action w; adal \<in> action_loc_aux P w; w = x\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 xs) x adal = \<lfloor>(v, b)\<rfloor>
 2. \<And>x xs. \<lbrakk>w \<in> set xs \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; is_new_action w; adal \<in> action_loc_aux P w; w \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 xs) x adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(fastforce simp add: split_beta elim!: action_loc_aux_cases is_new_action.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>w \<in> set xs \<Longrightarrow> \<exists>v b. mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>; is_new_action w; adal \<in> action_loc_aux P w; w \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 xs) x adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs v b. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set xs; mrw_values P vs0 xs adal = \<lfloor>(v, b)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 xs) x adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(rename_tac w' obs' v b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w' obs' v b. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
apply(case_tac w' rule: mrw_value_cases)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>w' obs' v b ad al va. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (WriteMem ad al va)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 2. \<And>w' obs' v b ad hT. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (NewHeapElem ad hT)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 3. \<And>w' obs' v b ad M vs va. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ExternalCall ad M vs va)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 4. \<And>w' obs' v b ad al va. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ReadMem ad al va)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 5. \<And>w' obs' v b t. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ThreadStart t)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 6. \<And>w' obs' v b t. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ThreadJoin t)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 7. \<And>w' obs' v b ad. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (SyncLock ad)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 8. \<And>w' obs' v b ad. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (SyncUnlock ad)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 9. \<And>w' obs' v b t. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ObsInterrupt t)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
 10. \<And>w' obs' v b t. \<lbrakk>is_new_action w; adal \<in> action_loc_aux P w; w \<in> set obs'; mrw_values P vs0 obs' adal = \<lfloor>(v, b)\<rfloor>; w' = NormalAction (ObsInterrupted t)\<rbrakk> \<Longrightarrow> \<exists>v b. mrw_value P (mrw_values P vs0 obs') w' adal = \<lfloor>(v, b)\<rfloor>
A total of 12 subgoals...
[PROOF STEP]
apply(auto simp add: split_beta)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mrw_value_dom_mono:
  "dom vs \<subseteq> dom (mrw_value P vs ob)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom vs \<subseteq> dom (mrw_value P vs ob)
[PROOF STEP]
by(cases ob rule: mrw_value_cases) auto


[STATEMENT]
lemma mrw_values_dom_mono:
  "dom vs \<subseteq> dom (mrw_values P vs obs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom vs \<subseteq> dom (mrw_values P vs obs)
[PROOF STEP]
by(induct obs arbitrary: vs)(auto intro: subset_trans[OF mrw_value_dom_mono] del: subsetI)


[STATEMENT]
lemma mrw_values_eq_NoneD:
  assumes "mrw_values P vs0 obs adal = None"
  and "w \<in> set obs" and "is_write_action w" and "adal \<in> action_loc_aux P w"
  shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mrw_values P vs0 obs adal = None
w \<in> set obs
is_write_action w
adal \<in> action_loc_aux P w

goal (1 subgoal):
 1. False
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mrw_values P vs0 obs adal = None; w \<in> set obs; is_write_action w; adal \<in> action_loc_aux P w\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule is_write_action.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ad hT. \<lbrakk>mrw_values P vs0 obs adal = None; w \<in> set obs; adal \<in> action_loc_aux P w; w = NormalAction (NewHeapElem ad hT)\<rbrakk> \<Longrightarrow> False
 2. \<And>ad al v. \<lbrakk>mrw_values P vs0 obs adal = None; w \<in> set obs; adal \<in> action_loc_aux P w; w = NormalAction (WriteMem ad al v)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(fastforce dest: mrw_values_WriteMemD[where ?vs0.0=vs0 and P=P] mrw_values_new_actionD[where ?vs0.0=vs0] elim: action_loc_aux_cases)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mrw_values_mrw:
  assumes mrw: "mrw_values P vs0 (map snd obs) (ad, al) = \<lfloor>(v, b)\<rfloor>"
  and initial: "vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> \<exists>wa. wa \<in> set (map snd obs) \<and> is_write_action wa \<and> (ad, al) \<in> action_loc_aux P wa \<and> (b \<longrightarrow> \<not> is_new_action wa)"
  shows "\<exists>i. i < length obs \<and> P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
from mrw_values_eq_SomeD[OF mrw initial]
[PROOF STATE]
proof (chain)
picking this:
(vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> vs0 (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> \<exists>obs' wa obs''. map snd obs = 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> b) \<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> b)
[PROOF STEP]
obtain obs' wa obs'' where obs: "map snd obs = obs' @ wa # obs''"
    and wa: "is_write_action wa"
    and adal: "(ad, al) \<in> action_loc_aux P wa"
    and written: "value_written_aux P wa al = v"
    and new: "is_new_action wa \<longleftrightarrow> \<not> b"
    and last: "\<And>ob. \<lbrakk> ob \<in> set obs''; is_write_action ob; (ad, al) \<in> action_loc_aux P ob \<rbrakk> \<Longrightarrow> is_new_action ob \<and> b"
[PROOF STATE]
proof (prove)
using this:
(vs0 (ad, al) = \<lfloor>(v, b)\<rfloor> \<Longrightarrow> vs0 (ad, al) = \<lfloor>(v, b)\<rfloor>) \<Longrightarrow> \<exists>obs' wa obs''. map snd obs = 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> b) \<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> b)

goal (1 subgoal):
 1. (\<And>obs' wa obs''. \<lbrakk>map snd obs = obs' @ wa # obs''; is_write_action wa; (ad, al) \<in> action_loc_aux P wa; value_written_aux P wa al = v; is_new_action wa = (\<not> b); \<And>ob. \<lbrakk>ob \<in> set obs''; is_write_action ob; (ad, al) \<in> action_loc_aux P ob\<rbrakk> \<Longrightarrow> is_new_action ob \<and> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map snd obs = obs' @ wa # obs''
is_write_action wa
(ad, al) \<in> action_loc_aux P wa
value_written_aux P wa al = v
is_new_action wa = (\<not> b)
\<lbrakk>?ob \<in> set obs''; is_write_action ?ob; (ad, al) \<in> action_loc_aux P ?ob\<rbrakk> \<Longrightarrow> is_new_action ?ob \<and> b

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
let ?i = "length obs'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
let ?E = "llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
from obs
[PROOF STATE]
proof (chain)
picking this:
map snd obs = obs' @ wa # obs''
[PROOF STEP]
have len: "length (map snd obs) = Suc (length obs') + length obs''"
[PROOF STATE]
proof (prove)
using this:
map snd obs = obs' @ wa # obs''

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

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
hence "?i < length obs"
[PROOF STATE]
proof (prove)
using this:
length (map snd obs) = Suc (length obs') + length obs''

goal (1 subgoal):
 1. length obs' < length obs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length obs' < length obs

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length obs' < length obs

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
hence obs_i: "action_obs ?E ?i = wa"
[PROOF STATE]
proof (prove)
using this:
length obs' < length obs

goal (1 subgoal):
 1. action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
[PROOF STEP]
using len obs
[PROOF STATE]
proof (prove)
using this:
length obs' < length obs
length (map snd obs) = Suc (length obs') + length obs''
map snd obs = obs' @ wa # obs''

goal (1 subgoal):
 1. action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
[PROOF STEP]
by(auto simp add: action_obs_def map_eq_append_conv)
[PROOF STATE]
proof (state)
this:
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
have "P,?E \<turnstile> length obs \<leadsto>mrw ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw length obs'
[PROOF STEP]
proof(rule most_recent_write_for.intros)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. length obs \<in> read_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
 2. ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs)
 3. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs
 4. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
 5. ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
 6. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
show "length obs \<in> read_actions ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length obs \<in> read_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
by(auto intro: read_actions.intros simp add: actions_def action_obs_def)
[PROOF STATE]
proof (state)
this:
length obs \<in> read_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (5 subgoals):
 1. ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs)
 2. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs
 3. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
 4. ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
 5. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); ?adal \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
show "(ad, al) \<in> action_loc P ?E (length obs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs)
[PROOF STEP]
by(simp add: action_obs_def lnth_llist_of)
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs)

goal (4 subgoals):
 1. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs
 2. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
 3. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
 4. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
show "?E \<turnstile> length obs' \<le>a length obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
length (map snd obs) = Suc (length obs') + length obs''

goal (1 subgoal):
 1. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs
[PROOF STEP]
by-(rule action_orderI, auto simp add: actions_def action_obs_def nth_append)
[PROOF STATE]
proof (state)
this:
llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs' \<le>a length obs

goal (3 subgoals):
 1. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
 2. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
 3. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
show "?i \<in> write_actions ?E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
using len obs wa
[PROOF STATE]
proof (prove)
using this:
length (map snd obs) = Suc (length obs') + length obs''
map snd obs = obs' @ wa # obs''
is_write_action wa

goal (1 subgoal):
 1. length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
by-(rule write_actions.intros, auto simp add: actions_def action_obs_def nth_append map_eq_append_conv)
[PROOF STATE]
proof (state)
this:
length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (2 subgoals):
 1. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
 2. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
show "(ad, al) \<in> action_loc P ?E ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
[PROOF STEP]
using obs_i adal
[PROOF STATE]
proof (prove)
using this:
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
(ad, al) \<in> action_loc_aux P wa

goal (1 subgoal):
 1. (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')

goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
fix wa'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
assume wa': "wa' \<in> write_actions ?E"
      and adal': "(ad, al) \<in> action_loc P ?E wa'"
[PROOF STATE]
proof (state)
this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'

goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
from wa' \<open>?i \<in> write_actions ?E\<close>
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "wa' \<in> actions ?E" "?i \<in> actions ?E"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
length obs' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. wa' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) &&& length obs' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
wa' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
length obs' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
hence "?E \<turnstile> wa' \<le>a ?i"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
length obs' \<in> actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs'
[PROOF STEP]
proof(rule action_orderI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'); is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))\<rbrakk> \<Longrightarrow> wa' \<le> length obs'
 2. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
assume new_wa': "is_new_action (action_obs ?E wa')"
        and new_i: "is_new_action (action_obs ?E ?i)"
[PROOF STATE]
proof (state)
this:
is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')
is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))

goal (2 subgoals):
 1. \<lbrakk>is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'); is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))\<rbrakk> \<Longrightarrow> wa' \<le> length obs'
 2. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
from new_i obs_i new
[PROOF STATE]
proof (chain)
picking this:
is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
is_new_action wa = (\<not> b)
[PROOF STEP]
have b: "\<not> b"
[PROOF STATE]
proof (prove)
using this:
is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
is_new_action wa = (\<not> b)

goal (1 subgoal):
 1. \<not> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> b

goal (2 subgoals):
 1. \<lbrakk>is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'); is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))\<rbrakk> \<Longrightarrow> wa' \<le> length obs'
 2. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
show "wa' \<le> ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa' \<le> length obs'
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> wa' \<le> length obs'

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
hence "?i < wa'"
[PROOF STATE]
proof (prove)
using this:
\<not> wa' \<le> length obs'

goal (1 subgoal):
 1. length obs' < wa'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length obs' < wa'

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
hence "snd (obs ! wa') \<in> set obs''"
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'

goal (1 subgoal):
 1. snd (obs ! wa') \<in> set obs''
[PROOF STEP]
using obs wa'
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'
map snd obs = obs' @ wa # obs''
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. snd (obs ! wa') \<in> set obs''
[PROOF STEP]
unfolding in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'
map snd obs = obs' @ wa # obs''
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. \<exists>i<length obs''. obs'' ! i = snd (obs ! wa')
[PROOF STEP]
by -(rule exI[where x="wa' - Suc (length obs')"], auto elim!: write_actions.cases actionsE simp add: action_obs_def lnth_llist_of actions_def nth_append map_eq_append_conv nth_Cons' split: if_split_asm)
[PROOF STATE]
proof (state)
this:
snd (obs ! wa') \<in> set obs''

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
snd (obs ! wa') \<in> set obs''

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
from wa'
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "is_write_action (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. is_write_action (snd (obs ! wa'))
[PROOF STEP]
by cases(auto simp add: action_obs_def nth_append actions_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
is_write_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_write_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
from adal' wa'
[PROOF STATE]
proof (chain)
picking this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. (ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
[PROOF STEP]
by(auto simp add: action_obs_def nth_append nth_Cons' actions_def split: if_split_asm elim!: write_actions.cases)
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))

goal (1 subgoal):
 1. False
[PROOF STEP]
using last[of "snd (obs ! wa')"] b
[PROOF STATE]
proof (prove)
using this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
\<lbrakk>snd (obs ! wa') \<in> set obs''; is_write_action (snd (obs ! wa')); (ad, al) \<in> action_loc_aux P (snd (obs ! wa'))\<rbrakk> \<Longrightarrow> is_new_action (snd (obs ! wa')) \<and> b
\<not> b

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:
wa' \<le> length obs'

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
assume new_wa': "\<not> is_new_action (action_obs ?E wa')"
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
with wa' adal'
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')
[PROOF STEP]
obtain v' where "NormalAction (WriteMem ad al v') \<in> set (map snd obs)"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')

goal (1 subgoal):
 1. (\<And>v'. NormalAction (WriteMem ad al v') \<in> set (map snd obs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')

goal (1 subgoal):
 1. (\<And>v'. \<exists>i<length (map snd obs). map snd obs ! i = NormalAction (WriteMem ad al v') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce elim!: write_actions.cases is_write_action.cases simp add: action_obs_def actions_def nth_append split: if_split_asm intro!: exI[where x=wa'])
[PROOF STATE]
proof (state)
this:
NormalAction (WriteMem ad al v') \<in> set (map snd obs)

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
from mrw_values_WriteMemD[OF this, of P vs0] mrw
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. mrw_values P vs0 (map snd obs) (ad, al) = \<lfloor>(v, True)\<rfloor>
mrw_values P vs0 (map snd obs) (ad, al) = \<lfloor>(v, b)\<rfloor>
[PROOF STEP]
have b
[PROOF STATE]
proof (prove)
using this:
\<exists>v. mrw_values P vs0 (map snd obs) (ad, al) = \<lfloor>(v, True)\<rfloor>
mrw_values P vs0 (map snd obs) (ad, al) = \<lfloor>(v, b)\<rfloor>

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

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
with new obs_i
[PROOF STATE]
proof (chain)
picking this:
is_new_action wa = (\<not> b)
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
b
[PROOF STEP]
have "\<not> is_new_action (action_obs ?E ?i)"
[PROOF STATE]
proof (prove)
using this:
is_new_action wa = (\<not> b)
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
b

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
have "wa' \<le> ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wa' \<le> length obs'
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> wa' \<le> length obs'

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
hence "?i < wa'"
[PROOF STATE]
proof (prove)
using this:
\<not> wa' \<le> length obs'

goal (1 subgoal):
 1. length obs' < wa'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length obs' < wa'

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
hence "snd (obs ! wa') \<in> set obs''"
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'

goal (1 subgoal):
 1. snd (obs ! wa') \<in> set obs''
[PROOF STEP]
using obs wa'
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'
map snd obs = obs' @ wa # obs''
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. snd (obs ! wa') \<in> set obs''
[PROOF STEP]
unfolding in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
length obs' < wa'
map snd obs = obs' @ wa # obs''
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. \<exists>i<length obs''. obs'' ! i = snd (obs ! wa')
[PROOF STEP]
by -(rule exI[where x="wa' - Suc (length obs')"], auto elim!: write_actions.cases actionsE simp add: action_obs_def lnth_llist_of actions_def nth_append map_eq_append_conv nth_Cons' split: if_split_asm)
[PROOF STATE]
proof (state)
this:
snd (obs ! wa') \<in> set obs''

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
snd (obs ! wa') \<in> set obs''

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
from wa'
[PROOF STATE]
proof (chain)
picking this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "is_write_action (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. is_write_action (snd (obs ! wa'))
[PROOF STEP]
by cases(auto simp add: action_obs_def nth_append actions_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
is_write_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_write_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
from adal' wa'
[PROOF STATE]
proof (chain)
picking this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
(ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. (ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
[PROOF STEP]
by(auto simp add: action_obs_def nth_append nth_Cons' actions_def split: if_split_asm elim!: write_actions.cases)
[PROOF STATE]
proof (state)
this:
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
[PROOF STEP]
have "is_new_action (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))

goal (1 subgoal):
 1. is_new_action (snd (obs ! wa'))
[PROOF STEP]
using last[of "snd (obs ! wa')"]
[PROOF STATE]
proof (prove)
using this:
snd (obs ! wa') \<in> set obs''
is_write_action (snd (obs ! wa'))
(ad, al) \<in> action_loc_aux P (snd (obs ! wa'))
\<lbrakk>snd (obs ! wa') \<in> set obs''; is_write_action (snd (obs ! wa')); (ad, al) \<in> action_loc_aux P (snd (obs ! wa'))\<rbrakk> \<Longrightarrow> is_new_action (snd (obs ! wa')) \<and> b

goal (1 subgoal):
 1. is_new_action (snd (obs ! wa'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_new_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_new_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
from new_wa' wa'
[PROOF STATE]
proof (chain)
picking this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))
[PROOF STEP]
have "\<not> is_new_action (snd (obs ! wa'))"
[PROOF STATE]
proof (prove)
using this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa')
wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]))

goal (1 subgoal):
 1. \<not> is_new_action (snd (obs ! wa'))
[PROOF STEP]
by(auto elim!: write_actions.cases simp add: action_obs_def nth_append actions_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (snd (obs ! wa'))

goal (1 subgoal):
 1. \<not> wa' \<le> length obs' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_new_action (snd (obs ! wa'))
\<not> is_new_action (snd (obs ! wa'))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
is_new_action (snd (obs ! wa'))
\<not> is_new_action (snd (obs ! wa'))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wa' \<le> length obs'

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa') \<Longrightarrow> \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))
wa' \<le> length obs'
[PROOF STEP]
show "\<not> is_new_action (action_obs ?E ?i) \<and> wa' \<le> ?i"
[PROOF STATE]
proof (prove)
using this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs'))
wa' \<le> length obs'

goal (1 subgoal):
 1. \<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_new_action (action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs')) \<and> wa' \<le> length obs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs'

goal (1 subgoal):
 1. \<And>wa'. \<lbrakk>wa' \<in> write_actions (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])); (ad, al) \<in> action_loc P (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) wa'\<rbrakk> \<Longrightarrow> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
thus "?E \<turnstile> wa' \<le>a ?i \<or> ?E \<turnstile> length obs \<le>a wa'"
[PROOF STATE]
proof (prove)
using this:
llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs'

goal (1 subgoal):
 1. llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> wa' \<le>a length obs' \<or> llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<le>a wa'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw length obs'

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw length obs'

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
from written \<open>?i < length obs\<close> obs_i
[PROOF STATE]
proof (chain)
picking this:
value_written_aux P wa al = v
length obs' < length obs
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa
[PROOF STEP]
have "value_written P (llist_of obs) ?i (ad, al) = v"
[PROOF STATE]
proof (prove)
using this:
value_written_aux P wa al = v
length obs' < length obs
action_obs (llist_of (obs @ [(t, NormalAction (ReadMem ad al v))])) (length obs') = wa

goal (1 subgoal):
 1. value_written P (llist_of obs) (length obs') (ad, al) = v
[PROOF STEP]
by(simp add: value_written_def action_obs_def nth_append)
[PROOF STATE]
proof (state)
this:
value_written P (llist_of obs) (length obs') (ad, al) = v

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length obs' < length obs
P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw length obs'
value_written P (llist_of obs) (length obs') (ad, al) = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length obs' < length obs
P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw length obs'
value_written P (llist_of obs) (length obs') (ad, al) = v

goal (1 subgoal):
 1. \<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i<length obs. P,llist_of (obs @ [(t, NormalAction (ReadMem ad al v))]) \<turnstile> length obs \<leadsto>mrw i \<and> value_written P (llist_of obs) i (ad, al) = v

goal:
No subgoals!
[PROOF STEP]
qed