Theory Paper_Value_Setup

(* The value setup for paper confidentiality *)
theory Paper_Value_Setup
imports Paper_Intro
begin

(* The observed values: *)
consts PID :: paperID

subsection‹Preliminaries›

declare updates_commute_paper[simp]

(* two papers equal everywhere but w.r.t. their content: *)
fun eqButC :: "paper ⇒ paper ⇒ bool" where
"eqButC (Paper name info ct reviews dis decs )
        (Paper name1 info1 ct1 reviews1 dis1 decs1) =
 (name = name1 ∧ info = info1 ∧ reviews = reviews1 ∧ dis = dis1 ∧ decs = decs1)"

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

lemma eqButC_eq[simp,intro!]: "eqButC pap pap"
by(cases pap) auto

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

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

(* Auxiliary notion: two functions are equal everywhere but on the NIC (content) of
   the value corresponding to PID *)
definition eeqButPID where
"eeqButPID paps paps1 ≡
 ∀ pid. if pid = PID then eqButC (paps pid) (paps1 pid) else paps pid = paps1 pid"

lemma eeqButPID_eeq[simp,intro!]: "eeqButPID s s"
unfolding eeqButPID_def by auto

lemma eeqButPID_sym:
assumes "eeqButPID s s1" shows "eeqButPID s1 s"
using assms eqButC_sym unfolding eeqButPID_def by auto

lemma eeqButPID_trans:
assumes "eeqButPID s s1" and "eeqButPID s1 s2" shows "eeqButPID s s2"
using assms eqButC_trans unfolding eeqButPID_def by simp blast

lemma eeqButPID_imp:
"eeqButPID paps paps1 ⟹ eqButC (paps PID) (paps1 PID)"
"⟦eeqButPID paps paps1; pid ≠ PID⟧ ⟹ paps pid = paps1 pid"
unfolding eeqButPID_def by auto

lemma eeqButPID_cong:
assumes "eeqButPID paps paps1"
and "pid = PID ⟹ eqButC uu uu1"
and "pid ≠ PID ⟹ uu = uu1"
shows "eeqButPID (paps (pid := uu)) (paps1(pid := uu1))"
using assms unfolding eeqButPID_def by auto

lemma eeqButPID_RDD:
"eeqButPID paps paps1 ⟹
 titlePaper (paps PID) = titlePaper (paps1 PID) ∧
 abstractPaper (paps PID) = abstractPaper (paps1 PID) ∧
 reviewsPaper (paps PID) = reviewsPaper (paps1 PID) ∧
 disPaper (paps PID) = disPaper (paps1 PID) ∧
 decsPaper (paps PID) = decsPaper (paps1 PID)"
using eeqButPID_def unfolding eqButC by auto

(* The notion of two states being equal everywhere but on the content of
   the paper associated to a given PID *)
definition eqButPID :: "state ⇒ state ⇒ bool" where
"eqButPID 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
 ∧
 eeqButPID (paper s) (paper s1)
 ∧
 pref s = pref s1 ∧
 voronkov s = voronkov s1 ∧
 news s = news s1 ∧ phase s = phase s1"

lemma eqButPID_eq[simp,intro!]: "eqButPID s s"
unfolding eqButPID_def by auto

lemma eqButPID_sym:
assumes "eqButPID s s1" shows "eqButPID s1 s"
using assms eeqButPID_sym unfolding eqButPID_def by auto

lemma eqButPID_trans:
assumes "eqButPID s s1" and "eqButPID s1 s2" shows "eqButPID s s2"
using assms eeqButPID_trans unfolding eqButPID_def by auto

(* Implications from eqButPID, including w.r.t. auxiliary operations: *)
lemma eqButPID_imp:
"eqButPID 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
 ∧
 eeqButPID (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 eqButPID_def getAllPaperIDs_def
unfolding isRev_def getReviewIndex_def getRevRole_def by auto

lemma eqButPID_imp1:
"eqButPID s s1 ⟹ eqButC (paper s pid) (paper s1 pid)"
"eqButPID s s1 ⟹ pid ≠ PID ∨ PID ≠ pid ⟹
    paper s pid = paper s1 pid ∧
    getNthReview s pid n = getNthReview s1 pid n"
unfolding eqButPID_def getNthReview_def eeqButPID_def
apply auto
by (metis eqButC_eq)

lemma eqButPID_imp2:
assumes "eqButPID 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: eqButPID_imp eqButPID_imp1)
  thus ?thesis unfolding getReviewersReviews_def using assms by (simp add: eqButPID_imp)
qed

lemma eqButPID_RDD:
"eqButPID s s1 ⟹
 titlePaper (paper s PID) = titlePaper (paper s1 PID) ∧
 abstractPaper (paper s PID) = abstractPaper (paper s1 PID) ∧
 reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) ∧
 disPaper (paper s PID) = disPaper (paper s1 PID) ∧
 decsPaper (paper s PID) = decsPaper (paper s1 PID)"
using eqButPID_imp eeqButPID_RDD by auto

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

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

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

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇pref := uu1⦈) (s1 ⦇pref := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇voronkov := uu1⦈) (s1 ⦇voronkov := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇news := uu1⦈) (s1 ⦇news := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇phase := uu1⦈) (s1 ⦇phase := uu2⦈)"

unfolding eqButPID_def by auto

lemma eqButPID_Paper:
assumes s's1': "eqButPID s s1"
and "paper s pid = Paper title abstract pc reviews dis decs"
and "paper s1 pid = Paper title1 abstract1 pc1 reviews1 dis1 decs1"
shows "title = title1 ∧ abstract = abstract1 ∧ reviews = reviews1 ∧ dis = dis1 ∧ decs = decs1"
using assms unfolding eqButPID_def apply (auto simp: eqButC eeqButPID_def)
by (metis titlePaper.simps abstractPaper.simps reviewsPaper.simps disPaper.simps decsPaper.simps)+

definition "NOSIMP a ≡ a"
lemma [cong]: "NOSIMP a = NOSIMP a" by simp

lemma eqButPID_paper:
  assumes "eqButPID s s1"
  shows "paper s = (paper s1)(PID :=
    Paper (titlePaper (paper s1 PID))
      (abstractPaper (paper s1 PID))
      (contentPaper (NOSIMP (paper s PID)))
      (reviewsPaper (paper s1 PID))
      (disPaper (paper s1 PID))
      (decsPaper (paper s1 PID))
    )"
  apply (rule sym)
  using assms unfolding NOSIMP_def eqButPID_def eeqButPID_def
  apply (intro ext)
  apply simp
  apply (cases "paper s1 PID", simp_all)
  apply (cases "paper s PID", simp_all)
  done

(* lemmas eqButPID_simps = eqButPID_simps1 eqButPID_simps2 eqButPID_paper *)
lemmas eqButPID_simps = eqButPID_imp eqButPID_paper


subsection‹Value Setup›

type_synonym "value" = pcontent

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

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

fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans _ (Uact (uPaperC cid uid p pid ct)) _ _) = ct"

lemma Uact_uPaperC_step_eqButPID:
assumes a: "a = Uact (uPaperC cid uid p PID ct)"
and "step s a = (ou,s')"
shows "eqButPID s s'"
using assms unfolding eqButPID_def eeqButPID_def by (auto simp: u_defs)

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

(* major *) lemma eqButPID_step:
assumes s's1': "eqButPID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
shows "eqButPID s' s1'"
proof -
  note eqs = eqButPID_imp[OF s's1']
  note eqs' = eqButPID_imp1[OF s's1']

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqButPID_def eeqButPID_def eqButC
  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 eqButPID_step_φ_imp:
assumes s's1': "eqButPID 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: u_defs eqButPID_imp)

lemma eqButPID_step_φ:
assumes s's1': "eqButPID 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 eqButPID_step_φ_imp eqButPID_sym assms)


end