[STATEMENT]
lemma rev_justify:
  assumes "trace_to tr s"
  assumes "isRev' tr cid uid pid"
  shows "isRev s cid uid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isRev s cid uid pid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
isRev' tr cid uid pid

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

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

goal (1 subgoal):
 1. isRev istate cid s pid
[PROOF STEP]
by (auto simp add: istate_def elim!: isRev'.cases)
[PROOF STATE]
proof (state)
this:
isRev istate cid s pid

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isRev' tr cid uid pid \<Longrightarrow> isRev s cid uid pid; reach s; reach s'; step s a = (ou, s'); isRev' (tr ## Trans s a ou s') cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isRev' tr cid uid pid \<Longrightarrow> isRev s cid uid pid; reach s; reach s'; step s a = (ou, s'); isRev' (tr ## Trans s a ou s') cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[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')
isRev' tr cid ?uid pid \<Longrightarrow> isRev s cid ?uid pid
isRev' (tr ## Trans s a ou s') cid uid pid

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isRev' tr cid uid pid \<Longrightarrow> isRev s cid uid pid; reach s; reach s'; step s a = (ou, s'); isRev' (tr ## Trans s a ou s') cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
from step.prems
[PROOF STATE]
proof (chain)
picking this:
isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
isRev' (tr ## Trans s a ou s') cid uid pid

goal (1 subgoal):
 1. isRev s' cid uid pid
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tr uid' trn uu_ uv_ uw_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uu_ (Cact (cReview cid uid' uv_ pid uid)) outOK uw_\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
case (add_rev _ uid' _ _ pass)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
isChair' tr_ cid uid'
trn_ = Trans uu_ (Cact (cReview cid uid' pass pid uid)) outOK uw_

goal (2 subgoals):
 1. \<And>tr uid' trn uu_ uv_ uw_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uu_ (Cact (cReview cid uid' uv_ pid uid)) outOK uw_\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
hence [simp]: "a=Cact (cReview cid uid' pass pid uid)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
isChair' tr_ cid uid'
trn_ = Trans uu_ (Cact (cReview cid uid' pass pid uid)) outOK uw_

goal (1 subgoal):
 1. a = Cact (cReview cid uid' pass pid uid) &&& ou = outOK
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cReview cid uid' pass pid uid)
ou = outOK

goal (2 subgoals):
 1. \<And>tr uid' trn uu_ uv_ uw_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uu_ (Cact (cReview cid uid' uv_ pid uid)) outOK uw_\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
from step.hyps
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')

goal (1 subgoal):
 1. isRev s' cid uid pid
[PROOF STEP]
by (auto simp add: c_defs isRev_def)
[PROOF STATE]
proof (state)
this:
isRev s' cid uid pid

goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
case (irrelevant)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## ux_
isRev' tr_ cid uid pid

goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
isRev' tr cid ?uid pid \<Longrightarrow> isRev s cid ?uid pid
tr ## Trans s a ou s' = tr_ ## ux_
isRev' tr_ cid uid pid
[PROOF STEP]
have REV: "isRev s cid uid pid"
[PROOF STATE]
proof (prove)
using this:
isRev' tr cid ?uid pid \<Longrightarrow> isRev s cid ?uid pid
tr ## Trans s a ou s' = tr_ ## ux_
isRev' tr_ cid uid pid

goal (1 subgoal):
 1. isRev s cid uid pid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isRev s cid uid pid

goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
note roles_confIDs[OF step.hyps(2)]
[PROOF STATE]
proof (state)
this:
?rl \<in>\<in> roles s ?confID ?uID \<Longrightarrow> ?confID \<in>\<in> confIDs s

goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isRev' tr cid uid pid\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
with REV \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
isRev s cid uid pid
step s a = (ou, s')
?rl \<in>\<in> roles s ?confID ?uID \<Longrightarrow> ?confID \<in>\<in> confIDs s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isRev s cid uid pid
step s a = (ou, s')
?rl \<in>\<in> roles s ?confID ?uID \<Longrightarrow> ?confID \<in>\<in> confIDs s

goal (1 subgoal):
 1. isRev s' cid uid pid
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Cact x1\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>x2. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Uact x2\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 3. \<And>x3. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = UUact x3\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 4. \<And>x4. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Ract x4\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 5. \<And>x5. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Lact x5\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Cact x1\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
apply (cases x1, auto simp: c_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Uact x2\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>x3. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = UUact x3\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 3. \<And>x4. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Ract x4\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 4. \<And>x5. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Lact x5\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Uact x2\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
apply (cases x2, auto simp: u_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = UUact x3\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>x4. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Ract x4\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 3. \<And>x5. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Lact x5\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = UUact x3\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
apply (cases x3, auto simp: uu_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Ract x4\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
 2. \<And>x5. \<lbrakk>isRev s cid uid pid; step s a = (ou, s'); \<And>rl confID uID. rl \<in>\<in> roles s confID uID \<Longrightarrow> confID \<in>\<in> confIDs s; a = Lact x5\<rbrakk> \<Longrightarrow> isRev s' cid uid pid
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
isRev s' cid uid pid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
isRev s' cid uid pid

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem isRev_eq: "trace_to tr s \<Longrightarrow> isRev s cid uid pid = isRev' tr cid uid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isRev s cid uid pid = isRev' tr cid uid pid
[PROOF STEP]
(* "Trace-based equivalent of being a reviewer" *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isRev s cid uid pid = isRev' tr cid uid pid
[PROOF STEP]
using justify_rev rev_justify
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trace_to ?tr ?s; isRev ?s ?cid ?uid ?pid\<rbrakk> \<Longrightarrow> isRev' ?tr ?cid ?uid ?pid
\<lbrakk>trace_to ?tr ?s; isRev' ?tr ?cid ?uid ?pid\<rbrakk> \<Longrightarrow> isRev ?s ?cid ?uid ?pid

goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isRev s cid uid pid = isRev' tr cid uid pid
[PROOF STEP]
by (blast)


[STATEMENT]
lemma irrev_conflict_impl_author:
  assumes "trace_to tr s"
  assumes "\<exists>trn\<in>set tr. irrev_conflict uid pid trn"
  shows "\<exists>cid. isAut s cid uid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cid. isAut s cid uid pid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
\<exists>trn\<in>set tr. irrev_conflict uid pid trn

goal (1 subgoal):
 1. \<exists>cid. isAut s cid uid pid
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Bex (set []) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut istate cid uid pid
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; Bex (set tr) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s cid uid pid; reach s; reach s'; step s a = (ou, s'); Bex (set (tr ## Trans s a ou s')) (irrev_conflict uid pid)\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s' cid uid pid
[PROOF STEP]
apply (auto simp add: istate_def) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; Bex (set tr) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s cid uid pid; reach s; reach s'; step s a = (ou, s'); Bex (set (tr ## Trans s a ou s')) (irrev_conflict uid pid)\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s' cid uid pid
[PROOF STEP]
subgoal for _ _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid)\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Cact x1\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 2. \<And>x2. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Uact x2\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 3. \<And>x3. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = UUact x3\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 4. \<And>x4. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Ract x4\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 5. \<And>x5. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Lact x5\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Cact x1\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
apply (cases x1, auto simp: c_defs, (metis roles_confIDs)+) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Uact x2\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 2. \<And>x3. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = UUact x3\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 3. \<And>x4. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Ract x4\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 4. \<And>x5. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Lact x5\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Uact x2\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[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>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = UUact x3\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 2. \<And>x4. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Ract x4\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 3. \<And>x5. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Lact x5\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = UUact x3\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[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>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Ract x4\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
 2. \<And>x5. \<lbrakk>trace_to tr_ s_; Bex (set tr_) (irrev_conflict uid pid) \<Longrightarrow> \<exists>cid. isAut s_ cid uid pid; reach s_; reach s'_; step s_ a = (ou_, s'_); Bex (set (tr_ ## Trans s_ a ou_ s'_)) (irrev_conflict uid pid); a = Lact x5\<rbrakk> \<Longrightarrow> \<exists>cid. isAut s'_ cid uid pid
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma irrev_conflict_impl_conflict:
  assumes "trace_to tr s"
  assumes "\<exists>trn\<in>set tr. irrev_conflict uid pid trn"
  shows "pref s uid pid = Conflict"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pref s uid pid = Conflict
[PROOF STEP]
by (metis assms(1) assms(2) irrev_conflict_impl_author
    isAut_pref_Conflict reach_trace_to_conv)


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

goal (1 subgoal):
 1. pref s uid pid = Conflict
[PROOF STEP]
unfolding conflict_trace_def
[PROOF STATE]
proof (prove)
using this:
(\<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. pref s uid pid = Conflict
[PROOF STEP]
proof (cases rule: disjE[consumes 1, case_names irrev set])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>trn\<in>set tr. irrev_conflict uid pid trn \<Longrightarrow> pref s uid pid = Conflict
 2. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
case irrev
[PROOF STATE]
proof (state)
this:
\<exists>trn\<in>set tr. irrev_conflict uid pid trn

goal (2 subgoals):
 1. \<exists>trn\<in>set tr. irrev_conflict uid pid trn \<Longrightarrow> pref s uid pid = Conflict
 2. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>trn\<in>set tr. irrev_conflict uid pid trn

goal (1 subgoal):
 1. pref s uid pid = Conflict
[PROOF STEP]
by (simp add: irrev_conflict_impl_conflict[OF TR])
[PROOF STATE]
proof (state)
this:
pref s uid pid = Conflict

goal (1 subgoal):
 1. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
case set
[PROOF STATE]
proof (state)
this:
\<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>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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<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)
[PROOF STEP]
obtain tr1 trn tr2 where
    [simp]: "tr = tr1 @ trn # tr2" and
    SET: "set_conflict uid pid trn"
    and NRESET: "\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn"
[PROOF STATE]
proof (prove)
using this:
\<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. (\<And>tr1 trn tr2. \<lbrakk>tr = tr1 @ trn # tr2; set_conflict uid pid trn; \<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
tr = tr1 @ trn # tr2
set_conflict uid pid trn
\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn

goal (1 subgoal):
 1. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
from TR
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
[PROOF STEP]
obtain s1 s2 a ou where
    [simp]: "trn = Trans s1 a ou s2" and
    TR1: "trace_to tr1 s1" and
    STEP: "step s1 a = (ou,s2)" and
    TR2: "trace_between s2 tr2 s"
[PROOF STATE]
proof (prove)
using this:
trace_to tr s

goal (1 subgoal):
 1. (\<And>s1 a ou s2. \<lbrakk>trn = Trans s1 a ou s2; trace_to tr1 s1; step s1 a = (ou, s2); trace_between s2 tr2 s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp add: trace_to_ft trace_ft_simps)
[PROOF STATE]
proof (state)
this:
trn = Trans s1 a ou s2
trace_to tr1 s1
step s1 a = (ou, s2)
trace_between s2 tr2 s

goal (1 subgoal):
 1. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
from STEP SET
[PROOF STATE]
proof (chain)
picking this:
step s1 a = (ou, s2)
set_conflict uid pid trn
[PROOF STEP]
have "pref s2 uid pid = Conflict"
[PROOF STATE]
proof (prove)
using this:
step s1 a = (ou, s2)
set_conflict uid pid trn

goal (1 subgoal):
 1. pref s2 uid pid = Conflict
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Cact x1\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 2. \<And>x2. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Uact x2\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 3. \<And>x3. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = UUact x3\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 4. \<And>x4. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Ract x4\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 5. \<And>x5. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Lact x5\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Cact x1\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
[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>step s1 a = (ou, s2); set_conflict uid pid trn; a = Uact x2\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 2. \<And>x3. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = UUact x3\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 3. \<And>x4. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Ract x4\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 4. \<And>x5. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Lact x5\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Uact x2\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
[PROOF STEP]
apply (cases x2, auto simp: u_defs) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x61 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 uid (pass s1 uid) pid x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if uid = a' \<and> pid = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 uid (pass s1 uid) pid x65); x2 = uPref x61 uid (pass s1 uid) pid x65; x61 \<in>\<in> confIDs s1; uid \<in>\<in> userIDs s1; pid \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 uid; Aut pid \<notin> set (roles s1 x61 uid); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if uid = a' \<and> pid = b' then x65 else pref s1 a' b'\<rparr>\<rbrakk> \<Longrightarrow> x65 = Conflict
 2. \<And>x61 x62 x64 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 x62 (pass s1 x62) x64 x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 x62 (pass s1 x62) x64 x65); x2 = uPref x61 x62 (pass s1 x62) x64 x65; x61 \<in>\<in> confIDs s1; x62 \<in>\<in> userIDs s1; x64 \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 x62; Aut x64 \<notin> set (roles s1 x61 x62); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>; x62 \<noteq> uid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
 3. \<And>x61 x62 x64 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 x62 (pass s1 x62) x64 x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 x62 (pass s1 x62) x64 x65); x2 = uPref x61 x62 (pass s1 x62) x64 x65; x61 \<in>\<in> confIDs s1; x62 \<in>\<in> userIDs s1; x64 \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 x62; Aut x64 \<notin> set (roles s1 x61 x62); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>; x64 \<noteq> pid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
[PROOF STEP]
subgoal for _ x65
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61_ uid (pass s1 uid) pid x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if uid = a' \<and> pid = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61_ uid (pass s1 uid) pid x65); x2 = uPref x61_ uid (pass s1 uid) pid x65; x61_ \<in>\<in> confIDs s1; uid \<in>\<in> userIDs s1; pid \<in>\<in> paperIDs s1 x61_; phase s1 x61_ = bidPH; isPC s1 x61_ uid; Aut pid \<notin> set (roles s1 x61_ uid); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if uid = a' \<and> pid = b' then x65 else pref s1 a' b'\<rparr>\<rbrakk> \<Longrightarrow> x65 = Conflict
[PROOF STEP]
apply (cases x65, auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x64 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 x62 (pass s1 x62) x64 x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 x62 (pass s1 x62) x64 x65); x2 = uPref x61 x62 (pass s1 x62) x64 x65; x61 \<in>\<in> confIDs s1; x62 \<in>\<in> userIDs s1; x64 \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 x62; Aut x64 \<notin> set (roles s1 x61 x62); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>; x62 \<noteq> uid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
 2. \<And>x61 x62 x64 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 x62 (pass s1 x62) x64 x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 x62 (pass s1 x62) x64 x65); x2 = uPref x61 x62 (pass s1 x62) x64 x65; x61 \<in>\<in> confIDs s1; x62 \<in>\<in> userIDs s1; x64 \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 x62; Aut x64 \<notin> set (roles s1 x61 x62); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>; x64 \<noteq> pid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
[PROOF STEP]
subgoal for _ _ _ x65
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61_ x62_ (pass s1 x62_) x64_ x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62_ = a' \<and> x64_ = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61_ x62_ (pass s1 x62_) x64_ x65); x2 = uPref x61_ x62_ (pass s1 x62_) x64_ x65; x61_ \<in>\<in> confIDs s1; x62_ \<in>\<in> userIDs s1; x64_ \<in>\<in> paperIDs s1 x61_; phase s1 x61_ = bidPH; isPC s1 x61_ x62_; Aut x64_ \<notin> set (roles s1 x61_ x62_); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62_ = a' \<and> x64_ = b' then x65 else pref s1 a' b'\<rparr>; x62_ \<noteq> uid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
[PROOF STEP]
apply (cases x65, auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x61 x62 x64 x65. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61 x62 (pass s1 x62) x64 x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61 x62 (pass s1 x62) x64 x65); x2 = uPref x61 x62 (pass s1 x62) x64 x65; x61 \<in>\<in> confIDs s1; x62 \<in>\<in> userIDs s1; x64 \<in>\<in> paperIDs s1 x61; phase s1 x61 = bidPH; isPC s1 x61 x62; Aut x64 \<notin> set (roles s1 x61 x62); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62 = a' \<and> x64 = b' then x65 else pref s1 a' b'\<rparr>; x64 \<noteq> pid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
[PROOF STEP]
subgoal for _ _ _ x65
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set_conflict uid pid (Trans s1 (Uact (uPref x61_ x62_ (pass s1 x62_) x64_ x65)) outOK (s1\<lparr>pref := \<lambda>a' b'. if x62_ = a' \<and> x64_ = b' then x65 else pref s1 a' b'\<rparr>)); a = Uact (uPref x61_ x62_ (pass s1 x62_) x64_ x65); x2 = uPref x61_ x62_ (pass s1 x62_) x64_ x65; x61_ \<in>\<in> confIDs s1; x62_ \<in>\<in> userIDs s1; x64_ \<in>\<in> paperIDs s1 x61_; phase s1 x61_ = bidPH; isPC s1 x61_ x62_; Aut x64_ \<notin> set (roles s1 x61_ x62_); ou = outOK; s2 = s1\<lparr>pref := \<lambda>a' b'. if x62_ = a' \<and> x64_ = b' then x65 else pref s1 a' b'\<rparr>; x64_ \<noteq> pid\<rbrakk> \<Longrightarrow> pref s1 uid pid = Conflict
[PROOF STEP]
apply (cases x65, auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = UUact x3\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 2. \<And>x4. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Ract x4\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
 3. \<And>x5. \<lbrakk>step s1 a = (ou, s2); set_conflict uid pid trn; a = Lact x5\<rbrakk> \<Longrightarrow> pref s2 uid pid = Conflict
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
pref s2 uid pid = Conflict

goal (1 subgoal):
 1. \<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) \<Longrightarrow> pref s uid pid = Conflict
[PROOF STEP]
with TR2 NRESET
[PROOF STATE]
proof (chain)
picking this:
trace_between s2 tr2 s
\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn
pref s2 uid pid = Conflict
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace_between s2 tr2 s
\<forall>trn\<in>set tr2. \<not> reset_conflict uid pid trn
pref s2 uid pid = Conflict

goal (1 subgoal):
 1. pref s uid pid = Conflict
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>trn\<in>set []. \<not> reset_conflict uid pid trn; pref s uid pid = Conflict\<rbrakk> \<Longrightarrow> pref s uid pid = Conflict
 2. \<And>s tr sh a ou s'. \<lbrakk>trace_between s tr sh; \<lbrakk>\<forall>trn\<in>set tr. \<not> reset_conflict uid pid trn; pref s uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh uid pid = Conflict; step sh a = (ou, s'); \<forall>trn\<in>set (tr ## Trans sh a ou s'). \<not> reset_conflict uid pid trn; pref s uid pid = Conflict\<rbrakk> \<Longrightarrow> pref s' uid pid = Conflict
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>trn\<in>set []. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref s_ uid pid = Conflict
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s tr sh a ou s'. \<lbrakk>trace_between s tr sh; \<lbrakk>\<forall>trn\<in>set tr. \<not> reset_conflict uid pid trn; pref s uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh uid pid = Conflict; step sh a = (ou, s'); \<forall>trn\<in>set (tr ## Trans sh a ou s'). \<not> reset_conflict uid pid trn; pref s uid pid = Conflict\<rbrakk> \<Longrightarrow> pref s' uid pid = Conflict
[PROOF STEP]
subgoal for _ _ _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 2. \<And>x2. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 3. \<And>x3. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 4. \<And>x4. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 5. \<And>x5. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Cact x1\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[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>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 2. \<And>x3. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 3. \<And>x4. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 4. \<And>x5. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Uact x2\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[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>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 2. \<And>x4. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 3. \<And>x5. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = UUact x3\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[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>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Ract x4\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
 2. \<And>x5. \<lbrakk>trace_between s_ tr_ sh_; \<lbrakk>\<forall>trn\<in>set tr_. \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict\<rbrakk> \<Longrightarrow> pref sh_ uid pid = Conflict; step sh_ a = (ou_, s'_); \<forall>trn\<in>set (tr_ ## Trans sh_ a ou_ s'_). \<not> reset_conflict uid pid trn; pref s_ uid pid = Conflict; a = Lact x5\<rbrakk> \<Longrightarrow> pref s'_ uid pid = Conflict
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pref s uid pid = Conflict

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem conflict_eq:
  assumes "trace_to tr s"
  shows "pref s uid pid = Conflict \<longleftrightarrow> conflict_trace uid pid tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pref s uid pid = Conflict) = conflict_trace uid pid tr
[PROOF STEP]
using assms conflict_justify justify_conflict
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
\<lbrakk>trace_to ?tr ?s; conflict_trace ?uid ?pid ?tr\<rbrakk> \<Longrightarrow> pref ?s ?uid ?pid = Conflict
\<lbrakk>trace_to ?tr ?s; pref ?s ?uid ?pid = Conflict\<rbrakk> \<Longrightarrow> conflict_trace ?uid ?pid ?tr

goal (1 subgoal):
 1. (pref s uid pid = Conflict) = conflict_trace uid pid tr
[PROOF STEP]
by auto


[STATEMENT]
lemma justify_phase:
  assumes "trace_to tr s"
  assumes "phase s cid = ph"
  shows "phase' tr cid ph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase' tr cid ph
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
phase s cid = ph

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

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

goal (1 subgoal):
 1. phase' [] cid s
[PROOF STEP]
by (auto simp add: istate_def phase'.initial)
[PROOF STATE]
proof (state)
this:
phase' [] cid s

goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; reach s; reach s'; step s a = (ou, s'); phase s' cid = ph\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; reach s; reach s'; step s a = (ou, s'); phase s' cid = ph\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[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')
phase s cid = ?ph \<Longrightarrow> phase' tr cid ?ph
phase s' cid = ph

goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; reach s; reach s'; step s a = (ou, s'); phase s' cid = ph\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
phase s cid = ?ph \<Longrightarrow> phase' tr cid ?ph
phase s' cid = ph

goal (1 subgoal):
 1. phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Cact x1\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 2. \<And>x2. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Uact x2\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 3. \<And>x3. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = UUact x3\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 4. \<And>x4. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Ract x4\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 5. \<And>x5. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Lact x5\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Cact x1\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
apply (cases x1, auto simp: c_defs intro: phase'.advance phase'.irrelevant) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Uact x2\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 2. \<And>x3. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = UUact x3\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 3. \<And>x4. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Ract x4\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 4. \<And>x5. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Lact x5\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Uact x2\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
apply (cases x2,
      auto
        simp: u_defs isChair_eq
        intro: phase'.advance phase'.irrelevant phase'.approve,
      (fastforce intro: phase'.approve phase'.irrelevant phase'.advance)+
    ) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = UUact x3\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 2. \<And>x4. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Ract x4\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 3. \<And>x5. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Lact x5\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = UUact x3\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
apply (cases x3, auto simp: uu_defs intro: phase'.irrelevant) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Ract x4\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
 2. \<And>x5. \<lbrakk>trace_to tr s; reach s; reach s'; step s a = (ou, s'); \<And>ph. phase s cid = ph \<Longrightarrow> phase' tr cid ph; phase s' cid = ph; a = Lact x5\<rbrakk> \<Longrightarrow> phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
by (auto intro: phase'.advance phase'.irrelevant)
[PROOF STATE]
proof (state)
this:
phase' (tr ## Trans s a ou s') cid ph

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phase_justify:
  assumes "trace_to tr s"
  assumes "phase' tr cid ph"
  shows "phase s cid = ph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase s cid = ph
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
phase' tr cid ph

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

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

goal (1 subgoal):
 1. phase istate cid = s
[PROOF STEP]
by (auto simp add: istate_def elim: phase'.cases)
[PROOF STATE]
proof (state)
this:
phase istate cid = s

goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase' tr cid ph \<Longrightarrow> phase s cid = ph; reach s; reach s'; step s a = (ou, s'); phase' (tr ## Trans s a ou s') cid ph\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase' tr cid ph \<Longrightarrow> phase s cid = ph; reach s; reach s'; step s a = (ou, s'); phase' (tr ## Trans s a ou s') cid ph\<rbrakk> \<Longrightarrow> phase s' cid = ph
[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')
phase' tr cid ?ph \<Longrightarrow> phase s cid = ?ph
phase' (tr ## Trans s a ou s') cid ph

goal (1 subgoal):
 1. \<And>tr s a ou s' ph. \<lbrakk>trace_to tr s; \<And>ph. phase' tr cid ph \<Longrightarrow> phase s cid = ph; reach s; reach s'; step s a = (ou, s'); phase' (tr ## Trans s a ou s') cid ph\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
from step.prems
[PROOF STATE]
proof (chain)
picking this:
phase' (tr ## Trans s a ou s') cid ph
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
phase' (tr ## Trans s a ou s') cid ph

goal (1 subgoal):
 1. phase s' cid = ph
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn s uu_ uv_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; ph = setPH; phase' tr cid noPH; trn = Trans s (Uact (uConfA cid (voronkov s) uu_)) outOK uv_\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 4. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
case (approve _ _ _ pass _)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
ph = setPH
phase' tr_ cid noPH
trn_ = Trans s_ (Uact (uConfA cid (voronkov s_) pass)) outOK uv_

goal (4 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn s uu_ uv_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; ph = setPH; phase' tr cid noPH; trn = Trans s (Uact (uConfA cid (voronkov s) uu_)) outOK uv_\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 4. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
hence [simp]: "a=Uact (uConfA cid (voronkov s) pass)" "ou=outOK" "ph=setPH"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
ph = setPH
phase' tr_ cid noPH
trn_ = Trans s_ (Uact (uConfA cid (voronkov s_) pass)) outOK uv_

goal (1 subgoal):
 1. a = Uact (uConfA cid (voronkov s) pass) &&& ou = outOK &&& ph = setPH
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Uact (uConfA cid (voronkov s) pass)
ou = outOK
ph = setPH

goal (4 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn s uu_ uv_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; ph = setPH; phase' tr cid noPH; trn = Trans s (Uact (uConfA cid (voronkov s) uu_)) outOK uv_\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 4. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
from step.hyps
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')

goal (1 subgoal):
 1. phase s' cid = ph
[PROOF STEP]
by (auto simp add: u_defs)
[PROOF STATE]
proof (state)
this:
phase s' cid = ph

goal (3 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
case (advance _ _ uid pass _ _)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uw_ (Uact (uPhase cid uid pass ph)) outOK uy_
isChair' tr_ cid uid

goal (3 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
hence [simp]: "a=Uact (uPhase cid uid pass ph)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uw_ (Uact (uPhase cid uid pass ph)) outOK uy_
isChair' tr_ cid uid

goal (1 subgoal):
 1. a = Uact (uPhase cid uid pass ph) &&& ou = outOK
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Uact (uPhase cid uid pass ph)
ou = outOK

goal (3 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>trn uw_ uid ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uw_ (Uact (uPhase cid uid ux_ ph)) outOK uy_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
from step.hyps
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')

goal (1 subgoal):
 1. phase s' cid = ph
[PROOF STEP]
by (auto simp add: u_defs)
[PROOF STATE]
proof (state)
this:
phase s' cid = ph

goal (2 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
case (irrelevant)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
phase' tr_ cid ph
\<not> is_uPhase cid trn_

goal (2 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
phase' tr cid ?ph \<Longrightarrow> phase s cid = ?ph
tr ## Trans s a ou s' = tr_ ## trn_
phase' tr_ cid ph
\<not> is_uPhase cid trn_
[PROOF STEP]
have PH: "phase s cid = ph" "\<not> is_uPhase cid (Trans s a ou s')"
[PROOF STATE]
proof (prove)
using this:
phase' tr cid ?ph \<Longrightarrow> phase s cid = ?ph
tr ## Trans s a ou s' = tr_ ## trn_
phase' tr_ cid ph
\<not> is_uPhase cid trn_

goal (1 subgoal):
 1. phase s cid = ph &&& \<not> is_uPhase cid (Trans s a ou s')
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
phase s cid = ph
\<not> is_uPhase cid (Trans s a ou s')

goal (2 subgoals):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>tr trn. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; phase' tr cid ph; \<not> is_uPhase cid trn\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
from PH \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
phase s cid = ph
\<not> is_uPhase cid (Trans s a ou s')
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
phase s cid = ph
\<not> is_uPhase cid (Trans s a ou s')
step s a = (ou, s')

goal (1 subgoal):
 1. phase s' cid = ph
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Cact x1\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>x2. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>x3. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> phase s' cid = ph
 4. \<And>x4. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> phase s' cid = ph
 5. \<And>x5. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Cact x1\<rbrakk> \<Longrightarrow> phase s' cid = ph
[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>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>x3. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>x4. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> phase s' cid = ph
 4. \<And>x5. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Uact x2\<rbrakk> \<Longrightarrow> phase s' cid = ph
[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>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>x4. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> phase s' cid = ph
 3. \<And>x5. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = UUact x3\<rbrakk> \<Longrightarrow> phase s' cid = ph
[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>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Ract x4\<rbrakk> \<Longrightarrow> phase s' cid = ph
 2. \<And>x5. \<lbrakk>phase s cid = ph; \<not> is_uPhase cid (Trans s a ou s'); step s a = (ou, s'); a = Lact x5\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
phase s' cid = ph

goal (1 subgoal):
 1. \<lbrakk>tr ## Trans s a ou s' = []; ph = noPH\<rbrakk> \<Longrightarrow> phase s' cid = ph
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
phase s' cid = ph

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem phase_eq:
  assumes "trace_to tr s"
  shows "phase s cid = ph \<longleftrightarrow> phase' tr cid ph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (phase s cid = ph) = phase' tr cid ph
[PROOF STEP]
using assms phase_justify justify_phase
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
\<lbrakk>trace_to ?tr ?s; phase' ?tr ?cid ?ph\<rbrakk> \<Longrightarrow> phase ?s ?cid = ?ph
\<lbrakk>trace_to ?tr ?s; phase ?s ?cid = ?ph\<rbrakk> \<Longrightarrow> phase' ?tr ?cid ?ph

goal (1 subgoal):
 1. (phase s cid = ph) = phase' tr cid ph
[PROOF STEP]
by blast


[STATEMENT]
lemma qiter_fun_exp: "qiter_fun x y z = x \<squnion> y \<cdot> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qiter_fun x y z = x \<squnion> y \<cdot> z
[PROOF STEP]
unfolding qiter_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<squnion>) x \<circ> (\<cdot>) y) z = x \<squnion> y \<cdot> z
[PROOF STEP]
by simp


[STATEMENT]
lemma iso_qiter_fun: "mono (\<lambda>z::'a::unital_pre_quantale. qiter_fun x y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (qiter_fun x y)
[PROOF STEP]
by (metis monoI proto_pre_quantale_class.mult_isol qiter_fun_exp sup.idem sup.mono sup.orderI)


[STATEMENT]
lemma qiterl_unfoldl [simp]: "x \<squnion> y \<cdot> qiterl x y = qiterl (x::'a::unital_pre_quantale) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<cdot> qiterl x y = qiterl x y
[PROOF STEP]
by (metis iso_qiter_fun lfp_unfold qiter_fun_exp qiterl_def)


[STATEMENT]
lemma qiterg_unfoldl [simp]: "x \<squnion> y \<cdot> qiterg x y = qiterg (x::'a::unital_pre_quantale) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<cdot> qiterg x y = qiterg x y
[PROOF STEP]
by (metis gfp_fixpoint iso_qiter_fun qiter_fun_exp qiterg_def)


[STATEMENT]
lemma qiterl_inductl: "x \<squnion> y \<cdot> z \<le> z \<Longrightarrow> qiterl (x::'a::unital_near_quantale) y \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<cdot> z \<le> z \<Longrightarrow> qiterl x y \<le> z
[PROOF STEP]
by (simp add: lfp_lowerbound qiterl_def qiter_fun_def)


[STATEMENT]
lemma qiterg_coinductl: "z \<le> x \<squnion> y \<cdot> z \<Longrightarrow> z \<le> qiterg (x::'a::unital_near_quantale) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> x \<squnion> y \<cdot> z \<Longrightarrow> z \<le> qiterg x y
[PROOF STEP]
by (simp add: gfp_upperbound qiterg_def qiter_fun_def)


[STATEMENT]
lemma powers_distr: "qstar x \<cdot> y = (\<Squnion>i. x ^ i \<cdot> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qstar x \<cdot> y = (\<Squnion>i. x ^ i \<cdot> y)
[PROOF STEP]
by (simp add: qstar_def Sup_distr image_comp)


[STATEMENT]
lemma Sup_iter_unfold: "x ^ 0 \<squnion> (\<Squnion>n. x ^ (Suc n)) = (\<Squnion>n. x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ^ 0 \<squnion> (\<Squnion>n. x ^ Suc n) = \<Squnion> range ((^) x)
[PROOF STEP]
using fSup_unfold
[PROOF STATE]
proof (prove)
using this:
?f 0 \<squnion> (\<Squnion>n. ?f (Suc n)) = \<Squnion> range ?f

goal (1 subgoal):
 1. x ^ 0 \<squnion> (\<Squnion>n. x ^ Suc n) = \<Squnion> range ((^) x)
[PROOF STEP]
by presburger


[STATEMENT]
lemma Sup_iter_unfold_var: "1 \<squnion> (\<Squnion>n. x \<cdot> x ^ n) = (\<Squnion>n. x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<squnion> (\<Squnion>n. x \<cdot> x ^ n) = \<Squnion> range ((^) x)
[PROOF STEP]
by (simp only: Sup_iter_unfold[symmetric]) auto


[STATEMENT]
lemma power_inductr: "z \<squnion> y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ i \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> x ^ i \<le> y
[PROOF STEP]
by (induct i, simp_all, metis power_commutes order.eq_iff mult_isor order.trans mult_assoc power.power.power_Suc)


[STATEMENT]
lemma powers_subdistl: "(\<Squnion>i. x \<cdot> y ^ i) \<le> x \<cdot> qstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>i. x \<cdot> y ^ i) \<le> x \<cdot> qstar y
[PROOF STEP]
by (simp add: SUP_le_iff SUP_upper mult_isol qstar_def)


[STATEMENT]
lemma qstar_subcomm: "qstar x \<cdot> x \<le> x \<cdot> qstar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qstar x \<cdot> x \<le> x \<cdot> qstar x
[PROOF STEP]
by (simp add: powers_distr powers_subdistl power_commutes)


[STATEMENT]
lemma power_inductl: "z \<squnion> x \<cdot> y \<le> y \<Longrightarrow> x ^ i \<cdot> z \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> x \<cdot> y \<le> y \<Longrightarrow> x ^ i \<cdot> z \<le> y
[PROOF STEP]
by (induct i, simp_all, metis dual_order.trans mult_isol mult_assoc)


[STATEMENT]
lemma powers_distl: "x \<cdot> qstar y = (\<Squnion>i. x \<cdot> y ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> qstar y = (\<Squnion>i. x \<cdot> y ^ i)
[PROOF STEP]
by (simp add: qstar_def weak_Sup_distl image_comp)


[STATEMENT]
lemma qstar_unfoldl: "1 \<squnion> x \<cdot> qstar x \<le> qstar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<squnion> x \<cdot> qstar x \<le> qstar x
[PROOF STEP]
by (simp only: powers_distl Sup_iter_unfold_var, simp add: qstar_def)


[STATEMENT]
lemma qstar_comm: "x \<cdot> qstar x = qstar x \<cdot> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> qstar x = qstar x \<cdot> x
[PROOF STEP]
using power_commutes powers_distr powers_distl
[PROOF STATE]
proof (prove)
using this:
?a ^ ?n \<cdot> ?a = ?a \<cdot> ?a ^ ?n
qstar ?x \<cdot> ?y = (\<Squnion>i. ?x ^ i \<cdot> ?y)
?x \<cdot> qstar ?y = (\<Squnion>i. ?x \<cdot> ?y ^ i)

goal (1 subgoal):
 1. x \<cdot> qstar x = qstar x \<cdot> x
[PROOF STEP]
by auto


[STATEMENT]
lemma qstar_unfoldr [simp]: "1 \<squnion> qstar x \<cdot> x = qstar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<squnion> qstar x \<cdot> x = qstar x
[PROOF STEP]
using qstar_comm qstar_unfoldl Sup_iter_unfold_var qstar_def powers_distl
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> qstar ?x = qstar ?x \<cdot> ?x
(1::'a) \<squnion> ?x \<cdot> qstar ?x \<le> qstar ?x
(1::'a) \<squnion> (\<Squnion>n. ?x \<cdot> ?x ^ n) = \<Squnion> range ((^) ?x)
qstar ?x = \<Squnion> range ((^) ?x)
?x \<cdot> qstar ?y = (\<Squnion>i. ?x \<cdot> ?y ^ i)

goal (1 subgoal):
 1. (1::'a) \<squnion> qstar x \<cdot> x = qstar x
[PROOF STEP]
by auto


[STATEMENT]
lemma qstar_inductl: "z \<squnion> x \<cdot> y \<le> y \<Longrightarrow> qstar x \<cdot> z \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> x \<cdot> y \<le> y \<Longrightarrow> qstar x \<cdot> z \<le> y
[PROOF STEP]
by (subst powers_distr, auto intro!: Sup_least power_inductl)


[STATEMENT]
lemma qstar_inductr: "z \<squnion> y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> qstar x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<squnion> y \<cdot> x \<le> y \<Longrightarrow> z \<cdot> qstar x \<le> y
[PROOF STEP]
by (subst powers_distl, auto intro!: Sup_least power_inductr)


[STATEMENT]
lemma  qstar_qiterl: "qstar (x::'a::unital_weak_quantale) = qiterl_id x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qstar x = qiterl_id x
[PROOF STEP]
by (simp add: antisym qiterl_inductl uwqlka.star_inductl_one)


[STATEMENT]
lemma act_star1: "1 \<squnion> x \<squnion> (qstar x) \<cdot> (qstar x) \<le> (qstar x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<squnion> x \<squnion> qstar x \<cdot> qstar x \<le> qstar x
[PROOF STEP]
by simp


[STATEMENT]
lemma (in unital_quantale) act_star3: "qstar (x \<rightarrow> x) \<le> x \<rightarrow> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qstar (x \<rightarrow> x) \<le> x \<rightarrow> x
[PROOF STEP]
by (simp add: bres_canc1 bres_galois_imp uqka.star_inductr_var)


[STATEMENT]
lemma act_star3_var: "qstar (x \<leftarrow> x) \<le> x \<leftarrow> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qstar (x \<leftarrow> x) \<le> x \<leftarrow> x
[PROOF STEP]
using fres_galois qstar_inductl
[PROOF STATE]
proof (prove)
using this:
(?x \<cdot> ?y \<le> ?z) = (?x \<le> ?z \<leftarrow> ?y)
?z \<squnion> ?x \<cdot> ?y \<le> ?y \<Longrightarrow> qstar ?x \<cdot> ?z \<le> ?y

goal (1 subgoal):
 1. qstar (x \<leftarrow> x) \<le> x \<leftarrow> x
[PROOF STEP]
by auto


[STATEMENT]
lemma microstep_choiceD [dest]:
  "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p \<Longrightarrow> p = p1 \<or> p = p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p \<Longrightarrow> p = p1 \<or> p = p2
[PROOF STEP]
by (ind_cases "(p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p") auto


[STATEMENT]
lemma microstep_choiceE [elim]:
  "\<lbrakk> (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p;
     (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1 \<Longrightarrow> P;
     (p1 \<oplus> p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2 \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p; (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p1 \<Longrightarrow> P; (p1
\<oplus>
p2) \<leadsto>\<^bsub>\<Gamma>\<^esub> p2 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (blast)


[STATEMENT]
lemma microstep_callD [dest]:
  "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> p \<Longrightarrow> p = \<Gamma> pn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> p \<Longrightarrow> p = \<Gamma> pn
[PROOF STEP]
by (ind_cases "(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> p")


[STATEMENT]
lemma microstep_callE [elim]:
  "\<lbrakk> (call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> p;  p = \<Gamma>(pn) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(call(pn)) \<leadsto>\<^bsub>\<Gamma>\<^esub> p; p = \<Gamma> pn \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by auto


[STATEMENT]
lemma no_microstep_guard: "\<not> (({l}\<langle>g\<rangle> p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}\<langle>g\<rangle>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}\<langle>g\<rangle> p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_assign: "\<not> ({l}\<lbrakk>f\<rbrakk> p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}\<lbrakk>f\<rbrakk>
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}\<lbrakk>f\<rbrakk> p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_unicast: "\<not> (({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g).p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g) .
p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub> r
[PROOF STEP]
by (rule notI) (ind_cases "({l}unicast(s\<^sub>i\<^sub>p, s\<^sub>m\<^sub>s\<^sub>g).p \<triangleright> q) \<leadsto>\<^bsub>\<Gamma>\<^esub> r")


[STATEMENT]
lemma no_microstep_broadcast: "\<not> (({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}broadcast(s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_groupcast: "\<not> (({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}groupcast(s\<^sub>i\<^sub>p\<^sub>s, s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_send: "\<not> (({l}send(s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}send(s\<^sub>m\<^sub>s\<^sub>g) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}send(s\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_deliver: "\<not> (({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}deliver(s\<^sub>d\<^sub>a\<^sub>t\<^sub>a).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma no_microstep_receive: "\<not> (({l}receive(u\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ({l}receive(u\<^sub>m\<^sub>s\<^sub>g) .
p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q
[PROOF STEP]
by (rule notI) (ind_cases "({l}receive(u\<^sub>m\<^sub>s\<^sub>g).p) \<leadsto>\<^bsub>\<Gamma>\<^esub> q")


[STATEMENT]
lemma microstep_call_or_choice [dest]:
  assumes "p \<leadsto>\<^bsub>\<Gamma>\<^esub> q"
    shows "(\<exists>pn. p = call(pn)) \<or> (\<exists>p1 p2. p = p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>pn. p = call(pn)) \<or> (\<exists>p1 p2. p = p1
\<oplus>
p2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<leadsto>\<^bsub>\<Gamma>\<^esub> q

goal (1 subgoal):
 1. (\<exists>pn. p = call(pn)) \<or> (\<exists>p1 p2. p = p1
\<oplus>
p2)
[PROOF STEP]
by clarsimp (metis microstep.simps)


[STATEMENT]
lemma wellformed_defP: "wellformed \<Gamma> = wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wellformed \<Gamma> = wfP (\<lambda>q p. p \<leadsto>\<^bsub>\<Gamma>\<^esub> q)
[PROOF STEP]
unfolding wellformed_def wfP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q} = wf {(q, p). p \<leadsto>\<^bsub>\<Gamma>\<^esub> q}
[PROOF STEP]
by simp