[STATEMENT]
lemma justify_conflict:
  assumes TR: "trace_to tr s"
  assumes "pref s uid pid = Conflict"
  shows "conflict_trace uid pid tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
pref s uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pref istate uid pid = Conflict \<Longrightarrow> conflict_trace uid pid []
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
pref istate uid pid = Conflict

goal (2 subgoals):
 1. pref istate uid pid = Conflict \<Longrightarrow> conflict_trace uid pid []
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pref istate uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid []
[PROOF STEP]
by (auto simp add: istate_def)
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid []

goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case (step tr s a ou s')
[PROOF STATE]
proof (state)
this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s' uid pid = Conflict

goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
let ?trn = "Trans s a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr; reach s; reach s'; step s a = (ou, s'); pref s' uid pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
proof (cases "pref s uid pid = Conflict")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pref s uid pid \<noteq> Conflict

goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
with step.prems \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
pref s' uid pid = Conflict
step s a = (ou, s')
pref s uid pid \<noteq> Conflict
[PROOF STEP]
have "irrev_conflict uid pid ?trn \<or> set_conflict uid pid ?trn"
[PROOF STATE]
proof (prove)
using this:
pref s' uid pid = Conflict
step s a = (ou, s')
pref s uid pid \<noteq> Conflict

goal (1 subgoal):
 1. irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 4. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 5. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x1, auto simp: c_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 4. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x2, auto simp: u_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 3. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases x3, auto simp: uu_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
 2. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); pref s uid pid \<noteq> Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (2 subgoals):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
 2. pref s uid pid \<noteq> Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
unfolding conflict_trace_def
[PROOF STATE]
proof (prove)
using this:
irrev_conflict uid pid (Trans s a ou s') \<or> set_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. (\<exists>trn\<in>set (tr ## Trans s a ou s'). irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr ## Trans s a ou s' = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pref s uid pid = Conflict

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s uid pid = Conflict
[PROOF STEP]
have CT: "conflict_trace uid pid tr"
[PROOF STATE]
proof (prove)
using this:
pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid tr
pref s uid pid = Conflict

goal (1 subgoal):
 1. conflict_trace uid pid tr
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid tr

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
from step.prems \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
pref s' uid pid = Conflict
step s a = (ou, s')
[PROOF STEP]
have "\<not>reset_conflict uid pid ?trn"
[PROOF STATE]
proof (prove)
using this:
pref s' uid pid = Conflict
step s a = (ou, s')

goal (1 subgoal):
 1. \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Cact x1\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 4. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 5. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Cact x1_\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 4. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by (cases x2, auto simp: u_defs)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 2. \<And>x4. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
 3. \<And>x5. \<lbrakk>pref s' uid pid = Conflict; step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> \<not> reset_conflict uid pid (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<not> reset_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. pref s uid pid = Conflict \<Longrightarrow> conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
using CT
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')
conflict_trace uid pid tr

goal (1 subgoal):
 1. conflict_trace uid pid (tr ## Trans s a ou s')
[PROOF STEP]
unfolding conflict_trace_def
[PROOF STATE]
proof (prove)
using this:
\<not> reset_conflict uid pid (Trans s a ou s')
(\<exists>trn\<in>set tr. irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))

goal (1 subgoal):
 1. (\<exists>trn\<in>set (tr ## Trans s a ou s'). irrev_conflict uid pid trn) \<or> (\<exists>tr1 trn tr2. tr ## Trans s a ou s' = tr1 @ trn # tr2 \<and> set_conflict uid pid trn \<and> (\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr1 trn tr2. \<lbrakk>\<not> reset_conflict uid pid (Trans s a ou s'); \<not> irrev_conflict uid pid (Trans s a ou s'); \<forall>tr1a trna. set_conflict uid pid trna \<longrightarrow> (\<forall>tr2a. tr1 @ trn # tr2 ## Trans s a ou s' = tr1a @ trna # tr2a \<longrightarrow> (\<exists>x\<in>set tr2a. reset_conflict uid pid x)); tr = tr1 @ trn # tr2; set_conflict uid pid trn; \<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn; \<forall>x\<in>set tr1 \<union> set tr2. \<not> irrev_conflict uid pid x\<rbrakk> \<Longrightarrow> irrev_conflict uid pid trn
[PROOF STEP]
by (metis rotate1.simps(2) set_ConsD set_rotate1)
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
conflict_trace uid pid (tr ## Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed