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

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

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

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

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou 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. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou 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')
isAut s cid ?uid pid \<Longrightarrow> isAut' tr cid ?uid pid
isAut s' cid uid pid

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
proof (cases "isAut s cid uid pid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isAut s cid uid pid \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
 2. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isAut s cid uid pid

goal (2 subgoals):
 1. isAut s cid uid pid \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
 2. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
isAut s cid ?uid pid \<Longrightarrow> isAut' tr cid ?uid pid
isAut s cid uid pid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isAut s cid ?uid pid \<Longrightarrow> isAut' tr cid ?uid pid
isAut s cid uid pid

goal (1 subgoal):
 1. isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
by (blast intro: isAut'.intros)
[PROOF STATE]
proof (state)
this:
isAut' (tr ## Trans s a ou s') cid uid pid

goal (1 subgoal):
 1. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Aut pid \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
with step.hyps step.prems
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isAut s' cid uid pid
Aut pid \<notin> set (roles s cid uid)
[PROOF STEP]
obtain
      pass s1 s2 uid' where
      "a=Cact (cPaper cid uid pass pid s1 s2)
      \<or> (a=Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid)"
      and [simp]: "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isAut s' cid uid pid
Aut pid \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. (\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Cact x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x2. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 5. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Cact x1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x1, auto simp add: c_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x2, auto simp add: u_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x3, auto simp add: uu_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isAut s' cid uid pid; Aut pid \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid
ou = outOK

goal (1 subgoal):
 1. Aut pid \<notin> set (roles s cid uid) \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid
ou = outOK

goal (1 subgoal):
 1. isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
a = Cact (cPaper cid uid pass pid s1 s2) \<or> a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid
ou = outOK
isAut s cid ?uid pid \<Longrightarrow> isAut' tr cid ?uid pid

goal (1 subgoal):
 1. isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ou = outOK; \<And>uid. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; a = Cact (cPaper cid uid pass pid s1 s2)\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
 2. \<lbrakk>ou = outOK; \<And>uid. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
apply (rule isAut'.creator, auto) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ou = outOK; \<And>uid. isAut s cid uid pid \<Longrightarrow> isAut' tr cid uid pid; a = Cact (cAuthor cid uid' pass pid uid) \<and> isAut s cid uid' pid\<rbrakk> \<Longrightarrow> isAut' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
apply (rule isAut'.co_author, auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
isAut' (tr ## Trans s a ou s') cid uid pid

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

goal (1 subgoal):
 1. isAut s' cid uid pid
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cPaper cid uid uv_ pid uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
case (creator _ _ pass s1 s2)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uu_ (Cact (cPaper cid uid pass pid s1 s2)) outOK uy_

goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cPaper cid uid uv_ pid uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
hence [simp]: "a=Cact (cPaper cid uid pass pid s1 s2)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uu_ (Cact (cPaper cid uid pass pid s1 s2)) outOK uy_

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

goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cPaper cid uid uv_ pid uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut 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. isAut s' cid uid pid
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
isAut s' cid uid pid

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
case (co_author _ uid' _ _ pass)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
isAut' tr_ cid uid' pid
trn_ = Trans uz_ (Cact (cAuthor cid uid' pass pid uid)) outOK vb_

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
hence [simp]: "a=Cact (cAuthor cid uid' pass pid uid)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
isAut' tr_ cid uid' pid
trn_ = Trans uz_ (Cact (cAuthor cid uid' pass pid uid)) outOK vb_

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

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isAut' tr cid uid' pid; trn = Trans uz_ (Cact (cAuthor cid uid' va_ pid uid)) outOK vb_\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut 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. isAut s' cid uid pid
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
isAut s' cid uid pid

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

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

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

goal (1 subgoal):
 1. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isAut' tr cid uid pid\<rbrakk> \<Longrightarrow> isAut s' cid uid pid
[PROOF STEP]
note roles_confIDs[OF \<open>reach s\<close> AUT]
[PROOF STATE]
proof (state)
this:
cid \<in>\<in> confIDs s

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem isAut_eq: "trace_to tr s \<Longrightarrow> isAut s cid uid pid \<longleftrightarrow> isAut' tr cid uid pid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isAut s cid uid pid = isAut' tr cid uid pid
[PROOF STEP]
(* "Trace-based equivalent of authorship" *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isAut s cid uid pid = isAut' tr cid uid pid
[PROOF STEP]
using justify_author author_justify
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trace_to ?tr ?s; isAut ?s ?cid ?uid ?pid\<rbrakk> \<Longrightarrow> isAut' ?tr ?cid ?uid ?pid
\<lbrakk>trace_to ?tr ?s; isAut' ?tr ?cid ?uid ?pid\<rbrakk> \<Longrightarrow> isAut ?s ?cid ?uid ?pid

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


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

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

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

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

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[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. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[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')
isChair s cid ?uid \<Longrightarrow> isChair' tr cid ?uid
isChair s' cid uid

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
proof (cases "isChair s cid uid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isChair s cid uid \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
 2. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isChair s cid uid

goal (2 subgoals):
 1. isChair s cid uid \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
 2. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
isChair s cid ?uid \<Longrightarrow> isChair' tr cid ?uid
isChair s cid uid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isChair s cid ?uid \<Longrightarrow> isChair' tr cid ?uid
isChair s cid uid

goal (1 subgoal):
 1. isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
by (blast intro: isChair'.intros)
[PROOF STATE]
proof (state)
this:
isChair' (tr ## Trans s a ou s') cid uid

goal (1 subgoal):
 1. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Chair \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
term cConf
[PROOF STATE]
proof (state)
this:
Chair \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
with step.hyps step.prems
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isChair s' cid uid
Chair \<notin> set (roles s cid uid)
[PROOF STEP]
obtain
      pass s1 s2 uid' where
      "a=Cact (cConf cid uid pass s1 s2)
      \<or> (a=Cact (cChair cid uid' pass uid) \<and> isChair s cid uid')"
      and [simp]: "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isChair s' cid uid
Chair \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. (\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Cact x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x2. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 5. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Cact x1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x1, auto simp add: c_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Uact x2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x2, auto simp add: u_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = UUact x3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x3, auto simp add: uu_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x5. \<lbrakk>\<And>pass s1 s2 uid'. \<lbrakk>a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isChair s' cid uid; Chair \<notin> set (roles s cid uid); a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. Chair \<notin> set (roles s cid uid) \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
a = Cact (cConf cid uid pass s1 s2) \<or> a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'
ou = outOK
isChair s cid ?uid \<Longrightarrow> isChair' tr cid ?uid

goal (1 subgoal):
 1. isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
apply (elim disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ou = outOK; \<And>uid. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; a = Cact (cConf cid uid pass s1 s2)\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
 2. \<lbrakk>ou = outOK; \<And>uid. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
apply (rule isChair'.creator, auto) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ou = outOK; \<And>uid. isChair s cid uid \<Longrightarrow> isChair' tr cid uid; a = Cact (cChair cid uid' pass uid) \<and> isChair s cid uid'\<rbrakk> \<Longrightarrow> isChair' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
apply (rule isChair'.add_chair, auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
isChair' (tr ## Trans s a ou s') cid uid

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isChair' tr cid uid \<Longrightarrow> isChair s cid uid; reach s; reach s'; step s a = (ou, s'); isChair' (tr ## Trans s a ou s') cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[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. isChair' tr cid uid \<Longrightarrow> isChair s cid uid; reach s; reach s'; step s a = (ou, s'); isChair' (tr ## Trans s a ou s') cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[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')
isChair' tr cid ?uid \<Longrightarrow> isChair s cid ?uid
isChair' (tr ## Trans s a ou s') cid uid

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

goal (1 subgoal):
 1. isChair s' cid uid
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cConf cid uid uv_ uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
case (creator _ _ pass s1 s2)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uu_ (Cact (cConf cid uid pass s1 s2)) outOK uy_

goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cConf cid uid uv_ uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
hence [simp]: "a=Cact (cConf cid uid pass s1 s2)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
trn_ = Trans uu_ (Cact (cConf cid uid pass s1 s2)) outOK uy_

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

goal (3 subgoals):
 1. \<And>trn uu_ uv_ uw_ ux_ uy_ tr. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; trn = Trans uu_ (Cact (cConf cid uid uv_ uw_ ux_)) outOK uy_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 3. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[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. isChair s' cid uid
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
isChair s' cid uid

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
case (add_chair _ uid' _ _ pass)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
isChair' tr_ cid uid'
trn_ = Trans uz_ (Cact (cChair cid uid' pass uid)) outOK vb_

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
hence [simp]: "a=Cact (cChair cid uid' pass uid)" "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
tr ## Trans s a ou s' = tr_ ## trn_
isChair' tr_ cid uid'
trn_ = Trans uz_ (Cact (cChair cid uid' pass uid)) outOK vb_

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

goal (2 subgoals):
 1. \<And>tr uid' trn uz_ va_ vb_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uz_ (Cact (cChair cid uid' va_ uid)) outOK vb_\<rbrakk> \<Longrightarrow> isChair s' cid uid
 2. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[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. isChair s' cid uid
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
isChair s' cid uid

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

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

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

goal (1 subgoal):
 1. \<And>tr vc_. \<lbrakk>tr ## Trans s a ou s' = tr ## vc_; isChair' tr cid uid\<rbrakk> \<Longrightarrow> isChair s' cid uid
[PROOF STEP]
from CH \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
isChair s cid uid
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isChair s cid uid
step s a = (ou, s')

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem isChair_eq: "trace_to tr s \<Longrightarrow> isChair s cid uid = isChair' tr cid uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isChair s cid uid = isChair' tr cid uid
[PROOF STEP]
(* "Trace-based equivalent of being a chair" *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isChair s cid uid = isChair' tr cid uid
[PROOF STEP]
using justify_chair chair_justify
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trace_to ?tr ?s; isChair ?s ?cid ?uid\<rbrakk> \<Longrightarrow> isChair' ?tr ?cid ?uid
\<lbrakk>trace_to ?tr ?s; isChair' ?tr ?cid ?uid\<rbrakk> \<Longrightarrow> isChair ?s ?cid ?uid

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


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

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

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

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

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isPC s cid uid \<Longrightarrow> isPC' tr cid uid; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid\<rbrakk> \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[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. isPC s cid uid \<Longrightarrow> isPC' tr cid uid; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid\<rbrakk> \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[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')
isPC s cid ?uid \<Longrightarrow> isPC' tr cid ?uid
isPC s' cid uid

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isPC s cid uid \<Longrightarrow> isPC' tr cid uid; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid\<rbrakk> \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
proof (cases "isPC s cid uid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isPC s cid uid \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
 2. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isPC s cid uid

goal (2 subgoals):
 1. isPC s cid uid \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
 2. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
isPC s cid ?uid \<Longrightarrow> isPC' tr cid ?uid
isPC s cid uid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isPC s cid ?uid \<Longrightarrow> isPC' tr cid ?uid
isPC s cid uid

goal (1 subgoal):
 1. isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
by (blast intro: isPC'.irrelevant)
[PROOF STATE]
proof (state)
this:
isPC' (tr ## Trans s a ou s') cid uid

goal (1 subgoal):
 1. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
PC \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
note noPC = this
[PROOF STATE]
proof (state)
this:
PC \<notin> set (roles s cid uid)

goal (1 subgoal):
 1. PC \<notin> set (roles s cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
proof (cases "isChair s' cid uid")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isChair s' cid uid \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
 2. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isChair s' cid uid

goal (2 subgoals):
 1. isChair s' cid uid \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
 2. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isChair s' cid uid

goal (1 subgoal):
 1. isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
by (metis chair justify_chair step.hyps(1) step.hyps(4) trace_to.step)
[PROOF STATE]
proof (state)
this:
isPC' (tr ## Trans s a ou s') cid uid

goal (1 subgoal):
 1. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Chair \<notin> set (roles s' cid uid)

goal (1 subgoal):
 1. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
note noChair=this
[PROOF STATE]
proof (state)
this:
Chair \<notin> set (roles s' cid uid)

goal (1 subgoal):
 1. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
from noPC noChair step.hyps step.prems
[PROOF STATE]
proof (chain)
picking this:
PC \<notin> set (roles s cid uid)
Chair \<notin> set (roles s' cid uid)
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isPC s' cid uid
[PROOF STEP]
obtain
        pass uid' where "(a=Cact (cPC cid uid' pass uid))"
        and "isChair s cid uid'"
        and [simp]: "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
PC \<notin> set (roles s cid uid)
Chair \<notin> set (roles s' cid uid)
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isPC s' cid uid

goal (1 subgoal):
 1. (\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Cact x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x2. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 5. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Cact x1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x1, auto simp add: c_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x2, auto simp add: u_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x3, auto simp add: uu_defs) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; PC \<notin> set (roles s cid uid); Chair \<notin> set (roles s' cid uid); trace_to tr s; reach s; reach s'; step s a = (ou, s'); isPC s' cid uid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cPC cid uid' pass uid)
isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. Chair \<notin> set (roles s' cid uid) \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact (cPC cid uid' pass uid)
isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = Cact (cPC cid uid' pass uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> isPC' (tr ## Trans s a ou s') cid uid
[PROOF STEP]
apply (rule isPC'.add_com, auto simp: isChair_eq[OF \<open>trace_to tr s\<close>]) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
isPC' (tr ## Trans s a ou s') cid uid

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

goal (1 subgoal):
 1. \<And>tr s a ou s' uid. \<lbrakk>trace_to tr s; \<And>uid. isPC' tr cid uid \<Longrightarrow> isPC s cid uid; reach s; reach s'; step s a = (ou, s'); isPC' (tr ## Trans s a ou s') cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[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. isPC' tr cid uid \<Longrightarrow> isPC s cid uid; reach s; reach s'; step s a = (ou, s'); isPC' (tr ## Trans s a ou s') cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[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')
isPC' tr cid ?uid \<Longrightarrow> isPC s cid ?uid
isPC' (tr ## Trans s a ou s') cid uid

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

goal (1 subgoal):
 1. isPC s' cid uid
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. isChair' (tr ## Trans s a ou s') cid uid \<Longrightarrow> isPC s' cid uid
 2. \<And>tr uid' trn uu_ uv_ uw_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uu_ (Cact (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 3. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
case chair
[PROOF STATE]
proof (state)
this:
isChair' (tr ## Trans s a ou s') cid uid

goal (3 subgoals):
 1. isChair' (tr ## Trans s a ou s') cid uid \<Longrightarrow> isPC s' cid uid
 2. \<And>tr uid' trn uu_ uv_ uw_. \<lbrakk>tr ## Trans s a ou s' = tr ## trn; isChair' tr cid uid'; trn = Trans uu_ (Cact (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 3. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
isChair' (tr ## Trans s a ou s') cid uid

goal (1 subgoal):
 1. isPC s' cid uid
[PROOF STEP]
by (metis isChair_eq isChair_isPC step.hyps(1) step.hyps(3) step.hyps(4) trace_to.step)
[PROOF STATE]
proof (state)
this:
isPC s' cid uid

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 (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
next
[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 (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
case (add_com _ uid' _ _ pass)
[PROOF STATE]
proof (state)
this:
tr ## Trans s a ou s' = tr_ ## trn_
isChair' tr_ cid uid'
trn_ = Trans uu_ (Cact (cPC cid uid' pass 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 (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
hence [simp]: "a=Cact (cPC cid uid' pass 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 (cPC cid uid' pass uid)) outOK uw_

goal (1 subgoal):
 1. a = Cact (cPC cid uid' pass uid) &&& ou = outOK
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cPC cid uid' pass 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 (cPC cid uid' uv_ uid)) outOK uw_\<rbrakk> \<Longrightarrow> isPC s' cid uid
 2. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[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. isPC s' cid uid
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
isPC s' cid uid

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

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

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

goal (1 subgoal):
 1. \<And>tr ux_. \<lbrakk>tr ## Trans s a ou s' = tr ## ux_; isPC' tr cid uid\<rbrakk> \<Longrightarrow> isPC s' cid uid
[PROOF STEP]
from COM \<open>step s a = (ou, s')\<close>
[PROOF STATE]
proof (chain)
picking this:
isPC s cid uid
step s a = (ou, s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isPC s cid uid
step s a = (ou, s')

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem isPC_eq: "trace_to tr s \<Longrightarrow> isPC s cid uid = isPC' tr cid uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isPC s cid uid = isPC' tr cid uid
[PROOF STEP]
(* "Trace-based equivalent of committee membership" *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s \<Longrightarrow> isPC s cid uid = isPC' tr cid uid
[PROOF STEP]
using justify_com com_justify
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trace_to ?tr ?s; isPC ?s ?cid ?uid\<rbrakk> \<Longrightarrow> isPC' ?tr ?cid ?uid
\<lbrakk>trace_to ?tr ?s; isPC' ?tr ?cid ?uid\<rbrakk> \<Longrightarrow> isPC ?s ?cid ?uid

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


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

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

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

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

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

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

goal (2 subgoals):
 1. isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
 2. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
with step.IH
[PROOF STATE]
proof (chain)
picking this:
isRev s cid uid pid \<Longrightarrow> isRev' tr cid uid pid
isRev s cid uid pid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isRev s cid uid pid \<Longrightarrow> isRev' tr cid uid pid
isRev s cid uid pid

goal (1 subgoal):
 1. isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
by (blast intro: isRev'.irrelevant)
[PROOF STATE]
proof (state)
this:
isRev' (tr ## Trans s a ou s') cid uid pid

goal (1 subgoal):
 1. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> isRev s cid uid pid

goal (1 subgoal):
 1. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
note noRev = this
[PROOF STATE]
proof (state)
this:
\<not> isRev s cid uid pid

goal (1 subgoal):
 1. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
with step.hyps step.prems
[PROOF STATE]
proof (chain)
picking this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isRev s' cid uid pid
\<not> isRev s cid uid pid
[PROOF STEP]
obtain
      pass uid' where "(a=Cact (cReview cid uid' pass pid uid))"
      and "isChair s cid uid'"
      and [simp]: "ou=outOK"
[PROOF STATE]
proof (prove)
using this:
trace_to tr s
reach s
reach s'
step s a = (ou, s')
isRev s' cid uid pid
\<not> isRev s cid uid pid

goal (1 subgoal):
 1. (\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Cact x1\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x2. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 5. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Cact x1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x1, auto simp add: c_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 4. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Uact x2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x2, auto simp add: u_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 3. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = UUact x3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (cases x3, auto simp add: uu_defs isRev_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Ract x4\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x5. \<lbrakk>\<And>uid' pass. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> thesis; trace_to tr s; reach s; reach s'; step s a = (ou, s'); isRev s' cid uid pid; \<not> isRev s cid uid pid; a = Lact x5\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a = Cact (cReview cid uid' pass pid uid)
isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. \<not> isRev s cid uid pid \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact (cReview cid uid' pass pid uid)
isChair s cid uid'
ou = outOK

goal (1 subgoal):
 1. isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = Cact (cReview cid uid' pass pid uid); isChair s cid uid'; ou = outOK\<rbrakk> \<Longrightarrow> isRev' (tr ## Trans s a ou s') cid uid pid
[PROOF STEP]
apply (rule isRev'.add_rev, auto simp: isChair_eq[OF \<open>trace_to tr s\<close>]) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
isRev' (tr ## Trans s a ou s') cid uid pid

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

goal:
No subgoals!
[PROOF STEP]
qed