Theory Post_Unwinding_Helper_ISSUER

theory Post_Unwinding_Helper_ISSUER
  imports Post_Observation_Setup_ISSUER
begin

locale Issuer_State_Equivalence_Up_To_PID = Fixed_PID
begin

subsubsection ‹Unwinding helper lemmas and definitions›

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

lemmas eeqButPID_intro = eeqButPID_def[THEN meta_eq_to_obj_eq, THEN iffD2]

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

lemma eeqButPID_sym:
assumes "eeqButPID psts psts1" shows "eeqButPID psts1 psts"
using assms unfolding eeqButPID_def by auto

lemma eeqButPID_trans:
assumes "eeqButPID psts psts1" and "eeqButPID psts1 psts2" shows "eeqButPID psts psts2"
using assms unfolding eeqButPID_def by (auto split: if_splits)

lemma eeqButPID_cong:
assumes "eeqButPID psts psts1"
and "pid = PID ⟹ eqButT uu uu1"
and "pid ≠ PID ⟹ uu = uu1"
shows "eeqButPID (psts (pid := uu)) (psts1(pid := uu1))"
using assms unfolding eeqButPID_def by (auto split: if_splits)

(*
lemma eeqButPID_eqButT:
"eeqButPID psts psts1 ⟹ eqButT (psts PID) (psts1 PID)"
unfolding eeqButPID_def by (auto split: if_splits)
*)

lemma eeqButPID_not_PID:
"⟦eeqButPID psts psts1; pid ≠ PID⟧ ⟹ psts pid = psts1 pid"
unfolding eeqButPID_def by (auto split: if_splits)

(*
lemma eeqButPID_postSelectors:
"eeqButPID psts psts1 ⟹
 titlePost (psts pid) = titlePost (psts1 pid) ∧
 imgPost (psts pid) = imgPost (psts1 pid) ∧
 visPost (psts pid) = visPost (psts1 pid)"
unfolding eeqButPID_def by (metis eqButT.simps)
*)

lemma eeqButPID_toEq:
assumes "eeqButPID psts psts1"
shows "psts (PID := pid) =
       psts1 (PID := pid)"
using eeqButPID_not_PID[OF assms] by auto

lemma eeqButPID_update_post:
assumes "eeqButPID psts psts1"
shows "eeqButPID (psts (pid := pst)) (psts1 (pid := pst))"
using eeqButPID_not_PID[OF assms]
using assms unfolding eeqButPID_def by auto


(* lists two pairs (apiID, boolean flag) are equal save for the boolean flag: *)
fun eqButF :: "(apiID × bool) list ⇒ (apiID × bool) list ⇒ bool" where
"eqButF aID_bl aID_bl1 = (map fst aID_bl = map fst aID_bl1)"

lemma eqButF_eq[simp,intro!]: "eqButF aID_bl aID_bl"
by auto

lemma eqButF_sym:
assumes "eqButF aID_bl aID_bl1"
shows "eqButF aID_bl1 aID_bl"
using assms by auto

lemma eqButF_trans:
assumes "eqButF aID_bl aID_bl1" and "eqButF aID_bl1 aID_bl2"
shows "eqButF aID_bl aID_bl2"
using assms by auto

lemma eqButF_insert2:
"eqButF aID_bl aID_bl1 ⟹
 eqButF (insert2 aID b aID_bl) (insert2 aID b aID_bl1)"
unfolding insert2_def
by simp (smt map_eq_conv o_apply o_id prod.collapse prod.sel(1) split_conv)


(* Auxiliary notion: two functions are equal everywhere but on the second component of NIC of
   the value corresponding to PID, which is a list of pairs *)
definition eeqButPID_F where
"eeqButPID_F sw sw1 ≡
 ∀ pid. if pid = PID then eqButF (sw PID) (sw1 PID) else sw pid = sw1 pid"

lemmas eeqButPID_F_intro = eeqButPID_F_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eeqButPID_F_eeq[simp,intro!]: "eeqButPID_F sw sw"
unfolding eeqButPID_F_def by auto

lemma eeqButPID_F_sym:
assumes "eeqButPID_F sw sw1" shows "eeqButPID_F sw1 sw"
using assms eqButF_sym unfolding eeqButPID_F_def
by presburger

lemma eeqButPID_F_trans:
assumes "eeqButPID_F sw sw1" and "eeqButPID_F sw1 sw2" shows "eeqButPID_F sw sw2"
using assms unfolding eeqButPID_F_def by (auto split: if_splits)

lemma eeqButPID_F_cong:
assumes "eeqButPID_F sw sw1"
and "PID = PID ⟹ eqButF uu uu1"
and "pid ≠ PID ⟹ uu = uu1"
shows "eeqButPID_F (sw (pid := uu)) (sw1(pid := uu1))"
using assms unfolding eeqButPID_F_def by (auto split: if_splits)

lemma eeqButPID_F_eqButF:
"eeqButPID_F sw sw1 ⟹ eqButF (sw PID) (sw1 PID)"
unfolding eeqButPID_F_def by (auto split: if_splits)

lemma eeqButPID_F_not_PID:
"⟦eeqButPID_F sw sw1; pid ≠ PID⟧ ⟹ sw pid = sw1 pid"
unfolding eeqButPID_F_def by (auto split: if_splits)

lemma eeqButPID_F_postSelectors:
"eeqButPID_F sw sw1 ⟹ map fst (sw pid) = map fst (sw1 pid)"
unfolding eeqButPID_F_def by (metis eqButF.simps)

lemma eeqButPID_F_insert2:
"eeqButPID_F sw sw1 ⟹
 eqButF (insert2 aID b (sw PID)) (insert2 aID b (sw1 PID))"
unfolding eeqButPID_F_def using eqButF_insert2 by metis

lemma eeqButPID_F_toEq:
assumes "eeqButPID_F sw sw1"
shows "sw (PID := map (λ (aID,_). (aID,b)) (sw PID)) =
       sw1 (PID := map (λ (aID,_). (aID,b)) (sw1 PID))"
using length_map eeqButPID_F_eqButF[OF assms] eeqButPID_F_not_PID[OF assms]
apply(auto simp: o_def split_def map_replicate_const intro!: map_prod_cong ext)
by (metis length_map)

lemma eeqButPID_F_updateShared:
assumes "eeqButPID_F sw sw1"
shows "eeqButPID_F (sw (pid := aID_b)) (sw1 (pid := aID_b))"
using eeqButPID_F_eqButF[OF assms] eeqButPID_F_not_PID[OF assms]
using assms unfolding eeqButPID_F_def by auto


(* The notion of two states being equal everywhere but on the content of
   the post associated to a given PID and the update status of the PID shareWith info: *)
definition eqButPID :: "state ⇒ state ⇒ bool" where
"eqButPID s s1 ≡
 admin s = admin s1 ∧

 pendingUReqs s = pendingUReqs s1 ∧ userReq s = userReq s1 ∧
 userIDs s = userIDs s1 ∧ user s = user s1 ∧ pass s = pass s1 ∧

 pendingFReqs s = pendingFReqs s1 ∧ friendReq s = friendReq s1 ∧ friendIDs s = friendIDs s1 ∧
 sentOuterFriendIDs s = sentOuterFriendIDs s1 ∧ recvOuterFriendIDs s = recvOuterFriendIDs s1 ∧

 postIDs s = postIDs s1 ∧ admin s = admin s1 ∧
 eeqButPID (post s) (post s1) ∧
 owner s = owner s1 ∧
 vis s = vis s1 ∧

 pendingSApiReqs s = pendingSApiReqs s1 ∧ sApiReq s = sApiReq s1 ∧
 serverApiIDs s = serverApiIDs s1 ∧ serverPass s = serverPass s1 ∧
 outerPostIDs s = outerPostIDs s1 ∧ outerPost s = outerPost s1 ∧
 outerOwner s = outerOwner s1 ∧
 outerVis s = outerVis s1 ∧

 pendingCApiReqs s = pendingCApiReqs s1 ∧ cApiReq s = cApiReq s1 ∧
 clientApiIDs s = clientApiIDs s1 ∧ clientPass s = clientPass s1 ∧
 eeqButPID_F (sharedWith s) (sharedWith s1)"

lemmas eqButPID_intro = eqButPID_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButPID_refl[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 eeqButPID_F_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 eeqButPID_F_trans unfolding eqButPID_def
by simp blast

(* Implications from eqButPID, including w.r.t. auxiliary operations: *)
lemma eqButPID_stateSelectors:
"eqButPID s s1 ⟹
 admin s = admin s1 ∧

 pendingUReqs s = pendingUReqs s1 ∧ userReq s = userReq s1 ∧
 userIDs s = userIDs s1 ∧ user s = user s1 ∧ pass s = pass s1 ∧

 pendingFReqs s = pendingFReqs s1 ∧ friendReq s = friendReq s1 ∧ friendIDs s = friendIDs s1 ∧
 sentOuterFriendIDs s = sentOuterFriendIDs s1 ∧ recvOuterFriendIDs s = recvOuterFriendIDs s1 ∧

 postIDs s = postIDs s1 ∧ admin s = admin s1 ∧
 eeqButPID (post s) (post s1) ∧
 owner s = owner s1 ∧
 vis s = vis s1 ∧

 pendingSApiReqs s = pendingSApiReqs s1 ∧ sApiReq s = sApiReq s1 ∧
 serverApiIDs s = serverApiIDs s1 ∧ serverPass s = serverPass s1 ∧
 outerPostIDs s = outerPostIDs s1 ∧ outerPost s = outerPost s1 ∧
 outerOwner s = outerOwner s1 ∧
 outerVis s = outerVis s1 ∧

 pendingCApiReqs s = pendingCApiReqs s1 ∧ cApiReq s = cApiReq s1 ∧
 clientApiIDs s = clientApiIDs s1 ∧ clientPass s = clientPass s1 ∧
 eeqButPID_F (sharedWith s) (sharedWith s1) ∧

 IDsOK s = IDsOK s1"
unfolding eqButPID_def IDsOK_def[abs_def] by auto

(* lemma eqButPID_eqButT:
"eqButPID s s1 ⟹ eqButT (post s PID) (post s1 PID)"
unfolding eqButPID_def using eeqButPID_eqButT by auto *)

lemma eqButPID_not_PID:
"eqButPID s s1 ⟹ pid ≠ PID ⟹ post s pid = post s1 pid"
unfolding eqButPID_def using eeqButPID_not_PID by auto

lemma eqButPID_eqButF:
"eqButPID s s1 ⟹ eqButF (sharedWith s PID) (sharedWith s1 PID)"
unfolding eqButPID_def using eeqButPID_F_eqButF by auto

lemma eqButPID_not_PID_sharedWith:
"eqButPID s s1 ⟹ pid ≠ PID ⟹ sharedWith s pid = sharedWith s1 pid"
unfolding eqButPID_def using eeqButPID_F_not_PID by auto

(* lemma eqButPID_imp0:
assumes "eqButPID s s1" and 1: "pid ≠ PID"
shows "post s pid = post s1 pid"
proof-
  have "eeqButPID (post s) (post s1)"
  using assms using eqButPID_imp by simp
  from eeqButPID_imp(2)[OF this] 1 show ?thesis by auto
qed *)

(*
lemma eqButPID_postSelectors:
assumes "eqButPID s s1"
shows "titlePost (post s pid) = titlePost (post s1 pid) ∧
       imgPost (post s pid) = imgPost (post s1 pid) ∧
       visPost (post s pid) = visPost (post s1 pid)"
using assms unfolding eqButPID_def using eeqButPID_postSelectors by auto
*)

lemma eqButPID_insert2:
"eqButPID s s1 ⟹
 eqButF (insert2 aID b (sharedWith s PID)) (insert2 aID b (sharedWith s1 PID))"
unfolding eqButPID_def using eeqButPID_F_insert2 by metis

lemma eqButPID_actions:
assumes "eqButPID s s1"
shows "listInnerPosts s uid p = listInnerPosts s1 uid p"
using eqButPID_stateSelectors[OF assms] (* eqButPID_postSelectors[OF assms *)
by (auto simp: l_defs intro!: arg_cong2[of _ _ _ _ cmap])

(*
lemma eqButPID_setTextPost:
assumes "eqButPID s s1"
shows "setTextPost (post s PID) pst =
       setTextPost (post s1 PID) pst"
using assms unfolding eqButPID_def using eeqButPID_toEq
by (meson fun_upd_eqD)
*)

lemma eqButPID_update:
assumes "eqButPID s s1"
shows "(post s)(PID := txt) = (post s1)(PID := txt)"
using assms unfolding eqButPID_def using eeqButPID_toEq by auto

lemma eqButPID_update_post:
assumes "eqButPID s s1"
shows "eeqButPID ((post s) (pid := pst)) ((post s1) (pid := pst))"
using assms unfolding eqButPID_def using eeqButPID_update_post by auto

lemma eqButPID_setShared:
assumes "eqButPID s s1"
shows "(sharedWith s) (PID := map (λ (aID,_). (aID,b)) (sharedWith s PID)) =
       (sharedWith s1) (PID := map (λ (aID,_). (aID,b)) (sharedWith s1 PID))"
using assms unfolding eqButPID_def using eeqButPID_F_toEq by auto

lemma eqButPID_updateShared:
assumes "eqButPID s s1"
shows "eeqButPID_F ((sharedWith s) (pid := aID_b)) ((sharedWith s1) (pid := aID_b))"
using assms unfolding eqButPID_def using eeqButPID_F_updateShared by auto


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

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

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇postIDs := uu1⦈) (s1 ⦇postIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ eeqButPID uu1 uu2 ⟹ eqButPID (s ⦇post := uu1⦈) (s1 ⦇post := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇owner := uu1⦈) (s1 ⦇owner := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇vis := uu1⦈) (s1 ⦇vis := uu2⦈)"

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇pendingFReqs := uu1⦈) (s1 ⦇pendingFReqs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇friendReq := uu1⦈) (s1 ⦇friendReq := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇friendIDs := uu1⦈) (s1 ⦇friendIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇sentOuterFriendIDs := uu1⦈) (s1 ⦇sentOuterFriendIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇recvOuterFriendIDs := uu1⦈) (s1 ⦇recvOuterFriendIDs := uu2⦈)"

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇pendingSApiReqs := uu1⦈) (s1 ⦇pendingSApiReqs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇sApiReq := uu1⦈) (s1 ⦇sApiReq := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇serverApiIDs := uu1⦈) (s1 ⦇serverApiIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇serverPass := uu1⦈) (s1 ⦇serverPass := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerPostIDs := uu1⦈) (s1 ⦇outerPostIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerPost := uu1⦈) (s1 ⦇outerPost := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerOwner := uu1⦈) (s1 ⦇outerOwner := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerVis := uu1⦈) (s1 ⦇outerVis := uu2⦈)"

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇pendingCApiReqs := uu1⦈) (s1 ⦇pendingCApiReqs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇cApiReq := uu1⦈) (s1 ⦇cApiReq := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇clientApiIDs := uu1⦈) (s1 ⦇clientApiIDs := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇clientPass := uu1⦈) (s1 ⦇clientPass := uu2⦈)"

"⋀ uu1 uu2. eqButPID s s1 ⟹ eeqButPID_F uu1 uu2 ⟹ eqButPID (s ⦇sharedWith := uu1⦈) (s1 ⦇sharedWith:= uu2⦈)"
unfolding eqButPID_def by auto


(* major *) lemma eqButPID_step:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
shows "eqButPID s' s1'"
proof -
  note [simp] = all_defs eeqButPID_F_def
  note [intro!] = eqButPID_cong
  note * = step step1 ss1 eqButPID_stateSelectors[OF ss1]
           eqButPID_update[OF ss1] eqButPID_update_post[OF ss1]
           eqButPID_setShared[OF ss1] eqButPID_updateShared[OF ss1]
           eqButPID_insert2[OF ss1]
  then show ?thesis
  proof (cases a)
    case (Sact x1)
    with * show ?thesis by (cases x1) auto
  next
    case (Cact x2)
    with * show ?thesis by (cases x2) auto
  next
    case (Dact x3)
    with * show ?thesis by (cases x3) auto
  next
    case (Uact x4)
    with * show ?thesis
    proof (cases x4)
      case (uPost x21 x22 x23 x24)
      with Uact * show ?thesis by (cases "x23 = PID") auto
    next
      case (uVisPost x31 x32 x33 x34)
      with Uact * show ?thesis by (cases "x33 = PID") auto
    qed auto
  next
    case (COMact x7)
    with * show ?thesis
    proof (cases x7)
      case (comSendPost x61 x62 x63 x64)
      with COMact * show ?thesis by (cases "x64 = PID") auto
    qed auto
  qed auto
qed

end

end