Theory Friend_State_Indistinguishability

(* The state equivalence used for the unwinding proofs for the friendship confidentiality
   properties *)
theory Friend_State_Indistinguishability
  imports "Friend_Observation_Setup"
begin

subsection ‹Unwinding helper definitions and lemmas›

(* The secret: One will be interested in the friendship information of two arbitary,
   but fixed users UID1 and UID2 *)
locale Friend = FriendObservationSetup +
fixes
  UID1 :: userID
and
  UID2 :: userID
assumes
  UID1_UID2_UIDs: "{UID1,UID2} ∩ UIDs = {}"
and
  UID1_UID2: "UID1 ≠ UID2"
begin

(* The notion of two userID lists being equal save for at most one occurrence of uid: *)
fun eqButUIDl :: "userID ⇒ userID list ⇒ userID list ⇒ bool" where
"eqButUIDl uid uidl uidl1 = (remove1 uid uidl = remove1 uid uidl1)"

lemma eqButUIDl_eq[simp,intro!]: "eqButUIDl uid uidl uidl"
by auto

lemma eqButUIDl_sym:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid uidl1 uidl"
using assms by auto

lemma eqButUIDl_trans:
assumes "eqButUIDl uid uidl uidl1" and "eqButUIDl uid uidl1 uidl2"
shows "eqButUIDl uid uidl uidl2"
using assms by auto

lemma eqButUIDl_remove1_cong:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)"
proof -
  have "remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)" by (simp add: remove1_commute)
  also have "… = remove1 uid' (remove1 uid uidl1)" using assms by simp
  also have "… = remove1 uid (remove1 uid' uidl1)" by (simp add: remove1_commute)
  finally show ?thesis by simp
qed

lemma eqButUIDl_snoc_cong:
assumes "eqButUIDl uid uidl uidl1"
and "uid' ∈∈ uidl ⟷ uid' ∈∈ uidl1"
shows "eqButUIDl uid (uidl ## uid') (uidl1 ## uid')"
using assms by (auto simp add: remove1_append remove1_idem)

(* The notion of two functions each taking a userID and returning a list of user IDs
  being equal everywhere but on UID1 and UID2, where their return results are allowed
  to be eqButUIDl : *)
definition eqButUIDf where
"eqButUIDf frds frds1 ≡
  eqButUIDl UID2 (frds UID1) (frds1 UID1)
∧ eqButUIDl UID1 (frds UID2) (frds1 UID2)
∧ (∀uid. uid ≠ UID1 ∧ uid ≠ UID2 ⟶ frds uid = frds1 uid)"

lemmas eqButUIDf_intro = eqButUIDf_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUIDf_eeq[simp,intro!]: "eqButUIDf frds frds"
unfolding eqButUIDf_def by auto

lemma eqButUIDf_sym:
assumes "eqButUIDf frds frds1" shows "eqButUIDf frds1 frds"
using assms eqButUIDl_sym unfolding eqButUIDf_def
by presburger

lemma eqButUIDf_trans:
assumes "eqButUIDf frds frds1" and "eqButUIDf frds1 frds2"
shows "eqButUIDf frds frds2"
using assms eqButUIDl_trans unfolding eqButUIDf_def by (auto split: if_splits)

lemma eqButUIDf_cong:
assumes "eqButUIDf frds frds1"
and "uid = UID1 ⟹ eqButUIDl UID2 uu uu1"
and "uid = UID2 ⟹ eqButUIDl UID1 uu uu1"
and "uid ≠ UID1 ⟹ uid ≠ UID2 ⟹ uu = uu1"
shows "eqButUIDf (frds (uid := uu)) (frds1(uid := uu1))"
using assms unfolding eqButUIDf_def by (auto split: if_splits)

lemma eqButUIDf_eqButUIDl:
assumes "eqButUIDf frds frds1"
shows "eqButUIDl UID2 (frds UID1) (frds1 UID1)"
  and "eqButUIDl UID1 (frds UID2) (frds1 UID2)"
using assms unfolding eqButUIDf_def by (auto split: if_splits)

lemma eqButUIDf_not_UID:
"⟦eqButUIDf frds frds1; uid ≠ UID1; uid ≠ UID2⟧ ⟹ frds uid = frds1 uid"
unfolding eqButUIDf_def by (auto split: if_splits)

lemma eqButUIDf_not_UID':
assumes eq1: "eqButUIDf frds frds1"
and uid: "(uid,uid') ∉ {(UID1,UID2), (UID2,UID1)}"
shows "uid ∈∈ frds uid' ⟷ uid ∈∈ frds1 uid'"
proof -
  from uid have "(uid' = UID1 ∧ uid ≠ UID2)
               ∨ (uid' = UID2 ∧ uid ≠ UID1)
               ∨ (uid' ∉ {UID1,UID2})" (is "?u1 ∨ ?u2 ∨ ?n12")
    by auto
  then show ?thesis proof (elim disjE)
    assume "?u1"
    moreover then have "uid ∈∈ remove1 UID2 (frds uid') ⟷ uid ∈∈ remove1 UID2 (frds1 uid')"
      using eq1 unfolding eqButUIDf_def by auto
    ultimately show ?thesis by auto
  next
    assume "?u2"
    moreover then have "uid ∈∈ remove1 UID1 (frds uid') ⟷ uid ∈∈ remove1 UID1 (frds1 uid')"
      using eq1 unfolding eqButUIDf_def by auto
    ultimately show ?thesis by auto
  next
    assume "?n12"
    then show ?thesis using eq1 unfolding eqButUIDf_def by auto
  qed
qed

(* The notion of two functions each taking two userID arguments being
  equal everywhere but on the values (UID1,UID2) and (UID2,UID1): *)
definition eqButUID12 where
"eqButUID12 freq freq1 ≡
 ∀ uid uid'. if (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)} then True else freq uid uid' = freq1 uid uid'"

lemmas eqButUID12_intro = eqButUID12_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUID12_eeq[simp,intro!]: "eqButUID12 freq freq"
unfolding eqButUID12_def by auto

lemma eqButUID12_sym:
assumes "eqButUID12 freq freq1" shows "eqButUID12 freq1 freq"
using assms unfolding eqButUID12_def
by presburger

lemma eqButUID12_trans:
assumes "eqButUID12 freq freq1" and "eqButUID12 freq1 freq2"
shows "eqButUID12 freq freq2"
using assms unfolding eqButUID12_def by (auto split: if_splits)

lemma eqButUID12_cong:
assumes "eqButUID12 freq freq1"
(*and "uid = UID1 ⟹ eqButUID2 uu uu1"*)
and "¬ (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)} ⟹ uu = uu1"
shows "eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)"
using assms unfolding eqButUID12_def fun_upd2_def by (auto split: if_splits)

lemma eqButUID12_not_UID:
"⟦eqButUID12 freq freq1; ¬ (uid,uid') ∈ {(UID1,UID2), (UID2,UID1)}⟧ ⟹ freq uid uid' = freq1 uid uid'"
unfolding eqButUID12_def by (auto split: if_splits)


(* The notion of two states being equal everywhere but on the friendship requests or status of users UID1 and UID2: *)
definition eqButUID :: "state ⇒ state ⇒ bool" where
"eqButUID 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 ∧

 eqButUIDf (pendingFReqs s) (pendingFReqs s1) ∧
 eqButUID12 (friendReq s) (friendReq s1) ∧
 eqButUIDf (friendIDs s) (friendIDs s1) ∧

 postIDs s = postIDs s1 ∧ admin s = admin s1 ∧
 post s = post s1 ∧ vis s = vis s1 ∧
 owner s = owner 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 ∧ outerVis s = outerVis s1 ∧
 outerOwner s = outerOwner s1 ∧
 sentOuterFriendIDs s = sentOuterFriendIDs s1 ∧
 recvOuterFriendIDs s = recvOuterFriendIDs s1 ∧

 pendingCApiReqs s = pendingCApiReqs s1 ∧ cApiReq s = cApiReq s1 ∧
 clientApiIDs s = clientApiIDs s1 ∧ clientPass s = clientPass s1 ∧
 sharedWith s = sharedWith s1"

lemmas eqButUID_intro = eqButUID_def[THEN meta_eq_to_obj_eq, THEN iffD2]

lemma eqButUID_refl[simp,intro!]: "eqButUID s s"
unfolding eqButUID_def by auto

lemma eqButUID_sym[sym]:
assumes "eqButUID s s1" shows "eqButUID s1 s"
using assms eqButUIDf_sym eqButUID12_sym unfolding eqButUID_def by auto

lemma eqButUID_trans[trans]:
assumes "eqButUID s s1" and "eqButUID s1 s2" shows "eqButUID s s2"
using assms eqButUIDf_trans eqButUID12_trans unfolding eqButUID_def by metis

(* Implications from eqButUID, including w.r.t. auxiliary operations: *)
lemma eqButUID_stateSelectors:
assumes "eqButUID s s1"
shows "admin s = admin s1"
"pendingUReqs s = pendingUReqs s1" "userReq s = userReq s1"
"userIDs s = userIDs s1" "user s = user s1" "pass s = pass s1"
"eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
"eqButUID12 (friendReq s) (friendReq s1)"
"eqButUIDf (friendIDs s) (friendIDs s1)"

"postIDs s = postIDs s1"
"post s = post s1" "vis s = vis s1"
"owner s = owner 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" "outerVis s = outerVis s1"
"outerOwner s = outerOwner s1"
"sentOuterFriendIDs s = sentOuterFriendIDs s1"
"recvOuterFriendIDs s = recvOuterFriendIDs 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"
using assms unfolding eqButUID_def IDsOK_def[abs_def] by auto

lemma eqButUID_eqButUID2:
"eqButUID s s1 ⟹ eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)"
unfolding eqButUID_def using eqButUIDf_eqButUIDl
by (smt eqButUIDf_eqButUIDl eqButUIDl.simps)

lemma eqButUID_not_UID:
"eqButUID s s1 ⟹ uid ≠ UID ⟹ post s uid = post s1 uid"
unfolding eqButUID_def by auto


lemma eqButUID_cong[simp, intro]:
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇admin := uu1⦈) (s1 ⦇admin := uu2⦈)"

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

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

"⋀ uu1 uu2. eqButUID s s1 ⟹ eqButUIDf uu1 uu2 ⟹ eqButUID (s ⦇pendingFReqs := uu1⦈) (s1 ⦇pendingFReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ eqButUID12 uu1 uu2 ⟹ eqButUID (s ⦇friendReq := uu1⦈) (s1 ⦇friendReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ eqButUIDf uu1 uu2 ⟹ eqButUID (s ⦇friendIDs := uu1⦈) (s1 ⦇friendIDs := uu2⦈)"

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

"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇pendingCApiReqs := uu1⦈) (s1 ⦇pendingCApiReqs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇cApiReq := uu1⦈) (s1 ⦇cApiReq := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇clientApiIDs := uu1⦈) (s1 ⦇clientApiIDs := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇clientPass := uu1⦈) (s1 ⦇clientPass := uu2⦈)"
"⋀ uu1 uu2. eqButUID s s1 ⟹ uu1 = uu2 ⟹ eqButUID (s ⦇sharedWith := uu1⦈) (s1 ⦇sharedWith:= uu2⦈)"
unfolding eqButUID_def by auto

definition "friends12" :: "state ⇒ bool"
where "friends12 s ≡ UID1 ∈∈ friendIDs s UID2 ∧ UID2 ∈∈ friendIDs s UID1"

lemma step_friendIDs:
assumes "step s a = (ou, s')"
and "a ≠ Cact (cFriend uid (pass s uid) uid') ∧ a ≠ Cact (cFriend uid' (pass s uid') uid) ∧
     a ≠ Dact (dFriend uid (pass s uid) uid') ∧ a ≠ Dact (dFriend uid' (pass s uid') uid)"
shows "uid ∈∈ friendIDs s' uid' ⟷ uid ∈∈ friendIDs s uid'" (is ?uid)
  and "uid' ∈∈ friendIDs s' uid ⟷ uid' ∈∈ friendIDs s uid" (is ?uid')
proof -
  from assms have "?uid ∧ ?uid'"
  proof (cases a)
    case (Sact sa) then show ?thesis using assms by (cases sa) (auto simp: s_defs) next
    case (Uact ua) then show ?thesis using assms by (cases ua) (auto simp: u_defs) next
    case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: com_defs) next
    case (Cact ca) then show ?thesis using assms by (cases ca) (auto simp: c_defs) next
    case (Dact da) then show ?thesis using assms by (cases da) (auto simp: d_defs)
  qed auto
  then show ?uid and ?uid' by auto
qed

lemma step_friends12:
assumes "step s a = (ou, s')"
and "a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧ a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
     a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧ a ≠ Dact (dFriend UID2 (pass s UID2) UID1)"
shows "friends12 s' ⟷ friends12 s"
using step_friendIDs[OF assms] unfolding friends12_def by auto

lemma step_pendingFReqs:
assumes step: "step s a = (ou, s')"
and "∀req. a ≠ Cact (cFriend uid (pass s uid) uid') ∧ a ≠ Cact (cFriend uid' (pass s uid') uid) ∧
           a ≠ Dact (dFriend uid (pass s uid) uid') ∧ a ≠ Dact (dFriend uid' (pass s uid') uid) ∧
           a ≠ Cact (cFriendReq uid (pass s uid) uid' req) ∧
           a ≠ Cact (cFriendReq uid' (pass s uid') uid req)"
shows "uid ∈∈ pendingFReqs s' uid' ⟷ uid ∈∈ pendingFReqs s uid'" (is ?uid)
  and "uid' ∈∈ pendingFReqs s' uid ⟷ uid' ∈∈ pendingFReqs s uid" (is ?uid')
proof -
  from assms have "?uid ∧ ?uid'"
  proof (cases a)
    case (Sact sa) then show ?thesis using assms by (cases sa) (auto simp: s_defs) next
    case (Uact ua) then show ?thesis using assms by (cases ua) (auto simp: u_defs) next
    case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: com_defs) next
    case (Cact ca) then show ?thesis using assms proof (cases ca)
      case (cFriend uid1 p uid1')
        then have "((uid1 = uid ⟶ uid1' ≠ uid') ∧ (uid1 = uid' ⟶ uid1' ≠ uid)) ∨ ou = outErr"
          using Cact assms by (auto simp: c_defs)
        then show ?thesis using step Cact cFriend by (auto simp: c_defs)
    qed (auto simp: c_defs) next
    case (Dact da) then show ?thesis using assms by (cases da) (auto simp: d_defs)
  qed auto
  then show ?uid and ?uid' by auto
qed

lemma eqButUID_friends12_set_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and f12: "friends12 s = friends12 s1"
and rs: "reach s" and rs1: "reach s1"
shows "set (friendIDs s uid) = set (friendIDs s1 uid)"
proof -
  have dfIDs: "distinct (friendIDs s uid)" "distinct (friendIDs s1 uid)"
    using reach_distinct_friends_reqs[OF rs] reach_distinct_friends_reqs[OF rs1] by auto
  from f12 have uid12: "UID1 ∈∈ friendIDs s UID2 ⟷ UID1 ∈∈ friendIDs s1 UID2"
                       "UID2 ∈∈ friendIDs s UID1 ⟷ UID2 ∈∈ friendIDs s1 UID1"
    using reach_friendIDs_symmetric[OF rs] reach_friendIDs_symmetric[OF rs1]
    unfolding friends12_def by auto
  from ss1 have fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)" unfolding eqButUID_def by simp
  show "set (friendIDs s uid) = set (friendIDs s1 uid)"
  proof (intro equalityI subsetI)
    fix uid'
    assume "uid' ∈∈ friendIDs s uid"
    then show "uid' ∈∈ friendIDs s1 uid"
      using fIDs dfIDs uid12 eqButUIDf_not_UID' unfolding eqButUIDf_def
      by (metis (no_types, lifting) insert_iff prod.inject singletonD)
  next
    fix uid'
    assume "uid' ∈∈ friendIDs s1 uid"
    then show "uid' ∈∈ friendIDs s uid"
      using fIDs dfIDs uid12 eqButUIDf_not_UID' unfolding eqButUIDf_def
      by (metis (no_types, lifting) insert_iff prod.inject singletonD)
  qed
qed


lemma distinct_remove1_idem: "distinct xs ⟹ remove1 y (remove1 y xs) = remove1 y xs"
by (induction xs) (auto simp add: remove1_idem)

lemma Cact_cFriend_step_eqButUID:
assumes step: "step s (Cact (cFriend uid p uid')) = (ou,s')"
and s: "reach s"
and uids: "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)" (is "?u12 ∨ ?u21")
shows "eqButUID s s'"
using assms proof (cases)
  assume ou: "ou = outOK"
  then have "uid' ∈∈ pendingFReqs s uid" using step by (auto simp add: c_defs)
  then have fIDs: "uid' ∉ set (friendIDs s uid)" "uid ∉ set (friendIDs s uid')"
        and fRs: "distinct (pendingFReqs s uid)" "distinct (pendingFReqs s uid')"
    using reach_distinct_friends_reqs[OF s] by auto
  have "eqButUIDf (friendIDs s) (friendIDs (createFriend s uid p uid'))"
    using fIDs uids UID1_UID2 unfolding eqButUIDf_def
    by (cases "?u12") (auto simp add: c_defs remove1_idem remove1_append)
  moreover have "eqButUIDf (pendingFReqs s) (pendingFReqs (createFriend s uid p uid'))"
    using fRs uids UID1_UID2 unfolding eqButUIDf_def
    by (cases "?u12") (auto simp add: c_defs distinct_remove1_idem)
  moreover have "eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))"
    using uids unfolding eqButUID12_def
    by (auto simp add: c_defs fun_upd2_eq_but_a_b)
  ultimately show "eqButUID s s'" using step ou unfolding eqButUID_def by (auto simp add: c_defs)
qed (auto)

lemma Cact_cFriendReq_step_eqButUID:
assumes step: "step s (Cact (cFriendReq uid p uid' req)) = (ou,s')"
and uids: "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)" (is "?u12 ∨ ?u21")
shows "eqButUID s s'"
using assms proof (cases)
  assume ou: "ou = outOK"
  then have "uid ∉ set (pendingFReqs s uid')" "uid ∉ set (friendIDs s uid')"
    using step by (auto simp add: c_defs)
  then have "eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))"
    using uids UID1_UID2 unfolding eqButUIDf_def
    by (cases "?u12") (auto simp add: c_defs remove1_idem remove1_append)
  moreover have "eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))"
    using uids unfolding eqButUID12_def
    by (auto simp add: c_defs fun_upd2_eq_but_a_b)
  ultimately show "eqButUID s s'" using step ou unfolding eqButUID_def by (auto simp add: c_defs)
qed (auto)


lemma Dact_dFriend_step_eqButUID:
assumes step: "step s (Dact (dFriend uid p uid')) = (ou,s')"
and s: "reach s"
and uids: "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)" (is "?u12 ∨ ?u21")
shows "eqButUID s s'"
using assms proof (cases)
  assume ou: "ou = outOK"
  then have "uid' ∈∈ friendIDs s uid" using step by (auto simp add: d_defs)
  then have fRs: "distinct (friendIDs s uid)" "distinct (friendIDs s uid')"
    using reach_distinct_friends_reqs[OF s] by auto
  have "eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))"
    using fRs uids UID1_UID2 unfolding eqButUIDf_def
    by (cases "?u12") (auto simp add: d_defs remove1_idem distinct_remove1_removeAll)
  then show "eqButUID s s'" using step ou unfolding eqButUID_def by (auto simp add: d_defs)
qed (auto)


(* major *) lemma eqButUID_step:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and rs: "reach s"
and rs1: "reach s1"
shows "eqButUID s' s1'"
proof -
  note simps = eqButUID_stateSelectors s_defs c_defs u_defs r_defs l_defs com_defs
  from assms show ?thesis proof (cases a)
    case (Sact sa) with assms show ?thesis by (cases sa) (auto simp add: simps)
  next
    case (Cact ca) note a = this
      with assms show ?thesis proof (cases ca)
        case (cFriendReq uid p uid' req) note ca = this
          then show ?thesis
          proof (cases "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)")
            case True
              then have "eqButUID s s'" and "eqButUID s1 s1'"
                using step step1 unfolding a ca
                by (auto intro: Cact_cFriendReq_step_eqButUID)
              with ss1 show "eqButUID s' s1'" by (auto intro: eqButUID_sym eqButUID_trans)
          next
            case False
              have fRs: "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
               and fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)" using ss1 by (auto simp: simps)
              then have uid_uid': "uid ∈∈ pendingFReqs s uid' ⟷ uid ∈∈ pendingFReqs s1 uid'"
                                  "uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'"
                using False by (auto intro!: eqButUIDf_not_UID')
              have "eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid))
                              ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))"
                using fRs False
                by (intro eqButUIDf_cong) (auto simp add: remove1_append remove1_idem eqButUIDf_def)
              moreover have "eqButUID12 (fun_upd2 (friendReq s) uid uid' req)
                                        (fun_upd2 (friendReq s1) uid uid' req)"
                using ss1 by (intro eqButUID12_cong) (auto simp: simps)
              moreover have "e_createFriendReq s uid p uid' req
                         ⟷ e_createFriendReq s1 uid p uid' req"
                using uid_uid' ss1 by (auto simp: simps)
              ultimately show ?thesis using assms unfolding a ca by (auto simp: simps)
          qed
      next
        case (cFriend uid p uid') note ca = this
          then show ?thesis
          proof (cases "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)")
            case True
              then have "eqButUID s s'" and "eqButUID s1 s1'"
                using step step1 rs rs1 unfolding a ca
                by (auto intro!: Cact_cFriend_step_eqButUID)+
              with ss1 show "eqButUID s' s1'" by (auto intro: eqButUID_sym eqButUID_trans)
          next
            case False
              have fRs: "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
                    (is "eqButUIDf (?pfr s) (?pfr s1)")
               and fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)" using ss1 by (auto simp: simps)
              then have uid_uid': "uid ∈∈ pendingFReqs s uid' ⟷ uid ∈∈ pendingFReqs s1 uid'"
                                  "uid' ∈∈ pendingFReqs s uid ⟷ uid' ∈∈ pendingFReqs s1 uid"
                                  "uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'"
                                  "uid' ∈∈ friendIDs s uid ⟷ uid' ∈∈ friendIDs s1 uid"
                using False by (auto intro!: eqButUIDf_not_UID')
              have "eqButUIDl UID1 (remove1 uid' (?pfr s UID2)) (remove1 uid' (?pfr s1 UID2))"
               and "eqButUIDl UID2 (remove1 uid' (?pfr s UID1)) (remove1 uid' (?pfr s1 UID1))"
               and "eqButUIDl UID1 (remove1 uid (?pfr s UID2)) (remove1 uid (?pfr s1 UID2))"
               and "eqButUIDl UID2 (remove1 uid (?pfr s UID1)) (remove1 uid (?pfr s1 UID1))"
               using fRs unfolding eqButUIDf_def
               by (auto intro!: eqButUIDl_remove1_cong simp del: eqButUIDl.simps)
              then have 1: "eqButUIDf ((?pfr s)(uid := remove1 uid' (?pfr s uid),
                                                uid' := remove1 uid (?pfr s uid')))
                                     ((?pfr s1)(uid := remove1 uid' (?pfr s1 uid),
                                                uid' := remove1 uid (?pfr s1 uid')))"
                using fRs False
                by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
              have "uid = UID1 ⟹ eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')"
               and "uid = UID2 ⟹ eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')"
               and "uid' = UID1 ⟹ eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)"
               and "uid' = UID2 ⟹ eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)"
                using fIDs uid_uid' by - (intro eqButUIDl_snoc_cong; simp add: eqButUIDf_def)+
              then have 2: "eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid',
                                                      uid' := friendIDs s uid' ## uid))
                                       ((friendIDs s1)(uid := friendIDs s1 uid ## uid',
                                                       uid' := friendIDs s1 uid' ## uid))"
                using fIDs by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
              have 3: "eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo)
                                                                    uid uid' emptyRequestInfo)
                                  (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo)
                                                                     uid uid' emptyRequestInfo)"
                using ss1 by (intro eqButUID12_cong) (auto simp: simps)
              have "e_createFriend s uid p uid'
                ⟷ e_createFriend s1 uid p uid'"
                using uid_uid' ss1 by (auto simp: simps)
              with 1 2 3 show ?thesis using assms unfolding a ca by (auto simp: simps)
          qed
      qed (auto simp: simps)
  next
    case (Uact ua) with assms show ?thesis by (cases ua) (auto simp add: simps)
  next
    case (Ract ra) with assms show ?thesis by (cases ra) (auto simp add: simps)
  next
    case (Lact la) with assms show ?thesis by (cases la) (auto simp add: simps)
  next
    case (COMact ca) with assms show ?thesis by (cases ca) (auto simp add: simps)
  next
    case (Dact da) note a = this
      with assms show ?thesis proof (cases da)
        case (dFriend uid p uid') note ca = this
          then show ?thesis
          proof (cases "(uid = UID1 ∧ uid' = UID2) ∨ (uid = UID2 ∧ uid' = UID1)")
            case True
              then have "eqButUID s s'" and "eqButUID s1 s1'"
                using step step1 rs rs1 unfolding a ca
                by (auto intro!: Dact_dFriend_step_eqButUID)+
              with ss1 show "eqButUID s' s1'" by (auto intro: eqButUID_sym eqButUID_trans)
          next
            case False
              have fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)" using ss1 by (auto simp: simps)
              then have uid_uid': "uid ∈∈ friendIDs s uid' ⟷ uid ∈∈ friendIDs s1 uid'"
                                  "uid' ∈∈ friendIDs s uid ⟷ uid' ∈∈ friendIDs s1 uid"
                using False by (auto intro!: eqButUIDf_not_UID')
              have dfIDs: "distinct (friendIDs s uid)" "distinct (friendIDs s uid')"
                          "distinct (friendIDs s1 uid)" "distinct (friendIDs s1 uid')"
                using reach_distinct_friends_reqs[OF rs] reach_distinct_friends_reqs[OF rs1] by auto
              have "uid = UID1 ⟹ eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))"
               and "uid = UID2 ⟹ eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))"
               and "uid' = UID1 ⟹ eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))"
               and "uid' = UID2 ⟹ eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))"
                using fIDs uid_uid' by - (intro eqButUIDl_remove1_cong; simp add: eqButUIDf_def)+
              then have 1: "eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid),
                                                      uid' := remove1 uid (friendIDs s uid')))
                                       ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid),
                                                       uid' := remove1 uid (friendIDs s1 uid')))"
                using fIDs by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
              have "e_deleteFriend s uid p uid'
                ⟷ e_deleteFriend s1 uid p uid'"
                using uid_uid' ss1 by (auto simp: simps d_defs)
              with 1 show ?thesis using assms dfIDs unfolding a ca
                by (auto simp: simps d_defs distinct_remove1_removeAll)
          qed
      qed
  qed
qed

lemma eqButUID_step_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "a ≠ Cact (cFriend UID1 (pass s UID1) UID2) ∧ a ≠ Cact (cFriend UID2 (pass s UID2) UID1) ∧
        a ≠ Dact (dFriend UID1 (pass s UID1) UID2) ∧ a ≠ Dact (dFriend UID2 (pass s UID2) UID1)"
and "friendIDs s = friendIDs s1"
shows "friendIDs s' = friendIDs s1'"
using assms proof (cases a)
  case (Sact sa) then show ?thesis using assms by (cases sa) (auto simp: s_defs) next
  case (Uact ua) then show ?thesis using assms by (cases ua) (auto simp: u_defs) next
  case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: com_defs) next
  case (Dact da) then show ?thesis using assms proof (cases da)
    case (dFriend uid p uid')
      with Dact assms show ?thesis
        by (cases "(uid,uid') ∈ {(UID1,UID2), (UID2,UID1)}")
           (auto simp: d_defs eqButUID_stateSelectors eqButUIDf_not_UID')
    qed
next
  case (Cact ca) then show ?thesis using assms proof (cases ca)
    case (cFriend uid p uid')
      { assume "p = pass s uid"
        then have "uid' ∈∈ pendingFReqs s uid ⟷ uid' ∈∈ pendingFReqs s1 uid"
          using Cact cFriend ss1 a by (intro eqButUIDf_not_UID') (auto simp: eqButUID_stateSelectors)
      }
      with Cact cFriend assms show ?thesis
        by (auto simp: c_defs eqButUID_stateSelectors)
    qed (auto simp: c_defs)
qed auto

lemma createFriend_sym: "createFriend s uid p uid' = createFriend s uid' p' uid"
unfolding c_defs by (cases "uid = uid'") (auto simp: fun_upd2_comm fun_upd_twist)

lemma deleteFriend_sym: "deleteFriend s uid p uid' = deleteFriend s uid' p' uid"
unfolding d_defs by (cases "uid = uid'") (auto simp: fun_upd_twist)

lemma createFriendReq_createFriend_absorb:
assumes "e_createFriendReq s uid' p uid req"
shows "createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'"
using assms unfolding c_defs by (auto simp: remove1_idem remove1_append fun_upd2_absorb)

lemma eqButUID_deleteFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
shows "friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)"
proof -
  have "distinct (friendIDs s UID1)" "distinct (friendIDs s UID2)"
       "distinct (friendIDs s1 UID1)" "distinct (friendIDs s1 UID2)"
    using rs rs1 by (auto intro: reach_distinct_friends_reqs)
  then show ?thesis
    using ss1 unfolding eqButUID_def eqButUIDf_def unfolding d_defs
    by (auto simp: distinct_remove1_removeAll)
qed

lemma eqButUID_createFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and f12: "¬friends12 s" "¬friends12 s1"
shows "friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)"
proof -
  have f12': "UID1 ∉ set (friendIDs s UID2)" "UID2 ∉ set (friendIDs s UID1)"
             "UID1 ∉ set (friendIDs s1 UID2)" "UID2 ∉ set (friendIDs s1 UID1)"
    using f12 rs rs1 reach_friendIDs_symmetric unfolding friends12_def by auto
  have "friendIDs s = friendIDs s1"
  proof (intro ext)
    fix uid
    show "friendIDs s uid = friendIDs s1 uid"
      using ss1 f12' unfolding eqButUID_def eqButUIDf_def
      by (cases "uid = UID1 ∨ uid = UID2") (auto simp: remove1_idem)
  qed
  then show ?thesis by (auto simp: c_defs)
qed

end

end