Theory SPRViewSingle
theory SPRViewSingle
imports
KBPsAlg
SPRView
List_local
ODList
Trie2
"HOL-Library.Mapping"
begin
subsection‹Perfect Recall for a Single Agent›
text‹
\label{sec:kbps-spr-single-agent}
We capture our expectations of a single-agent scenario in the
following locale:
›
locale FiniteSingleAgentEnvironment =
FiniteEnvironment jkbp envInit envAction envTrans envVal envObs
for jkbp :: "('a, 'p, 'aAct) JKBP"
and envInit :: "('s :: {finite, linorder}) list"
and envAction :: "'s ⇒ 'eAct list"
and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's"
and envVal :: "'s ⇒ 'p ⇒ bool"
and envObs :: "'a ⇒ 's ⇒ 'obs"
+ fixes agent :: "'a"
assumes envSingleAgent: "a = agent"
text‹
As per the clock semantics of \S\ref{sec:kbps-theory-clock-view}, we
assume that the set of states is finite and linearly ordered. We give
the sole agent the name ‹agent›.
Our simulation is quite similar to the one for the clock semantics of
\S\ref{sec:kbps-theory-clock-view}: it records the set of worlds that
the agent considers possible relative to a trace and the SPR view. The
key difference is that it is path-sensitive:
›
context FiniteSingleAgentEnvironment
begin
definition spr_abs :: "'s Trace ⇒ 's set" where
"spr_abs t ≡
tLast ` { t' ∈ SPR.jkbpC . spr_jview agent t' = spr_jview agent t }"
type_synonym (in -) 's spr_simWorlds = "'s set × 's"
definition spr_sim :: "'s Trace ⇒ 's spr_simWorlds" where
"spr_sim ≡ λt. (spr_abs t, tLast t)"
lemma spr_absI[elim]:
"⟦ t' ∈ SPR.jkbpC; spr_jview a t' = spr_jview a t; v = tLast t' ⟧
⟹ v ∈ spr_abs t"
unfolding spr_abs_def
using envSingleAgent[where a=a] by blast
lemma spr_abs_tLastD[simp]:
"v ∈ spr_abs t ⟹ envObs a v = envObs a (tLast t)"
unfolding spr_abs_def
using envSingleAgent[where a=a] by auto
lemma spr_abs_conv:
"v ∈ spr_abs t
⟷ (∃t'. t' ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t ∧ v = tLast t')"
unfolding spr_abs_def
using envSingleAgent[where a=a] by blast
lemma spr_abs_eq[dest]:
"spr_jview a t = spr_jview a t' ⟹ spr_abs t = spr_abs t'"
unfolding spr_abs_def
using envSingleAgent[where a=a] by auto
lemma spr_abs_refl[intro, simp]:
"t ∈ SPR.jkbpC ⟹ tLast t ∈ spr_abs t"
unfolding spr_abs_def
using envSingleAgent[where a=a] by auto
lemma spr_sim_simps[simp]:
"fst (spr_sim t) = spr_abs t"
unfolding spr_sim_def by simp
text‹
The Kripke structure for this simulation relates worlds for @{term
"agent"} if the sets of states it considers possible coincide, and the
observation of the final states of the trace is the same. Propositions
are evaluated at the final state.
›
definition spr_simRels :: "'a ⇒ 's spr_simWorlds Relation" where
"spr_simRels ≡ λa. { ((U, u), (V, v)) |U u V v.
U = V ∧ {u, v} ⊆ U ∧ envObs a u = envObs a v }"
definition spr_simVal :: "'s spr_simWorlds ⇒ 'p ⇒ bool" where
"spr_simVal ≡ envVal ∘ snd"
abbreviation spr_simMC :: "('a, 'p, 's spr_simWorlds) KripkeStructure" where
"spr_simMC ≡ mkKripke (spr_sim ` SPR.jkbpC) spr_simRels spr_simVal"
lemma spr_simVal[iff]:
"spr_simVal (spr_sim t) = envVal (tLast t)"
unfolding spr_sim_def spr_simVal_def by simp
lemma spr_sim_r:
"sim_r SPR.MC spr_simMC spr_sim"
proof
fix a t v'
assume t: "t ∈ worlds SPR.MC"
and tv': "(spr_sim t, v') ∈ relations spr_simMC a"
from tv' obtain s
where vv': "v' = (spr_abs t, s)"
and st: "s ∈ spr_abs t"
unfolding spr_simRels_def spr_sim_def mkKripke_def SPR.mkM_def
by auto
from st obtain v
where "v ∈ SPR.jkbpC"
and "spr_jview a v = spr_jview a t"
and "tLast v = s"
by (autoiff: spr_abs_conv)
with t vv'
have "(t, v) ∈ relations SPR.MC a"
and "spr_sim v = v'"
unfolding spr_simRels_def spr_sim_def mkKripke_def SPR.mkM_def
by auto
thus "∃v. (t, v) ∈ relations SPR.MC a ∧ spr_sim v = v'" by blast
qed
text‹
Demonstrating that this is a simulation
(\S\ref{sec:kripke-theory-simulations}) is straightforward.
›
lemma spr_sim: "sim SPR.MC spr_simMC spr_sim"
proof
show "sim_f SPR.MC spr_simMC spr_sim"
unfolding spr_simRels_def spr_sim_def mkKripke_def SPR.mkM_def
by (rule) auto
next
show "sim_r SPR.MC spr_simMC spr_sim"
by (rule spr_sim_r)
qed auto
text‹›
end
sublocale FiniteSingleAgentEnvironment
< SPRsingle: 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‹
\label{sec:kbps-theory-spr-single-rep}
As in \S\ref{sec:kbps-theory-clock-view-algops}, we quotient @{typ "'s
spr_simWorlds"} by @{term "spr_simRels"}. Because there is only a
single agent, an element of this quotient corresponding to a cononical
trace @{term "t"} is isomorphic to the set of states that are possible
given the sequence of observations made by @{term "agent"} on @{term
"t"}. Therefore we have a very simple representation:
›
context FiniteSingleAgentEnvironment
begin
type_synonym (in -) 's spr_simWorldsRep = "'s odlist"
text‹
It is very easy to map these representations back to simulated
equivalence classes:
›
definition
spr_simAbs :: "'s spr_simWorldsRep ⇒ 's spr_simWorlds set"
where
"spr_simAbs ≡ λss. { (toSet ss, s) |s. s ∈ toSet ss }"
text‹
This time our representation is unconditionally canonical:
›
lemma spr_simAbs_inj: "inj spr_simAbs"
apply (rule injI)
unfolding spr_simAbs_def
apply (subgoal_tac "toSet x = toSet y")
apply auto
using toSet_inj
apply (erule injD)
done
lemma spr_sim_rep_abs[simp]:
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class a t"
shows "toSet ec = spr_abs t"
proof
show "toSet ec ⊆ spr_abs t"
proof
fix x assume x: "x ∈ toSet ec"
hence "(toSet ec, x) ∈ spr_simAbs ec"
unfolding spr_simAbs_def by simp
with ec have "(toSet ec, x) ∈ SPRsingle.sim_equiv_class a t"
by simp
with x envSingleAgent[where a=a] show "x ∈ spr_abs t"
unfolding spr_sim_def spr_abs_def by auto
qed
next
show "spr_abs t ⊆ toSet ec"
proof
fix x assume x: "x ∈ spr_abs t"
with ec envSingleAgent[where a=a] show "x ∈ toSet ec"
unfolding spr_simAbs_def spr_sim_def spr_abs_def by auto
qed
qed
lemma spr_sim_rep_abs_syn[simp]:
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
shows "set (toList ec) = spr_abs t"
using spr_sim_rep_abs[OF ec] unfolding toSet_def by simp
lemma spr_simAbs_list:
"spr_simAbs ` fromList ` X = (λss. { (ss, s) |s. s ∈ ss }) ` set ` X"
unfolding spr_simAbs_def Set.image_def by auto
text‹
We again make use of the following Kripke structure, where the worlds
are the final states of the subset of the temporal slice that @{term
"agent"} believes possible:
›
definition spr_repRels :: "'a ⇒ ('s × 's) set" where
"spr_repRels ≡ λa. { (s, s'). envObs a s' = envObs a s }"
abbreviation spr_repMC :: "'s set ⇒ ('a, 'p, 's) KripkeStructure" where
"spr_repMC ≡ λX. mkKripke X spr_repRels envVal"
text‹
Similarly we show that this Kripke structure is adequate by
introducing an intermediate structure and connecting them all with a
tower of simulations:
›
abbreviation spr_jkbpCSt :: "'s Trace ⇒ 's spr_simWorlds set" where
"spr_jkbpCSt t ≡ SPRsingle.sim_equiv_class agent t"
abbreviation
spr_simMCt :: "'s Trace ⇒ ('a, 'p, 's spr_simWorlds) KripkeStructure"
where
"spr_simMCt t ≡ mkKripke (spr_jkbpCSt t) spr_simRels spr_simVal"
definition spr_repSim :: "'s spr_simWorlds ⇒ 's" where
"spr_repSim ≡ snd"
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
lemma jkbpCSt_jkbpCS_subset:
"SPRsingle.sim_equiv_class agent t ⊆ spr_sim ` SPR.jkbpC"
by auto
lemma spr_simRep_sim_simps[simp]:
"spr_repSim ` spr_sim ` T = tLast ` T"
"spr_repSim (spr_sim t) = tLast t"
unfolding spr_repSim_def spr_sim_def Set.image_def by auto
text‹›
lemma spr_repSim:
assumes tC: "t ∈ SPR.jkbpC"
shows "sim (spr_simMCt t)
((spr_repMC ∘ fst) (spr_sim t))
spr_repSim"
(is "sim ?M ?M' ?f")
proof
show "sim_range ?M ?M' ?f"
proof
show "worlds ?M' = ?f ` worlds ?M"
unfolding spr_sim_def spr_repSim_def spr_abs_def Set.image_def
by auto
next
fix a
show "relations ?M' a ⊆ worlds ?M' × worlds ?M'"
unfolding spr_sim_def spr_repSim_def by simp
qed
next
show "sim_val ?M ?M' ?f"
unfolding spr_sim_def spr_simVal_def spr_repSim_def by auto
next
from tC
show "sim_f ?M ?M' ?f"
unfolding spr_sim_def spr_simVal_def spr_repSim_def
apply -
apply rule
apply (cut_tac a=a in envSingleAgent)
apply (auto iff: spr_sim_def spr_repRels_def)
apply (rule spr_tLast)
apply auto
done
next
show "sim_r ?M ?M' ?f"
unfolding spr_sim_def spr_simVal_def spr_repSim_def
apply -
apply rule
apply (cut_tac a=a in envSingleAgent)
unfolding spr_abs_def spr_sim_def spr_repRels_def spr_simRels_def Set.image_def
apply auto
done
qed
text‹
As before, the following sections discharge the requirements of the
‹Algorithm› locale of Figure~\ref{fig:kbps-alg-alg-locale}.
›
subsubsection‹Initial states›
text‹
The initial states of the automaton for @{term "agent"} is simply the
partition of @{term "envInit"} under @{term "agent"}'s observation.
›
definition (in -)
spr_simInit :: "('s :: linorder) list ⇒ ('a ⇒ 's ⇒ 'obs)
⇒ 'a ⇒ 'obs ⇒ 's spr_simWorldsRep"
where
"spr_simInit envInit envObs ≡ λa iobs.
ODList.fromList [ s. s ← envInit, envObs a s = iobs ]"
abbreviation
spr_simInit :: "'a ⇒ 'obs ⇒ 's spr_simWorldsRep"
where
"spr_simInit ≡ SPRViewSingle.spr_simInit envInit 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
using envSingleAgent[where a=a]
unfolding spr_simAbs_def spr_sim_def [abs_def] spr_abs_def
apply (auto iff: spr_jview_def SPR.jviewInit)
apply (rule_tac x="tInit s" in image_eqI)
apply (auto iff: spr_jview_def)[1]
apply (rule_tac x="tInit xa" in image_eqI)
apply auto[1]
apply simp
apply simp
apply (rule_tac x="tInit xb" in image_eqI)
apply auto
done
subsubsection‹Simulated observations›
text‹
As the agent makes the same observation on the entire equivalence
class, we arbitrarily choose the first element of the representation:
›
definition (in -)
spr_simObs :: "('a ⇒ 's ⇒ 'obs)
⇒ 'a ⇒ ('s :: linorder) spr_simWorldsRep ⇒ 'obs"
where
"spr_simObs envObs ≡ λa. envObs a ∘ ODList.hd"
abbreviation
spr_simObs :: "'a ⇒ 's spr_simWorldsRep ⇒ 'obs"
where
"spr_simObs ≡ SPRViewSingle.spr_simObs envObs"
text‹›
lemma spr_simObs:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class a t"
shows "spr_simObs a ec = envObs a (tLast t)"
proof -
have A: "∀s ∈ set (toList ec). envObs a s = envObs a (tLast t)"
using spr_sim_rep_abs[OF ec] by (simp add: toSet_def)
from tC ec have B: "tLast t ∈ set (toList ec)"
using envSingleAgent[where a=a] by simp
show ?thesis
unfolding spr_simObs_def
by (simp add: list_choose_hd[OF A B] ODList.hd_def)
qed
subsubsection‹Evaluation›
text‹
\label{sec:kbps-spr-single-agent-eval}
As the single-agent case is much simpler than the multi-agent ones, we
define an evaluation function specialised to its representation.
Intuitively @{term "eval"} yields the subset of @{term "X"} where the
formula holds, where @{term "X"} is taken to be a representation of a
canonical equivalence class for @{term "agent"}.
›
fun (in -)
eval :: "(('s :: linorder) ⇒ 'p ⇒ bool)
⇒ 's odlist ⇒ ('a, 'p) Kform ⇒ 's odlist"
where
"eval val X (Kprop p) = ODList.filter (λs. val s p) X"
| "eval val X (Knot φ) = ODList.difference X (eval val X φ)"
| "eval val X (Kand φ ψ) = ODList.intersect (eval val X φ) (eval val X ψ)"
| "eval val X (Kknows a φ) = (if eval val X φ = X then X else ODList.empty)"
| "eval val X (Kcknows as φ) =
(if as = [] ∨ eval val X φ = X then X else ODList.empty)"
text‹
In general this is less efficient than the tableau approach of
\<^citet>‹‹Proposition~3.2.1› in "FHMV:1995"›, which labels all states with all
formulas. However it is often the case that the set of relevant worlds
is much smaller than the set of all system states.
Showing that this corresponds with the standard models relation is
routine.
›
lemma eval_ec_subseteq:
shows "toSet (eval envVal ec φ) ⊆ toSet ec"
by (induct φ) auto
lemma eval_models_aux:
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
assumes s: "s ∈ toSet ec"
shows "s ∈ toSet (eval envVal ec φ) ⟷ spr_repMC (toSet ec), s ⊨ φ"
using s
proof(induct φ arbitrary: s)
case (Kknows a φ s) with ec envSingleAgent[where a=a] show ?case
unfolding spr_repRels_def
by (auto simp: inj_eq[OF toSet_inj, symmetric] dest: subsetD[OF eval_ec_subseteq])
next
case (Kcknows as φ s)
from ec show ?case
proof(cases as)
case Nil with Kcknows show ?thesis by clarsimp
next
case (Cons x xs)
hence "set as = {agent}"
by (induct as) (auto simp: envSingleAgent)
moreover
have "(spr_repRels agent ∩ toSet ec × toSet ec)⇧+ = (spr_repRels agent ∩ toSet ec × toSet ec)"
by (rule trancl_id) (simp add: spr_repRels_def trans_def)
moreover note Kcknows ec
ultimately show ?thesis
unfolding spr_repRels_def
by (auto simp: inj_eq[OF toSet_inj, symmetric] dest: subsetD[OF eval_ec_subseteq])
qed
qed simp_all
lemma eval_all_or_nothing:
assumes subj_phi: "subjective agent φ"
shows "toSet (eval envVal ec φ) = {} ∨ toSet (eval envVal ec φ) = toSet ec"
using subj_phi by (induct φ rule: subjective.induct) auto
lemma eval_models:
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
assumes subj: "subjective agent φ"
assumes s: "s ∈ toSet ec"
shows "toSet (eval envVal ec φ) ≠ {} ⟷ spr_repMC (toSet ec), s ⊨ φ"
using eval_models_aux[OF ec s, symmetric] eval_all_or_nothing[OF subj] s
by auto
subsubsection‹Simulated actions›
text‹
The actions enabled on a canonical equivalence class are those for
which @{term "eval"} yields a non-empty set of states:
›
definition (in -)
spr_simAction :: "('a, 'p, 'aAct) KBP ⇒ (('s :: linorder) ⇒ 'p ⇒ bool)
⇒ 'a ⇒ 's spr_simWorldsRep ⇒ 'aAct list"
where
"spr_simAction kbp envVal ≡ λa X.
[ action gc. gc ← kbp, eval envVal X (guard gc) ≠ ODList.empty ]"
abbreviation
spr_simAction :: "'a ⇒ 's spr_simWorldsRep ⇒ 'aAct list"
where
"spr_simAction ≡ SPRViewSingle.spr_simAction (jkbp agent) envVal"
text‹
The key lemma relates the agent's behaviour on an equivalence class to
that on its representation:
›
lemma spr_simAction_jAction:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
shows "set (spr_simAction agent ec)
= set (jAction (spr_repMC (toSet ec)) (tLast t) agent)"
proof -
have "⋀P. (set (jkbp agent) ∩ {gc. P gc})
= { gc ∈ set (jkbp agent). P gc }"
by blast
then
show ?thesis
unfolding spr_simAction_def jAction_def
apply clarsimp
apply (rule SUP_cong)
apply simp_all
apply (rule Collect_cong)
apply rule
apply clarsimp
apply (subst eval_models[OF ec, symmetric])
apply (simp_all add: toSet_eq_iff)
using subj tC ec
apply (fastforce+)[2]
apply clarsimp
apply (subst (asm) eval_models[OF ec, symmetric])
using subj tC ec
apply fastforce+
done
qed
lemma spr_submodel_aux:
assumes tC: "t ∈ SPR.jkbpC"
and s: "s ∈ worlds (spr_simMCt t)"
shows "gen_model SPRsingle.MCS s = gen_model (spr_simMCt t) s"
proof(rule gen_model_subset[where T="SPRsingle.sim_equiv_class agent t"])
fix a
let ?X = "SPRsingle.sim_equiv_class agent t"
show "relations SPRsingle.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 = "SPRsingle.sim_equiv_class agent t"
from s show "(⋃a. relations (spr_simMCt t) a)⇧* `` {s} ⊆ ?X"
apply (clarsimp simp del: mkKripke_simps)
apply (erule kripke_rels_trc_worlds)
apply auto
done
next
let ?Y = "{ t' ∈ SPR.jkbpC . spr_jview agent t' = spr_jview agent 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: "spr_jview agent t = spr_jview agent 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 tt' t'O have t''O: "spr_jview agent t = spr_jview agent t''"
apply induct
unfolding SPR.mkM_def
apply auto
apply (cut_tac a=x in envSingleAgent)
apply simp
done
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 SPRsingle.MCS a)⇧* `` {s} ⊆ ?X"
using sim_trc_commute[OF SPR.mkM_kripke spr_sim, where t=t'] by simp
qed (insert s, auto)
text‹
The ‹Algorithm› locale requires the following lemma, which is
a straightforward chaining of the above simulations.
›
lemma spr_simAction:
assumes tC: "t ∈ SPR.jkbpC"
and ec: "spr_simAbs ec = SPRsingle.sim_equiv_class a t"
shows "set (spr_simAction a ec) = set (jAction SPR.MC t a)"
proof -
from ec
have ec': "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
by (simp only: envSingleAgent[where a=a])
have "set (spr_simAction a ec) = set (spr_simAction agent ec)"
by (simp only: envSingleAgent[where a=a])
also from tC ec' have "... = set (jAction (spr_repMC (toSet ec)) (tLast t) agent)"
by (rule spr_simAction_jAction)
also from tC ec' have "... = set (jAction (spr_simMCt t) (spr_sim t) agent)"
by (simp add: simulation_jAction_eq[OF _ spr_repSim])
also from tC have "... = set (jAction SPRsingle.MCS (spr_sim t) agent)"
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 agent)"
by (simp add: simulation_jAction_eq[OF _ spr_sim])
finally show ?thesis by (simp only: envSingleAgent[where a=a])
qed
subsubsection‹Simulated transitions›
text‹
It is straightforward to determine the possible successor states of a
given canonical equivalence class @{term "X"}:
›
definition (in -)
spr_trans :: "('a, 'p, 'aAct) KBP
⇒ ('s ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's)
⇒ ('s ⇒ 'p ⇒ bool)
⇒ 'a ⇒ ('s :: linorder) spr_simWorldsRep ⇒ 's list"
where
"spr_trans kbp envAction envTrans val ≡ λa X.
[ envTrans eact (λa'. aact) s .
s ← toList X, eact ← envAction s, aact ← spr_simAction kbp val a X ]"
abbreviation
spr_trans :: "'a ⇒ 's spr_simWorldsRep ⇒ 's list"
where
"spr_trans ≡ SPRViewSingle.spr_trans (jkbp agent) envAction envTrans envVal"
text‹
Using this function we can determine the set of possible successor
equivalence classes from @{term "X"}:
›
abbreviation (in -) envObs_rel :: "('s ⇒ 'obs) ⇒ 's × 's ⇒ bool" where
"envObs_rel envObs ≡ λ(s, s'). envObs s' = envObs s"
definition (in -)
spr_simTrans :: "('a, 'p, 'aAct) KBP
⇒ (('s::linorder) ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's)
⇒ ('s ⇒ 'p ⇒ bool)
⇒ ('a ⇒ 's ⇒ 'obs)
⇒ 'a ⇒ 's spr_simWorldsRep ⇒ 's spr_simWorldsRep list"
where
"spr_simTrans kbp envAction envTrans val envObs ≡ λa X.
map ODList.fromList (partition (envObs_rel (envObs a))
(spr_trans kbp envAction envTrans val a X))"
abbreviation
spr_simTrans :: "'a ⇒ 's spr_simWorldsRep ⇒ 's spr_simWorldsRep list"
where
"spr_simTrans ≡ SPRViewSingle.spr_simTrans (jkbp agent) envAction envTrans envVal envObs"
lemma envObs_rel_equiv:
"equiv UNIV (rel_ext (envObs_rel (envObs agent)))"
by (intro equivI refl_onI symI transI) auto
lemma spr_trans:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
shows "set (spr_trans agent ec)
= { s |t' s. t' ↝ s ∈ SPR.jkbpC ∧ spr_jview agent t' = spr_jview agent 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)
apply (frule spr_sim_rep_abs)
unfolding toSet_def
apply clarsimp
apply (simp only: spr_abs_conv[where a=agent])
apply clarify
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 (rule_tac x=xa in exI)
apply (rule_tac x="λa'. aact" in exI)
apply auto
apply (subst envSingleAgent)
apply (simp add: spr_simAction[where a=agent])
apply (subst SPR.jkbpC_jkbpCn_jAction_eq[symmetric])
apply auto
apply (subst S5n_jAction_eq[where w'=t])
apply simp_all
unfolding SPR.mkM_def
apply simp
done
qed
next
show "?rhs ⊆ ?lhs"
proof
fix s assume s: "s ∈ ?rhs"
then obtain t'
where t'sC: "t' ↝ s ∈ SPR.jkbpC"
and tt': "spr_jview agent t' = spr_jview agent 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 ec s eact aact tt' t'sC
show "s ∈ ?lhs"
unfolding spr_trans_def
apply (clarsimp)
apply (rule bexI[where x="tLast t'"])
apply (rule bexI[where x=eact])
apply simp_all
prefer 2
apply (blast intro: spr_absI)
apply (simp add: spr_simAction[where a=agent])
apply (rule image_eqI[where x="aact agent"])
apply (subgoal_tac "(λa'. aact agent) = aact")
apply simp
apply (rule ext)
apply (cut_tac a=a' in envSingleAgent)
apply simp
apply (erule allE[where x=agent])
apply (subst SPR.jkbpC_jkbpCn_jAction_eq)
apply auto
apply (subst S5n_jAction_eq[where w=t and w'=t'])
apply simp
apply (unfold SPR.mkM_def)[1]
apply simp
apply (blast dest: SPR.sync[rule_format])
apply (auto dest: SPR.sync[rule_format])
done
qed
qed
text‹
The ‹partition› function splits a list into equivalence
classes under the given equivalence relation.
The property asked for by the ‹Algorithm› locale follows from
the properties of ‹partition› and ‹spr_trans›:
›
lemma spr_simTrans:
assumes tC: "t ∈ SPR.jkbpC"
assumes ec: "spr_simAbs ec = SPRsingle.sim_equiv_class a t"
shows "spr_simAbs ` set (spr_simTrans a ec)
= { SPRsingle.sim_equiv_class a (t' ↝ s)
|t' s. t' ↝ s ∈ SPR.jkbpC ∧ spr_jview a t' = spr_jview a t}"
(is "?lhs a = ?rhs a")
proof -
from ec have ec': "spr_simAbs ec = SPRsingle.sim_equiv_class agent t"
by (simp only: envSingleAgent[where a=a])
from ec' have "?lhs agent = ?rhs agent"
unfolding spr_simTrans_def
apply clarsimp
apply (simp only: spr_simAbs_list partition[OF envObs_rel_equiv subset_UNIV] spr_trans[OF tC ec'])
apply clarsimp
apply rule
apply clarsimp
apply (erule quotientE)
apply clarsimp
apply (rule_tac x=t' in exI)
apply (rule_tac x=x in exI)
apply clarsimp
apply rule
apply clarsimp
apply (rule_tac x="t'a ↝ s" in image_eqI)
apply (unfold spr_sim_def [abs_def] spr_abs_def)[1]
apply clarsimp
apply (auto iff: spr_jview_def)[1]
apply (rule_tac x="t'c ↝ xa" in image_eqI)
apply simp
apply simp
apply (simp add: spr_jview_def)
apply clarsimp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (rule_tac x=s' in exI)
apply (unfold spr_sim_def [abs_def] spr_abs_def)[1]
apply clarsimp
apply (auto iff: spr_jview_def)[1]
apply (rule_tac x="t'b ↝ xa" in image_eqI)
apply simp
apply simp
apply clarsimp
apply (rule_tac x="spr_abs (t' ↝ s)" in image_eqI)
apply rule
apply clarsimp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (unfold spr_sim_def [abs_def])[1]
apply clarsimp
apply rule
apply (erule spr_abs_eq)
apply (erule spr_absI[where a=agent]) back
apply simp
apply simp
apply clarsimp
apply (simp only: spr_abs_conv[where a=agent])
apply clarsimp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (rule_tac x="t'' ↝ s'" in image_eqI)
apply (unfold spr_sim_def [abs_def])[1]
apply clarsimp
apply blast
apply blast
apply (rule_tac x=s in quotientI2)
apply auto[1]
apply rule
apply clarsimp
apply rule
apply blast
apply (cut_tac v=x and t="t' ↝ s" in spr_abs_conv[where a=agent])
apply clarsimp
apply (frule spr_jview_tStep_eq_inv)
apply clarsimp
apply (rule_tac x=t'' in exI)
apply (simp add: Let_def spr_jview_def)
apply clarsimp
apply (erule spr_absI[where a=agent]) back back
apply (auto iff: spr_jview_def)
done
thus "?lhs a = ?rhs a" by (simp only: envSingleAgent[where a=a])
qed
text‹›
end
subsubsection‹Maps›
text‹
\label{sec:kbps-theory-spr-single-maps}
As in \S\ref{sec:kbps-theory-clock-view-maps}, we use a pair of tries
and an association list to handle the automata representation. Recall
that the keys of these tries are lists of system states.
›
type_synonym ('s, 'obs) spr_trans_trie = "('s, ('obs, 's odlist) mapping) trie"
type_synonym ('s, 'aAct) spr_acts_trie = "('s, ('s, 'aAct) trie) trie"
definition
trans_MapOps_lookup :: "('s::linorder, 'obs) spr_trans_trie
⇒ 's odlist × 'obs ⇀ 's odlist"
where
"trans_MapOps_lookup ≡ λm k.
Option.bind (trie_odlist_lookup m (fst k)) (λm'. Mapping.lookup m' (snd k))"
definition
trans_MapOps_update :: "'s odlist × 'obs ⇒ ('s :: linorder) odlist
⇒ ('s, ('obs, 's odlist) mapping) trie
⇒ ('s, ('obs, 's odlist) mapping) trie"
where
"trans_MapOps_update ≡ λk v m.
trie_odlist_update_with (fst k) m Mapping.empty
(λm. Mapping.update (snd k) v m)"
definition
trans_MapOps :: "(('s :: linorder, ('obs, 's odlist) mapping) trie, 's odlist × 'obs, 's odlist) MapOps"
where
"trans_MapOps ≡
⦇ MapOps.empty = empty_trie,
lookup = trans_MapOps_lookup,
update = trans_MapOps_update ⦈"
lemma (in FiniteSingleAgentEnvironment) trans_MapOps[intro, simp]:
"MapOps (λk. (spr_simAbs (fst k), snd k)) (SPRsingle.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 trie_odlist_lookup_def
by (auto split: prod.split)
next
fix e k k' M
assume k: "(spr_simAbs (fst k), snd k) ∈ SPRsingle.jkbpSEC × (UNIV :: 'z set)"
and k': "(spr_simAbs (fst k'), snd k') ∈ SPRsingle.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 injD[OF spr_simAbs_inj] k k' by (auto iff: prod_eqI)
thus ?thesis
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def trie_odlist_lookup_def trie_odlist_update_with_def
by (simp add: lookup_trie_update_with lookup_update split: option.split prod.split)
next
case False thus ?thesis
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def trie_odlist_lookup_def trie_odlist_update_with_def
by (auto simp: lookup_empty lookup_update_neq lookup_trie_update_with split: option.split prod.split)
qed
qed
subsubsection‹Locale instantiation›
text‹
The above is sufficient to instantiate the @{term "Algorithm"} locale.
›
sublocale FiniteSingleAgentEnvironment
< SPRsingle: 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
trie_odlist_MapOps trans_MapOps
apply (unfold_locales)
using spr_simInit
apply auto[1]
using spr_simObs
apply auto[1]
using spr_simAction
apply blast
using spr_simTrans
apply blast
apply (rule trie_odlist_MapOps[OF subset_inj_on[OF spr_simAbs_inj subset_UNIV]])
apply (rule trans_MapOps)
done
definition
mkSPRSingleAuto :: "('a, 'p, 'aAct) KBP
⇒ ('s :: linorder) list
⇒ ('s ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's)
⇒ ('s ⇒ 'p ⇒ bool)
⇒ ('a ⇒ 's ⇒ 'obs)
⇒ 'a ⇒ ('obs, 'aAct, 's odlist) Protocol"
where
"mkSPRSingleAuto ≡ λkbp envInit envAction envTrans envVal envObs.
mkAlgAuto trie_odlist_MapOps
trans_MapOps
(spr_simObs envObs)
(spr_simInit envInit envObs)
(spr_simTrans kbp envAction envTrans envVal envObs)
(spr_simAction kbp envVal)
(λa. map (spr_simInit envInit envObs a ∘ envObs a) envInit)"
lemma (in FiniteSingleAgentEnvironment) mkSPRSingleAuto_implements:
"SPR.implements (mkSPRSingleAuto (jkbp agent) envInit envAction envTrans envVal envObs)"
using SPRsingle.k_mkAlgAuto_implements
unfolding mkSPRSingleAuto_def mkAlgAuto_def alg_dfs_def SPRsingle.KBP.k_ins_def SPRsingle.KBP.k_empt_def SPRsingle.k_frontier_def SPRsingle.KBP.k_memb_def SPRsingle.KBP.transUpdate_def SPRsingle.KBP.actsUpdate_def
apply simp
done
type_synonym (in -)
('aAct, 'obs, 's) SPRSingleAutoDFS = "(('s, 'aAct list) trie, (('s, ('obs, 's odlist) mapping) trie)) AlgState"
definition
SPRSingleAutoDFS :: "('a, 'p, 'aAct) KBP
⇒ ('s :: linorder) list
⇒ ('s ⇒ 'eAct list)
⇒ ('eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's)
⇒ ('s ⇒ 'p ⇒ bool)
⇒ ('a ⇒ 's ⇒ 'obs)
⇒ 'a ⇒ ('aAct, 'obs, 's) SPRSingleAutoDFS"
where
"SPRSingleAutoDFS ≡ λkbp envInit envAction envTrans envVal envObs. λa.
alg_dfs trie_odlist_MapOps
trans_MapOps
(spr_simObs envObs a)
(spr_simTrans kbp envAction envTrans envVal envObs a)
(spr_simAction kbp envVal a)
(map (spr_simInit envInit envObs a ∘ envObs a) envInit)"
lemma (in FiniteSingleAgentEnvironment)
"mkSPRSingleAuto kbp envInit envAction envTrans envVal envObs
= (λa. alg_mk_auto trie_odlist_MapOps trans_MapOps (spr_simInit a) (SPRSingleAutoDFS kbp envInit envAction envTrans envVal envObs a))"
unfolding mkSPRSingleAuto_def SPRSingleAutoDFS_def mkAlgAuto_def alg_mk_auto_def by (simp add: Let_def)
text‹
We use this theory to synthesise a solution to the robot of
\S\ref{sec:kbps-robot-intro} in \S\ref{sec:kbps-theory-robot}.
›
end