Theory Post_Unwinding_Helper_RECEIVER

theory Post_Unwinding_Helper_RECEIVER
  imports Post_Observation_Setup_RECEIVER
begin

subsubsection ‹Unwinding helper definitions and lemmas›

locale Receiver_State_Equivalence_Up_To_PID = Fixed_PID + Fixed_AID
begin

(* Auxiliary notion: two functions are equal everywhere but on the content of
   the value corresponding to PID *)
definition eeqButPID where
"eeqButPID psts psts1 ≡
 ∀ aid pid. if aid = AID ∧ pid = PID then True
                                     else psts aid pid = psts1 aid 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 "aid = AID ⟹ pid = PID ⟹ eqButT uu uu1"
and "aid ≠ AID ∨ pid ≠ PID ⟹ uu = uu1"
shows "eeqButPID (fun_upd2 psts aid pid uu) (fun_upd2 psts1 aid pid uu1)"
using assms unfolding eeqButPID_def fun_upd2_def by (auto split: if_splits)

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

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

lemma eeqButPID_toEq:
assumes "eeqButPID psts psts1"
shows "fun_upd2 psts AID PID pst =
       fun_upd2 psts1 AID PID pst"
using eeqButPID_not_PID[OF assms]
unfolding fun_upd2_def by (auto split: if_splits intro!: ext)

lemma eeqButPID_update_post:
assumes "eeqButPID psts psts1"
shows "eeqButPID (fun_upd2 psts aid pid pst) (fun_upd2 psts1 aid pid pst)"
using eeqButPID_not_PID[OF assms]
unfolding fun_upd2_def
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 comp_apply fst_conv map_eq_conv split_def)


(* 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 ∧
 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 ∧
 eeqButPID (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 ∧
 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 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 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 ∧
 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 ∧
 eeqButPID (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 ∧
 sharedWith s = sharedWith s1 ∧

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

lemma eqButPID_not_PID:
"eqButPID s s1 ⟹ aid ≠ AID ∨ pid ≠ PID ⟹ outerPost s aid pid = outerPost s1 aid pid"
unfolding eqButPID_def using eeqButPID_not_PID by auto

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

lemma eqButPID_update:
assumes "eqButPID s s1"
shows "fun_upd2 (outerPost s) AID PID pst = fun_upd2 (outerPost s1) AID PID pst"
using assms unfolding eqButPID_def using eeqButPID_toEq by (metis fun_upd2_absorb)

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

lemma eqButPID_cong[simp, intro]:
"⋀ 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 ⟹ 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 ⟹ eeqButPID uu1 uu2 ⟹ eqButPID (s ⦇outerPost := uu1⦈) (s1 ⦇outerPost := uu2⦈)"
"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerVis := uu1⦈) (s1 ⦇outerVis := uu2⦈)"

"⋀ uu1 uu2. eqButPID s s1 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇outerOwner := uu1⦈) (s1 ⦇outerOwner := 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 ⟹ uu1 = uu2 ⟹ eqButPID (s ⦇sharedWith := uu1⦈) (s1 ⦇sharedWith:= uu2⦈)"
unfolding eqButPID_def by auto


(* major *) lemma comReceivePost_step_eqButPID:
assumes a: "a = COMact (comReceivePost AID sp PID pst uid vs)"
and a1: "a1 = COMact (comReceivePost AID sp PID pst1 uid vs)"
and "step s a = (ou,s')" and "step s1 a1 = (ou1,s1')"
and "eqButPID s s1"
shows "eqButPID s' s1'"
using assms unfolding eqButPID_def eeqButPID_def
unfolding a a1 by (fastforce simp: com_defs fun_upd2_def)

(* 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
  note * = step step1 ss1 eqButPID_stateSelectors[OF ss1] eqButPID_update_post[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 by (cases x4) auto
  next
    case (COMact x7)
    with * show ?thesis by (cases x7) auto
  qed auto
qed

end

end