Theory SPRView

(*<*)
theory SPRView
imports
  KBPsAuto
begin
(*>*)

subsection‹The Synchronous Perfect-Recall View›

text‹

\label{sec:kbps-theory-pr-view}

The synchronous perfect-recall (SPR) view records all observations the
agent has made on a given trace. This is the canonical
full-information synchronous view; all others are functions of this
one.

Intuitively it maintains a list of all observations made on the trace,
with the length of the list recording the time:

›

definition (in Environment) spr_jview :: "('a, 's, 'obs Trace) JointView" where
  "spr_jview a = tMap (envObs a)"
(*<*)

context Environment
begin

lemma spr_jview_length_eq:
  "tLength (spr_jview a t) = tLength t"
  by (simp add: spr_jview_def)

lemma spr_jview_tInit_inv[simp]:
  "spr_jview a t = tInit obs ⟷ (∃s. t = tInit s ∧ envObs a s = obs)"
  by (cases t) (simp_all add: spr_jview_def)

lemma spr_jview_tStep_eq_inv:
  "spr_jview a t' = spr_jview a (t ↝ s) ⟹ ∃t'' s'. t' = t'' ↝ s'"
  by (cases t') (simp_all add: spr_jview_def)

lemma spr_jview_prefix_closed[dest]:
  "spr_jview a (t ↝ s) = spr_jview a (t' ↝ s') ⟹ spr_jview a t = spr_jview a t'"
  by (simp add: spr_jview_def)

end

(*>*)
text‹

The corresponding incremental view appends a new observation to the
existing ones:

›

definition (in Environment) spr_jviewInit :: "'a ⇒ 'obs ⇒ 'obs Trace" where
  "spr_jviewInit ≡ λa obs. tInit obs"

definition (in Environment)
  spr_jviewIncr :: "'a ⇒ 'obs ⇒ 'obs Trace ⇒ 'obs Trace"
where
  "spr_jviewIncr ≡ λa obs' tobs. tobs ↝ obs'"

sublocale Environment
        < SPR: IncrEnvironment jkbp envInit envAction envTrans envVal
                spr_jview envObs spr_jviewInit spr_jviewIncr
(*<*)
proof
  { fix a t t' assume "spr_jview a t = spr_jview a t'"
    hence "tLength t = tLength t'"
      using spr_jview_length_eq[where a=a, symmetric] by simp }
  thus "∀a t t'. spr_jview a t = spr_jview a t' ⟶ tLength t = tLength t'"
    by blast
next
  show "∀a s. spr_jviewInit a (envObs a s) = spr_jview a (tInit s)"
    unfolding spr_jviewInit_def by (simp add: spr_jview_def)
next
  show "∀a t s. spr_jview a (t ↝ s) = spr_jviewIncr a (envObs a s) (spr_jview a t)"
    unfolding spr_jviewIncr_def by (simp add: spr_jview_def)
qed

(* These need to follow the locale instantiation as we appeal to
sync. *)

lemma (in Environment) spr_tFirst[dest]:
  assumes v: "spr_jview a t = spr_jview a t'"
  shows "envObs a (tFirst t) = envObs a (tFirst t')"
  using SPR.sync[rule_format, OF v] v
  apply (induct rule: trace_induct2)
  apply (simp_all add: spr_jview_def)
  done

lemma (in Environment) spr_tLast[dest]:
  assumes v: "spr_jview a t = spr_jview a t'"
  shows "envObs a (tLast t) = envObs a (tLast t')"
  using SPR.sync[rule_format, OF v] v
  apply (induct rule: trace_induct2)
  apply (simp_all add: spr_jview_def)
  done

(*>*)

text‹

\<^citet>‹‹Theorem~5› in "Ron:1996"› showed that it is not the case that
finite-state implementations always exist with respect to the SPR
view, and so we consider three special cases:
\begin{itemize}

\item[\S\ref{sec:kbps-spr-single-agent}] where there is a single
agent;

\item[\S\ref{sec:kbps-theory-spr-deterministic-protocols}] when the
protocols of the agents are deterministic and communication is by
broadcast; and

\item[\S\ref{sec:kbps-theory-spr-non-deterministic-protocols}] when
the agents use non-deterministic protocols and again use broadcast to
communicate.

\end{itemize}
Note that these cases do overlap but none is wholly
contained in another.

›

(*<*)
end
(*>*)