Theory Decision_Value_Setup

theory Decision_Value_Setup
imports Decision_Intro
begin

text ‹The ID of the paper under scrutiny:›

consts PID :: paperID

subsection ‹Preliminaries›

declare updates_commute_paper[simp]

(* two papers equal everywhere but w.r.t. decision: *)
fun eqExcD :: "paper ⇒ paper ⇒ bool" where
"eqExcD (Paper title abstract ct reviews dis decs)
        (Paper title1 abstract1 ct1 reviews1 dis1 decs1) =
 (title = title1 ∧ abstract = abstract1 ∧ ct = ct1 ∧ reviews = reviews1 ∧ dis = dis1)"

lemma eqExcD:
"eqExcD pap pap1 =
 (titlePaper pap = titlePaper pap1 ∧ abstractPaper pap = abstractPaper pap1 ∧
  contentPaper pap = contentPaper pap1 ∧
  reviewsPaper pap = reviewsPaper pap1 ∧ disPaper pap = disPaper pap1)"
by(cases pap, cases pap1, auto)

lemma eqExcD_eq[simp,intro!]: "eqExcD pap pap"
by(cases pap) auto

lemma eqExcD_sym:
assumes "eqExcD pap pap1"
shows "eqExcD pap1 pap"
apply(cases pap, cases pap1)
using assms by auto

lemma eqExcD_trans:
assumes "eqExcD pap pap1" and "eqExcD pap1 pap2"
shows "eqExcD pap pap2"
apply(cases pap, cases pap1, cases pap2)
using assms by auto

(* Auxiliary notion:  *)
definition eeqExcPID where
"eeqExcPID paps paps1 ≡
 ∀ pid. if pid = PID then eqExcD (paps pid) (paps1 pid) else paps pid = paps1 pid"

lemma eeqExcPID_eeq[simp,intro!]: "eeqExcPID s s"
unfolding eeqExcPID_def by auto

lemma eeqExcPID_sym:
assumes "eeqExcPID s s1" shows "eeqExcPID s1 s"
using assms eqExcD_sym unfolding eeqExcPID_def by auto

lemma eeqExcPID_trans:
assumes "eeqExcPID s s1" and "eeqExcPID s1 s2" shows "eeqExcPID s s2"
using assms eqExcD_trans unfolding eeqExcPID_def by simp blast

lemma eeqExcPID_imp:
"eeqExcPID paps paps1 ⟹ eqExcD (paps PID) (paps1 PID)"
"⟦eeqExcPID paps paps1; pid ≠ PID⟧ ⟹ paps pid = paps1 pid"
unfolding eeqExcPID_def by auto

lemma eeqExcPID_cong:
assumes "eeqExcPID paps paps1"
and "pid = PID ⟹ eqExcD uu uu1"
and "pid ≠ PID ⟹ uu = uu1"
shows "eeqExcPID (paps (pid := uu)) (paps1(pid := uu1))"
using assms unfolding eeqExcPID_def by auto

lemma eeqExcPID_RDD:
"eeqExcPID paps paps1 ⟹
 titlePaper (paps PID) = titlePaper (paps1 PID) ∧
 abstractPaper (paps PID) = abstractPaper (paps1 PID) ∧
 contentPaper (paps PID) = contentPaper (paps1 PID) ∧
 reviewsPaper (paps PID) = reviewsPaper (paps1 PID) ∧
 disPaper (paps PID) = disPaper (paps1 PID)"
using eeqExcPID_def unfolding eqExcD by auto

(* The notion of two states being equal everywhere but on the decision of
   the paper associated to a given PID *)
definition eqExcPID :: "state ⇒ state ⇒ bool" where
"eqExcPID s s1 ≡
 confIDs s = confIDs s1 ∧ conf s = conf s1 ∧
 userIDs s = userIDs s1 ∧ pass s = pass s1 ∧ user s = user s1 ∧ roles s = roles s1 ∧
 paperIDs s = paperIDs s1
 ∧
 eeqExcPID (paper s) (paper s1)
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1"

lemma eqExcPID_eq[simp,intro!]: "eqExcPID s s"
unfolding eqExcPID_def by auto

lemma eqExcPID_sym:
assumes "eqExcPID s s1" shows "eqExcPID s1 s"
using assms eeqExcPID_sym unfolding eqExcPID_def by auto

lemma eqExcPID_trans:
assumes "eqExcPID s s1" and "eqExcPID s1 s2" shows "eqExcPID s s2"
using assms eeqExcPID_trans unfolding eqExcPID_def by auto

(* Implications from eqExcPID, including w.r.t. auxiliary operations: *)
lemma eqExcPID_imp:
"eqExcPID s s1 ⟹
 confIDs s = confIDs s1 ∧ conf s = conf s1 ∧
 userIDs s = userIDs s1 ∧ pass s = pass s1 ∧ user s = user s1 ∧ roles s = roles s1 ∧
 paperIDs s = paperIDs s1
 ∧
 eeqExcPID (paper s) (paper s1)
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1 ∧

 getAllPaperIDs s = getAllPaperIDs s1 ∧
 isRev s cid uid pid = isRev s1 cid uid pid ∧
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid ∧
 getRevRole s cid uid pid = getRevRole s1 cid uid pid"
unfolding eqExcPID_def getAllPaperIDs_def
unfolding isRev_def getReviewIndex_def getRevRole_def by auto

lemma eqExcPID_imp1:
"eqExcPID s s1 ⟹ eqExcD (paper s pid) (paper s1 pid)"
"eqExcPID s s1 ⟹ pid ≠ PID ∨ PID ≠ pid ⟹
    paper s pid = paper s1 pid ∧
    getNthReview s pid n = getNthReview s1 pid n"
unfolding eqExcPID_def getNthReview_def eeqExcPID_def
apply auto
by (metis eqExcD_eq)

lemma eqExcPID_imp2:
assumes "eqExcPID s s1" and "pid ≠ PID ∨ PID ≠ pid"
shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid"
proof-
  have
  "(λuID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) =
   (λuID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])"
  apply(rule ext)
  using assms by (auto simp: eqExcPID_imp eqExcPID_imp1)
  thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID_imp)
qed

lemma eqExcPID_RDD:
"eqExcPID s s1 ⟹
 titlePaper (paper s PID) = titlePaper (paper s1 PID) ∧
 abstractPaper (paper s PID) = abstractPaper (paper s1 PID) ∧
 contentPaper (paper s PID) = contentPaper (paper s1 PID) ∧
 reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) ∧
 disPaper (paper s PID) = disPaper (paper s1 PID)"
using eqExcPID_imp eeqExcPID_RDD by auto

lemma eqExcPID_cong[simp, intro]:
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇confIDs := uu1⦈) (s1 ⦇confIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇conf := uu1⦈) (s1 ⦇conf := uu2⦈)"

"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇userIDs := uu1⦈) (s1 ⦇userIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇pass := uu1⦈) (s1 ⦇pass := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇user := uu1⦈) (s1 ⦇user := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇roles := uu1⦈) (s1 ⦇roles := uu2⦈)"

"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇paperIDs := uu1⦈) (s1 ⦇paperIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ eeqExcPID uu1 uu2 ⟹ eqExcPID (s ⦇paper := uu1⦈) (s1 ⦇paper := uu2⦈)"

"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇pref := uu1⦈) (s1 ⦇pref := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇voronkov := uu1⦈) (s1 ⦇voronkov := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇news := uu1⦈) (s1 ⦇news := uu2⦈)"
"⋀ uu1 uu2. eqExcPID s s1 ⟹ uu1 = uu2 ⟹ eqExcPID (s ⦇phase := uu1⦈) (s1 ⦇phase := uu2⦈)"
unfolding eqExcPID_def by auto

lemma eqExcPID_Paper:
assumes s's1': "eqExcPID s s1"
and "paper s pid = Paper title abstract content reviews dis decs"
and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1"
shows "title = title1 ∧ abstract = abstract1 ∧ content = content1 ∧ reviews = reviews1 ∧ dis = dis1"
using assms unfolding eqExcPID_def apply (auto simp: eqExcD eeqExcPID_def)
by (metis titlePaper.simps abstractPaper.simps contentPaper.simps reviewsPaper.simps disPaper.simps
          )+

text ‹Weaker equivalence relations that allow differences in the final decision.  This is used for
verifying the confidentiality property that only protects earlier updates to the decision.›

(* two papers equal everywhere but w.r.t. the tail of the decision: *)
fun eqExcD2 :: "paper ⇒ paper ⇒ bool" where
"eqExcD2 (Paper title abstract ct reviews dis decs )
         (Paper title1 abstract1 ct1 reviews1 dis1 decs1) =
 (title = title1 ∧ abstract = abstract1 ∧ ct = ct1 ∧ reviews = reviews1 ∧ dis = dis1 ∧
 hd decs = hd decs1)"

lemma eqExcD2:
"eqExcD2 pap pap1 =
 (titlePaper pap = titlePaper pap1 ∧ abstractPaper pap = abstractPaper pap1 ∧
  contentPaper pap = contentPaper pap1 ∧
  reviewsPaper pap = reviewsPaper pap1 ∧ disPaper pap = disPaper pap1 ∧
  hd (decsPaper pap) = hd (decsPaper pap1)
 )"
by(cases pap, cases pap1, auto)

lemma eqExcD2_eq[simp,intro!]: "eqExcD2 pap pap"
by(cases pap) auto

lemma eqExcD2_sym:
assumes "eqExcD2 pap pap1"
shows "eqExcD2 pap1 pap"
apply(cases pap, cases pap1)
using assms by auto

lemma eqExcD2_trans:
assumes "eqExcD2 pap pap1" and "eqExcD2 pap1 pap2"
shows "eqExcD2 pap pap2"
apply(cases pap, cases pap1, cases pap2)
using assms by auto

(* Auxiliary notion:  *)
definition eeqExcPID2 where
"eeqExcPID2 paps paps1 ≡
 ∀ pid. if pid = PID then eqExcD2 (paps pid) (paps1 pid) else paps pid = paps1 pid"

lemma eeqExcPID2_eeq[simp,intro!]: "eeqExcPID2 s s"
unfolding eeqExcPID2_def by auto

lemma eeqExcPID2_sym:
assumes "eeqExcPID2 s s1" shows "eeqExcPID2 s1 s"
using assms eqExcD2_sym unfolding eeqExcPID2_def by auto

lemma eeqExcPID2_trans:
assumes "eeqExcPID2 s s1" and "eeqExcPID2 s1 s2" shows "eeqExcPID2 s s2"
using assms eqExcD2_trans unfolding eeqExcPID2_def by simp blast

lemma eeqExcPID2_imp:
"eeqExcPID2 paps paps1 ⟹ eqExcD2 (paps PID) (paps1 PID)"
"⟦eeqExcPID2 paps paps1; pid ≠ PID⟧ ⟹ paps pid = paps1 pid"
unfolding eeqExcPID2_def by auto

lemma eeqExcPID2_cong:
assumes "eeqExcPID2 paps paps1"
and "pid = PID ⟹ eqExcD2 uu uu1"
and "pid ≠ PID ⟹ uu = uu1"
shows "eeqExcPID2 (paps (pid := uu)) (paps1(pid := uu1))"
using assms unfolding eeqExcPID2_def by auto

lemma eeqExcPID2_RDD:
"eeqExcPID2 paps paps1 ⟹
 titlePaper (paps PID) = titlePaper (paps1 PID) ∧
 abstractPaper (paps PID) = abstractPaper (paps1 PID) ∧
 contentPaper (paps PID) = contentPaper (paps1 PID) ∧
 reviewsPaper (paps PID) = reviewsPaper (paps1 PID) ∧
 disPaper (paps PID) = disPaper (paps1 PID) ∧
 hd (decsPaper (paps PID)) = hd (decsPaper (paps PID))"
using eeqExcPID2_def unfolding eqExcD2 by auto

(* The notion of two states being equal everywhere but on the tail of the decision of
   the paper associated to a given PID *)
definition eqExcPID2 :: "state ⇒ state ⇒ bool" where
"eqExcPID2 s s1 ≡
 confIDs s = confIDs s1 ∧ conf s = conf s1 ∧
 userIDs s = userIDs s1 ∧ pass s = pass s1 ∧ user s = user s1 ∧ roles s = roles s1 ∧
 paperIDs s = paperIDs s1
 ∧
 eeqExcPID2 (paper s) (paper s1)
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1"

lemma eqExcPID2_eq[simp,intro!]: "eqExcPID2 s s"
unfolding eqExcPID2_def by auto

lemma eqExcPID2_sym:
assumes "eqExcPID2 s s1" shows "eqExcPID2 s1 s"
using assms eeqExcPID2_sym unfolding eqExcPID2_def by auto

lemma eqExcPID2_trans:
assumes "eqExcPID2 s s1" and "eqExcPID2 s1 s2" shows "eqExcPID2 s s2"
using assms eeqExcPID2_trans unfolding eqExcPID2_def by auto

(* Implications from eqExcPID2, including w.r.t. auxiliary operations: *)
lemma eqExcPID2_imp:
"eqExcPID2 s s1 ⟹
 confIDs s = confIDs s1 ∧ conf s = conf s1 ∧
 userIDs s = userIDs s1 ∧ pass s = pass s1 ∧ user s = user s1 ∧ roles s = roles s1 ∧
 paperIDs s = paperIDs s1
 ∧
 eeqExcPID2 (paper s) (paper s1)
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1 ∧

 getAllPaperIDs s = getAllPaperIDs s1 ∧
 isRev s cid uid pid = isRev s1 cid uid pid ∧
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid ∧
 getRevRole s cid uid pid = getRevRole s1 cid uid pid"
unfolding eqExcPID2_def getAllPaperIDs_def
unfolding isRev_def getReviewIndex_def getRevRole_def by auto

lemma eqExcPID2_imp1:
"eqExcPID2 s s1 ⟹ eqExcD2 (paper s pid) (paper s1 pid)"
"eqExcPID2 s s1 ⟹ pid ≠ PID ∨ PID ≠ pid ⟹
    paper s pid = paper s1 pid ∧
    getNthReview s pid n = getNthReview s1 pid n"
unfolding eqExcPID2_def getNthReview_def eeqExcPID2_def
apply auto
by (metis eqExcD2_eq)

lemma eqExcPID2_imp2:
assumes "eqExcPID2 s s1" and "pid ≠ PID ∨ PID ≠ pid"
shows "getReviewersReviews s cid pid = getReviewersReviews s1 cid pid"
proof-
  have
  "(λuID. if isRev s cid uID pid then [(uID, getNthReview s pid (getReviewIndex s cid uID pid))] else []) =
   (λuID. if isRev s1 cid uID pid then [(uID, getNthReview s1 pid (getReviewIndex s1 cid uID pid))] else [])"
  apply(rule ext)
  using assms by (auto simp: eqExcPID2_imp eqExcPID2_imp1)
  thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID2_imp)
qed

lemma eqExcPID2_RDD:
"eqExcPID2 s s1 ⟹
 titlePaper (paper s PID) = titlePaper (paper s1 PID) ∧
 abstractPaper (paper s PID) = abstractPaper (paper s1 PID) ∧
 contentPaper (paper s PID) = contentPaper (paper s1 PID) ∧
 reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) ∧
 disPaper (paper s PID) = disPaper (paper s1 PID)"
using eqExcPID2_imp eeqExcPID2_RDD by auto

lemma eqExcPID2_cong[simp, intro]:
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇confIDs := uu1⦈) (s1 ⦇confIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇conf := uu1⦈) (s1 ⦇conf := uu2⦈)"

"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇userIDs := uu1⦈) (s1 ⦇userIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇pass := uu1⦈) (s1 ⦇pass := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇user := uu1⦈) (s1 ⦇user := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇roles := uu1⦈) (s1 ⦇roles := uu2⦈)"

"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇paperIDs := uu1⦈) (s1 ⦇paperIDs := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ eeqExcPID2 uu1 uu2 ⟹ eqExcPID2 (s ⦇paper := uu1⦈) (s1 ⦇paper := uu2⦈)"

"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇pref := uu1⦈) (s1 ⦇pref := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇voronkov := uu1⦈) (s1 ⦇voronkov := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇news := uu1⦈) (s1 ⦇news := uu2⦈)"
"⋀ uu1 uu2. eqExcPID2 s s1 ⟹ uu1 = uu2 ⟹ eqExcPID2 (s ⦇phase := uu1⦈) (s1 ⦇phase := uu2⦈)"
unfolding eqExcPID2_def by auto

lemma eqExcPID2_Paper:
assumes s's1': "eqExcPID2 s s1"
and "paper s pid = Paper title abstract content reviews dis decs"
and "paper s1 pid = Paper title1 abstract1 content1 reviews1 dis1 decs1"
shows "title = title1 ∧ abstract = abstract1 ∧ content = content1 ∧ reviews = reviews1 ∧
    dis = dis1"
using assms unfolding eqExcPID2_def apply (auto simp: eqExcD2 eeqExcPID2_def)
  by (metis titlePaper.simps abstractPaper.simps contentPaper.simps reviewsPaper.simps
disPaper.simps)+


subsection ‹Value Setup›

type_synonym "value" = decision

fun φ :: "(state,act,out) trans ⇒ bool" where
"φ (Trans _ (UUact (uuDec cid uid p pid dec)) ou _) = (pid = PID ∧ ou = outOK)"
|
"φ _ = False"

lemma φ_def2:
"φ (Trans s a ou s') = (∃ cid uid p dec. a = UUact (uuDec cid uid p PID dec) ∧ ou = outOK)"
proof (cases a)
  case (UUact x3)
  then show ?thesis by (cases x3; auto)
qed auto

fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans _ (UUact (uuDec cid uid p pid dec)) _ _) = dec"

lemma UUact_uuDec_step_eqExcPID:
assumes a: "a = UUact (uuDec cid uid p PID dec)"
and "step s a = (ou,s')"
shows "eqExcPID s s'"
using assms unfolding eqExcPID_def eeqExcPID_def by (auto simp: uu_defs)

lemma φ_step_eqExcPID:
assumes φ: "φ (Trans s a ou s')"
and s: "step s a = (ou,s')"
shows "eqExcPID s s'"
using φ UUact_uuDec_step_eqExcPID[OF _ s] unfolding φ_def2 by blast

(* major *) lemma eqExcPID_step:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
shows "eqExcPID s' s1'"
proof -
  note eqs = eqExcPID_imp[OF s's1']
  note eqs' = eqExcPID_imp1[OF s's1']

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def eeqExcPID_def eqExcD
  note * = step step1 eqs eqs'

  then show ?thesis
  proof (cases a)
    case (Cact x1)
    then show ?thesis using * by (cases x1; auto)
  next
    case (Uact x2)
    then show ?thesis using * by (cases x2; auto)
  next
    case (UUact x3)
    then show ?thesis using * by (cases x3; auto)
  qed auto
qed

lemma eqExcPID_step_φ_imp:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
shows "φ (Trans s1 a ou1 s1')"
using assms unfolding φ_def2 by (auto simp add: uu_defs eqExcPID_imp)

lemma eqExcPID_step_φ:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "φ (Trans s a ou s') = φ (Trans s1 a ou1 s1')"
by (metis eqExcPID_step_φ_imp eqExcPID_sym assms)


(* These hold for eeqExcPID, but not for eeqExcPID2:
lemma UUact_uuDec_step_eqExcPID2:
assumes a: "a = UUact (uuDec cid uid p PID dec)"
and "step s a = (ou,s')"
shows "eqExcPID2 s s'"
using assms unfolding eqExcPID2_def eeqExcPID2_def by (auto simp: uu_defs)

lemma φ_step_eqExcPID2:
assumes φ: "φ (Trans s a ou s')"
and s: "step s a = (ou,s')"
shows "eqExcPID2 s s'"
using φ UUact_uuDec_step_eqExcPID2[OF _ s] unfolding φ_def2 by blast
*)

(* major *) lemma eqExcPID2_step:
assumes s's1': "eqExcPID2 s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
shows "eqExcPID2 s' s1'"
proof -
  note eqs = eqExcPID2_imp[OF s's1']
  note eqs' = eqExcPID2_imp1[OF s's1']

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID2_def eeqExcPID2_def eqExcD2
  note * = s's1' step step1 eqs eqs'

  then show ?thesis
  proof (cases a)
    case (Cact x1)
    then show ?thesis using * by (cases x1; auto)
  next
    case (Uact x2)
    then show ?thesis using * by (cases x2; auto)
  next
    case (UUact x3)
    then show ?thesis using * by (cases x3; auto)
  qed auto
qed

lemma eqExcPID2_step_φ_imp:
assumes s's1': "eqExcPID2 s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
shows "φ (Trans s1 a ou1 s1')"
using assms unfolding φ_def2 by (auto simp add: uu_defs eqExcPID2_imp)

lemma eqExcPID2_step_φ:
assumes s's1': "eqExcPID2 s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "φ (Trans s a ou s') = φ (Trans s1 a ou1 s1')"
by (metis eqExcPID2_step_φ_imp eqExcPID2_sym assms)

end