Theory Outer_Friend

theory Outer_Friend
  imports Outer_Friend_Intro
begin


type_synonym obs = "act * out"

text ‹The observers ‹UIDs j› are an arbitrary, but fixed sets of users at each node ‹j› of the
network, and the secret is the friendship information of user ‹UID› at node ‹AID›.›

locale OuterFriend =
fixes UIDs :: "apiID ⇒ userID set"
and AID :: "apiID"
and UID :: "userID"
assumes UID_UIDs: "UID ∉ UIDs AID"
and emptyUserID_not_UIDs: "⋀aid. emptyUserID ∉ UIDs aid"

datatype "value" =
  isFrVal: FrVal apiID userID bool ― ‹updates to the friendship status of UID›
| isOVal: OVal bool ― ‹a change in the ``openness" status of the UID friendship info›

end