Theory SPRViewDet
theory SPRViewDet
imports
SPRView
KBPsAlg
Eval
List_local
ODList Trie2
"Transitive-Closure.Transitive_Closure_List_Impl"
"HOL-Library.Mapping"
begin
subsection‹Perfect Recall in Deterministic Broadcast Environments›
text‹
\label{sec:kbps-theory-spr-deterministic-protocols}
It is well known that simultaneous broadcast has the effect of making
information \emph{common knowledge}; roughly put, the agents all learn
the same things at the same time as the system evolves, so the
relation amongst the agents' states of knowledge never becomes more
complex than it is in the initial state
\<^citep>‹‹Chapter~6› in "FHMV:1995"›. For this reason we might hope to find
finite-state implementations of JKBPs in broadcast environments.
The broadcast assumption by itself is insufficient in general, however
\<^citep>‹‹\S7› in "Ron:1996"›, and so we need to further constrain the
scenario. Here we require that for each canonical trace the JKBP
prescribes at most one action. In practice this constraint is easier
to verify than the circularity would suggest; we return to this point
at the end of this section.
›
text_raw‹
\begin{figure}[tb]
\begin{isabellebody}%
›
record (overloaded) ('a, 'es, 'ps) BEState =
es :: "'es"
ps :: "('a × 'ps) odlist"
locale FiniteDetBroadcastEnvironment =
Environment jkbp envInit envAction envTrans envVal envObs
for jkbp :: "'a ⇒ ('a :: {finite,linorder}, 'p, 'aAct) KBP"
and envInit
:: "('a, 'es :: {finite,linorder}, 'as :: {finite,linorder}) BEState list"
and envAction :: "('a, 'es, 'as) BEState ⇒ 'eAct list"
and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct)
⇒ ('a, 'es, 'as) BEState ⇒ ('a, 'es, 'as) BEState"
and envVal :: "('a, 'es, 'as) BEState ⇒ 'p ⇒ bool"
and envObs :: "'a ⇒ ('a, 'es, 'as) BEState ⇒ ('cobs × 'as option)"
+ fixes agents :: "'a odlist"
fixes envObsC :: "'es ⇒ 'cobs"
defines "envObs a s ≡ (envObsC (es s), ODList.lookup (ps s) a)"
assumes agents: "ODList.toSet agents = UNIV"
assumes envTrans: "∀s s' a eact eact' aact aact'.
ODList.lookup (ps s) a = ODList.lookup (ps s') a ∧ aact a = aact' a
⟶ ODList.lookup (ps (envTrans eact aact s)) a
= ODList.lookup (ps (envTrans eact' aact' s')) a"
assumes jkbpDet: "∀a. ∀t ∈ SPR.jkbpC. length (jAction SPR.MC t a) ≤ 1"
text_raw‹
\end{isabellebody}%
\caption{Finite broadcast environments with a deterministic JKBP.}
\label{fig:kbps-theory-det-broadcast-envs}
\end{figure}
›
instantiation BEState_ext :: (linorder, linorder, linorder, linorder) linorder
begin
definition less_eq_BEState_ext
where "x ≤ y ≡ es x < es y ∨ (es x = es y ∧ (ps x < ps y ∨ (ps x = ps y ∧ more x ≤ more y)))"
definition less_BEState_ext
where "x < y ≡ es x < es y ∨ (es x = es y ∧ (ps x < ps y ∨ (ps x = ps y ∧ more x < more y)))"
instance
apply intro_classes
apply (unfold less_eq_BEState_ext_def less_BEState_ext_def)
apply auto
done
end
instance BEState_ext :: ("{finite, linorder}", finite, "{finite, linorder}", finite) finite
proof
let ?U = "UNIV :: ('a, 'b, 'c, 'd) BEState_ext set"
{ fix x :: "('a, 'b, 'c, 'd) BEState_scheme"
have "∃a b c. x = BEState_ext a b c"
by (cases x) simp
} then have U:
"?U = (λ((a, b), c). BEState_ext a b c) ` ((UNIV × UNIV) × UNIV)"
by (auto simp add: Set.image_def)
show "finite ?U" by (simp add: U)
qed
text‹
We encode our expectations of the scenario in the @{term
"FiniteBroadcastEnvironment"} locale of
Figure~\ref{fig:kbps-theory-det-broadcast-envs}. The broadcast is
modelled by having all agents make the same common observation of the
shared state of type @{typ "'es"}. We also allow each agent to
maintain a private state of type @{typ "'ps"}; that other agents
cannot influence it or directly observe it is enforced by the
constraint ‹envTrans› and the definition of @{term "envObs"}.
We do however allow the environment's protocol to be non-deterministic
and a function of the entire system state, including private states.
›
context FiniteDetBroadcastEnvironment
begin
lemma envObs_def_raw:
"envObs a = (λs. (envObsC (es s), ODList.lookup (ps s) a))"
apply (rule ext)+
apply (simp add: envObs_def)
done
text‹
We seek a suitable simulation space by considering what determines an
agent's knowledge. Intuitively any set of traces that is relevant to
the agents' states of knowledge with respect to @{term "t ∈ jkbpC"}
need include only those with the same common observation as @{term
"t"}:
›
definition tObsC :: "('a, 'es, 'as) BEState Trace ⇒ 'cobs Trace" where
"tObsC ≡ tMap (envObsC ∘ es)"
text‹
Clearly this is an abstraction of the SPR jview of the given trace.
›
lemma spr_jview_tObsC:
assumes "spr_jview a t = spr_jview a t'"
shows "tObsC t = tObsC t'"
using SPR.sync[rule_format, OF assms] assms
by (induct rule: trace_induct2) (auto simp: envObs_def tObsC_def)
lemma tObsC_tLength:
"tObsC t = tObsC t' ⟹ tLength t = tLength t'"
unfolding tObsC_def by (rule tMap_eq_imp_tLength_eq)
lemma tObsC_tStep_eq_inv:
"tObsC t' = tObsC (t ↝ s) ⟹ ∃t'' s'. t' = t'' ↝ s'"
unfolding tObsC_def by auto
lemma tObsC_prefix_closed[dest]:
"tObsC (t ↝ s) = tObsC (t' ↝ s') ⟹ tObsC t = tObsC t'"
unfolding tObsC_def by simp
lemma tObsC_tLast[iff]:
"tLast (tObsC t) = envObsC (es (tLast t))"
unfolding tObsC_def by simp
lemma tObsC_initial[iff]:
"tFirst (tObsC t) = envObsC (es (tFirst t))"
"tObsC (tInit s) = tInit (envObsC (es s))"
"tObsC t = tInit cobs ⟷ (∃s. t = tInit s ∧ envObsC (es s) = cobs)"
unfolding tObsC_def by simp_all
lemma spr_tObsC_trc_aux:
assumes "(t, t') ∈ (⋃a. relations SPR.MC a)⇧*"
shows "tObsC t = tObsC t'"
using assms
apply (induct)
apply simp
apply clarsimp
apply (rule_tac a=x in spr_jview_tObsC)
apply simp
done
lemma spr_jview_tObsC_trans:
"⟦spr_jview a t = spr_jview a t'; spr_jview a' t' = spr_jview a' t''⟧
⟹ tObsC t = tObsC t''"
by (fastforce dest: spr_jview_tObsC)
text‹
Unlike the single-agent case of \S\ref{sec:kbps-spr-single-agent}, it
is not sufficient for a simulation to record only the final states; we
need to relate the initial private states of the agents with the final
states they consider possible, as the initial states may contain
information that is not common knowledge. This motivates the following
abstraction:
›
definition
tObsC_abs :: "('a, 'es, 'as) BEState Trace ⇒ ('a, 'es, 'as) BEState Relation"
where
"tObsC_abs t ≡ { (tFirst t', tLast t')
|t'. t' ∈ SPR.jkbpC ∧ tObsC t' = tObsC t}"
lemma tObsC_abs_jview_eq[dest]:
"spr_jview a t' = spr_jview a t
⟹ tObsC_abs t = tObsC_abs t'"
unfolding tObsC_abs_def by (fastforce dest: spr_jview_tObsC)
lemma tObsC_abs_tObsC_eq[dest]:
"tObsC t' = tObsC t
⟹ tObsC_abs t = tObsC_abs t'"
unfolding tObsC_abs_def by (fastforce dest: spr_jview_tObsC)
lemma spr_jview_tObsCI:
assumes tt': "tObsC t = tObsC t'"
and first: "envObs a (tFirst t) = envObs a (tFirst t')"
and "tMap (λs. ODList.lookup (ps s) a) t = tMap (λs. ODList.lookup (ps s) a) t'"
shows "spr_jview a t = spr_jview a t'"
using tObsC_tLength[OF tt'] assms
by (induct rule: trace_induct2, auto iff: tObsC_def envObs_def spr_jview_def)
lemma tObsC_absI[intro]:
"⟦ t' ∈ SPR.jkbpC; tObsC t' = tObsC t; u = tFirst t'; v = tLast t' ⟧
⟹ (u, v) ∈ tObsC_abs t"
unfolding tObsC_abs_def by blast
lemma tObsC_abs_conv:
"(u, v) ∈ tObsC_abs t
⟷ (∃t'. t' ∈ SPR.jkbpC ∧ tObsC t' = tObsC t ∧ u = tFirst t' ∧ v = tLast t')"
unfolding tObsC_abs_def by blast
lemma tObsC_abs_tLast[simp]:
"(u, v) ∈ tObsC_abs t ⟹ envObsC (es v) = envObsC (es (tLast t))"
unfolding tObsC_abs_def tObsC_def
by (auto iff: o_def elim: tMap_tLast_inv)
lemma tObsC_abs_tInit[iff]:
"tObsC_abs (tInit s)
= { (s', s') |s'. s' ∈ set envInit ∧ envObsC (es s') = envObsC (es s) }"
unfolding tObsC_abs_def
apply auto
apply (rule_tac x="tInit s'" in exI)
apply simp
done
text‹›
end
text‹
We use the following record to represent the worlds of the simulated
Kripke structure:
›
record (overloaded) ('a, 'es, 'as) spr_simWorld =
sprFst :: "('a, 'es, 'as) BEState"
sprLst :: "('a, 'es, 'as) BEState"
sprCRel :: "('a, 'es, 'as) BEState Relation"
instance spr_simWorld_ext :: ("{finite, linorder}", finite, "{finite, linorder}", finite) finite
proof
let ?U = "UNIV :: ('a, 'b, 'c, 'd) spr_simWorld_ext set"
{ fix x :: "('a, 'b, 'c, 'd) spr_simWorld_scheme"
have "∃a b c d. x = spr_simWorld_ext a b c d"
by (cases x) simp
} then have U:
"?U = (λ(a, (b, (c, d))). spr_simWorld_ext a b c d) ` (UNIV × (UNIV × (UNIV × UNIV)))"
by (auto simp add: Set.image_def)
show "finite ?U" by (simp add: U)
qed
context FiniteDetBroadcastEnvironment
begin
text‹
The simulation of a trace @{term "t ∈ jkbpC"} records its initial and
final states, and the relation between initial and final states of all
commonly-plausible traces:
›
definition
spr_sim :: "('a, 'es, 'as) BEState Trace ⇒ ('a, 'es, 'as) spr_simWorld"
where
"spr_sim ≡ λt. ⦇ sprFst = tFirst t, sprLst = tLast t, sprCRel = tObsC_abs t ⦈"
text‹
The associated Kripke structure relates two worlds for an agent if the
agent's observation on the the first and last states corresponds, and
the worlds have the same common observation relation. As always, we
evaluate propositions on the final state of the trace.
›
definition
spr_simRels :: "'a ⇒ ('a, 'es, 'as) spr_simWorld Relation"
where
"spr_simRels ≡ λa. { (s, s') |s s'.
envObs a (sprFst s) = envObs a (sprFst s')
∧ envObs a (sprLst s) = envObs a (sprLst s')
∧ sprCRel s = sprCRel s' }"
definition spr_simVal :: "('a, 'es, 'as) spr_simWorld ⇒ 'p ⇒ bool" where
"spr_simVal ≡ envVal ∘ sprLst"
abbreviation
"spr_simMC ≡ mkKripke (spr_sim ` SPR.jkbpC) spr_simRels spr_simVal"
lemma spr_sim_tFirst_tLast:
"⟦ spr_sim t = s; t ∈ SPR.jkbpC ⟧ ⟹ (sprFst s, sprLst s) ∈ sprCRel s"
unfolding spr_sim_def by auto
lemma spr_sim_tObsC_abs:
shows "tObsC_abs t = sprCRel (spr_sim t)"
unfolding tObsC_abs_def spr_sim_def by simp
lemma spr_simVal_eq[iff]:
"spr_simVal (spr_sim t) = envVal (tLast t)"
unfolding spr_sim_def spr_simVal_def by simp
lemma spr_sim_range:
"sim_range SPR.MC spr_simMC spr_sim"
by (rule sim_rangeI) (simp_all add: spr_sim_def)
lemma spr_simVal:
"sim_val SPR.MC spr_simMC spr_sim"
by (rule sim_valI) simp
lemma spr_sim_f:
"sim_f SPR.MC spr_simMC spr_sim"
unfolding spr_simRels_def spr_sim_def mkKripke_def SPR.mkM_def
by (rule sim_fI, auto)
lemma envDetJKBP':
assumes tCn: "t ∈ SPR.jkbpCn n"
and aact: "act ∈ set (jAction (SPR.MCn n) t a)"
shows "jAction (SPR.MCn n) t a = [act]"
using jkbpDet[rule_format, where t=t and a=a] assms
apply -
apply (cases "jAction SPR.MC t a")
apply (auto iff: SPR.jkbpC_jkbpCn_jAction_eq[OF tCn] dest: SPR.jkbpCn_jkbpC_inc)
done
text‹
All the properties of a simulation are easy to show for @{term
"spr_sim"} except for reverse simulation.
The critical lemma states that if we have two traces that yield the
same common observations, and an agent makes the same observation on
their initial states, then that agent's private states at each point
on the two traces are identical.
›
lemma spr_jview_det_ps:
assumes tt'C: "{t, t'} ⊆ SPR.jkbpC"
assumes obsCtt': "tObsC t = tObsC t'"
assumes first: "envObs a (tFirst t) = envObs a (tFirst t')"
shows "tMap (λs. ODList.lookup (ps s) a) t
= tMap (λs. ODList.lookup (ps s) a) t'"
using tObsC_tLength[OF obsCtt'] first tt'C obsCtt'
proof(induct rule: trace_induct2)
case (tInit s s') thus ?case
by (simp add: envObs_def)
next
case (tStep s s' t t')
from tStep
have ts: "t ↝ s ∈ SPR.jkbpCn (tLength (t ↝ s))"
and t's': "t' ↝ s' ∈ SPR.jkbpCn (tLength (t' ↝ s'))"
by blast+
from tStep have jvtt': "spr_jview a t = spr_jview a t'"
by - (rule spr_jview_tObsCI, auto)
with tStep have jatt':
"jAction (SPR.MCn (tLength t)) t a
= jAction (SPR.MCn (tLength t')) t' a"
apply -
apply simp
apply (rule S5n_jAction_eq)
apply blast
unfolding SPR.mkM_def
apply auto
done
from jvtt'
have tt'Last: "ODList.lookup (ps (tLast t)) a
= ODList.lookup (ps (tLast t')) a"
by (auto simp: envObs_def)
from ts obtain eact aact
where aact: "∀a. aact a ∈ set (jAction (SPR.MCn (tLength t)) t a)"
and s: "s = envTrans eact aact (tLast t)"
by (auto iff: Let_def)
from t's' obtain eact' aact'
where aact': "∀a. aact' a ∈ set (jAction (SPR.MCn (tLength t')) t' a)"
and s': "s' = envTrans eact' aact' (tLast t')"
by (auto iff: Let_def)
from tStep have tCn: "t ∈ SPR.jkbpCn (tLength t)" by auto
from aact
obtain act
where act: "jAction (SPR.MCn (tLength t)) t a = [act]"
using envDetJKBP'[OF tCn, where a=a and act="aact a"]
by auto
hence "jAction (SPR.MCn (tLength t')) t' a = [act]"
by (simp only: jatt')
with act aact aact'
have "aact a = aact' a"
by (auto elim!: allE[where x=a])
with agents tt'Last s s'
have "ODList.lookup (ps s) a = ODList.lookup (ps s') a"
by (simp add: envTrans)
moreover
from tStep have "tMap (λs. ODList.lookup (ps s) a) t = tMap (λs. ODList.lookup (ps s) a) t'"
by auto
moreover
from tStep have "envObsC (es s) = envObsC (es s')"
unfolding tObsC_def by simp
ultimately show ?case by simp
qed
lemma spr_sim_r:
"sim_r SPR.MC spr_simMC spr_sim"
proof(rule sim_rI)
fix a p q'
assume pT: "p ∈ worlds SPR.MC"
and fpq': "(spr_sim p, q') ∈ relations spr_simMC a"
from fpq' obtain uq fq vq
where q': "q' = ⦇ sprFst = uq, sprLst = vq, sprCRel = tObsC_abs p ⦈"
and uq: "envObs a (tFirst p) = envObs a uq"
and vq: "envObs a (tLast p) = envObs a vq"
unfolding mkKripke_def spr_sim_def spr_simRels_def
by fastforce
from fpq' have "q' ∈ worlds spr_simMC" by simp
with q' have "(uq, vq) ∈ tObsC_abs p"
using spr_sim_tFirst_tLast[where s=q']
apply auto
done
then obtain t
where tT: "t ∈ SPR.jkbpC"
and tp: "tObsC t = tObsC p"
and tuq: "tFirst t = uq"
and tvq: "tLast t = vq"
by (auto iff: tObsC_abs_conv)
from pT tT tp tuq uq
have "tMap (λs. ODList.lookup (ps s) a) p = tMap (λs. ODList.lookup (ps s) a) t"
by (auto intro: spr_jview_det_ps)
with tp tuq uq
have "spr_jview a p = spr_jview a t"
by (auto intro: spr_jview_tObsCI)
with pT tT have pt: "(p, t) ∈ relations SPR.MC a"
unfolding SPR.mkM_def by simp
from q' uq vq tp tuq tvq have ftq': "spr_sim t = q'"
unfolding spr_sim_def by auto
from pt ftq'
show "∃q. (p, q) ∈ relations SPR.MC a ∧ spr_sim q = q'"
by blast
qed
text‹
The proof proceeds by lock-step induction over @{term "t"} and @{term
"t'"}, appealing to the @{term "jkbpDet"} assumption, the definition
of @{term "envObs"} and the constraint @{term "envTrans"}.
It is then a short step to showing reverse simulation, and hence
simulation:
›
lemma spr_sim: "sim SPR.MC spr_simMC spr_sim"
using spr_sim_range spr_simVal spr_sim_f spr_sim_r
unfolding sim_def
by blast
end
sublocale FiniteDetBroadcastEnvironment
< SPRdet: SimIncrEnvironment jkbp envInit envAction envTrans envVal
spr_jview envObs spr_jviewInit spr_jviewIncr
spr_sim spr_simRels spr_simVal
by standard (rule spr_sim)
subsubsection‹Representations›
text‹
As before we canonically represent the quotient of the simulated
worlds @{typ "('a, 'es, 'as) spr_simWorld"} under @{term
"spr_simRels"} using ordered, distinct lists. In particular, we use
the type @{typ "('a × 'a) odlist"} (abbreviated @{typ "'a
odrelation"}) to canonically represent relations.
›
context FiniteDetBroadcastEnvironment
begin
type_synonym (in -) ('a, 'es, 'as) spr_simWorldsECRep
= "('a, 'es, 'as) BEState odrelation"
type_synonym (in -) ('a, 'es, 'as) spr_simWorldsRep
= "('a, 'es, 'as) spr_simWorldsECRep × ('a, 'es, 'as) spr_simWorldsECRep"
text‹
We can abstract such a representation into a set of simulated
equivalence classes:
›
definition
spr_simAbs :: "('a, 'es, 'as) spr_simWorldsRep
⇒ ('a, 'es, 'as) spr_simWorld set"
where
"spr_simAbs ≡ λ(cec, aec). { ⦇ sprFst = s, sprLst = s', sprCRel = toSet cec ⦈
|s s'. (s, s') ∈ toSet aec }"
text‹
Assuming @{term "X"} represents a simulated equivalence class for
@{term "t ∈ jkbpC"}, we can decompose @{term "spr_simAbs X"} in terms
of @{term "tObsC_abs t"} and @{term "agent_abs t"}:
›
definition
agent_abs :: "'a ⇒ ('a, 'es, 'as) BEState Trace
⇒ ('a, 'es, 'as) BEState Relation"
where
"agent_abs a t ≡ { (tFirst t', tLast t')
|t'. t' ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t }"
lemma agent_absI[intro]:
"⟦ spr_jview a t' = spr_jview a t; t' ∈ SPR.jkbpC; t ∈ SPR.jkbpC ⟧
⟹ (tFirst t', tLast t') ∈ agent_abs a t"
unfolding agent_abs_def by auto
lemma spr_simAbs_refl:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "spr_sim t ∈ spr_simAbs ec"
using assms by simp
lemma spr_simAbs_tObsC_abs[simp]:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "toSet (fst ec) = tObsC_abs t"
using tC spr_simAbs_refl[OF tC ec]
unfolding spr_sim_def spr_simAbs_def by auto
lemma spr_simAbs_agent_abs[simp]:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "toSet (snd ec) = agent_abs a t"
using tC ec
unfolding spr_sim_def spr_simAbs_def agent_abs_def
apply (cases ec)
apply auto
apply (subgoal_tac "⦇sprFst = aaa, sprLst = ba, sprCRel = toSet aa⦈ ∈ {⦇sprFst = s, sprLst = s', sprCRel = toSet aa⦈ |s s'. (s, s') ∈ toSet b}")
apply auto
done
text‹
This representation is canonical on the domain of interest (though not
in general):
›
lemma spr_simAbs_inj_on:
"inj_on spr_simAbs { x . spr_simAbs x ∈ SPRdet.jkbpSEC }"
proof(rule inj_onI)
fix x y
assume x: "x ∈ { x . spr_simAbs x ∈ SPRdet.jkbpSEC }"
and y: "y ∈ { x . spr_simAbs x ∈ SPRdet.jkbpSEC }"
and xy: "spr_simAbs x = spr_simAbs y"
from x obtain a t
where tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs x = SPRdet.sim_equiv_class a t"
by auto
from spr_simAbs_tObsC_abs[OF tC ec] spr_simAbs_tObsC_abs[OF tC trans[OF xy[symmetric] ec], symmetric]
have "fst x = fst y" by (blast intro: injD[OF toSet_inj])
moreover
from spr_simAbs_agent_abs[OF tC ec] spr_simAbs_agent_abs[OF tC trans[OF xy[symmetric] ec], symmetric]
have "snd x = snd y" by (blast intro: injD[OF toSet_inj])
ultimately show "x = y" by (simp add: prod_eqI)
qed
text‹
The following sections make use of a Kripke structure constructed over
@{term "tObsC_abs t"} for some canonical trace @{term "t"}. Note that
we use the relation in the generated code.
›
type_synonym (in -) ('a, 'es, 'as) spr_simWorlds
= "('a, 'es, 'as) BEState × ('a, 'es, 'as) BEState"
definition (in -)
spr_repRels :: "('a ⇒ ('a, 'es, 'as) BEState ⇒ 'cobs × 'as option)
⇒ 'a ⇒ ('a, 'es, 'as) spr_simWorlds Relation"
where
"spr_repRels envObs ≡ λa. { ((u, v), (u', v')).
envObs a u = envObs a u' ∧ envObs a v = envObs a v' }"
definition
spr_repVal :: "('a, 'es, 'as) spr_simWorlds ⇒ 'p ⇒ bool"
where
"spr_repVal ≡ envVal ∘ snd"
abbreviation
spr_repMC :: "('a, 'es, 'as) BEState Relation
⇒ ('a, 'p, ('a, 'es, 'as) spr_simWorlds) KripkeStructure"
where
"spr_repMC ≡ λtcobsR. mkKripke tcobsR (spr_repRels envObs) spr_repVal"
abbreviation
spr_repRels :: "'a ⇒ ('a, 'es, 'as) spr_simWorlds Relation"
where
"spr_repRels ≡ SPRViewDet.spr_repRels envObs"
lemma spr_repMC_kripke[intro, simp]: "kripke (spr_repMC X)"
by (rule kripkeI) simp
lemma spr_repMC_S5n[intro, simp]: "S5n (spr_repMC X)"
unfolding spr_repRels_def
by (intro S5nI equivI refl_onI symI transI) auto
text‹
As before we can show that this Kripke structure is adequate for a
particular canonical trace @{term "t"} by showing that it simulates
@{term "spr_repMC"} We introduce an intermediate structure:
›
abbreviation
spr_jkbpCSt :: "('a, 'es, 'as) BEState Trace ⇒ ('a, 'es, 'as) spr_simWorld set"
where
"spr_jkbpCSt t ≡ spr_sim ` { t' . t' ∈ SPR.jkbpC ∧ tObsC t = tObsC t' }"
abbreviation
spr_simMCt :: "('a, 'es, 'as) BEState Trace
⇒ ('a, 'p, ('a, 'es, 'as) spr_simWorld) KripkeStructure"
where
"spr_simMCt t ≡ mkKripke (spr_jkbpCSt t) spr_simRels spr_simVal"
definition
spr_repSim :: "('a, 'es, 'as) spr_simWorld ⇒ ('a, 'es, 'as) spr_simWorlds"
where
"spr_repSim ≡ λs. (sprFst s, sprLst s)"
lemma spr_repSim_simps[simp]:
"spr_repSim ` spr_sim ` T = (λt. (tFirst t, tLast t)) ` T"
"spr_repSim (spr_sim t) = (tFirst t, tLast t)"
unfolding spr_repSim_def spr_sim_def
apply auto
apply (rule_tac x="⦇ sprFst = tFirst t, sprLst = tLast t, sprCRel = tObsC_abs t ⦈" in image_eqI)
apply auto
done
lemma jkbpCSt_jkbpCS_subset:
"spr_jkbpCSt t ⊆ spr_sim ` SPR.jkbpC"
by auto
text‹›
lemma spr_repSim:
assumes tC: "t ∈ SPR.jkbpC"
shows "sim (spr_simMCt t)
((spr_repMC ∘ sprCRel) (spr_sim t))
spr_repSim"
(is "sim ?M ?M' ?f")
proof
show "sim_range ?M ?M' ?f"
proof
show "worlds ?M' = ?f ` worlds ?M"
apply (simp add: spr_sim_def spr_repSim_def)
apply (auto iff: tObsC_abs_def)
apply (rule_tac x="⦇ sprFst = tFirst t', sprLst = tLast t', sprCRel = tObsC_abs t ⦈" in image_eqI)
apply simp
apply (rule_tac x=t' in image_eqI)
apply (simp add: tObsC_abs_def)
apply auto[1]
done
next
fix a
show "relations ?M' a ⊆ worlds ?M' × worlds ?M'"
by (simp add: spr_sim_def spr_repSim_def)
qed
next
show "sim_val ?M ?M' ?f"
by rule (simp add: spr_sim_def spr_simVal_def spr_repSim_def spr_repVal_def split: prod.split)
next
show "sim_f ?M ?M' ?f"
by rule (auto iff: spr_sim_def simp: spr_simRels_def spr_repRels_def spr_repSim_def)
next
show "sim_r ?M ?M' ?f"
apply rule
unfolding spr_repRels_def spr_repSim_def spr_simRels_def spr_sim_def
apply clarsimp
apply (rule_tac x="⦇ sprFst = aa, sprLst = b, sprCRel = tObsC_abs ta ⦈" in exI)
apply (auto iff: tObsC_abs_def)
apply (rule_tac x=t'a in image_eqI)
apply auto
done
qed
text‹
As before we define a set of constants that satisfy the ‹Algorithm› locale given the assumptions of the @{term
"FiniteDetBroadcastEnvironment"} locale.
›
subsubsection‹Initial states›
text‹
The initial states for agent @{term "a"} given an initial observation
@{term "iobs"} consist of the set of states that yield a common
observation consonant with @{term "iobs"} paired with the set of
states where @{term "a"} observes @{term "iobs"}:
›
definition (in -)
spr_simInit ::
"('a, 'es, 'as) BEState list ⇒ ('es ⇒ 'cobs)
⇒ ('a ⇒ ('a, 'es, 'as) BEState ⇒ 'cobs × 'obs)
⇒ 'a ⇒ ('cobs × 'obs)
⇒ ('a :: linorder, 'es :: linorder, 'as :: linorder) spr_simWorldsRep"
where
"spr_simInit envInit envObsC envObs ≡ λa iobs.
(ODList.fromList [ (s, s). s ← envInit, envObsC (es s) = fst iobs ],
ODList.fromList [ (s, s). s ← envInit, envObs a s = iobs ])"
abbreviation
spr_simInit :: "'a ⇒ ('cobs × 'as option) ⇒ ('a, 'es, 'as) spr_simWorldsRep"
where
"spr_simInit ≡ SPRViewDet.spr_simInit envInit envObsC envObs"
text‹›
lemma spr_simInit:
assumes "iobs ∈ envObs a ` set envInit"
shows "spr_simAbs (spr_simInit a iobs)
= spr_sim ` { t' ∈ SPR.jkbpC. spr_jview a t' = spr_jviewInit a iobs }"
using assms
unfolding spr_simInit_def spr_simAbs_def spr_sim_def [abs_def]
apply (clarsimp simp: Let_def SPR.jviewInit split: prod.split)
apply rule
apply clarsimp
apply (rule_tac x="tInit s" in image_eqI)
apply (auto iff: spr_jview_def envObs_def)
done
subsubsection‹Simulated observations›
text‹
An observation can be made at any element of the representation of a
simulated equivalence class of a canonical trace:
›
definition (in -)
spr_simObs ::
"('es ⇒ 'cobs)
⇒ 'a ⇒ ('a :: linorder, 'es :: linorder, 'as :: linorder) spr_simWorldsRep
⇒ 'cobs × 'as option"
where
"spr_simObs envObsC ≡ λa. (λs. (envObsC (es s), ODList.lookup (ps s) a))
∘ snd ∘ ODList.hd ∘ snd"
abbreviation
spr_simObs :: "'a ⇒ ('a, 'es, 'as) spr_simWorldsRep ⇒ 'cobs × 'as option"
where
"spr_simObs ≡ SPRViewDet.spr_simObs envObsC"
text‹›
lemma spr_simObs:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "spr_simObs a ec = envObs a (tLast t)"
proof -
have A: "∀s ∈ set (toList (snd ec)). envObs a (snd s) = envObs a (tLast t)"
using spr_simAbs_agent_abs[OF tC ec]
apply (clarsimp simp: toSet_def)
apply (auto simp: agent_abs_def)
done
from tC ec have B: "(tFirst t, tLast t) ∈ set (toList (snd ec))"
by (auto iff: spr_simAbs_def spr_sim_def toSet_def split_def)
show ?thesis
unfolding spr_simObs_def
using list_choose_hd[OF A B]
by (simp add: ODList.hd_def envObs_def)
qed
subsubsection‹Evaluation›
text‹
As for the clock semantics (\S\ref{sec:kbps-theory-clock-view-eval}),
we use the general evalation function @{term "evalS"}.
Once again we propositions are used to filter the set of possible
worlds @{term "X"}:
›
abbreviation (in -)
spr_evalProp ::
"(('a::linorder, 'es::linorder, 'as::linorder) BEState ⇒ 'p ⇒ bool)
⇒ ('a, 'es, 'as) BEState odrelation
⇒ 'p ⇒ ('a, 'es, 'as) BEState odrelation"
where
"spr_evalProp envVal ≡ λX p. ODList.filter (λs. envVal (snd s) p) X"
text‹
The knowledge operation computes the subset of possible worlds @{term
"cec"} that yield the same observation as @{term "s"} for agent @{term
"a"}:
›
definition (in -)
spr_knowledge ::
"('a ⇒ ('a::linorder, 'es::linorder, 'as::linorder) BEState
⇒ 'cobs × 'as option)
⇒ ('a, 'es, 'as) BEState odrelation
⇒ 'a ⇒ ('a, 'es, 'as) spr_simWorlds
⇒ ('a, 'es, 'as) spr_simWorldsECRep"
where
"spr_knowledge envObs cec ≡ λa s.
ODList.fromList [ s' . s' ← toList cec, (s, s') ∈ spr_repRels envObs a ]"
declare (in -) spr_knowledge_def[code del]
lemma (in -) [code]:
"spr_knowledge envObs cec = (λa s.
ODList.fromList [ s' . s' ← toList cec,
envObs a (fst s) = envObs a (fst s') ∧ envObs a (snd s) = envObs a (snd s') ])"
unfolding spr_knowledge_def spr_repRels_def by (simp add: split_def)
text‹
Similarly the common knowledge operation computes the transitive
closure \<^citep>‹"AFP:TRANCL"› of the union of the knowledge relations for
the agents ‹as›:
›
definition (in -)
spr_commonKnowledge ::
"('a ⇒ ('a::linorder, 'es::linorder, 'as::linorder) BEState
⇒ 'cobs × 'as option)
⇒ ('a, 'es, 'as) BEState odrelation
⇒ 'a list
⇒ ('a, 'es, 'as) spr_simWorlds
⇒ ('a, 'es, 'as) spr_simWorldsECRep"
where
"spr_commonKnowledge envObs cec ≡ λas s.
let r = λa. ODList.fromList
[ (s', s'') . s' ← toList cec, s'' ← toList cec,
(s', s'') ∈ spr_repRels envObs a ];
R = toList (ODList.big_union r as)
in ODList.fromList (memo_list_trancl R s)"
declare (in -) spr_commonKnowledge_def[code del]
lemma (in -) [code]:
"spr_commonKnowledge envObs cec = (λas s.
let r = λa. ODList.fromList
[ (s', s'') . s' ← toList cec, s'' ← toList cec,
envObs a (fst s') = envObs a (fst s'') ∧ envObs a (snd s') = envObs a (snd s'') ];
R = toList (ODList.big_union r as)
in ODList.fromList (memo_list_trancl R s))"
unfolding spr_commonKnowledge_def spr_repRels_def by (simp add: split_def)
text‹
The evaluation function evaluates a subjective knowledge formula on
the representation of an equivalence class:
›
definition (in -)
"eval envVal envObs ≡ λ(cec, X).
evalS (spr_evalProp envVal)
(spr_knowledge envObs cec)
(spr_commonKnowledge envObs cec)
X"
lemma spr_knowledge:
"s ∈ toSet cec
⟹ toSet (spr_knowledge envObs cec a s) = relations (spr_repMC (toSet cec)) a `` {s}"
unfolding spr_knowledge_def spr_repRels_def by (auto simp: toSet_def[symmetric])
lemma spr_commonKnowledge_relation_image:
"s ∈ toSet cec
⟹ toSet (spr_commonKnowledge envObs cec as s) = (⋃a ∈ set as. relations (spr_repMC (toSet cec)) a)⇧+ `` {s}"
unfolding spr_commonKnowledge_def Let_def
apply (simp add: memo_list_trancl toSet_def[symmetric] Image_def split_def)
apply (rule Collect_cong)
apply (rule_tac f="λx. (s, b) ∈ x" in arg_cong)
apply (rule arg_cong[where f=trancl])
apply fastforce
done
lemma eval_rec_models:
assumes XY: "toSet X ⊆ toSet Y"
and s: "s ∈ toSet X"
shows "s ∈ toSet (eval_rec (spr_evalProp envVal) (spr_knowledge envObs Y) (spr_commonKnowledge envObs Y) X φ)
⟷ spr_repMC (toSet Y), s ⊨ φ"
using XY s
proof(induct φ arbitrary: X s)
case (Kknows a' φ X s)
from ‹s ∈ toSet X› spr_knowledge[OF subsetD[OF Kknows(2) Kknows(3)], where a=a']
show ?case
apply simp
apply rule
apply (drule arg_cong[where f="toSet"])
apply (clarsimp simp: odlist_all_iff)
apply (cut_tac s1="(a, b)" and X1="spr_knowledge envObs Y a' (aa, ba)" in Kknows.hyps)
using Kknows(2) Kknows(3)
apply (auto simp add: S5n_rels_closed[OF spr_repMC_S5n])[3]
apply (clarsimp simp: toSet_eq_iff odlist_all_iff)
apply (subst Kknows.hyps)
using Kknows(2) Kknows(3)
apply (auto simp add: S5n_rels_closed[OF spr_repMC_S5n] o_def)
done
next
case (Kcknows as φ X s)
show ?case
proof(cases "as = Nil")
case True with ‹s ∈ toSet X› show ?thesis by clarsimp
next
case False
with ‹s ∈ toSet X› spr_commonKnowledge_relation_image[OF subsetD[OF Kcknows(2) Kcknows(3)], where as=as]
show ?thesis
apply simp
apply rule
apply (drule arg_cong[where f="toSet"])
apply (clarsimp simp: odlist_all_iff)
apply (cut_tac s1="(a, b)" and X1="spr_commonKnowledge envObs Y as (aa, ba)" in Kcknows.hyps)
using Kcknows(2) Kcknows(3)
apply (auto simp add: S5n_rels_closed[OF spr_repMC_S5n])[2]
apply (subst (asm) trancl_unfold) back back back
apply (auto simp add: S5n_rels_closed[OF spr_repMC_S5n])[2]
apply (clarsimp simp: toSet_eq_iff odlist_all_iff)
apply (subst Kcknows.hyps)
using Kcknows(2) Kcknows(3)
apply (auto simp add: S5n_rels_closed[OF spr_repMC_S5n] o_def)
apply (subst (asm) trancl_unfold) back back back
apply blast
done
qed
qed (simp_all add: spr_repVal_def)
lemma agent_abs_tObsC_abs_subset:
"tObsC t' = tObsC t ⟹ agent_abs a t ⊆ tObsC_abs t'"
unfolding agent_abs_def tObsC_abs_def
by (auto intro: spr_jview_tObsC)
lemma spr_simAbs_fst_snd:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "toSet (snd ec) ⊆ toSet (fst ec)"
using assms by (simp add: agent_abs_tObsC_abs_subset)
lemma tObsC_abs_rel:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
and r: "(x, y) ∈ (⋃ (relations (spr_repMC (tObsC_abs t)) ` set as))⇧+"
shows "x ∈ tObsC_abs t ⟷y ∈ tObsC_abs t"
using assms
apply -
apply rule
apply (erule trancl_induct, auto)+
done
lemma spr_simAbs_fst_snd_trc:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "toSet (big_union (spr_commonKnowledge envObs (fst ec) as) (toList (snd ec))) ⊆ toSet (fst ec)"
using assms
apply clarsimp
apply (simp only: toSet_def[symmetric])
apply (subgoal_tac "(ab,ba) ∈ toSet (fst ec)")
apply (simp add: spr_commonKnowledge_relation_image tObsC_abs_rel[OF tC ec])
apply (simp add: subsetD[OF agent_abs_tObsC_abs_subset[OF refl]])
done
lemma agent_abs_rel_inv:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
and x: "x ∈ agent_abs a t"
and xy: "(x, y) ∈ relations (spr_repMC (toSet (fst ec))) a"
shows "y ∈ agent_abs a t"
using assms
apply simp
unfolding agent_abs_def tObsC_abs_def spr_repRels_def
apply auto
apply (rule_tac x=t'b in exI)
apply clarsimp
apply (rule spr_jview_tObsCI)
apply simp
apply auto[1]
apply (rule spr_jview_det_ps)
using tC
apply auto
done
lemma agent_abs_tObsC_abs:
assumes tC: "t ∈ SPR.jkbpC"
and x: "x ∈ agent_abs a t"
and y: "y ∈ agent_abs a t"
shows "(x, y) ∈ relations (spr_repMC (tObsC_abs t)) a"
using assms
unfolding agent_abs_def spr_repRels_def
apply clarsimp
apply safe
prefer 3
apply (erule tObsC_absI) back
apply simp_all
apply (erule spr_jview_tObsC)
prefer 3
apply (erule tObsC_absI) back back
apply simp_all
apply (erule spr_jview_tObsC)
apply (rule spr_tFirst)
apply simp
apply (rule spr_tLast)
apply simp
done
lemma agent_abs_spr_repRels:
assumes tC: "t ∈ SPR.jkbpC"
and x: "x ∈ agent_abs a t"
and y: "y ∈ agent_abs a t"
shows "(x, y) ∈ spr_repRels a"
using assms
unfolding agent_abs_def spr_repRels_def
by (auto elim!: spr_tFirst spr_tLast)
lemma evalS_models:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
and subj_phi: "subjective a φ"
and s: "s ∈ toSet (snd ec)"
shows "evalS (spr_evalProp envVal) (spr_knowledge envObs (fst ec)) (spr_commonKnowledge envObs (fst ec)) (snd ec) φ
⟷ spr_repMC (toSet (fst ec)), s ⊨ φ" (is "?lhs φ = ?rhs φ")
using subj_phi s ec
proof(induct φ rule: subjective.induct[case_names Kprop Knot Kand Kknows Kcknows])
case (Kknows a a' ψ) thus ?case
apply (clarsimp simp: toSet_eq_iff)
apply rule
apply clarsimp
apply (subgoal_tac "(a, b) ∈ toSet (snd ec)")
apply (drule (1) subsetD) back
apply (simp only: eval_rec_models[OF spr_simAbs_fst_snd[OF tC ec]])
using tC Kknows
apply simp
using tC ec
apply -
apply (erule (1) agent_abs_rel_inv[OF tC])
apply simp
apply clarsimp
apply (subst eval_rec_models[OF spr_simAbs_fst_snd[OF tC ec]])
apply simp
using agent_abs_tObsC_abs[OF tC]
apply auto
done
next
case (Kcknows a as ψ)
have "?lhs (Kcknows as ψ)
= (∀y∈agent_abs a t.
∀x∈((⋃a∈set as. relations (spr_repMC (toSet (fst ec))) a)⇧+ `` {y}).
x ∈ toSet (eval_rec (spr_evalProp envVal) (spr_knowledge envObs (fst ec)) (spr_commonKnowledge envObs (fst ec))
(big_union (spr_commonKnowledge envObs (fst ec) as) (toList (snd ec))) ψ))"
using toSet_def[symmetric] spr_simAbs_agent_abs[OF tC Kcknows(3)] spr_simAbs_tObsC_abs[OF tC Kcknows(3)]
apply (clarsimp simp: toSet_eq_iff toSet_def[symmetric] subset_eq)
apply (rule ball_cong[OF refl])
apply (rule ball_cong)
apply (subst spr_commonKnowledge_relation_image)
apply (simp_all add: subsetD[OF agent_abs_tObsC_abs_subset[OF refl]])
done
also have "... = (∀s∈agent_abs a t. spr_repMC (toSet (fst ec)), s ⊨ Kcknows as ψ)"
apply (rule ball_cong[OF refl])
apply simp
apply (rule ball_cong[OF refl])
apply (subst eval_rec_models[OF spr_simAbs_fst_snd_trc[OF tC Kcknows(3), where as=as], symmetric])
using spr_simAbs_agent_abs[OF tC Kcknows(3)] spr_simAbs_tObsC_abs[OF tC Kcknows(3)]
apply (simp add: toSet_def[symmetric])
apply (rule_tac x=y in bexI)
apply (subst spr_commonKnowledge_relation_image)
apply (auto elim: subsetD[OF agent_abs_tObsC_abs_subset[OF refl]])[1]
apply simp
apply assumption
apply (rule refl)
done
also have "... = spr_repMC (toSet (fst ec)), s ⊨ Kknows a (Kcknows as ψ)"
using spr_simAbs_agent_abs[OF tC Kcknows(3)] spr_simAbs_tObsC_abs[OF tC Kcknows(3)]
Kcknows(2) tC
apply simp
apply (rule ball_cong[OF _ refl])
apply rule
apply (clarsimp simp: subsetD[OF agent_abs_tObsC_abs_subset] agent_abs_spr_repRels[OF tC])
apply (clarsimp elim!: agent_abs_rel_inv[OF tC Kcknows(3)])
done
also have "... = spr_repMC (toSet (fst ec)), s ⊨ Kcknows as ψ"
apply (rule S5n_common_knowledge_fixed_point_simpler[symmetric])
using spr_simAbs_agent_abs[OF tC Kcknows(3)] spr_simAbs_tObsC_abs[OF tC Kcknows(3)]
Kcknows(1) Kcknows(2)
apply (auto elim: subsetD[OF agent_abs_tObsC_abs_subset[OF refl]])
done
finally show ?case .
qed simp_all
text‹
This function corresponds with the standard semantics:
›
lemma eval_models:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
assumes subj_phi: "subjective a φ"
assumes s: "s ∈ toSet (snd ec)"
shows "eval envVal envObs ec φ ⟷ spr_repMC (toSet (fst ec)), s ⊨ φ"
unfolding eval_def
using evalS_models[OF tC ec subj_phi s]
apply auto
done
subsubsection‹Simulated actions›
text‹
From a common equivalence class and a subjective equivalence class for
agent @{term "a"}, we can compute the actions enabled for @{term "a"}:
›
definition (in -)
spr_simAction ::
"('a, 'p, 'aAct) JKBP ⇒ (('a, 'es, 'as) BEState ⇒ 'p ⇒ bool)
⇒ ('a ⇒ ('a, 'es, 'as) BEState ⇒ 'cobs × 'as option)
⇒ 'a
⇒ ('a::linorder, 'es::linorder, 'as::linorder) spr_simWorldsRep
⇒ 'aAct list"
where
"spr_simAction jkbp envVal envObs ≡ λa ec.
[ action gc. gc ← jkbp a, eval envVal envObs ec (guard gc) ]"
abbreviation
spr_simAction :: "'a ⇒ ('a, 'es, 'as) spr_simWorldsRep ⇒ 'aAct list"
where
"spr_simAction ≡ SPRViewDet.spr_simAction jkbp envVal envObs"
text‹
Using the above result about evaluation, we can relate ‹spr_simAction› to @{term "jAction"}. Firstly, ‹spr_simAction› behaves the same as @{term "jAction"} using the
@{term "spr_repMC"} structure:
›
lemma spr_action_jaction:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "set (spr_simAction a ec)
= set (jAction (spr_repMC (toSet (fst ec))) (tFirst t, tLast t) a)"
unfolding spr_simAction_def jAction_def
apply clarsimp
apply rule
apply clarsimp
apply (rule_tac x=xa in bexI)
apply simp
apply clarsimp
apply (subst eval_models[OF tC ec, symmetric])
using tC ec subj
apply simp_all
apply (rule agent_absI)
apply simp_all
apply clarsimp
apply (rule_tac x=xa in bexI)
apply simp
apply clarsimp
apply (subst eval_models[OF tC ec])
using tC ec subj
apply simp_all
apply (rule agent_absI)
apply simp_all
done
lemma spr_submodel_aux:
assumes tC: "t ∈ SPR.jkbpC"
and s: "s ∈ worlds (spr_simMCt t)"
shows "gen_model SPRdet.MCS s = gen_model (spr_simMCt t) s"
proof(rule gen_model_subset[where T="spr_jkbpCSt t"])
fix a
let ?X = "spr_sim ` { t' . t' ∈ SPR.jkbpC ∧ tObsC t = tObsC t' }"
show "relations SPRdet.MCS a ∩ ?X × ?X
= relations (spr_simMCt t) a ∩ ?X × ?X"
by (simp add: Int_ac Int_absorb1
relation_mono[OF jkbpCSt_jkbpCS_subset jkbpCSt_jkbpCS_subset])
next
let ?X = "spr_sim ` { t' . t' ∈ SPR.jkbpC ∧ tObsC t = tObsC t' }"
from s show "(⋃a. relations (spr_simMCt t) a)⇧* `` {s} ⊆ ?X"
apply (clarsimp simp del: mkKripke_simps)
apply (erule (1) kripke_rels_trc_worlds)
apply auto
done
next
let ?Y = "{ t' . t' ∈ SPR.jkbpC ∧ tObsC t = tObsC t' }"
let ?X = "spr_sim ` ?Y"
from s obtain t'
where st': "s = spr_sim t'"
and t'C: "t' ∈ SPR.jkbpC"
and t'O: "tObsC t = tObsC t'"
by fastforce
{ fix t''
assume tt': "(t', t'') ∈ (⋃a. relations SPR.MC a)⇧*"
from t'C tt' have t''C: "t'' ∈ SPR.jkbpC"
by - (erule kripke_rels_trc_worlds, simp_all)
from t'O tt' have t''O: "tObsC t = tObsC t''"
by (simp add: spr_tObsC_trc_aux)
from t''C t''O have "t'' ∈ ?Y" by simp }
hence "(⋃a. relations SPR.MC a)⇧* `` {t'} ⊆ ?Y"
by clarsimp
hence "spr_sim ` ((⋃a. relations SPR.MC a)⇧* `` {t'}) ⊆ ?X"
by (rule image_mono)
with st' t'C
show "(⋃a. relations SPRdet.MCS a)⇧* `` {s} ⊆ ?X"
using sim_trc_commute[OF SPR.mkM_kripke spr_sim, where t=t'] by simp
qed (insert s, auto)
text‹
We can connect the agent's choice of actions on the ‹spr_repMC› structure to those on the ‹SPR.MC› structure
using our earlier results about actions being preserved by generated
models and simulations.
›
lemma spr_simAction:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "set (spr_simAction a ec) = set (jAction SPR.MC t a)"
(is "?lhs = ?rhs")
proof -
from tC ec
have "?lhs = set (jAction (spr_repMC (toSet (fst ec))) (tFirst t, tLast t) a)"
by (rule spr_action_jaction)
also from tC ec have "... = set (jAction (spr_simMCt t) (spr_sim t) a)"
by (simp add: simulation_jAction_eq[OF _ spr_repSim] spr_sim_tObsC_abs)
also from tC have "... = set (jAction SPRdet.MCS (spr_sim t) a)"
using gen_model_jAction_eq[OF spr_submodel_aux[OF tC, where s="spr_sim t"], where w'="spr_sim t"]
gen_model_world_refl[where w="spr_sim t" and M="spr_simMCt t"]
by simp
also from tC have "... = set (jAction SPR.MC t a)"
by (simp add: simulation_jAction_eq[OF _ spr_sim])
finally show ?thesis .
qed
subsubsection‹Simulated transitions›
text‹
The story of simulated transitions takes some doing. We begin by
computing the successor relation of a given equivalence class @{term
"X"} with respect to the common equivalence class @{term "cec"}:
›
abbreviation (in -)
"spr_jAction jkbp envVal envObs cec s ≡ λa.
spr_simAction jkbp envVal envObs a (cec, spr_knowledge envObs cec a s)"
definition (in -)
spr_trans :: "'a odlist
⇒ ('a, 'p, 'aAct) JKBP
⇒ (('a::linorder, 'es::linorder, 'as::linorder) BEState ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct)
⇒ ('a, 'es, 'as) BEState ⇒ ('a, 'es, 'as) BEState)
⇒ (('a, 'es, 'as) BEState ⇒ 'p ⇒ bool)
⇒ ('a ⇒ ('a, 'es, 'as) BEState ⇒ 'cobs × 'as option)
⇒ ('a, 'es, 'as) spr_simWorldsECRep
⇒ ('a, 'es, 'as) spr_simWorldsECRep
⇒ (('a, 'es, 'as) BEState × ('a, 'es, 'as) BEState) list"
where
"spr_trans agents jkbp envAction envTrans envVal envObs ≡ λcec X.
[ (initialS, succS) .
(initialS, finalS) ← toList X,
eact ← envAction finalS,
succS ← [ envTrans eact aact finalS .
aact ← listToFuns (spr_jAction jkbp envVal envObs cec
(initialS, finalS))
(toList agents) ] ]"
text‹
We will split the result of this function according to the common
observation and also agent @{term "a"}'s observation, where @{term
"a"} is the agent we are constructing the automaton for.
›
definition (in -)
spr_simObsC :: "('es ⇒ 'cobs)
⇒ (('a::linorder, 'es::linorder, 'as::linorder) BEState
× ('a, 'es, 'as) BEState) odlist
⇒ 'cobs"
where
"spr_simObsC envObsC ≡ envObsC ∘ es ∘ snd ∘ ODList.hd"
abbreviation (in -)
envObs_rel :: "(('a, 'es, 'as) BEState ⇒ 'cobs × 'as option)
⇒ ('a, 'es, 'as) spr_simWorlds × ('a, 'es, 'as) spr_simWorlds ⇒ bool"
where
"envObs_rel envObs ≡ λ(s, s'). envObs (snd s') = envObs (snd s)"
text‹
The above combine to yield the successor equivalence classes like so:
›
definition (in -)
spr_simTrans :: "'a odlist
⇒ ('a, 'p, 'aAct) JKBP
⇒ (('a::linorder, 'es::linorder, 'as::linorder) BEState ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct)
⇒ ('a, 'es, 'as) BEState ⇒ ('a, 'es, 'as) BEState)
⇒ (('a, 'es, 'as) BEState ⇒ 'p ⇒ bool)
⇒ ('es ⇒ 'cobs)
⇒ ('a ⇒ ('a, 'es, 'as) BEState ⇒ 'cobs × 'as option)
⇒ 'a
⇒ ('a, 'es, 'as) spr_simWorldsRep
⇒ ('a, 'es, 'as) spr_simWorldsRep list"
where
"spr_simTrans agents jkbp envAction envTrans envVal envObsC envObs ≡ λa ec.
let aSuccs = spr_trans agents jkbp envAction envTrans envVal envObs
(fst ec) (snd ec);
cec' = ODList.fromList
(spr_trans agents jkbp envAction envTrans envVal envObs
(fst ec) (fst ec))
in [ (ODList.filter (λs. envObsC (es (snd s)) = spr_simObsC envObsC aec') cec',
aec') .
aec' ← map ODList.fromList (partition (envObs_rel (envObs a)) aSuccs) ]"
abbreviation
spr_trans :: "('a, 'es, 'as) spr_simWorldsECRep
⇒ ('a, 'es, 'as) spr_simWorldsECRep
⇒ (('a, 'es, 'as) spr_simWorlds) list"
where
"spr_trans ≡ SPRViewDet.spr_trans agents jkbp envAction envTrans envVal envObs"
abbreviation
spr_simTrans :: "'a ⇒ ('a, 'es, 'as) spr_simWorldsRep ⇒ ('a, 'es, 'as) spr_simWorldsRep list"
where
"spr_simTrans ≡ SPRViewDet.spr_simTrans agents jkbp envAction envTrans envVal envObsC envObs"
lemma spr_trans_aec:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "set (spr_trans (fst ec) (snd ec))
= { (tFirst t', s) |t' s. t' ↝ s ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t }" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
proof
fix x assume x: "x ∈ ?lhs"
with assms show "x ∈ ?rhs"
unfolding spr_trans_def
apply (clarsimp simp del: split_paired_Ex split_paired_All simp add: toSet_def[symmetric] agent_abs_def)
apply (rule_tac x=t' in exI)
apply simp
apply (rule_tac n="Suc (tLength t')" in SPR.jkbpCn_jkbpC_inc)
apply (auto iff: Let_def simp del: split_paired_Ex split_paired_All)
apply (simp add: listToFuns_ext[OF agents[unfolded toSet_def]])
apply (rule_tac x=xa in exI)
apply simp
apply (subst (asm) spr_simAction)
apply assumption
apply rule
apply clarsimp
apply (clarsimp simp: spr_simAbs_def)
apply (subst (asm) spr_knowledge)
apply (simp add: ec)
apply (erule tObsC_absI)
apply simp_all
apply (erule spr_jview_tObsC)
using ec
apply clarsimp
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv)
apply (rule_tac x=t'b in image_eqI)
apply (auto iff: spr_sim_def)[1]
apply clarsimp
apply (rule spr_jview_tObsCI[OF _ _ spr_jview_det_ps])
apply simp_all
apply (erule spr_jview_tObsC[symmetric])
apply (erule spr_jview_tObsC[symmetric])
apply clarsimp
apply (clarsimp simp: spr_simAbs_def)
apply (subst spr_knowledge)
apply (simp_all add: ec)
apply (erule tObsC_absI)
apply (erule spr_jview_tObsC)
apply simp_all
apply (rule_tac x="tFirst xc" in exI)
apply (rule_tac x="tLast xc" in exI)
apply (simp add: spr_sim_def)
apply rule
apply (drule tObsC_abs_jview_eq)
apply simp
apply (erule tObsC_abs_jview_eq[symmetric])
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv)
apply rule
apply (rule spr_tFirst)
apply simp
apply rule
apply (rule spr_tLast)
apply simp
apply rule
apply (rule_tac x=t' in exI)
apply simp
apply (erule spr_jview_tObsC)
apply (rule_tac x=xc in exI)
apply simp
apply (drule spr_jview_tObsC)
apply (drule spr_jview_tObsC)
apply simp
apply (subst SPR.jkbpC_jkbpCn_jAction_eq[symmetric])
apply auto
done
qed
show "?rhs ⊆ ?lhs"
proof
fix x assume x: "x ∈ ?rhs"
then obtain t' s
where x': "x = (tFirst t', s)"
and t'sC: "t' ↝ s ∈ SPR.jkbpC"
and F: "spr_jview a t' = spr_jview a t"
by blast
from t'sC have t'Cn: "t' ∈ SPR.jkbpCn (tLength t')" by blast
from t'sC obtain eact aact
where eact: "eact ∈ set (envAction (tLast t'))"
and aact: "∀a. aact a ∈ set (jAction (SPR.mkM (SPR.jkbpCn (tLength t'))) t' a)"
and s: "s = envTrans eact aact (tLast t')"
using SPR.jkbpC_tLength_inv[where t="t' ↝ s" and n="Suc (tLength t')"]
by (auto iff: Let_def)
from tC t'sC ec F x' s eact aact
show "x ∈ ?lhs"
unfolding spr_trans_def
apply (clarsimp simp del: split_paired_Ex split_paired_All simp: toSet_def[symmetric])
apply (rule bexI[where x="(tFirst t', tLast t')"])
apply simp
apply (rule bexI[where x="eact"])
apply (rule_tac x="aact" in image_eqI)
apply simp_all
apply (simp add: listToFuns_ext[OF agents[unfolded toSet_def]])
defer
apply blast
apply (subst spr_simAction[where t=t'])
apply blast
defer
apply (auto iff: SPR.jkbpC_jkbpCn_jAction_eq[OF t'Cn])[1]
apply (clarsimp simp: spr_simAbs_def)
apply (subst spr_knowledge)
apply (simp_all add: ec)
apply (rule tObsC_absI[where t=t and t'=t'])
apply simp_all
apply blast
apply (blast intro: spr_jview_tObsC)
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv)
apply rule
apply clarsimp
apply (rule_tac x=t'aa in image_eqI)
apply (auto iff: spr_sim_def)[1]
apply simp
apply (rule spr_jview_tObsCI[OF _ _ spr_jview_det_ps])
apply simp_all
apply (erule spr_jview_tObsC[symmetric])
apply blast
apply (erule spr_jview_tObsC[symmetric])
apply (clarsimp simp: spr_sim_def)
apply rule
apply (drule tObsC_abs_jview_eq)
apply (drule tObsC_abs_jview_eq)
apply simp
apply rule
apply (rule spr_tFirst)
apply simp
apply rule
apply (rule spr_tLast)
apply simp
apply rule
apply (rule_tac x=t' in exI)
apply (auto dest: spr_jview_tObsC intro: spr_jview_tObsC_trans)
done
qed
qed
lemma spr_trans_cec:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "set (spr_trans (fst ec) (fst ec))
= { (tFirst t', s) |t' s. t' ↝ s ∈ SPR.jkbpC ∧ tObsC t' = tObsC t }" (is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
proof
fix x assume x: "x ∈ ?lhs"
with assms show "x ∈ ?rhs"
unfolding spr_trans_def
apply (clarsimp simp del: split_paired_Ex split_paired_All simp add: toSet_def[symmetric] tObsC_abs_def)
apply (rule_tac x=t' in exI)
apply simp
apply (rule_tac n="Suc (tLength t')" in SPR.jkbpCn_jkbpC_inc)
apply (auto iff: Let_def simp del: split_paired_Ex split_paired_All)
apply (simp add: listToFuns_ext[OF agents[unfolded toSet_def]])
apply (rule_tac x=xa in exI)
apply simp
apply (subst (asm) spr_simAction)
apply assumption
apply rule
apply clarsimp
apply (clarsimp simp: spr_simAbs_def)
apply (subst (asm) spr_knowledge)
apply (simp add: ec)
apply (erule tObsC_absI)
apply simp_all
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv ec)
apply (rule_tac x=t'b in image_eqI)
apply (auto iff: spr_sim_def ec)[1]
apply clarsimp
apply (rule spr_jview_tObsCI[OF _ _ spr_jview_det_ps])
apply simp_all
apply (clarsimp simp: spr_simAbs_def)
apply (subst spr_knowledge)
apply (simp_all add: ec)
apply (erule tObsC_absI)
apply simp_all
apply (rule_tac x="tFirst xc" in exI)
apply (rule_tac x="tLast xc" in exI)
apply (simp add: spr_sim_def)
apply rule
apply (drule tObsC_abs_jview_eq)
apply auto[1]
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv)
apply rule
apply (rule spr_tFirst)
apply simp
apply rule
apply (rule spr_tLast)
apply simp
apply rule
apply (rule_tac x=t' in exI)
apply simp
apply (rule_tac x=xc in exI)
apply simp
apply (drule spr_jview_tObsC)
apply simp
apply (subst SPR.jkbpC_jkbpCn_jAction_eq[symmetric])
apply auto
done
qed
show "?rhs ⊆ ?lhs"
proof
fix x assume x: "x ∈ ?rhs"
then obtain t' s
where x': "x = (tFirst t', s)"
and t'sC: "t' ↝ s ∈ SPR.jkbpC"
and F: "tObsC t' = tObsC t"
by blast
from t'sC have t'Cn: "t' ∈ SPR.jkbpCn (tLength t')" by blast
from t'sC obtain eact aact
where eact: "eact ∈ set (envAction (tLast t'))"
and aact: "∀a. aact a ∈ set (jAction (SPR.mkM (SPR.jkbpCn (tLength t'))) t' a)"
and s: "s = envTrans eact aact (tLast t')"
using SPR.jkbpC_tLength_inv[where t="t' ↝ s" and n="Suc (tLength t')"]
by (auto iff: Let_def)
from tC t'sC ec F x' s eact aact
show "x ∈ ?lhs"
unfolding spr_trans_def
apply (clarsimp simp del: split_paired_Ex split_paired_All simp: toSet_def[symmetric])
apply (rule bexI[where x="(tFirst t', tLast t')"])
apply simp
apply (rule bexI[where x="eact"])
apply (rule_tac x="aact" in image_eqI)
apply simp_all
apply (simp add: listToFuns_ext[OF agents[unfolded toSet_def]])
defer
apply blast
apply (subst spr_simAction[where t=t'])
apply blast
defer
apply (auto iff: SPR.jkbpC_jkbpCn_jAction_eq[OF t'Cn])[1]
apply (clarsimp simp: spr_simAbs_def)
apply (subst spr_knowledge)
apply (simp_all add: ec)
apply (rule tObsC_absI[where t=t and t'=t'])
apply simp_all
apply blast
apply (clarsimp simp: spr_repRels_def tObsC_abs_conv)
apply rule
apply clarsimp
apply (rule_tac x=t'aa in image_eqI)
apply (auto iff: spr_sim_def [abs_def])[1]
apply simp
apply (rule spr_jview_tObsCI[OF _ _ spr_jview_det_ps])
apply simp_all
apply blast
apply (clarsimp simp: spr_sim_def [abs_def])
apply (rule conjI)
apply (auto dest!: tObsC_abs_jview_eq intro: spr_tFirst spr_tLast)[1]
apply (rule conjI)
apply (auto intro: spr_tFirst)[1]
apply (rule conjI)
apply (auto intro: spr_tLast)[1]
apply (rule conjI)
apply (auto intro: spr_tLast)[1]
apply (rule_tac x=xb in exI)
apply (auto dest: spr_jview_tObsC intro: spr_jview_tObsC_trans)[1]
done
qed
qed
lemma spr_simObsC:
assumes t'sC: "t ↝ s ∈ SPR.jkbpC"
and aec': "toSet aec = (rel_ext (envObs_rel (envObs a)) ∩ X × X) `` {(tFirst t, s)}"
and X: "X = {(tFirst t', s) |t' s. t' ↝ s ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t}"
shows "spr_simObsC envObsC aec = envObsC (es s)"
unfolding spr_simObsC_def
apply (cases aec)
using assms
apply auto[1]
using assms
apply (simp add: ODList.hd_def toList_fromList)
apply (subgoal_tac "x ∈ insert x (set xs)")
apply (auto iff: envObs_def)[1]
apply blast
done
lemma envObs_rel_equiv:
"equiv UNIV (rel_ext (envObs_rel (envObs a)))"
by (intro equivI refl_onI symI transI) auto
text‹
Showing that ‹spr_simTrans› works requires a series of
auxiliary lemmas that show we do in fact compute the correct successor
equivalence classes. We elide the unedifying details, skipping
straight to the lemma that the @{term "Algorithm"} locale expects:
›
lemma spr_simTrans:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRdet.sim_equiv_class a t"
shows "spr_simAbs ` set (spr_simTrans a ec)
= { SPRdet.sim_equiv_class a (t' ↝ s)
|t' s. t' ↝ s ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t}"
(is "?lhs = ?rhs")
proof
show "?lhs ⊆ ?rhs"
proof
fix x assume x: "x ∈ ?lhs"
then obtain rx
where xrx: "x = spr_simAbs rx"
and rx: "rx ∈ set (spr_simTrans a ec)" by blast
with tC ec obtain cec' aec' UV' t' s
where rxp: "rx = (cec', aec')"
and t'sC: "t' ↝ s ∈ SPR.jkbpC"
and tt': "spr_jview a t' = spr_jview a t"
and aec': "toSet aec' = (rel_ext (envObs_rel (envObs a)) ∩ set (spr_trans (fst ec) (snd ec))
× set (spr_trans (fst ec) (snd ec))) `` {(tFirst t', s)}"
and cec': "cec' = ODList.filter (λs. envObsC (es (snd s)) = spr_simObsC envObsC aec') (fromList (spr_trans (fst ec) (fst ec)))"
unfolding spr_simTrans_def
using spr_trans_aec[OF assms]
apply (auto split: prod.split_asm)
apply (drule imageI[where f=set])
apply (simp add: partition[OF envObs_rel_equiv subset_UNIV])
apply (erule quotientE)
apply fastforce
done
from t'sC tt' aec' cec'
have "spr_simAbs (cec', aec') = SPRdet.sim_equiv_class a (t' ↝ s)"
unfolding spr_simAbs_def
apply clarsimp
apply rule
using spr_trans_aec[OF assms] spr_trans_cec[OF assms]
apply clarsimp
apply (rule_tac x="t'aa ↝ s'" in image_eqI)
apply (simp add: spr_sim_def)
apply (cut_tac aec=aec' and t=t' and s=s in spr_simObsC[where a=a])
apply simp_all
apply rule
apply clarsimp
apply (erule_tac t'="t'b ↝ sa" in tObsC_absI)
apply simp_all
apply (auto dest: spr_jview_tObsC iff: tObsC_def envObs_def_raw)[1]
apply (clarsimp simp: envObs_def_raw tObsC_abs_conv)
apply (case_tac t'b)
apply (simp add: tObsC_def)
apply clarsimp
apply (rename_tac Trace State)
apply (rule_tac x=Trace in exI)
apply (auto dest: spr_jview_tObsC simp: tObsC_def)[1]
apply (simp add: spr_jview_def)
using spr_trans_aec[OF assms] spr_trans_cec[OF assms]
apply (clarsimp simp: spr_sim_def)
apply (cut_tac aec=aec' and t=t' and s=s in spr_simObsC[where a=a])
apply simp_all
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply safe
apply (clarsimp simp: tObsC_abs_conv)
apply (case_tac t'a)
apply (simp add: tObsC_def)
apply clarsimp
apply (rename_tac Trace State)
apply (rule_tac x="Trace" in exI)
apply (drule spr_jview_prefix_closed)
apply (auto dest: spr_jview_tObsC simp: tObsC_def)[1]
apply (auto simp: spr_jview_def Let_def envObs_def_raw)[1]
apply (erule_tac t'="t'a ↝ sa" in tObsC_absI)
apply simp_all
apply (drule spr_jview_tObsC[symmetric])
apply (frule spr_jview_prefix_closed)
apply (auto dest: spr_jview_tObsC simp: tObsC_def)[1]
apply (simp add: spr_jview_def)
apply auto[1]
apply (rule_tac x="t''" in exI)
apply (drule spr_jview_prefix_closed)
apply simp
done
with xrx rxp t'sC tt'
show "x ∈ ?rhs"
apply simp
apply (rule_tac x=t' in exI)
apply (rule_tac x=s in exI)
apply simp
done
qed
next
note image_cong_simp [cong del]
show "?rhs ⊆ ?lhs"
proof
fix x assume x: "x ∈ ?rhs"
then obtain t' s
where t'sC: "t' ↝ s ∈ SPR.jkbpC"
and tt': "spr_jview a t' = spr_jview a t"
and xt's: "x = SPRdet.sim_equiv_class a (t' ↝ s)"
by auto
then have "(λs. (sprFst s, sprLst s)) ` x ∈ set ` set (partition (envObs_rel (envObs a)) (spr_trans (fst ec) (snd ec)))"
apply (simp add: partition[OF envObs_rel_equiv] spr_trans_aec[OF assms] spr_sim_def [abs_def])
apply (rule_tac x="(tFirst t', s)" in quotientI2)
apply auto[1]
apply (auto dest: spr_jview_tStep_eq_inv)
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_prefix_closed)
apply auto[1]
apply (rule_tac x="⦇sprFst = tFirst t'aa, sprLst = sa, sprCRel = tObsC_abs (t'aa ↝ sa)⦈" in image_eqI)
apply simp
apply (rule_tac x="t'aa ↝ sa" in image_eqI)
apply simp
apply (simp add: spr_jview_def)
done
then obtain rx
where "rx ∈ set (partition (envObs_rel (envObs a)) (spr_trans (fst ec) (snd ec)))"
and "set rx = (λs. (sprFst s, sprLst s)) ` x"
by auto
with t'sC tt' xt's show "x ∈ ?lhs"
unfolding spr_simTrans_def
apply clarsimp
apply (rule_tac x="(ODList.filter (λs. envObsC (es (snd s)) = spr_simObsC envObsC (fromList rx)) (fromList (spr_trans (fst ec) (fst ec))), fromList rx)" in image_eqI)
prefer 2
apply (rule_tac x="rx" in image_eqI)
apply simp
apply simp
apply (subst spr_simObsC[where a=a and t=t' and s=s, OF _ _ refl])
apply simp_all
apply rule
apply clarsimp
apply (frule spr_jview_tStep_eq_inv)
apply (auto simp: spr_jview_def spr_sim_def [abs_def])[1]
apply clarsimp
apply (rule_tac x="spr_sim (t'aa ↝ sa)" in image_eqI)
apply (simp add: spr_sim_def [abs_def])
apply (rule_tac x="t'aa ↝ sa" in image_eqI)
apply simp
apply (simp add: spr_jview_def)
apply (clarsimp simp: spr_trans_cec[OF assms] spr_sim_def [abs_def] spr_simAbs_def)
apply rule
apply (auto iff: tObsC_abs_conv)[1]
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (frule tObsC_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_prefix_closed)
apply (drule spr_jview_tObsC)
apply (drule spr_jview_tObsC)
apply (drule tObsC_prefix_closed)
apply (rule_tac x=t''a in exI)
apply simp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (frule tObsC_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_tObsC) back
apply (simp add: tObsC_def)
apply (rule_tac x="t'a ↝ sa" in exI)
apply simp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_tObsC)
apply (frule spr_jview_tObsC)
apply (simp add: tObsC_def)
apply (rule_tac x="spr_sim ta" in image_eqI)
apply (simp add: spr_sim_def [abs_def])
apply (rule_tac x=ta in image_eqI)
apply (simp add: spr_sim_def [abs_def])
apply simp
apply clarsimp
apply (rule_tac x=ta in image_eqI)
prefer 2
apply simp
apply (clarsimp simp: tObsC_abs_def)
apply auto[1]
apply (rule_tac x="t'a ↝ sa" in exI)
apply simp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_tObsC)
apply (frule spr_jview_tObsC)
apply (simp add: tObsC_def)
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (frule tObsC_tStep_eq_inv)
apply clarsimp
apply (rule_tac x="t''a" in exI)
apply (drule spr_jview_tObsC)
apply (frule spr_jview_tObsC)
apply (simp add: tObsC_def)
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (frule tObsC_tStep_eq_inv)
apply clarsimp
apply (drule spr_jview_tObsC) back
apply (simp add: tObsC_def)
done
qed
qed
text‹
The explicit-state approach sketched above is quite inefficient, and
also some distance from the symbolic techniques we use in
\S\ref{sec:kbps-prag-algorithmics}. However it does suffice to
demonstrate the theory on the muddy children example in
\S\ref{sec:kbps-theory-mc}.
›
end
subsubsection‹Maps›
text‹
As always we use a pair of tries. The domain of these maps is the pair
of relations.
›
type_synonym ('a, 'es, 'obs, 'as) trans_trie
= "(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState,
('obs, ('a, 'es, 'as) spr_simWorldsRep) mapping) trie) trie) trie) trie"
type_synonym
('a, 'es, 'aAct, 'as) acts_trie
= "(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState,
(('a, 'es, 'as) BEState, 'aAct) trie) trie) trie) trie"
definition
trans_MapOps_lookup :: "('a :: linorder, 'es :: linorder, 'obs, 'as :: linorder) trans_trie
⇒ ('a, 'es, 'as) spr_simWorldsRep × 'obs
⇀ ('a, 'es, 'as) spr_simWorldsRep"
where
"trans_MapOps_lookup ≡ λm ((cec, aec), obs).
Option.bind (lookup_trie m (map fst (toList cec)))
(λm. Option.bind (lookup_trie m (map snd (toList cec)))
(λm. Option.bind (lookup_trie m (map fst (toList aec)))
(λm. Option.bind (lookup_trie m (map snd (toList aec)))
(λm. Mapping.lookup m obs))))"
definition
trans_MapOps_update :: "('a, 'es, 'as) spr_simWorldsRep × 'obs
⇒ ('a, 'es, 'as) spr_simWorldsRep
⇒ ('a :: linorder, 'es :: linorder, 'obs, 'as :: linorder) trans_trie
⇒ ('a, 'es, 'obs, 'as) trans_trie"
where
"trans_MapOps_update ≡ λ((cec, aec), obs) v m.
trie_update_with' (map fst (toList cec)) m empty_trie
(λm. trie_update_with' (map snd (toList cec)) m empty_trie
(λm. trie_update_with' (map fst (toList aec)) m empty_trie
(λm. trie_update_with' (map snd (toList aec)) m Mapping.empty
(λm. Mapping.update obs v m))))"
definition
trans_MapOps :: "(('a :: linorder, 'es :: linorder, 'obs, 'as :: linorder) trans_trie,
('a, 'es, 'as) spr_simWorldsRep × 'obs,
('a, 'es, 'as) spr_simWorldsRep) MapOps"
where
"trans_MapOps ≡
⦇ MapOps.empty = empty_trie,
lookup = trans_MapOps_lookup,
update = trans_MapOps_update ⦈"
lemma (in FiniteDetBroadcastEnvironment) trans_MapOps[intro, simp]:
"MapOps (λk. (spr_simAbs (fst k), snd k)) (SPRdet.jkbpSEC × UNIV) trans_MapOps"
proof
fix k show "MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None"
unfolding trans_MapOps_def trans_MapOps_lookup_def
by (auto split: prod.split)
next
fix e k k' M
assume k: "(spr_simAbs (fst k), snd k) ∈ SPRdet.jkbpSEC × (UNIV :: 'z set)"
and k': "(spr_simAbs (fst k'), snd k') ∈ SPRdet.jkbpSEC × (UNIV :: 'z set)"
show "MapOps.lookup trans_MapOps (MapOps.update trans_MapOps k e M) k'
= (if (spr_simAbs (fst k'), snd k') = (spr_simAbs (fst k), snd k)
then Some e else MapOps.lookup trans_MapOps M k')"
proof(cases "(spr_simAbs (fst k'), snd k') = (spr_simAbs (fst k), snd k)")
case True hence "k = k'"
using inj_onD[OF spr_simAbs_inj_on] k k' by (auto iff: prod_eqI)
thus ?thesis
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def
by (auto simp: lookup_update lookup_trie_update_with split: option.split prod.split)
next
have *: "⋀ y ya. y ≠ ya ⟹ Mapping.lookup (Mapping.update y e Mapping.empty) ya = None" by transfer simp
case False thus ?thesis
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def
by (auto dest: map_prod_eq simp: lookup_trie_update_with split: option.split prod.split intro!: lookup_update_neq *)
qed
qed
definition
acts_MapOps_lookup :: "('a :: linorder, 'es :: linorder, 'aAct, 'as :: linorder) acts_trie
⇒ ('a, 'es, 'as) spr_simWorldsRep
⇀ 'aAct"
where
"acts_MapOps_lookup ≡ λm (cec, aec).
Option.bind (lookup_trie m (map fst (toList cec)))
(λm. Option.bind (lookup_trie m (map snd (toList cec)))
(λm. Option.bind (lookup_trie m (map fst (toList aec)))
(λm. lookup_trie m (map snd (toList aec)))))"
definition
acts_MapOps_update :: "('a, 'es, 'as) spr_simWorldsRep
⇒ 'aAct
⇒ ('a :: linorder, 'es :: linorder, 'aAct, 'as :: linorder) acts_trie
⇒ ('a, 'es, 'aAct, 'as) acts_trie"
where
"acts_MapOps_update ≡ λ(cec, aec) pAct m.
trie_update_with' (map fst (toList cec)) m empty_trie
(λm. trie_update_with' (map snd (toList cec)) m empty_trie
(λm. trie_update_with' (map fst (toList aec)) m empty_trie
(λm. trie_update (map snd (toList aec)) pAct m)))"
definition
acts_MapOps :: "(('a :: linorder, 'es :: linorder, 'aAct, 'as :: linorder) acts_trie,
('a, 'es, 'as) spr_simWorldsRep,
'aAct) MapOps"
where
"acts_MapOps ≡
⦇ MapOps.empty = empty_trie,
lookup = acts_MapOps_lookup,
update = acts_MapOps_update ⦈"
lemma (in FiniteDetBroadcastEnvironment) acts_MapOps[intro, simp]:
"MapOps spr_simAbs SPRdet.jkbpSEC acts_MapOps"
proof
fix k show "MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None"
unfolding acts_MapOps_def acts_MapOps_lookup_def by auto
next
fix e k k' M
assume k: "spr_simAbs k ∈ SPRdet.jkbpSEC"
and k': "spr_simAbs k' ∈ SPRdet.jkbpSEC"
show "MapOps.lookup acts_MapOps (MapOps.update acts_MapOps k e M) k'
= (if spr_simAbs k' = spr_simAbs k
then Some e else MapOps.lookup acts_MapOps M k')"
proof(cases "spr_simAbs k' = spr_simAbs k")
case True hence "k = k'"
using inj_onD[OF spr_simAbs_inj_on] k k' by (auto iff: prod_eqI)
thus ?thesis
unfolding acts_MapOps_def acts_MapOps_lookup_def acts_MapOps_update_def
by (auto simp: lookup_trie_update_with lookup_trie_update split: option.split prod.split)
next
case False thus ?thesis
unfolding acts_MapOps_def acts_MapOps_lookup_def acts_MapOps_update_def
by (auto dest: map_prod_eq simp: lookup_trie_update_with lookup_trie_update split: option.split prod.split)
qed
qed
text‹
This suffices to placate the @{term "Algorithm"} locale.
›
sublocale FiniteDetBroadcastEnvironment
< SPRdet: Algorithm
jkbp envInit envAction envTrans envVal
spr_jview envObs spr_jviewInit spr_jviewIncr
spr_sim spr_simRels spr_simVal
spr_simAbs spr_simObs spr_simInit spr_simTrans spr_simAction
acts_MapOps trans_MapOps
apply (unfold_locales)
using spr_simInit
apply auto[1]
using spr_simObs
apply auto[1]
using spr_simAction
apply auto[1]
using spr_simTrans
apply auto[1]
apply (rule acts_MapOps)
apply (rule trans_MapOps)
done
definition
"mkSPRDetAuto ≡ λagents jkbp envInit envAction envTrans envVal envObsC envObs.
mkAlgAuto acts_MapOps
trans_MapOps
(spr_simObs envObsC)
(spr_simInit envInit envObsC envObs)
(spr_simTrans agents jkbp envAction envTrans envVal envObsC envObs)
(spr_simAction jkbp envVal envObs)
(λa. map (spr_simInit envInit envObsC envObs a ∘ envObs a) envInit)"
lemma (in FiniteDetBroadcastEnvironment) mkSPRDetAuto_implements:
"SPR.implements (mkSPRDetAuto agents jkbp envInit envAction envTrans envVal envObsC envObs)"
using SPRdet.k_mkAlgAuto_implements
unfolding mkSPRDetAuto_def mkAlgAuto_def SPRdet.k_frontier_def
by simp
definition
"SPRDetAutoDFS ≡ λagents jkbp envInit envAction envTrans envVal envObsC envObs. λa.
alg_dfs acts_MapOps
trans_MapOps
(spr_simObs envObsC a)
(spr_simTrans agents jkbp envAction envTrans envVal envObsC envObs a)
(spr_simAction jkbp envVal envObs a)
(map (spr_simInit envInit envObsC envObs a ∘ envObs a) envInit)"
lemma (in FiniteDetBroadcastEnvironment)
"mkSPRDetAuto agents jkbp envInit envAction envTrans envVal envObsC envObs
= (λa. alg_mk_auto acts_MapOps trans_MapOps
(spr_simInit a)
(SPRDetAutoDFS agents jkbp envInit envAction envTrans envVal envObsC envObs a))"
unfolding mkSPRDetAuto_def mkAlgAuto_def SPRDetAutoDFS_def alg_mk_auto_def by (simp add: Let_def)
text‹
As we remarked earlier in this section, in general it may be difficult
to establish the determinacy of a KBP as it is a function of the
environment. However in many cases determinism is syntactically
manifest as the guards are logically disjoint, independently of the
knowledge subformulas. The following lemma generates the required
proof obligations for this case:
›
lemma (in PreEnvironmentJView) jkbpDetI:
assumes tC: "t ∈ jkbpC"
assumes jkbpSynDet: "∀a. distinct (map guard (jkbp a))"
assumes jkbpSemDet: "∀a gc gc'.
gc ∈ set (jkbp a) ∧ gc' ∈ set (jkbp a) ∧ t ∈ jkbpC
⟶ guard gc = guard gc' ∨ ¬(MC, t ⊨ guard gc ∧ MC, t ⊨ guard gc')"
shows "length (jAction MC t a) ≤ 1"
proof -
{ fix a X
assume "set X ⊆ set (jkbp a)"
and "distinct (map guard X)"
with tC have "length [ action gc . gc ← X, MC, t ⊨ guard gc ] ≤ 1"
apply (induct X)
using jkbpSemDet[rule_format, where a=a]
apply auto
done }
from this[OF subset_refl jkbpSynDet[rule_format]] show ?thesis
unfolding jAction_def by simp
qed
text‹
The scenario presented here is a variant of the broadcast environments
treated by \<^citet>‹"Ron:1996"›, which we cover in the next section.
\FloatBarrier
›
end