(* 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