Theory Discussion_Value_Setup

theory Discussion_Value_Setup
imports Discussion_Intro
begin

text ‹The ID of the paper under scrutiny:›

consts PID :: paperID

subsection ‹Preliminaries›

declare updates_commute_paper[simp]

(* two papers equal everywhere except w.r.t. discussion: *)
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 ∧ decs = decs1)"

lemma eqExcD:
"eqExcD pap pap1 =
 (titlePaper pap = titlePaper pap1 ∧ abstractPaper pap = abstractPaper pap1 ∧
  contentPaper pap = contentPaper pap1 ∧
  reviewsPaper pap = reviewsPaper pap1 ∧ decsPaper pap = decsPaper 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) ∧
 decsPaper (paps PID) = decsPaper (paps1 PID)"
using eeqExcPID_def unfolding eqExcD by auto

(* The notion of two states being equal everywhere but on the discussion 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) ∧
 decsPaper (paper s PID) = decsPaper (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 ∧ decs = decs1 "
using assms unfolding eqExcPID_def apply (auto simp: eqExcD eeqExcPID_def)
by (metis titlePaper.simps abstractPaper.simps contentPaper.simps reviewsPaper.simps decsPaper.simps
         )+


subsection ‹Value Setup›

type_synonym "value" = string

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

lemma φ_def2:
"φ (Trans s a ou s') = (∃ cid uid p com. a = UUact (uuDis cid uid p PID com) ∧ 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 (uuDis cid uid p pid com)) _ _) = com"

lemma UUact_uuDis_step_eqExcPID:
assumes a: "a = UUact (uuDis cid uid p PID com)"
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_uuDis_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)


end