Theory Reviewer_Assignment_Value_Setup

(* The value setup for reviewer confidentiality *)
theory Reviewer_Assignment_Value_Setup
  imports Reviewer_Assignment_Intro
begin


subsection ‹Preliminaries›

declare updates_commute_paper[simp]

consts PID :: paperID

(* Equality of two role lists everywhere except on their PID reviewer roles *)
definition eqExcRLR :: "role list ⇒ role list ⇒ bool" where
"eqExcRLR rl rl1 ≡ [r ← rl . ¬ isRevRoleFor PID r] = [r ← rl1 . ¬ isRevRoleFor PID r]"

lemma eqExcRLR_set:
assumes 1: "eqExcRLR rl rl1" and 2: "¬ isRevRoleFor PID r"
shows "r ∈∈ rl ⟷ r ∈∈ rl1"
proof-
  have "set ([r←rl . ¬ isRevRoleFor PID r]) = set ([r←rl1 . ¬ isRevRoleFor PID r])"
  using 1 unfolding eqExcRLR_def by auto
  thus ?thesis using 2 unfolding set_filter by auto
qed

lemmas eqExcRLR = eqExcRLR_def

lemma eqExcRLR_eq[simp,intro!]: "eqExcRLR rl rl"
unfolding eqExcRLR by auto

lemma eqExcRLR_sym:
assumes "eqExcRLR rl rl1"
shows "eqExcRLR rl1 rl"
using assms unfolding eqExcRLR by auto

lemma eqExcRLR_trans:
assumes "eqExcRLR rl rl1" and "eqExcRLR rl1 rl2"
shows "eqExcRLR rl rl2"
using assms unfolding eqExcRLR by auto

lemma eqExcRLR_imp:
assumes s: "reach s" and pid: "pid ≠ PID" and
1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)"
shows
"isRevNth s cid uid pid = isRevNth s1 cid uid pid ∧
 isRev s cid uid pid = isRev s1 cid uid pid ∧
 getRevRole s cid uid pid = getRevRole s1 cid uid pid ∧
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid" (is "?A ∧ ?B ∧ ?C ∧ ?D")
proof(intro conjI)
  show A: ?A
    apply(rule ext)
    using 1 by (metis eqExcRLR_set isRevRoleFor.simps(1) pid)
  show B: ?B using A unfolding isRev_def2 by auto
  show C: ?C
    apply(cases "isRev s cid uid pid")
    subgoal by (metis A B getRevRole_Some_Rev_isRevNth isRevNth_equals isRev_getRevRole2 s)
    by (metis B Bex_set_list_ex find_None_iff getRevRole_def isRev_def)
  show D: ?D unfolding getReviewIndex_def using C by auto
qed

lemma eqExcRLR_imp2:
assumes "eqExcRLR (roles s cid uid) (roles s1 cid uid)"
shows
"isPC s cid uid = isPC s1 cid uid ∧
 isChair s cid uid = isChair s1 cid uid ∧
 isAut s cid uid = isAut s1 cid uid"
by (metis (opaque_lifting, no_types) assms eqExcRLR_set isRevRoleFor.simps)

(* fixme: move where belong *)
lemma filter_eq_imp:
assumes "⋀ x. P x ⟹ Q x"
and "filter Q xs = filter Q ys"
shows "filter P xs = filter P ys"
using assms filter_filter
proof-
  have "filter P xs = filter P (filter Q xs)"
  unfolding filter_filter using assms by metis
  also have "... = filter P (filter Q ys)" using assms by simp
  also have "... = filter P ys" unfolding filter_filter using assms by metis
  finally show ?thesis .
qed

lemma arg_cong3: "a = a1 ⟹ b = b1 ⟹ c = c1 ⟹ h a b c = h a1 b1 c1"
by auto

lemmas map_concat_cong1 = arg_cong[where f = concat, OF arg_cong2[where f = map, OF _ refl]]
lemmas If_cong1 = arg_cong3[where h = If, OF _ refl refl]

lemma diff_cong1: "a = a1 ⟹ (a ≠ b) = (a1 ≠ b)" by auto

lemma isRev_pref_notConflict:
assumes "reach s" and "isRev s cid uid pid"
shows "pref s uid pid ≠ Conflict"
by (metis assms pref_Conflict_isRev)

lemma isRev_pref_notConflict_isPC:
assumes "reach s" and "isRev s cid uid pid"
shows "pref s uid pid ≠ Conflict ∧ isPC s cid uid"
by (metis assms(1) assms(2) isRev_isPC isRev_pref_notConflict)

lemma eqExcRLR_imp_isRevRole_imp:
assumes "eqExcRLR rl rl1"
shows "[r← rl. ¬ isRevRole r] = [r← rl1 . ¬ isRevRole r]"
using assms filter_eq_imp unfolding eqExcRLR_def
by (metis isRevRole.simps(1) isRevRoleFor.elims(2))

lemma notIsPC_eqExLRL_roles_eq:
assumes s: "reach s" and s1: "reach s1" and PID: "PID ∈∈ paperIDs s cid"
and pc: "¬ isPC s cid uid"
and eq: "eqExcRLR (roles s cid uid) (roles (s1::state) cid uid)"
shows "roles s cid uid = roles s1 cid uid"
proof-
  have "¬ isPC s1 cid uid" using pc eqExcRLR_imp2[OF eq] by auto
  hence "¬ isRev s cid uid PID ∧ ¬ isRev s1 cid uid PID" using pc s s1 PID
  by (metis isRev_pref_notConflict_isPC)
  thus ?thesis using eq unfolding eqExcRLR_def
  by (metis Bex_set_list_ex filter_id_conv isRev_def)
qed

lemma foo1: "P a ⟹ [r←List.insert a l . P r] = (if a∈set l then filter P l else a#filter P l)"
  by (metis filter.simps(2) in_set_insert not_in_set_insert)

lemma foo2: "⟦eqExcRLR rl rl'; ¬ isRevRoleFor PID x⟧ ⟹ eqExcRLR (List.insert x rl) (List.insert x rl')"
  unfolding eqExcRLR_def
  apply (auto simp: foo1) []
  apply (metis eqExcRLR_def eqExcRLR_set isRevRoleFor.simps)+
  done

lemma foo3:
  assumes "eqExcRLR rl rl'" "isRevRoleFor PID x"
  shows "eqExcRLR (List.insert x rl) (rl')"
  and "eqExcRLR (rl) (List.insert x rl')"
  using assms
  unfolding eqExcRLR_def
  by (auto simp: List.insert_def)


text ‹The notion of two states being equal everywhere except on the reviewer roles for 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
 ∧
 (∀ cid uid. eqExcRLR (roles s cid uid) (roles s1 cid uid))
 ∧
 paperIDs s = paperIDs s1
 ∧
 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 eqExcRLR_sym unfolding eqExcPID_def by auto

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

(* 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
 ∧
 eqExcRLR (roles s cid uid) (roles s1 cid uid)
 ∧
 paperIDs s = paperIDs s1
 ∧
 paper s = paper s1
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1 ∧
 getAllPaperIDs s = getAllPaperIDs s1"
unfolding eqExcPID_def eqExcRLR_def getAllPaperIDs_def by auto

(* does not work well with simp: *)
lemma eqExcPID_imp':
assumes s: "reach s" and ss1: "eqExcPID s s1" and pid: "pid ≠ PID ∨ PID ≠ pid"
shows
"isRev s cid uid pid = isRev s1 cid uid pid ∧
 getRevRole s cid uid pid = getRevRole s1 cid uid pid ∧
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid"
proof-
  have 1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)"
  using eqExcPID_imp[OF ss1] by auto
  show ?thesis proof (intro conjI)
    show 3: "isRev s cid uid pid = isRev s1 cid uid pid"
    by (metis "1" eqExcRLR_imp pid s)
    show 4: "getRevRole s cid uid pid = getRevRole s1 cid uid pid"
    by (metis "1" eqExcRLR_imp pid s)
    show "getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid"
    unfolding getReviewIndex_def using 4 by auto
  qed
qed

lemma eqExcPID_imp1:
"eqExcPID s s1 ⟹ pid ≠ PID ∨ PID ≠ pid ⟹
    getNthReview s pid n = getNthReview s1 pid n"
unfolding eqExcPID_def getNthReview_def
by auto

lemma eqExcPID_imp2:
assumes "reach s" and "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 using assms by (auto simp add: eqExcPID_imp' eqExcPID_imp1)
  thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID_imp)
qed

lemma eqExcPID_imp3:
"reach s ⟹ eqExcPID s s1 ⟹ pid ≠ PID ∨ PID ≠ pid
 ⟹
 getNthReview s pid = getNthReview s1 pid"
unfolding eqExcPID_def apply auto
apply (rule ext) by (metis getNthReview_def)

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 ⟹ 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

text ‹A slightly weaker state equivalence that allows differences in the reviews of paper \<^term>‹PID›.
It is used for the confidentiality property that doesn't cover the authors of that paper in the
notification phase (when the authors will learn the contents of the reviews).›

(* Equality of two papers everywhere except on their reviews *)
fun eqExcR :: "paper ⇒ paper ⇒ bool" where
"eqExcR (Paper name info ct reviews dis decs)
        (Paper name1 info1 ct1 reviews1 dis1 decs1) =
 (name = name1 ∧ info = info1 ∧ ct = ct1 ∧ dis = dis1 ∧ decs = decs1)"

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

lemma eqExcR_eq[simp,intro!]: "eqExcR pap pap"
unfolding eqExcR by auto

lemma eqExcR_sym:
assumes "eqExcR pap pap1"
shows "eqExcR pap1 pap"
using assms unfolding eqExcR by auto

lemma eqExcR_trans:
assumes "eqExcR pap pap1" and "eqExcR pap1 pap2"
shows "eqExcR pap pap2"
using assms unfolding eqExcR by auto

(* Auxiliary notion:  *)
definition eeqExcPID where
"eeqExcPID paps paps1 ≡
 ∀ pid. if pid = PID then eqExcR (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 eqExcR_sym unfolding eeqExcPID_def by auto

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

lemma eeqExcPID_imp:
"eeqExcPID paps paps1 ⟹ eqExcR (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 ⟹ eqExcR 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) ∧
 disPaper (paps PID) = disPaper (paps1 PID) ∧
 decsPaper (paps PID) = decsPaper (paps1 PID)"
using eeqExcPID_def unfolding eqExcR by auto

(* The notion of two states being equal everywhere except on the the reviews of PID
   and on the reviewer roles for 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
 ∧
 (∀ cid uid. eqExcRLR (roles s cid uid) (roles s1 cid uid))
 ∧
 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 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 eeqExcPID_sym eqExcRLR_sym unfolding eqExcPID2_def by auto

lemma eqExcPID2_trans:
assumes "eqExcPID2 s s1" and "eqExcPID2 s1 s2" shows "eqExcPID2 s s2"
using assms eeqExcPID_trans eqExcRLR_trans unfolding eqExcPID2_def by metis

(* 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
 ∧
 eqExcRLR (roles s cid uid) (roles s1 cid uid)
 ∧
 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"
unfolding eqExcPID2_def eqExcRLR_def getAllPaperIDs_def by auto


lemma eeqExcPID_imp2:
assumes pid: "pid ≠ PID" and
1: "eeqExcPID (paper s) (paper s1)"
shows
"reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)"
by (metis "1" eeqExcPID_imp(2) pid)

(* does not work well with simp: *)
lemma eqExcPID2_imp':
assumes s: "reach s" and ss1: "eqExcPID2 s s1" and pid: "pid ≠ PID ∨ PID ≠ pid"
shows
"isRev s cid uid pid = isRev s1 cid uid pid ∧
 getRevRole s cid uid pid = getRevRole s1 cid uid pid ∧
 getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid ∧
 reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)"
proof-
  have 1: "eqExcRLR (roles s cid uid) (roles s1 cid uid)"
  and 2: "eeqExcPID (paper s) (paper s1)"
  using eqExcPID2_imp[OF ss1] by auto
  show ?thesis proof (intro conjI)
    show 3: "isRev s cid uid pid = isRev s1 cid uid pid"
    by (metis "1" eqExcRLR_imp pid s)
    show 4: "getRevRole s cid uid pid = getRevRole s1 cid uid pid"
    by (metis "1" eqExcRLR_imp pid s)
    show "getReviewIndex s cid uid pid = getReviewIndex s1 cid uid pid"
    unfolding getReviewIndex_def using 4 by auto
    show "reviewsPaper (paper s pid) = reviewsPaper (paper s1 pid)"
    using pid 2 unfolding eeqExcPID_def by auto
  qed
qed

lemma eqExcPID2_imp1:
"eqExcPID2 s s1 ⟹ eqExcR (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 eeqExcPID_def getNthReview_def
apply auto by (metis eqExcR_eq)

lemma eqExcPID2_imp2:
assumes "reach s" and "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 using assms by (auto simp add: eqExcPID2_imp' eqExcPID2_imp1)
  thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqExcPID2_imp)
qed

lemma eqExcPID2_imp3:
"reach s ⟹ eqExcPID2 s s1 ⟹ pid ≠ PID ∨ PID ≠ pid
 ⟹
 getNthReview s pid = getNthReview s1 pid"
unfolding eqExcPID2_def apply auto
apply (rule ext) by (metis eeqExcPID_imp getNthReview_def)

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) ∧
 disPaper (paper s PID) = disPaper (paper s1 PID) ∧
 decsPaper (paper s PID) = decsPaper (paper s1 PID)"
using eqExcPID2_imp eeqExcPID_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 ⟹ eeqExcPID 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 ∧ dis = dis1 ∧ decs = decs1"
using assms unfolding eqExcPID2_def apply (auto simp: eqExcR eeqExcPID_def)
by (metis titlePaper.simps abstractPaper.simps contentPaper.simps disPaper.simps decsPaper.simps)+


lemma cReview_step_eqExcPID2:
assumes a:
"a = Cact (cReview cid uid p PID uid')"
and "step s a = (ou,s')"
shows "eqExcPID2 s s'"
using assms unfolding eqExcPID2_def eeqExcPID_def eqExcRLR_def
apply (auto simp: c_defs)
unfolding List.insert_def by (smt (verit) filter.simps(2) isRevRoleFor.simps(1))


subsection ‹Value Setup›

type_synonym "value" = "userID × userID set"

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

fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans s (Cact (cReview cid uid p pid uid')) _ s') =
 (uid', {uid'. isPC s cid uid' ∧ pref s uid' PID ≠ Conflict})"

lemma φ_def2:
"φ (Trans s a ou s') =
 (ou = outOK ∧
 (∃ cid uid p uid'. a = Cact (cReview cid uid p PID uid')))"
apply(cases a, simp_all) subgoal for x1 by (cases x1, auto) .


fun χ :: "act ⇒ bool" where
"χ (Uact (uReview cid uid p pid n rc)) = (pid = PID)"
|
"χ (UUact (uuReview cid uid p pid n rc)) = (pid = PID)"
|
"χ _ = False"

lemma χ_def2:
"χ a =
 (∃ cid uid p n rc. a = Uact (uReview cid uid p PID n rc) ∨
                    a = UUact (uuReview cid uid p PID n rc))"
apply(cases a, simp_all)
  subgoal for x2 apply (cases x2, auto) .
  subgoal for x3 by (cases x3, auto) .

lemma eqExcPID_step_φ_imp:
assumes s: "reach s" and ss1: "eqExcPID s s1"
(* new compared to the other properties: *)
and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid > revPH"
(* end new *)
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 apply (auto simp add: c_defs eqExcPID_imp)
unfolding eqExcPID_def
apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2)
apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2)
using eqExcRLR_imp[OF s] PID by (metis less_not_refl paperIDs_equals)

lemma eqExcPID_step_φ:
assumes "reach s" and "reach s1" and ss1: "eqExcPID s s1"
(* new compared to the other properties: *)
and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid > revPH"
(* end new *)
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')"
proof-
  have "PID ∈∈ paperIDs s1 cid ∧ phase s1 cid > revPH"
  using eqExcPID_imp[OF ss1] PID ph by auto
  thus ?thesis by (metis eqExcPID_step_φ_imp eqExcPID_sym assms)
qed

(* new lemma compared to the other properties: *)
lemma non_eqExcPID_step_φ_imp:
assumes s: "reach s" and ss1: "eqExcPID s s1"
and PID: "PID ∈∈ paperIDs s cid" and ou: "ou ≠ outErr"
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: c_defs eqExcPID_imp)

(* major *) lemma eqExcPID_step:
assumes s: "reach s" and s1: "reach s1"
and ss1: "eqExcPID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and PID: "PID ∈∈ paperIDs s cid"
and ou_ph: "ou ≠ outErr ∨ phase s cid > revPH"
and φ: "¬ φ (Trans s a ou s')" and χ: "¬ χ a"
shows "eqExcPID s' s1'"
proof -
  have s': "reach s'" by (metis reach_PairI s step)
  note eqs = eqExcPID_imp[OF ss1]
  note eqs' = eqExcPID_imp1[OF ss1]

  note eqss = eqExcPID_imp'[OF s ss1]

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def
  note simps2[simp] = eqExcRLR_imp2[where s=s and ?s1.0 = s1'] eqExcRLR_imp2[where s=s' and ?s1.0 = s1]
       eqExcRLR_set[of "(roles s cid uid)" "(roles s1' cid uid)" for uid cid]
       eqExcRLR_set[of "(roles s' cid uid)" "(roles s1 cid uid)" for uid cid]
       foo2 foo3 eqExcRLR_imp[OF s, where ?s1.0=s1'] eqExcRLR_imp[OF s', where ?s1.0=s1]

  note * = step step1 eqs eqs' φ χ PID ou_ph

  then show ?thesis
  proof (cases a)
    case (Cact x1)
    with * show ?thesis
    proof (cases x1)
      case (cReview x81 x82 x83 x84 x85)
      with Cact * show ?thesis
        by clarsimp (metis less_irrefl_nat paperIDs_equals s1 simps2(9))
    qed auto
  next
    case (Uact x2)
    with * show ?thesis
    proof (cases x2)
      case (uReview x71 x72 x73 x74 x75 x76)
      with Uact * show ?thesis
        by (clarsimp simp del: simps2) auto
    qed auto
  next
    case (UUact x3)
    with * show ?thesis
    proof (cases x3)
      case (uuReview x31 x32 x33 x34 x35 x36)
      with UUact * show ?thesis
        by (clarsimp simp del: simps2) auto
    qed auto
  qed auto
qed


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

(* major *) lemma eqExcPID2_step:
assumes s: "reach s"
and ss1: "eqExcPID2 s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid ≥ revPH"
and φ: "¬ φ (Trans s a ou s')"
shows "eqExcPID2 s' s1'"
proof -
  have s': "reach s'" by (metis reach_PairI s step)
  note eqs = eqExcPID2_imp[OF ss1]
  (* note eqss = eqExcPID2_imp'[OF s ss1] *)
  note eqs' = eqExcPID2_imp1[OF ss1]

  note eqss = eqExcPID2_imp'[OF s ss1]

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs
          Paper_dest_conv
          eqExcPID2_def eeqExcPID_def
          eqExcR
  note simps2[simp] = eqExcRLR_imp2[where s=s and ?s1.0 = s1'] eqExcRLR_imp2[where s=s' and ?s1.0 = s1]
      eqExcRLR_set[of "(roles s cid uid)" "(roles s1' cid uid)" for cid uid]
      eqExcRLR_set[of "(roles s' cid uid)" "(roles s1 cid uid)" for cid uid]
      foo2 foo3 eqExcRLR_imp[OF s, where ?s1.0=s1'] eqExcRLR_imp[OF s', where ?s1.0=s1]
  note * = step step1 eqs eqs' ph PID φ

  then show ?thesis
  proof (cases a)
    case (Cact x1)
    with * show ?thesis
    proof (cases x1)
      case (cReview x81 x82 x83 x84 x85)
      with Cact * show ?thesis
        by clarsimp (metis simps2(9))
    qed auto
  next
    case (Uact x2)
    with * show ?thesis
    proof (cases x2)
      case (uReview x71 x72 x73 x74 x75 x76)
      with Uact * show ?thesis
        by (clarsimp simp del: simps2) auto
    qed auto
  next
    case (UUact x3)
    with * show ?thesis
    proof (cases x3)
      case (uuReview x31 x32 x33 x34 x35 x36)
      with UUact * show ?thesis
        by (clarsimp simp del: simps2) auto
    qed auto
  next
    case (Lact x5)
    with * show ?thesis by (cases x5; auto)
  qed auto
qed

lemma eqExcPID2_step_φ_imp:
assumes s: "reach s" and ss1: "eqExcPID2 s s1"
(* new compared to the other properties: *)
and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid > revPH"
(* end new *)
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 apply (auto simp add: c_defs eqExcPID2_imp)
unfolding eqExcPID2_def
apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2)
apply(metis eqExcRLR_imp[OF s] eqExcRLR_imp2)
using eqExcRLR_imp[OF s] PID by (metis less_not_refl paperIDs_equals)

lemma eqExcPID2_step_φ:
assumes "reach s" and "reach s1" and ss1: "eqExcPID2 s s1"
(* new compared to the other properties: *)
and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid > revPH"
(* end new *)
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')"
proof-
  have "PID ∈∈ paperIDs s1 cid ∧ phase s1 cid > revPH"
  using eqExcPID2_imp[OF ss1] PID ph by auto
  thus ?thesis by (metis eqExcPID2_step_φ_imp eqExcPID2_sym assms)
qed

(* new lemma compared to the other properties: *)
lemma non_eqExcPID2_step_φ_imp:
assumes s: "reach s" and ss1: "eqExcPID2 s s1"
and PID: "PID ∈∈ paperIDs s cid" and ou: "ou ≠ outErr"
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: c_defs eqExcPID2_imp)




end