Quelle  SPRView.thy

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

subsection‹The Synchronous Perfect-Recall View›

text‹

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

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

  it maintains a list of all observations made on the trace,
  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‹

  corresponding incremental view appends a new observation to the
  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‹

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

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

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

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

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

 ›

(*<*)
end
(*>*)