(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

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}

  capture our expectations of a single-agent scenario in the
  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‹

  per the clock semantics of \S\ref{sec:kbps-theory-clock-view}, we
  that the set of states is finite and linearly ordered. We give
  sole agent the name ‹agent›.

  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
  agent considers possible relative to a trace and the SPR view. The
  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‹

  Kripke structure for this simulation relates worlds for @{term
 agent"} if the sets of states it considers possible coincide, and the
  of the final states of the trace is the same. Propositions
  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 (auto(*<*)iff: 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‹

  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 (* context FiniteSingleAgentEnvironment *)

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}

  in \S\ref{sec:kbps-theory-clock-view-algops}, we quotient @{typ "'s
 "} by @{term "spr_simRels"}. Because there is only a
  agent, an element of this quotient corresponding to a cononical
  @{term "t"} is isomorphic to the set of states that are possible
  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‹

  is very easy to map these representations back to simulated
  classes:

 ›

definition
  spr_simAbs :: "'s spr_simWorldsRep → 's spr_simWorlds set"
where
  "spr_simAbs ≡ λss. { (toSet ss, s) |s. s ∈ toSet ss }"

text‹

  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‹

  again make use of the following Kripke structure, where the worlds
  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‹

  we show that this Kripke structure is adequate by
  an intermediate structure and connecting them all with a
  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‹

  before, the following sections discharge the requirements of the
 ‹Algorithm› locale of Figure~\ref{fig:kbps-alg-alg-locale}.

 ›

(* **************************************** *)

subsubsection‹Initial states›

text‹

  initial states of the automaton for @{term "agent"} is simply the
  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‹

  the agent makes the same observation on the entire equivalence
 , 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}

  the single-agent case is much simpler than the multi-agent ones, we
  an evaluation function specialised to its representation.

  @{term "eval"} yields the subset of @{term "X"} where the
  holds, where @{term "X"} is taken to be a representation of a
  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‹

  general this is less efficient than the tableau approach of
 🚫‹‹Proposition~3.2.1› in "FHMV:1995"›, which labels all states with all
 . However it is often the case that the set of relevant worlds
  much smaller than the set of all system states.

  that this corresponds with the standard models relation is
 .

 ›
(*<*)

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‹

  actions enabled on a canonical equivalence class are those for
  @{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‹

  key lemma relates the agent's behaviour on an equivalence class to
  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 (* FIXME improve *)
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)<sup>*</sup>"
    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)<sup>*</sup> `` {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)<sup>*</sup> `` {s} ⊆ ?X"
    using sim_trc_commute[OF SPR.mkM_kripke spr_sim, where t=t'] by simp
qed (insert s, auto)

(*>*)
text‹

  ‹Algorithm› locale requires the following lemma, which is
  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‹

  is straightforward to determine the possible successor states of a
  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‹

  this function we can determine the set of possible successor
  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‹

  ‹partition› function splits a list into equivalence
  under the given equivalence relation.

  property asked for by the ‹Algorithm› locale follows from
  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

     (* left to right *)

     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

     (* right to left *)

     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 (* context FiniteSingleAgentEnvironment *)

(* **************************************** *)

subsubsection‹Maps›

text‹

 label{sec:kbps-theory-spr-single-maps}

  in \S\ref{sec:kbps-theory-clock-view-maps}, we use a pair of tries
  an association list to handle the automata representation. Recall
  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‹

  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 inj_on_subset[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

(*

We actually run this unfolding of the algorithm. The lemma is keeping
us honest.

*)

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‹

  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
(*>*)