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