Theory Traceback_Properties

theory Traceback_Properties
imports Safety_Properties
begin


section ‹Traceback properties›

text ‹In this section, we prove various traceback properties,
by essentially giving trace-based justifications of certain
occurring situations that are relevant for access to information:
%
\begin{description}
\item{\bf Being an author. }
If a user is an author of a paper, then either the user has registered the paper in the first
place or, inductively, has been appointed as coauthor by another author.
%
\item{\bf Being a chair. }
If a user is a chair of a conference, then either that user has registered the conference
which has been approved by the superuser or, inductively, that user has been appointed
by an existing chair of that conference.
%
%
\item{\bf Being a PC member. }
If a user is a PC member in a conference, then the user either must have been the original chair or must
have been appointed by a chair.
%
\item{\bf Being a reviewer. }
If a user is a paper's reviewer, then the user must have been appointed by a chair (from
among the PC members who have not declared a conflict with the paper).
%
\item{\bf Having conflict. }
If a user has conflict with a paper, then the user is either an author of the paper or the
conflict has been declared by that user or by a paper's author, in such a way that between
the moment when the conflict has been last declared and the current moment there is no
transition that successfully removes the conflict.
%
\item{\bf Conference reaching a phase. }
If a conference is in a given phase different from ``no phase'', then this has happened as
a consequence of either a conference approval action by the superuser (if the phase is
Setup) or a phase change action by a chair (otherwise).
\end{description}

More details and explanations can be found in \<^cite>‹‹Section 3.6› in "cocon-JAR2021"›.
›


subsection ‹Preliminaries›

inductive trace_between :: "state ⇒ (state,act,out) trans trace ⇒ state ⇒ bool" where
  empty[simp]: "trace_between s [] s"
| step: "⟦trace_between s tr sh; step sh a = (ou,s')⟧ ⟹ trace_between s (tr@[Trans sh a ou s']) s'"

inductive_simps
  trace_ft_empty[simp]: "trace_between s [] s'" and
  trace_ft_snoc: "trace_between s (tr@[trn]) s'"
thm trace_ft_empty trace_ft_snoc

lemma trace_ft_append: "trace_between s (tr1@tr2) s'
  ⟷ (∃sh. trace_between s tr1 sh ∧ trace_between sh tr2 s')"
  apply (induction tr2 arbitrary: s' rule: rev_induct)
   apply simp
  apply (subst append_assoc[symmetric], subst trace_ft_snoc)
  apply (auto simp: trace_ft_snoc)
  done

lemma trace_ft_Cons: "trace_between s (trn#tr) s'
  ⟷ (∃sh ou a. trn = Trans s a ou sh ∧ step s a = (ou,sh) ∧ trace_between sh tr s')"
  apply (subst trace_ft_append[where ?tr1.0 = "[trn]", simplified])
  apply (subst trace_ft_snoc[where tr = "[]", simplified])
  by auto

lemmas trace_ft_simps = trace_ft_empty trace_ft_snoc trace_ft_Cons trace_ft_append

inductive trace_to :: " (state,act,out) trans trace ⇒ state ⇒ bool" where
  empty: "trace_to [] istate"
| step: "⟦trace_to tr s; step s a = (ou,s')⟧ ⟹ trace_to (tr@[Trans s a ou s']) s'"

lemma trace_to_ft: "trace_to tr s ⟷ trace_between istate tr s"
proof (rule,goal_cases)
  case 1 thus ?case
    by induction (auto intro: trace_between.intros)
next
  case 2
  moreover
  {fix s' assume "trace_between s' tr s" hence "s' = istate ⟶ trace_to tr s"
   by induction (auto intro: trace_to.intros)
  }
  ultimately show ?case by auto
qed

inductive_simps trace_to_empty[simp]: "trace_to [] s"

lemma trace_to_reach: assumes "trace_to tr s" shows "reach s"
  using assms apply induction
   apply (rule reach.intros)
  by (metis reach_step snd_conv)

lemma reach_to_trace: assumes "reach s" obtains tr where "trace_to tr s"
  using assms apply (induction rule: reach_step_induct)
   apply (auto intro: trace_to.intros) []
  by (metis surjective_pairing trace_to.step)

lemma reach_trace_to_conv: "reach s ⟷ (∃tr. trace_to tr s)"
  by (blast intro: trace_to_reach elim: reach_to_trace)

thm trace_to.induct[no_vars]

lemma trace_to_induct[case_names empty step, induct set]:
  "⟦trace_to x1 x2; P [] istate;
  ⋀tr s a ou s'.
    ⟦trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')⟧
    ⟹ P (tr ## Trans s a ou s') s'⟧
  ⟹ P x1 x2"
  apply (erule trace_to.induct)
   apply simp
  apply (frule trace_to_reach)
  using reach_PairI by blast



subsection ‹Authorship›

text ‹
  Only the creator of a paper, and users explicitly added by other authors,
  are authors of a paper.
›

inductive isAut' :: "(state,act,out) trans trace ⇒ confID ⇒ userID ⇒ paperID ⇒ bool" where
  creator: "⟦ trn = Trans _ (Cact (cPaper cid uid _ pid _ _)) outOK _ ⟧
    ⟹ isAut' (tr@[trn]) cid uid pid"
  (* "The creator of a paper is an author"  *)
| co_author: "⟦
  isAut' tr cid uid' pid;
  trn = Trans _ (Cact (cAuthor cid uid' _ pid uid)) outOK _ ⟧
  ⟹ isAut' (tr@[trn]) cid uid pid"
  (* "An author can add any other user as a coauthor" *)
| irrelevant: "isAut' tr cid uid' pid ⟹ isAut' (tr@[_]) cid uid' pid"

lemma justify_author:
  assumes "trace_to tr s"
  assumes "isAut s cid uid pid"
  shows "isAut' tr cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')
  show ?case
  proof (cases "isAut s cid uid pid")
    case True with step.IH show ?thesis by (blast intro: isAut'.intros)
  next
    case False
    with step.hyps step.prems obtain
      pass s1 s2 uid' where
      "a=Cact (cPaper cid uid pass pid s1 s2)
      ∨ (a=Cact (cAuthor cid uid' pass pid uid) ∧ isAut s cid uid' pid)"
      and [simp]: "ou=outOK"
      apply (cases a)
        subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
        subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
        subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
        by simp_all
    thus ?thesis using step.IH
      apply (elim disjE)
      apply (rule isAut'.creator, auto) []
      apply (rule isAut'.co_author, auto) []
      done
  qed
qed


lemma author_justify:
  assumes "trace_to tr s"
  assumes "isAut' tr cid uid pid"
  shows "isAut s cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: isAut'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (creator _ _ pass s1 s2)
    hence [simp]: "a=Cact (cPaper cid uid pass pid s1 s2)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (co_author _ uid' _ _ pass)
    hence [simp]: "a=Cact (cAuthor cid uid' pass pid uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have AUT: "isAut s cid uid pid" by simp

    note roles_confIDs[OF ‹reach s› AUT]
    with AUT ‹step s a = (ou, s')› show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isAut_eq: "trace_to tr s ⟹ isAut s cid uid pid ⟷ isAut' tr cid uid pid"
  (* "Trace-based equivalent of authorship" *)
  using justify_author author_justify
  by (blast)


subsection ‹Becoming a Conference Chair›

inductive isChair' :: "(state,act,out) trans trace ⇒ confID ⇒ userID ⇒ bool" where
  creator: "⟦ trn=Trans _ (Cact (cConf cid uid _ _ _)) outOK _ ⟧
    ⟹ isChair' (tr@[trn]) cid uid"
| add_chair: "⟦ isChair' tr cid uid'; trn = Trans _ (Cact (cChair cid uid' _ uid)) outOK _ ⟧
  ⟹ isChair' (tr@[trn]) cid uid"
| irrelevant: "⟦isChair' tr cid uid⟧ ⟹ isChair' (tr@[_]) cid uid"

lemma justify_chair:
  assumes "trace_to tr s"
  assumes "isChair s cid uid"
  shows "isChair' tr cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')
  show ?case
  proof (cases "isChair s cid uid")
    case True with step.IH show ?thesis by (blast intro: isChair'.intros)
  next
    case False
    term cConf
    with step.hyps step.prems obtain
      pass s1 s2 uid' where
      "a=Cact (cConf cid uid pass s1 s2)
      ∨ (a=Cact (cChair cid uid' pass uid) ∧ isChair s cid uid')"
      and [simp]: "ou=outOK"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
      by simp_all
    thus ?thesis using step.IH
      apply (elim disjE)
      apply (rule isChair'.creator, auto) []
      apply (rule isChair'.add_chair, auto) []
      done
  qed
qed

lemma chair_justify:
  assumes "trace_to tr s"
  assumes "isChair' tr cid uid"
  shows "isChair s cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: isChair'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (creator _ _ pass s1 s2)
    hence [simp]: "a=Cact (cConf cid uid pass s1 s2)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (add_chair _ uid' _ _ pass)
    hence [simp]: "a=Cact (cChair cid uid' pass uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have CH: "isChair s cid uid" by simp

    from CH ‹step s a = (ou, s')› show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isChair_eq: "trace_to tr s ⟹ isChair s cid uid = isChair' tr cid uid"
  (* "Trace-based equivalent of being a chair" *)
  using justify_chair chair_justify
  by (blast)


subsection ‹Committee Membership›

inductive isPC' :: "(state,act,out) trans trace ⇒ confID ⇒ userID ⇒ bool" where
  chair: "isChair' tr cid uid ⟹ isPC' tr cid uid"
| add_com: "⟦ isChair' tr cid uid'; trn = Trans _ (Cact (cPC cid uid' _ uid)) outOK _ ⟧
  ⟹ isPC' (tr@[trn]) cid uid"
| irrelevant: "⟦isPC' tr cid uid⟧ ⟹ isPC' (tr@[_]) cid uid"

lemma justify_com:
  assumes "trace_to tr s"
  assumes "isPC s cid uid"
  shows "isPC' tr cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')

  show ?case
  proof (cases "isPC s cid uid")
    case True with step.IH show ?thesis by (blast intro: isPC'.irrelevant)
  next
    case False note noPC = this
    show ?thesis proof (cases "isChair s' cid uid")
      case True thus ?thesis
        by (metis chair justify_chair step.hyps(1) step.hyps(4) trace_to.step)
    next
      case False note noChair=this
      from noPC noChair step.hyps step.prems obtain
        pass uid' where "(a=Cact (cPC cid uid' pass uid))"
        and "isChair s cid uid'"
        and [simp]: "ou=outOK"
        apply (cases a)
        subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
        subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
        subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
        by simp_all
      thus ?thesis
        apply -
        apply (rule isPC'.add_com, auto simp: isChair_eq[OF ‹trace_to tr s›]) []
        done
    qed
  qed
qed

lemma com_justify:
  assumes "trace_to tr s"
  assumes "isPC' tr cid uid"
  shows "isPC s cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim!: isPC'.cases isChair'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case chair thus ?thesis
      by (metis isChair_eq isChair_isPC step.hyps(1) step.hyps(3) step.hyps(4) trace_to.step)
  next
    case (add_com _ uid' _ _ pass)
    hence [simp]: "a=Cact (cPC cid uid' pass uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have COM: "isPC s cid uid" by simp

    from COM ‹step s a = (ou, s')› show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isPC_eq: "trace_to tr s ⟹ isPC s cid uid = isPC' tr cid uid"
  (* "Trace-based equivalent of committee membership" *)
  using justify_com com_justify
  by (blast)


subsection ‹Being a Reviewer›

inductive isRev' :: "(state,act,out) trans trace ⇒ confID ⇒ userID ⇒ paperID ⇒ bool" where
  add_rev: "⟦ isChair' tr cid uid'; trn = Trans _ (Cact (cReview cid uid' _ pid uid)) outOK _ ⟧
  ⟹ isRev' (tr@[trn]) cid uid pid"
| irrelevant: "⟦isRev' tr cid uid pid⟧ ⟹ isRev' (tr@[_]) cid uid pid"

lemma justify_rev:
  assumes "trace_to tr s"
  assumes "isRev s cid uid pid"
  shows "isRev' tr cid uid pid"
  using assms
proof (induction)
  case empty thus ?case
    by (auto simp add: istate_def isRev_def)
next
  case (step tr s a ou s')

  show ?case
  proof (cases "isRev s cid uid pid")
    case True with step.IH show ?thesis by (blast intro: isRev'.irrelevant)
  next
    case False note noRev = this
    with step.hyps step.prems obtain
      pass uid' where "(a=Cact (cReview cid uid' pass pid uid))"
      and "isChair s cid uid'"
      and [simp]: "ou=outOK"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp add: c_defs isRev_def) [] .
      subgoal for x2 apply (cases x2, auto simp add: u_defs isRev_def) [] .
      subgoal for x3 apply (cases x3, auto simp add: uu_defs isRev_def) [] .
      by simp_all
    thus ?thesis
      apply -
      apply (rule isRev'.add_rev, auto simp: isChair_eq[OF ‹trace_to tr s›]) []
      done
  qed
qed

lemma rev_justify:
  assumes "trace_to tr s"
  assumes "isRev' tr cid uid pid"
  shows "isRev s cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim!: isRev'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (add_rev _ uid' _ _ pass)
    hence [simp]: "a=Cact (cReview cid uid' pass pid uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs isRev_def)
  next
    case (irrelevant) with step.IH have REV: "isRev s cid uid pid" by simp

    note roles_confIDs[OF step.hyps(2)]
    with REV ‹step s a = (ou, s')› show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs isRev_def) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs isRev_def) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs isRev_def) [] .
      by simp_all
  qed
qed

theorem isRev_eq: "trace_to tr s ⟹ isRev s cid uid pid = isRev' tr cid uid pid"
  (* "Trace-based equivalent of being a reviewer" *)
  using justify_rev rev_justify
  by (blast)



subsection "Conflicts"

fun irrev_conflict :: "userID ⇒ paperID ⇒ (state,act,out) trans ⇒ bool"
 (* "Transitions causing irrevokable conflicts" *)
where
  "irrev_conflict uid pid (Trans _ (Cact (cPaper _ uid' _ pid' _ _)) outOK _)
    ⟷ uid'=uid ∧ pid'=pid"
| "irrev_conflict uid pid (Trans _ (Cact (cAuthor _ _ _ pid' uid')) outOK _)
    ⟷ uid'=uid ∧ pid'=pid"
| "irrev_conflict uid pid _ ⟷ False"

fun set_conflict :: "userID ⇒ paperID ⇒ (state,act,out) trans ⇒ bool"
  (* "Transitions setting conflict state, can be revoked by later reset-actions" *)
  where
  "set_conflict uid pid (Trans _ (Cact (cConflict _ _ _ pid' uid')) outOK _)
    ⟷ uid'=uid ∧ pid'=pid"
| "set_conflict uid pid (Trans _ (Uact (uPref _ uid' _ pid' Conflict)) outOK _)
    ⟷ uid'=uid ∧ pid'=pid"
| "set_conflict _ _ _ ⟷ False"

fun reset_conflict :: "userID ⇒ paperID ⇒ (state,act,out)trans ⇒ bool"
  (* "Transitions re-setting conflict state, can be revoked by later set-actions" *)
  where
  "reset_conflict uid pid (Trans _ (Uact (uPref _ uid' _ pid' pr)) outOK _)
    ⟷ uid'=uid ∧ pid'=pid ∧ pr≠Conflict"
| "reset_conflict _ _ _ ⟷ False"

definition conflict_trace :: "userID ⇒ paperID ⇒ (state,act,out) trans trace ⇒ bool"
  (* "Trace that causes a conflict: It contains either an irrevokable conflict action,
    or the last action concerning conflicts was set-conflict" *)
  where
  "conflict_trace uid pid tr ≡
  (∃trn∈set tr. irrev_conflict uid pid trn)
∨ (∃tr1 trn tr2. tr=tr1@trn#tr2 ∧
    set_conflict uid pid trn ∧ (∀trn∈set tr2. ¬reset_conflict uid pid trn))"

lemma irrev_conflict_impl_author:
  assumes "trace_to tr s"
  assumes "∃trn∈set tr. irrev_conflict uid pid trn"
  shows "∃cid. isAut s cid uid pid"
  using assms
  apply induction
  apply (auto simp add: istate_def) []
  subgoal for _ _ a apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs, (metis roles_confIDs)+) [] .
    subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
    subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
    by simp_all
  done

lemma irrev_conflict_impl_conflict:
  assumes "trace_to tr s"
  assumes "∃trn∈set tr. irrev_conflict uid pid trn"
  shows "pref s uid pid = Conflict"
  by (metis assms(1) assms(2) irrev_conflict_impl_author
    isAut_pref_Conflict reach_trace_to_conv)

lemma conflict_justify:
  assumes TR: "trace_to tr s"
  assumes "conflict_trace uid pid tr"
  shows "pref s uid pid = Conflict"
  using assms(2)
  unfolding conflict_trace_def
proof (cases rule: disjE[consumes 1, case_names irrev set])
  case irrev thus ?thesis by (simp add: irrev_conflict_impl_conflict[OF TR])
next
  case set
  then obtain tr1 trn tr2 where
    [simp]: "tr = tr1 @ trn # tr2" and
    SET: "set_conflict uid pid trn"
    and NRESET: "∀trn∈set tr2. ¬ reset_conflict uid pid trn"
    by blast

  from TR obtain s1 s2 a ou where
    [simp]: "trn = Trans s1 a ou s2" and
    TR1: "trace_to tr1 s1" and
    STEP: "step s1 a = (ou,s2)" and
    TR2: "trace_between s2 tr2 s"
    by (fastforce simp add: trace_to_ft trace_ft_simps)

  from STEP SET have "pref s2 uid pid = Conflict"
    apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) []
        subgoal for _ x65 apply (cases x65, auto) [] .
        subgoal for _ _ _ x65 apply (cases x65, auto) [] .
        subgoal for _ _ _ x65 apply (cases x65, auto) [] . .
      by simp_all

  with TR2 NRESET show ?thesis
    apply induction
    subgoal by simp
    subgoal for _ _ _ a apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
    done
qed

lemma justify_conflict:
  assumes TR: "trace_to tr s"
  assumes "pref s uid pid = Conflict"
  shows "conflict_trace uid pid tr"
  using assms
proof induction
  case empty thus ?case by (auto simp add: istate_def)
next
  case (step tr s a ou s')

  let ?trn = "Trans s a ou s'"

  show ?case proof (cases "pref s uid pid = Conflict")
    case False
    with step.prems ‹step s a = (ou, s')›
    have "irrev_conflict uid pid ?trn ∨ set_conflict uid pid ?trn"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
    thus ?thesis
      unfolding conflict_trace_def by fastforce
  next
    case True with step.IH have CT: "conflict_trace uid pid tr" .

    from step.prems ‹step s a = (ou, s')› have "¬reset_conflict uid pid ?trn"
      apply (cases a)
      subgoal by simp
      subgoal for x2 by (cases x2, auto simp: u_defs)
      by simp_all

    thus ?thesis using CT
      unfolding conflict_trace_def
      apply clarsimp
      by (metis rotate1.simps(2) set_ConsD set_rotate1)

  qed
qed

theorem conflict_eq:
  assumes "trace_to tr s"
  shows "pref s uid pid = Conflict ⟷ conflict_trace uid pid tr"
  using assms conflict_justify justify_conflict by auto


subsection ‹Conference Phases›

fun is_uPhase where
  "is_uPhase cid (Trans _ (Uact (uConfA cid' _ _)) outOK _) ⟷ cid'=cid"
| "is_uPhase cid (Trans _ (Uact (uPhase cid' _ _ _)) outOK _) ⟷ cid'=cid"
| "is_uPhase _ _ ⟷ False"

inductive phase' :: "(state,act,out) trans trace ⇒ confID ⇒ nat ⇒ bool" where
  initial: "phase' [] cid noPH"
| approve: "⟦phase' tr cid noPH; trn=Trans s (Uact (uConfA cid (voronkov s) _)) outOK _ ⟧
  ⟹ phase' (tr@[trn]) cid setPH"
| advance: "⟦trn = (Trans _ (Uact (uPhase cid uid _ ph)) outOK _); isChair' tr cid uid⟧
  ⟹ phase' (tr@[trn]) cid ph"
| irrelevant: "⟦phase' tr cid ph; ¬is_uPhase cid trn ⟧ ⟹ phase' (tr@[trn]) cid ph"

lemma justify_phase:
  assumes "trace_to tr s"
  assumes "phase s cid = ph"
  shows "phase' tr cid ph"
  using assms
proof (induction arbitrary: ph)
  case (empty s) thus ?case
    by (auto simp add: istate_def phase'.initial)
next
  case (step tr s a ou s')
  thus ?case
    apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs intro: phase'.advance phase'.irrelevant) [] .
    subgoal for x2 apply (cases x2,
      auto
        simp: u_defs isChair_eq
        intro: phase'.advance phase'.irrelevant phase'.approve,
      (fastforce intro: phase'.approve phase'.irrelevant phase'.advance)+
    ) [] .

    subgoal for x3 apply (cases x3, auto simp: uu_defs intro: phase'.irrelevant) [] .
    by (auto intro: phase'.advance phase'.irrelevant)
qed

lemma phase_justify:
  assumes "trace_to tr s"
  assumes "phase' tr cid ph"
  shows "phase s cid = ph"
  using assms
proof (induction arbitrary: ph)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: phase'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (approve _ _ _ pass _)
    hence [simp]: "a=Uact (uConfA cid (voronkov s) pass)" "ou=outOK" "ph=setPH" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: u_defs)
  next
    case (advance _ _ uid pass _ _)
    hence [simp]: "a=Uact (uPhase cid uid pass ph)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: u_defs)
  next
    case (irrelevant) with step.IH have PH: "phase s cid = ph" "¬ is_uPhase cid (Trans s a ou s')"
      by simp_all

    from PH ‹step s a = (ou, s')› show ?thesis
    apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
    subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
    subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
    by simp_all
  qed auto
qed

theorem phase_eq:
  assumes "trace_to tr s"
  shows "phase s cid = ph ⟷ phase' tr cid ph"
  using assms phase_justify justify_phase by blast

end