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

theory ClockView
imports
  KBPsAlg
  Eval
  List_local
  ODList
  Trie2
  "Transitive-Closure.Transitive_Closure_List_Impl"
  "HOL-Library.Mapping"
begin
(*>*)

subsection‹The Clock View›

text‹

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

  \emph{clock view} records the current time and the observation for
  most recent state:

 ›

definition (in Environment)
  clock_jview :: "('a, 's, nat × 'obs) JointView"
where
  "clock_jview ≡ λa t. (tLength t, envObs a (tLast t))"
(*<*)

context Environment
begin

lemma clock_jview_tInit:
  "clock_jview a (tInit s) = (0, envObs a s)"
  unfolding clock_jview_def by simp

lemma clock_jview_tStep:
  "clock_jview a (t ↝ s) = (Suc (tLength t), envObs a s)"
  unfolding clock_jview_def by simp

lemma clock_jview_tStepI[intro]:
  "[ tLength t = Suc n; envObs a (tLast t) = obs ]
     ==> clock_jview a t = (Suc n, obs)"
  unfolding clock_jview_def by (cases t) simp_all

lemma clock_jview_inv:
  "clock_jview a t = (n, obs) ==> envObs a (tLast t) = obs"
  unfolding clock_jview_def by (cases t) simp_all

lemmas clock_jview_simps =
  clock_jview_tInit
  clock_jview_tStep
  clock_jview_inv

lemma clock_jview_eq_inv[iff]:
  "clock_jview a t' = clock_jview a t
    ⟷ tLength t' = tLength t ∧ envObs a (tLast t') = envObs a (tLast t)"
  by (fastforce simp: clock_jview_def)

end(*>*)

text‹

  is the least-information synchronous view, given the requirements
  \S\ref{sec:kbps-views}. We show that finite-state implementations
  for all environments with respect to this view as per
 🚫‹"Ron:1996"›.

  corresponding incremental view simply increments the counter
  the new observation.

 ›

definition (in Environment)
  clock_jviewInit :: "'a → 'obs → nat × 'obs"
where
  "clock_jviewInit ≡ λa obs. (0, obs)"

definition (in Environment)
  clock_jviewIncr :: "'a → 'obs → nat × 'obs → nat × 'obs"
where
  "clock_jviewIncr ≡ λa obs' (l, obs). (l + 1, obs')"

text‹

  is straightforward to demonstrate the assumptions of the
  environment locale (\S\ref{sec:kbps-environments}) with
  to an arbitrary environment.

 ›

sublocale Environment
        < Clock: IncrEnvironment jkbp envInit envAction envTrans envVal
                        clock_jview envObs clock_jviewInit clock_jviewIncr
(*<*)
  apply (unfold_locales)
  apply (simp_all add: clock_jviewInit_def clock_jviewIncr_def clock_jview_def)
  done

(*>*)
text‹

  we later show, satisfaction of a formula at a trace ‹t ∈
 .jkbpC› is determined by the set of final states of traces in
 ‹Clock.jkbpCn›:

 ›

context Environment
begin

abbreviation clock_commonAbs :: "'s Trace → 's set" where
  "clock_commonAbs t ≡ tLast ` Clock.jkbpCn (tLength t)"

text‹

  this set contains the states that the agents commonly
  possible at time @{term "n"}, which is sufficient for
  knowledge as the clock view ignores paths. Therefore we
  simulate trace @{term "t"} by pairing this abstraction of @{term
 t"} with its final state:

 ›

type_synonym (in -) 's clock_simWorlds = "'s set × 's"

definition clock_sim :: "'s Trace → 's clock_simWorlds" where
  "clock_sim ≡ λt. (clock_commonAbs t, tLast t)"

text‹

  the Kripke structure for our simulation, we relate worlds for
 {term "a"} if the sets of commonly-held states coincide, and the
  of the final states of the traces is the
 . Propositions are evaluated at the final state.

 ›

definition clock_simRels :: "'a → 's clock_simWorlds Relation" where
  "clock_simRels ≡ λa. { ((X, s), (X', s')) |X X' s s'.
                          X = X' ∧ {s, s'} ⊆ X ∧ envObs a s = envObs a s' }"

definition clock_simVal :: "'s clock_simWorlds → 'p → bool" where
  "clock_simVal ≡ envVal ∘ snd"

abbreviation clock_simMC :: "('a, 'p, 's clock_simWorlds) KripkeStructure" where
  "clock_simMC ≡ mkKripke (clock_sim ` Clock.jkbpC) clock_simRels clock_simVal"
(*<*)

lemma clock_simVal_def2[iff]: "clock_simVal (clock_sim t) = envVal (tLast t)"
  unfolding clock_sim_def clock_simVal_def by simp

lemma clock_sim_range:
  "sim_range Clock.MC clock_simMC clock_sim"
  by (rule sim_rangeI) (simp_all add: clock_sim_def)

lemma clock_simVal:
  "sim_val Clock.MC clock_simMC clock_sim"
  by (rule sim_valI) (simp add: clock_simVal_def clock_sim_def)

lemma clock_sim_f:
  "sim_f Clock.MC clock_simMC clock_sim"
apply (rule sim_fI)
apply (simp add: clock_simRels_def clock_sim_def)
apply (intro conjI)
   apply (fastforce intro!: imageI)
  apply (fastforce intro!: imageI)
 apply (fastforce dest: Clock.mkM_simps(2))
apply (rule_tac x=v in image_eqI)
 apply simp_all
done

lemma clock_sim_r:
  "sim_r Clock.MC clock_simMC clock_sim"
  apply (rule sim_rI)
  apply (clarsimp simp: clock_simRels_def clock_sim_def cong del: image_cong_simp)
  apply (rule_tac x=xa in exI)
  unfolding Clock.mkM_def
  apply auto
  done

(*>*)
text‹

  this is in fact a simulation
 \S\ref{sec:kripke-theory-simulations}) is entirely straightforward.

 ›

lemma clock_sim:
  "sim Clock.MC clock_simMC clock_sim"
(*<*)
  using clock_sim_range clock_simVal clock_sim_f clock_sim_r
  unfolding sim_def
  by blast
(*>*)

end (* context Environment *)

text‹

  ‹SimIncrEnvironment› of
 S\ref{sec:kbps-theory-automata-env-sims} only requires that we
  it an @{term "Environment"} and a simulation.

 ›

sublocale Environment
        < Clock: SimIncrEnvironment jkbp envInit envAction envTrans envVal
                  clock_jview envObs clock_jviewInit clock_jviewIncr
                  clock_sim clock_simRels clock_simVal
(*<*)
  by (unfold_locales, simp_all add: clock_sim)
(*>*)

text‹

  next consider algorithmic issues.

 ›

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

subsubsection‹Representations›

text‹

 label{sec:kbps-theory-clock-view-rep}

  now turn to the issue of how to represent equivalence classes of
 . As these are used as map keys, it is easiest to represent them
 . A simple approach is to use \emph{ordered distinct lists}
  type @{typ "'a odlist"} for the sets and \emph{tries} for the
 . Therefore we ask that environment states @{typ "'s"} belong to
  class ‹linorder› of linearly-ordered types, and moreover
  the set ‹agents› be effectively presented. We introduce a
  locale capturing these requirements:

 ›

locale FiniteLinorderEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
    for jkbp :: "('a::{finite, linorder}, '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 agents :: "'a odlist"
  assumes agents: "ODList.toSet agents = UNIV"

context FiniteLinorderEnvironment
begin

text‹

 label{sec:kbps-theory-clock-view-algops}

  a fixed agent @{term "a"}, we can reduce the number of worlds in
 {term "clock_simMC"} by taking its quotient with respect to the
  relation for @{term "a"}. In other words, we represent a
  equivalence class by a pair of the set of all states
  at a particular time, and the subset of these that @{term
 a"} considers possible. The worlds in our representational Kripke
  are therefore a pair of ordered, distinct lists:

 ›

type_synonym (in -) 's clock_simWorldsRep = "'s odlist × 's odlist"

text‹

  can readily abstract a representation to a set of simulated
  classes:

 ›

definition (in -)
  clock_simAbs :: "'s::linorder clock_simWorldsRep → 's clock_simWorlds set"
where
  "clock_simAbs X ≡ { (ODList.toSet (fst X), s) |s. s ∈ ODList.toSet (snd X) }"

text‹

  @{term "X"} represents a simulated equivalence class for
 {term "t ∈ jkbpC"}, @{term "clock_simAbs X"} decomposes into these
  functions:

 ›

definition
  agent_abs :: "'a → 's Trace → 's set"
where
  "agent_abs a t ≡
     { tLast t' |t'. t' ∈ Clock.jkbpC ∧ clock_jview a t' = clock_jview a t}"

definition
  common_abs :: "'s Trace → 's set"
where
  "common_abs t ≡ tLast ` Clock.jkbpCn (tLength t)"
(*<*)

lemma aec_refl[intro, simp]:
  "t ∈ Clock.jkbpC ==> tLast t ∈ agent_abs a t"
  unfolding agent_abs_def by auto

lemma aec_cec_subset:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "x ∈ ODList.toSet aec ==> x ∈ ODList.toSet cec"
  using assms
  unfolding agent_abs_def common_abs_def
  by fastforce

lemma clock_simAbs_refl:
  assumes tC: "t ∈ Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_sim t ∈ clock_simAbs ec"
  using assms by simp

lemma common_abs:
  assumes tC: "t ∈ Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (fst ec) = common_abs t"
  using tC clock_simAbs_refl[OF tC ec]
  unfolding clock_sim_def clock_simAbs_def common_abs_def
  by (auto simp: ODList.toSet_def[symmetric])

lemma agent_abs:
  assumes tC: "t ∈ Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (snd ec) = agent_abs a t"
  using assms
  unfolding clock_sim_def clock_simAbs_def agent_abs_def
  apply auto
  apply (subgoal_tac "(ODList.toSet (fst ec), x) ∈ {(ODList.toSet (fst ec), s) |s. s ∈ ODList.toSet (snd ec)}")
  apply auto (* FIXME filthy *)
  done

(*>*)
text‹

  representation is canonical on the domain of interest (though not
  general):

 ›

lemma clock_simAbs_inj_on:
  "inj_on clock_simAbs { x . clock_simAbs x ∈ Clock.jkbpSEC }"
(*<*)
proof(rule inj_onI)
  fix x y
  assume x: "x ∈ { x . clock_simAbs x ∈ Clock.jkbpSEC }"
     and y: "y ∈ { x . clock_simAbs x ∈ Clock.jkbpSEC }"
     and xy: "clock_simAbs x = clock_simAbs y"
  from x obtain a t
    where tC: "t ∈ Clock.jkbpC"
      and ec: "clock_simAbs x = Clock.sim_equiv_class a t"
    by auto
  from common_abs[OF tC ec] common_abs[OF tC trans[OF xy[symmetric] ec], symmetric]
  have "fst x = fst y" by (blast intro: injD[OF toSet_inj])
  moreover
  from agent_abs[OF tC ec] 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‹

  could further compress this representation by labelling each
  of the set of states reachable at time $n$ with a bit to
  whether the agent considers that state possible. Note,
 , that the representation would be non-canonical: if ‹(s, True)› is in the representation, indicating that the agent
  ‹s› possible, then ‹(s, False)› may or may
  be. The associated abstraction function is not injective and hence
  obfuscate the following. Repairing this would entail introducing
  new type, which would again complicate this development.



  following lemmas make use of this Kripke structure, constructed
  the set of final states of a temporal slice @{term "X"}:

 ›

definition
  clock_repRels :: "'a → ('s × 's) set"
where
  "clock_repRels ≡ λa. { (s, s'). envObs a s = envObs a s' }"

abbreviation
  clock_repMC :: "'s set → ('a, 'p, 's) KripkeStructure"
where
  "clock_repMC ≡ λX. mkKripke X clock_repRels envVal"
(*<*)

lemma clock_repMC_kripke[intro, simp]: "kripke (clock_repMC X)"
  by (rule kripkeI) simp

lemma clock_repMC_S5n[intro, simp]: "S5n (clock_repMC X)"
  unfolding clock_repRels_def
  by (intro S5nI equivI refl_onI symI transI) auto

(*>*)
text‹

  can show that this Kripke structure retains sufficient information
  @{term "Clock.MCS"} by showing simulation. This is eased by
  an intermediary structure that focusses on a particular
 :

 ›

abbreviation
  clock_jkbpCSt :: "'b Trace → 's clock_simWorlds set"
where
  "clock_jkbpCSt t ≡ clock_sim ` Clock.jkbpCn (tLength t)"

abbreviation
  clock_simMCt :: "'b Trace → ('a, 'p, 's clock_simWorlds) KripkeStructure"
where
  "clock_simMCt t ≡ mkKripke (clock_jkbpCSt t) clock_simRels clock_simVal"

definition clock_repSim :: "'s clock_simWorlds → 's" where
  "clock_repSim ≡ snd"
(*<*)

lemma jkbpCSt_jkbpCS_subset:
  "clock_jkbpCSt t ⊆ clock_sim ` Clock.jkbpC"
  by auto

lemma jkbpCSt_refl[iff]:
  "t ∈ Clock.jkbpC ==> clock_sim t ∈ clock_jkbpCSt t"
  by blast

lemma fst_clock_sim[iff]:
  "t ∈ Clock.jkbpC ==> fst (clock_sim t) = tLast ` Clock.jkbpCn (tLength t)"
  by (simp add: clock_sim_def)

lemma clock_repSim_simps[simp]:
  "clock_repSim ` clock_sim ` T = tLast ` T"
  "clock_repSim (clock_sim t) = tLast t"
  unfolding clock_repSim_def clock_sim_def
  by (auto intro!: image_eqI)

(*>*)
text‹›

lemma clock_repSim:
  assumes tC: "t ∈ Clock.jkbpC"
  shows "sim (clock_simMCt t)
             ((clock_repMC ∘ fst) (clock_sim t))
             clock_repSim"
(*<*) (is "sim ?M ?M' ?f")
proof
  show "sim_range ?M ?M' ?f"
  proof
    show "worlds ?M' = ?f ` worlds ?M"
      unfolding clock_sim_def clock_repSim_def by force
  next
    fix a
    show "relations ?M' a ⊆ worlds ?M' × worlds ?M'"
      by (simp add: clock_sim_def clock_repSim_def)
  qed
next
  show "sim_val ?M ?M' ?f"
    by (rule, simp add: clock_sim_def clock_simVal_def clock_repSim_def split: prod.split)
next
  show "sim_f ?M ?M' ?f"
    apply rule
    unfolding clock_repRels_def clock_repSim_def clock_simRels_def
    apply (auto iff: clock_sim_def)
    done
next
  show "sim_r ?M ?M' ?f"
    apply rule
    unfolding clock_repRels_def clock_repSim_def clock_simRels_def clock_sim_def
    apply clarsimp
    done
qed

(*>*)
text‹

  following sections show how we satisfy the remaining requirements
  the ‹Algorithm› locale of
 ~\ref{fig:kbps-alg-alg-locale}. Where the proof is routine, we
  present the lemma without proof or comment.

  to a limitation in the code generator in the present version of
  (2011), we need to define the equations we wish to execute
  of a locale; the syntax ‹(in -)› achieves this by
  definitons at the theory top-level. We then define (but elide)
 -local abbreviations that supply the locale-bound variables to
  definitions.

 ›

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

subsubsection‹Initial states›

text‹

  initial states of the automaton for an agent is simply @{term
 envInit"} paired with the partition of @{term "envInit"} under the
 's observation.

 ›

definition (in -)
  clock_simInit :: "('s::linorder) list → ('a → 's → 'obs)
                → 'a → 'obs → 's clock_simWorldsRep"
where
  "clock_simInit envInit envObs ≡ λa iobs.
    let cec = ODList.fromList envInit
     in (cec, ODList.filter (λs. envObs a s = iobs) cec)"
(*<*)

abbreviation
  clock_simInit :: "'a → 'obs → 's clock_simWorldsRep"
where
  "clock_simInit ≡ ClockView.clock_simInit envInit envObs"

(*>*)
text‹›

lemma clock_simInit:
  assumes "iobs ∈ envObs a ` set envInit"
  shows "clock_simAbs (clock_simInit a iobs)
       = clock_sim ` { t' ∈ Clock.jkbpC.
                       clock_jview a t' = clock_jviewInit a iobs }"
(*<*)
  using assms
  unfolding clock_simInit_def clock_simAbs_def clock_sim_def [abs_def] Let_def
  apply clarsimp
  apply rule
   apply clarsimp
   apply (rule_tac x="tInit s" in image_eqI)
    apply (auto simp: Set.image_def Clock.jviewInit)[2]
  apply clarsimp
  apply (case_tac xa)
   apply clarsimp
   apply rule
    apply rule
     apply clarsimp
    apply clarsimp
    apply (rule_tac x="tInit xa" in image_eqI)
    apply (auto intro!: image_eqI simp: Clock.jviewInit)
  done
(*>*)

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

subsubsection‹Simulated observations›

text‹

  @{term "a"} will make the same observation at any of the worlds
  it considers possible, so we choose the first one in the list:

 ›

definition (in -)
  clock_simObs :: "('a → ('s :: linorder) → 'obs)
                → 'a → 's clock_simWorldsRep → 'obs"
where
  "clock_simObs envObs ≡ λa. envObs a ∘ ODList.hd ∘ snd"
(*<*)

abbreviation
  clock_simObs :: "'a → 's clock_simWorldsRep → 'obs"
where
  "clock_simObs ≡ ClockView.clock_simObs envObs"

(*>*)
text‹›

lemma clock_simObs:
  assumes tC: "t ∈ Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_simObs a ec = envObs a (tLast t)"
(*<*)
proof -
  have A: "∀s ∈ set (toList (snd ec)). envObs a s = envObs a (tLast t)"
    using agent_abs[OF tC ec]
    by (clarsimp simp: agent_abs_def toSet_def)
  have B: "tLast t ∈ set (toList (snd ec))"
    using clock_simAbs_refl[OF assms]
    unfolding clock_simAbs_def clock_sim_def
    by (simp add: toSet_def snd_def)
  show ?thesis
    unfolding clock_simObs_def by (simp add: list_choose_hd[OF A B] ODList.hd_def)
qed
(*>*)

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

subsubsection‹Evaluation›

text‹

 label{sec:kbps-theory-clock-view-eval}

  define our ‹eval› function in terms of @{term "evalS"},
  implements boolean logic over @{typ "'s odlist"} in the usual
  -- see \S\ref{sec:kbps-spr-single-agent-eval} for the relevant
 . It requires three functions specific to the representation:
  each for propositions, knowledge and common knowledge.

  define subsets of the worlds considered possible:

 ›

abbreviation (in -)
  clock_evalProp :: "(('s::linorder) → 'p → bool)
                  → 's odlist → 'p → 's odlist"
where
  "clock_evalProp envVal ≡ λX p. ODList.filter (λs. envVal s p) X"

text‹

  knowledge relation computes the subset of the
 -held-possible worlds ‹cec› that agent @{term "a"}
  possible at world @{term "s"}:

 ›

definition (in -)
  clock_knowledge :: "('a → ('s :: linorder) → 'obs) → 's odlist
                  → 'a → 's → 's odlist"
where
  "clock_knowledge envObs cec ≡ λa s.
     ODList.filter (λs'. envObs a s = envObs a s') cec"

text‹


  the common knowledge operation computes the transitive
  of the union of the knowledge relations for the agents ‹as›:

 ›

definition (in -)
  clock_commonKnowledge :: "('a → ('s :: linorder) → 'obs) → 's odlist
           → 'a list → 's → 's odlist"
where
  "clock_commonKnowledge envObs cec ≡ λas s.
     let r = λa. ODList.fromList [ (s', s'') . s' ← toList cec, s'' ← toList cec,
                                   envObs a s' = envObs a s'' ];
         R = toList (ODList.big_union r as)
      in ODList.fromList (memo_list_trancl R s)"

text‹

  function ‹memo_list_trancl› comes from the executable
  closure theory of 🚫‹"AFP:TRANCL"›.

  evaluation function evaluates a subjective knowledge formula on
  representation of an equivalence class:

 ›

definition (in -)
  eval :: "(('s :: linorder) → 'p → bool)
        → ('a → 's → 'obs)
        → 's clock_simWorldsRep → ('a, 'p) Kform → bool"
where
  "eval envVal envObs ≡ λ(cec, aec). evalS (clock_evalProp envVal)
                                      (clock_knowledge envObs cec)
                                      (clock_commonKnowledge envObs cec)
                                      aec"

text‹

  function corresponds with the standard semantics:

 ›
(*<*)

lemma clock_coEC_relation_image:
  "s ∈ ODList.toSet Y
    ==> ODList.toSet (clock_knowledge envObs Y a s) = relations (clock_repMC (ODList.toSet Y)) a `` {s}"
  unfolding clock_knowledge_def clock_repRels_def Image_def
  by auto

lemma clock_commonKnowledge_relation_image_aux:
  "(∪x∈set as. ∪a∈ODList.toSet Y. ∪aa∈ODList.toSet Y ∩ {s''. envObs x a = envObs x s''}. {(a, aa)})
 = ((∪a∈set as. {(s, s'). envObs a s = envObs a s'}) ∩ ODList.toSet Y × ODList.toSet Y)"
  by auto

lemma clock_commonKnowledge_relation_image:
  "s ∈ ODList.toSet Y
    ==> ODList.toSet (clock_commonKnowledge envObs Y as s) = (∪a ∈ set as. relations (clock_repMC (ODList.toSet Y)) a)⁺ `` {s}"
  unfolding clock_commonKnowledge_def clock_repRels_def Let_def
  apply (simp add: memo_list_trancl toSet_def[symmetric] Image_def clock_commonKnowledge_relation_image_aux)
  done

lemma eval_rec_models:
  assumes XY: "ODList.toSet X ⊆ ODList.toSet Y"
      and s: "s ∈ ODList.toSet X"
  shows "s ∈ ODList.toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs Y) (clock_commonKnowledge envObs Y) X φ)
     ⟷ clock_repMC (ODList.toSet Y), s ⊨ φ"
using XY s
proof(induct φ arbitrary: X s)
  case (Kknows a' φ X s)
  from ‹s ∈ ODList.toSet X› clock_coEC_relation_image[OF subsetD[OF Kknows(2) Kknows(3)], where a=a']
  show ?case
    apply simp
    apply rule
     apply (drule arg_cong[where f="ODList.toSet"])
     apply (clarsimp simp: odlist_all_iff)
     apply (cut_tac s3="w'" and X3="clock_knowledge envObs Y a' s" in Kknows.hyps)
      using Kknows(2) Kknows(3)
      apply (auto simp add: S5n_rels_closed[OF clock_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 clock_repMC_S5n])
    done
next
  case (Kcknows as φ X s)
  show ?case
  proof(cases "as = Nil")
    case True with ‹s ∈ ODList.toSet X› show ?thesis by clarsimp
  next
    case False
    with ‹s ∈ ODList.toSet X› clock_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="ODList.toSet"])
       apply (clarsimp simp: odlist_all_iff)
       apply (cut_tac s3="w'" and X3="clock_commonKnowledge envObs Y as s" in Kcknows.hyps)
        using Kcknows(2) Kcknows(3)
        apply (auto simp add: S5n_rels_closed[OF clock_repMC_S5n])[3]
        apply (subst (asm) trancl_unfold) back back back
        apply auto[1] (* FIXME disgusting *)

      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 clock_repMC_S5n])
        apply (subst (asm) trancl_unfold) back back back
        apply auto[1] (* FIXME disgusting *)

      done
  qed
qed simp_all

lemma trc_aux:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "ODList.toSet (big_union (clock_commonKnowledge envObs cec as) (toList aec)) ⊆ ODList.toSet cec"
  apply (clarsimp simp: toSet_def[symmetric])
  apply (subst (asm) clock_commonKnowledge_relation_image)
   apply (erule aec_cec_subset[OF tC aec cec])
  apply (subst (asm) trancl_unfold)
  using assms
  apply (auto simp: agent_abs_def)
  done

lemma clock_repMC_aec:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and x: "x ∈ ODList.toSet aec"
      and xy: "(x, y) ∈ relations (clock_repMC (ODList.toSet cec)) a"
  shows "y ∈ ODList.toSet aec"
  using assms
  unfolding clock_repRels_def agent_abs_def common_abs_def
  by auto

lemma clock_repMC_cec:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and x: "x ∈ ODList.toSet aec"
      and y: "y ∈ ODList.toSet aec"
  shows "(x, y) ∈ relations (clock_repMC (ODList.toSet cec)) a"
  using assms
  unfolding clock_repRels_def agent_abs_def common_abs_def
  by auto

lemma evalS_models:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and subj_phi: "subjective a φ"
      and s: "s ∈ ODList.toSet aec"
  shows "evalS (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec) aec φ
     ⟷ clock_repMC (ODList.toSet cec), s ⊨ φ" (is "?lhs φ = ?rhs φ")
using subj_phi s aec cec
proof(induct φ rule: subjective.induct[case_names Kprop Knot Kand Kknows Kcknows])
  case (Kknows a a' ψ) show ?case
    apply (clarsimp simp: toSet_eq_iff)
    apply rule
     apply clarsimp
     apply (subgoal_tac "w' ∈ ODList.toSet aec")
     apply (drule_tac c="w'" in subsetD)
       apply assumption
      apply (simp add: eval_rec_models[OF subsetI[OF aec_cec_subset[OF tC aec cec]]])
     apply (rule clock_repMC_aec[OF tC Kknows(3) Kknows(4), rotated, where x=s])
       using Kknows
       apply simp
      using Kknows
      apply simp

    apply clarsimp
    apply (simp add: eval_rec_models[OF subsetI[OF aec_cec_subset[OF tC aec cec]]])
    using tC Kknows
    apply (clarsimp simp: agent_abs_def)
    apply (erule (1) ballE)
    using Kknows
    apply (cut_tac x="tLast t'" and y="tLast t'a" in clock_repMC_cec[OF tC Kknows(3) Kknows(4)])
      unfolding clock_repRels_def
      apply auto
    done
next
  case (Kcknows a as ψ)
  have "?lhs (Kcknows as ψ)
      = (∀y∈ODList.toSet aec.
           ∀x∈(∪a∈set as. relations (clock_repMC (ODList.toSet cec)) a)⁺ `` {y}.
              x ∈ ODList.toSet (eval_rec (clock_evalProp envVal) (clock_knowledge envObs cec) (clock_commonKnowledge envObs cec)
                       (big_union (clock_commonKnowledge envObs cec as) (toList aec)) ψ))"
    (* FIXME dreaming of a cong rule here. *)
    using toSet_def[symmetric]
    apply (clarsimp simp: toSet_eq_iff toSet_def[symmetric] subset_eq)
    apply (rule ball_cong[OF refl])
    apply (rule ball_cong)
    apply (subst clock_commonKnowledge_relation_image[OF aec_cec_subset[OF tC Kcknows(3) Kcknows(4)]])
    apply simp_all
    done
  also have "... = (∀s∈ODList.toSet aec. clock_repMC (ODList.toSet cec), s ⊨ Kcknows as ψ)"
    apply (rule ball_cong[OF refl])
    apply simp
    apply (rule ball_cong[OF refl])
    apply (subst eval_rec_models[OF trc_aux[OF tC Kcknows(3) Kcknows(4), where as=as], symmetric])
     apply (simp add: toSet_def[symmetric])
     apply (rule_tac x=y in bexI)
      apply (subst clock_commonKnowledge_relation_image[OF aec_cec_subset[OF tC Kcknows(3) Kcknows(4)]])
       apply simp_all
    done
  also have "... = clock_repMC (ODList.toSet cec), s ⊨ Kknows a (Kcknows as ψ)"
    using clock_repMC_aec[OF tC Kcknows(3) Kcknows(4) Kcknows(2)]
          clock_repMC_cec[OF tC Kcknows(3) Kcknows(4) Kcknows(2)]
    by (auto cong: ball_cong)
  also have "... = clock_repMC (ODList.toSet cec), s ⊨ Kcknows as ψ"
    apply (rule S5n_common_knowledge_fixed_point_simpler[symmetric])
    using Kcknows
    apply (auto intro: aec_cec_subset[OF tC Kcknows(3) Kcknows(4) Kcknows(2)])
    done
  finally show ?case .
qed simp_all

(*>*)
lemma eval_models:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
      and subj_phi: "subjective a φ"
      and s: "s ∈ ODList.toSet aec"
  shows "eval envVal envObs (cec, aec) φ
     ⟷ clock_repMC (ODList.toSet cec), s ⊨ φ"
(*<*)
  unfolding eval_def
  using evalS_models[OF tC aec cec subj_phi s]
  apply (simp add: Let_def)
  done

(*>*)

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

subsubsection‹Simulated actions›

text‹

  a common equivalence class and a subjective equivalence class for
  @{term "a"}, we can compute the actions enabled for @{term "a"}:

 ›

definition (in -)
  clock_simAction :: "('a, 'p, 'aAct) JKBP → (('s :: linorder) → 'p → bool)
                  → ('a → 's → 'obs)
                  → 'a → 's clock_simWorldsRep → 'aAct list"
where
  "clock_simAction jkbp envVal envObs ≡ λa (Y, X).
     [ action gc. gc ← jkbp a, eval envVal envObs (Y, X) (guard gc) ]"
(*<*)

abbreviation
  clock_simAction :: "'a → 's clock_simWorldsRep → 'aAct list"
where
  "clock_simAction ≡ ClockView.clock_simAction jkbp envVal envObs"

(*>*)
text‹

  the above result about evaluation, we can relate ‹clock_simAction› to @{term "jAction"}. Firstly, ‹clock_simAction› behaves the same as @{term "jAction"} using the
 {term "clock_repMC"} structure:

 ›

lemma clock_simAction_jAction:
  assumes tC: "t ∈ Clock.jkbpC"
      and aec: "ODList.toSet aec = agent_abs a t"
      and cec: "ODList.toSet cec = common_abs t"
  shows "set (clock_simAction a (cec, aec))
       = set (jAction (clock_repMC (ODList.toSet cec)) (tLast t) a)"
(*<*)
  unfolding clock_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 aec cec, symmetric])
     using tC aec cec subj
     apply simp_all
  apply clarsimp
  apply (rule_tac x=xa in bexI)
   apply (rule refl)
  apply clarsimp
  apply (subst eval_models[OF tC aec cec])
    using tC aec cec subj
    apply simp_all
  done

lemma clock_submodel_aux:
  assumes tC: "t ∈ Clock.jkbpC"
      and s: "s ∈ worlds (clock_simMCt t)"
  shows "gen_model Clock.MCS s = gen_model (clock_simMCt t) s"
proof(rule gen_model_subset[where T="clock_jkbpCSt t"])
  fix a
  let ?X = "clock_sim ` Clock.jkbpCn (tLength t)"
  show "relations Clock.MCS a ∩ ?X × ?X
      = relations (clock_simMCt t) a ∩ ?X × ?X"
    by (simp add: Int_ac Int_absorb1
                  relation_mono[OF jkbpCSt_jkbpCS_subset jkbpCSt_jkbpCS_subset])
next
  let ?X = "clock_sim ` Clock.jkbpCn (tLength t)"
  from s show "(∪a. relations (clock_simMCt t) a)^* `` {s} ⊆ ?X"
    apply (clarsimp simp del: mkKripke_simps)
    apply (erule kripke_rels_trc_worlds)
    apply auto
    done
next
  let ?Y = "Clock.jkbpCn (tLength t)"
  let ?X = "clock_sim ` ?Y"
  from s obtain t'
    where st': "s = clock_sim t'"
      and t'C: "t' ∈ Clock.jkbpC"
      and t'O: "tLength t = tLength t'"
    by fastforce
  { fix t''
    assume tt': "(t', t'') ∈ (∪a. relations Clock.MC a)<sup>*</sup>"
    from t'C tt' have t''C: "t'' ∈ Clock.jkbpC"
      by - (erule kripke_rels_trc_worlds, simp_all)
    from t'O tt' have t''O: "tLength t = tLength t''"
      by (simp add: Clock.sync_tLength_eq_trc)
    from t''C t''O have "t'' ∈ ?Y" by fastforce }
  hence "(∪a. relations Clock.MC a)<sup>*</sup> `` {t'} ⊆ ?Y"
    by clarsimp
  hence "clock_sim ` ((∪a. relations Clock.MC a)^* `` {t'}) ⊆ ?X"
    by (rule image_mono)
  with st' t'C
  show "(∪a. relations Clock.MCS a)<sup>*</sup> `` {s} ⊆ ?X"
    using sim_trc_commute[OF Clock.mkM_kripke clock_sim, where t=t'] by simp
qed (insert s, auto)

(*>*)
text‹

  can connect the agent's choice of actions on the ‹clock_repMC› structure to those on the ‹Clock.MC›
  using our earlier results about actions being preserved by
  models and simulations.

 ›

lemma clock_simAction':
  assumes tC: "t ∈ Clock.jkbpC"
  assumes aec: "ODList.toSet aec = agent_abs a t"
  assumes cec: "ODList.toSet cec = common_abs t"
  shows "set (clock_simAction a (cec, aec)) = set (jAction Clock.MC t a)"
(*<*) (is "?lhs = ?rhs")
proof -
  from tC aec cec
  have "?lhs = set (jAction (clock_repMC (ODList.toSet cec)) (tLast t) a)"
    by (rule clock_simAction_jAction)
  also from tC aec cec
  have "... = set (jAction (clock_simMCt t) (clock_sim t) a)"
    by (simp add: simulation_jAction_eq[OF _ clock_repSim] common_abs_def)
  also from tC
  have "... = set (jAction Clock.MCS (clock_sim t) a)"
    using gen_model_jAction_eq[OF clock_submodel_aux[OF tC, where s="clock_sim t"], where w'="clock_sim t"]
          gen_model_world_refl[where w="clock_sim t" and M="clock_simMCt t"]
    by simp
  also from tC have "... = set (jAction Clock.MC t a)"
    by (simp add: simulation_jAction_eq[OF _ clock_sim])
  finally show ?thesis .
qed

(*>*)
text‹

  @{term "Algorithm"} locale requires a specialisation of this
 :

 ›

lemma clock_simAction:
  assumes tC: "t ∈ Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "set (clock_simAction a ec) = set (jAction Clock.MC t a)"
(*<*)
  using assms clock_simAction'[OF tC, where cec="fst ec" and aec="snd ec"]
  apply (simp add: common_abs agent_abs)
  done
(*>*)

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

subsubsection‹Simulated transitions›

text‹

  need to determine the image of the set of commonly-held-possible
  under the transition function, and also for the agent's
  equivalence class. We do this with the ‹clock_trans› function:

 ›

definition (in -)
  clock_trans :: "('a :: linorder) odlist → ('a, 'p, 'aAct) JKBP
              → (('s :: linorder) → 'eAct list)
              → ('eAct → ('a → 'aAct) → 's → 's)
              → ('s → 'p → bool) → ('a → 's → 'obs)
              → 's odlist → 's odlist → 's odlist"
where
  "clock_trans agents jkbp envAction envTrans envVal envObs ≡ λcec X.
     ODList.fromList (concat
       [ [ envTrans eact aact s .
                     eact ← envAction s,
                     aact ← listToFuns (λa. clock_simAction jkbp envVal envObs a
                                        (cec, clock_knowledge envObs cec a s))
                                        (toList agents) ] .
                   s ← toList X ])"
(*<*)

abbreviation
  clock_trans :: "'s odlist → 's odlist → 's odlist"
where
  "clock_trans ≡ ClockView.clock_trans agents jkbp envAction envTrans envVal envObs"

lemma clock_trans_aux:
  assumes t'C: "t' ∈ Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a' t'"
      and tC: "t ∈ Clock.jkbpCn (tLength t')"
      and eact: "eact ∈ set (envAction (tLast t))"
  shows "(aact ∈ set (listToFuns (λa. clock_simAction a (fst ec, clock_knowledge envObs (fst ec) a (tLast t)))
                            (toList agents)))
     ⟷ (∀a. aact a ∈ set (jAction (Clock.MCn (tLength t')) t a))"
  using assms
  apply -
  apply (frule Clock.jkbpCn_jkbpC_inc)
  apply (clarsimp simp: listToFuns_ext[OF agents[unfolded toSet_def]])
  apply (subst clock_simAction')
     apply (erule Clock.jkbpCn_jkbpC_inc)
    apply (subst clock_coEC_relation_image)
     apply (simp add: common_abs common_abs_def toSet_def[symmetric])
    apply (fastforce simp: common_abs agent_abs_def common_abs_def clock_repRels_def)
   apply (simp add: common_abs common_abs_def)
  apply (simp add: Clock.jkbpC_jkbpCn_jAction_eq)
  done

(*>*)
text‹

  function @{term "listToFuns"} exhibits the isomorphism between @{typ
 ('a × 'b list) list"} and @{typ "('a → 'b) list"} for finite types
 {typ "'a"}.

  can show that the transition function works for both the
 -held set of states and the agent subjective one. The proofs
  straightforward.

 ›

lemma clock_trans_common:
  assumes tC: "t ∈ Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (clock_trans (fst ec) (fst ec))
       = { s |t' s. t' ↝ s ∈ Clock.jkbpC ∧ tLength t' = tLength t }"
(*<*) (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    unfolding clock_trans_def
    apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] common_abs_def)
    apply (rule_tac x=xa in exI)
    apply clarsimp
    apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
    apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
    done
next
  show "?rhs ⊆ ?lhs"
    unfolding clock_trans_def
    apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] common_abs_def)
    apply (drule Clock.jkbpC_tLength_inv[where n="Suc (tLength t)"])
    apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
    done
qed

(*>*)
text‹›

lemma clock_trans_agent:
  assumes tC: "t ∈ Clock.jkbpC"
  assumes ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "ODList.toSet (clock_trans (fst ec) (snd ec))
       = { s |t' s. t' ↝ s ∈ Clock.jkbpC ∧ clock_jview a t' = clock_jview a t }"
(*<*) (is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
    unfolding clock_trans_def
    apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] agent_abs[OF assms] common_abs_def agent_abs_def)
    apply (rule_tac x=t' in exI)
    apply clarsimp
    apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
    apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
    done
next
  show "?rhs ⊆ ?lhs"
    unfolding clock_trans_def
    apply (clarsimp simp: toSet_def[symmetric] common_abs[OF assms] agent_abs[OF assms] common_abs_def agent_abs_def)
    apply (drule Clock.jkbpC_tLength_inv[where n="Suc (tLength t)"])
    apply (auto simp: Let_def iff: clock_trans_aux[OF tC ec])
    done
qed

(*>*)
text‹

  that the clock semantics disregards paths, so we simply compute
  successors of the temporal slice and partition that. Similarly the
  of the agent's subjective equivalence class tell us what
  set of possible observations are:

 ›

definition (in -)
  clock_mkSuccs :: "('s :: linorder → 'obs) → 'obs → 's odlist
                → 's clock_simWorldsRep"
where
  "clock_mkSuccs envObs obs Y' ≡ (Y', ODList.filter (λs. envObs s = obs) Y')"

text‹

  we can define our transition function on simulated states:

 ›

definition (in -)
  clock_simTrans :: "('a :: linorder) odlist → ('a, 'p, 'aAct) JKBP
              → (('s :: linorder) → 'eAct list)
              → ('eAct → ('a → 'aAct) → 's → 's)
              → ('s → 'p → bool) → ('a → 's → 'obs)
              → 'a → 's clock_simWorldsRep → 's clock_simWorldsRep list"
where
  "clock_simTrans agents jkbp envAction envTrans envVal envObs ≡ λa (Y, X).
     let X' = clock_trans agents jkbp envAction envTrans envVal envObs Y X;
        Y' = clock_trans agents jkbp envAction envTrans envVal envObs Y Y
      in [ clock_mkSuccs (envObs a) obs Y' .
             obs ← map (envObs a) (toList X') ]"
(*<*)

abbreviation
  clock_simTrans :: "'a → 's clock_simWorldsRep → 's clock_simWorldsRep list"
where
  "clock_simTrans ≡ ClockView.clock_simTrans agents jkbp envAction envTrans envVal envObs"

(*>*)
text‹

  that this respects the property asked of it by the @{term
 Algorithm"} locale is straightforward:

 ›

lemma clock_simTrans:
  assumes tC: "t ∈ Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_simAbs ` set (clock_simTrans a ec)
      = { Clock.sim_equiv_class a (t' ↝ s)
          |t' s. t' ↝ s ∈ Clock.jkbpC ∧ clock_jview a t' = clock_jview a t }"
(*<*) (is "?lhs = ?rhs")
proof
  note image_cong_simp [cong del]
  show "?lhs ⊆ ?rhs"
    unfolding clock_simTrans_def clock_mkSuccs_def
    using clock_trans_common[OF tC ec] clock_trans_agent[OF tC ec]
    apply (clarsimp simp: toSet_def[symmetric] clock_simAbs_def Let_def)

    apply (rule_tac x=t' in exI)
    apply (rule_tac x=xa in exI)

    apply (clarsimp simp: clock_sim_def)
    apply safe

     apply clarsimp
     apply (rule_tac x="t'a ↝ s" in image_eqI)
      apply (clarsimp simp: Let_def Set.image_def)
      apply safe
        apply (rule_tac x="t'b ↝ x" in exI)
        apply (clarsimp simp: Let_def Set.image_def)
        apply (drule_tac t="t'b ↝ x" in Clock.jkbpC_tLength_inv[OF _ refl])
        apply (auto simp: Let_def)[1]
       apply (rule_tac x="ta" in exI)
       apply simp
       apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
       apply (auto simp: Let_def)[3]

    apply (rule_tac x="tLast ta" in exI)
    apply (clarsimp simp: Let_def Set.image_def)
    apply safe
      apply (rule_tac x="taa" in exI)
      apply simp
      apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
       apply (auto simp: Let_def)[1]
     apply (drule_tac t="t'a ↝ x" in Clock.jkbpC_tLength_inv[OF _ refl])
     apply (rule_tac x="t'a ↝ x" in exI)
     apply (auto simp: Let_def)[1]
    apply (drule_tac t="ta" in Clock.jkbpC_tLength_inv)
     apply blast
    apply (clarsimp simp: Let_def)
    apply (rule_tac x="ta" in exI)
    apply simp
    apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
    apply (auto simp: Let_def)
    done
next
  show "?rhs ⊆ ?lhs"
    unfolding clock_simTrans_def Let_def
    apply (cases ec)
    using clock_trans_common[OF tC ec] clock_trans_agent[OF tC ec]
    apply (clarsimp simp: toSet_def[symmetric] Set.image_def clock_simAbs_def
                simp del: split_paired_Ex)

    apply (rule_tac x="clock_mkSuccs (envObs a) (envObs a s) (clock_trans aa aa)" in exI)
    apply safe
      apply auto[1]
     apply (rule_tac x="tLast x" in exI)
     apply (clarsimp simp: clock_trans_common[OF tC ec] clock_mkSuccs_def)
     apply safe
       apply (clarsimp simp: clock_sim_def simp del: Clock.jkbpCn.simps)
       apply rule
        apply (clarsimp simp: Let_def)
        apply (rule_tac x="ta" in exI)
        apply (simp add: Let_def)
        apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
        apply (clarsimp simp: Let_def)
        apply (rule_tac x=eact in exI)
        apply (rule_tac x=aact in exI)
        apply clarsimp
       apply (clarsimp simp: Let_def Set.image_def)
       apply (drule_tac t="t'a ↝ xa" in Clock.jkbpC_tLength_inv[OF _ refl])
       apply (rule_tac x="t'a ↝ xa" in exI)
       apply (auto simp: Let_def)[1]
      apply (drule_tac t="x" in Clock.jkbpC_tLength_inv[OF _ refl])
      apply (simp only: Let_def Clock.jkbpCn.simps)
      apply clarify
      apply (rule_tac x="ta" in exI)
      apply simp
      apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
      apply (auto simp: Let_def)[1]
     apply (clarsimp simp: clock_trans_common[OF tC ec] clock_mkSuccs_def)
     apply (rule_tac x="t'a ↝ sa" in exI)
     apply (clarsimp simp: clock_sim_def Let_def)
     (* FIXME similar to above *)
     apply rule
      apply (clarsimp simp: Set.image_def)
      apply (rule_tac x="t'b ↝ x" in exI)
      apply (drule_tac t="t'b ↝ x" in Clock.jkbpC_tLength_inv[OF _ refl])
      apply (auto simp: Let_def)[1]
    apply clarsimp
    apply (rule_tac x="ta" in exI)
    apply auto
    apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
    apply (auto simp: Let_def)
    done
qed
(*>*)

end (* context FiniteLinorderEnvironment *)

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

subsubsection‹Maps›

text‹

 label{sec:kbps-theory-clock-view-maps}

  mentioned above, the canonicity of our ordered, distinct list
  of automaton states allows us to use them as keys in a
  trie; a value of type @{typ "('key, 'val) trie"} maps keys of
  @{typ "'key list"} to values of type @{typ "'val"}.

  this specific case we track automaton transitions using a two-level
  mapping sets of states to an association list mapping
  to sets of states, and for actions automaton states map
  to agent actions.

 ›

type_synonym ('s, 'obs) clock_trans_trie
  = "('s, ('s, ('obs, 's clock_simWorldsRep) mapping) trie) trie"
type_synonym ('s, 'aAct) clock_acts_trie = "('s, ('s, 'aAct) trie) trie"
(*<*)

definition
  trans_MapOps_lookup :: "('s :: linorder, 'obs) clock_trans_trie
                        → 's clock_simWorldsRep × 'obs
                        ⇀ 's clock_simWorldsRep"
where
  "trans_MapOps_lookup ≡ λm k.
     Option.bind (trie_odlist_lookup m (fst (fst k))) (λm.
       (Option.bind (trie_odlist_lookup m (snd (fst k))) (λm.
         Mapping.lookup m (snd k))))"

definition
  trans_MapOps_update :: "('s :: linorder) clock_simWorldsRep × 'obs → 's clock_simWorldsRep
                        → ('s :: linorder, 'obs) clock_trans_trie
                        → ('s :: linorder, 'obs) clock_trans_trie"
where
  "trans_MapOps_update ≡ λk v m.
     trie_odlist_update_with (fst (fst k)) m empty_trie (λm.
       trie_odlist_update_with (snd (fst k)) m Mapping.empty (λm.
          Mapping.update (snd k) v m))"

definition
  trans_MapOps :: "(('s :: linorder, 'obs) clock_trans_trie,
                    's clock_simWorldsRep × 'obs, 's clock_simWorldsRep) MapOps"
where
  "trans_MapOps ≡
     ( MapOps.empty = empty_trie,
       lookup = trans_MapOps_lookup,
       update = trans_MapOps_update )"

lemma (in FiniteLinorderEnvironment) trans_MapOps:
  "MapOps (λk. (clock_simAbs (fst k), snd k)) (Clock.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: "(clock_simAbs (fst k), snd k) ∈ Clock.jkbpSEC × (UNIV :: 'z set)"
     and k': "(clock_simAbs (fst k'), snd k') ∈ Clock.jkbpSEC × (UNIV :: 'z set)"
  show "MapOps.lookup trans_MapOps (MapOps.update trans_MapOps k e M) k'
         = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)
             then Some e else MapOps.lookup trans_MapOps M k')"
  proof(cases "(clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)")
    case True hence "k = k'"
      using inj_onD[OF clock_simAbs_inj_on] 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 (cases "fst k = fst k'")
       (auto simp add: lookup_empty lookup_update_neq prod_eq_iff lookup_trie_update_with split: option.split prod.split)
  qed
qed

(* A map for the agent actions. *)

definition
  acts_MapOps_lookup :: "('s :: linorder, 'aAct) clock_acts_trie
                      → 's clock_simWorldsRep
                      ⇀ 'aAct"
where
  "acts_MapOps_lookup ≡ λm k.
     Option.bind (trie_odlist_lookup m (fst k)) (λm.
       (trie_odlist_lookup m (snd k)))"

definition
  acts_MapOps_update :: "('s :: linorder) clock_simWorldsRep → 'aAct
                      → ('s :: linorder, 'aAct) clock_acts_trie
                      → ('s :: linorder, 'aAct) clock_acts_trie"
where
  "acts_MapOps_update ≡ λk v m.
     trie_odlist_update_with (fst k) m empty_trie (λm.
       trie_odlist_update (snd k) v m)"

definition
  acts_MapOps :: "(('s :: linorder, 'aAct) clock_acts_trie, 's clock_simWorldsRep, 'aAct) MapOps"
where
  "acts_MapOps ≡
     ( MapOps.empty = empty_trie,
       lookup = acts_MapOps_lookup,
       update = acts_MapOps_update )"

lemma (in FiniteLinorderEnvironment) acts_MapOps:
  "MapOps clock_simAbs Clock.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 trie_odlist_lookup_def
    by auto
next
  fix e k k' M
  assume k: "clock_simAbs k ∈ Clock.jkbpSEC"
     and k': "clock_simAbs k' ∈ Clock.jkbpSEC"
  show "MapOps.lookup acts_MapOps (MapOps.update acts_MapOps k e M) k'
         = (if clock_simAbs k' = clock_simAbs k
             then Some e else MapOps.lookup acts_MapOps M k')"
  proof(cases "clock_simAbs k' = clock_simAbs k")
    case True hence "k = k'"
      using inj_onD[OF clock_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 lookup_trie_update_with
                     trie_odlist_update_with_def trie_odlist_update_def trie_odlist_lookup_def)
  next
    case False thus ?thesis
      unfolding acts_MapOps_def acts_MapOps_lookup_def acts_MapOps_update_def
      by (auto simp: lookup_trie_update lookup_trie_update_with
                     trie_odlist_update_with_def trie_odlist_update_def trie_odlist_lookup_def
               dest: prod_eqI
              split: option.split)
  qed
qed

(*>*)
text‹

  define two records @{term "acts_MapOps"} and @{term "trans_MapOps"}
  the @{term "MapOps"} predicate
 \S\ref{sec:kbps-theory-map-ops}). Discharging the obligations in the
 {term "Algorithm"} locale is routine, leaning on the work of
 🚫‹"DBLP:conf/itp/LammichL10"›.

 ›

subsubsection‹Locale instantiation›

text‹

  we assemble the algorithm and discharge the proof obligations.

 ›

sublocale FiniteLinorderEnvironment
        < Clock: Algorithm
            jkbp envInit envAction envTrans envVal
            clock_jview envObs clock_jviewInit clock_jviewIncr
            clock_sim clock_simRels clock_simVal
            clock_simAbs clock_simObs clock_simInit clock_simTrans clock_simAction
            acts_MapOps trans_MapOps
(*<*)
  apply (unfold_locales)

  apply clarify
  apply (rule clock_simInit)
  apply simp

  apply clarify
  apply (erule (1) clock_simObs)

  apply clarify
  apply (erule (1) clock_simAction)

  apply clarify
  apply (erule (1) clock_simTrans)

  apply (rule acts_MapOps)
  apply (rule trans_MapOps)

  done

(*>*)
text‹

 , the algorithm for this case is:

 ›

definition
  "mkClockAuto ≡ λagents jkbp envInit envAction envTrans envVal envObs.
    mkAlgAuto acts_MapOps
              trans_MapOps
              (clock_simObs envObs)
              (clock_simInit envInit envObs)
              (clock_simTrans agents jkbp envAction envTrans envVal envObs)
              (clock_simAction jkbp envVal envObs)
              (λa. map (clock_simInit envInit envObs a ∘ envObs a) envInit)"

lemma (in FiniteLinorderEnvironment) mkClockAuto_implements:
  "Clock.implements
    (mkClockAuto agents jkbp envInit envAction envTrans envVal envObs)"
(*<*)
  using Clock.k_mkAlgAuto_implements
  unfolding mkClockAuto_def mkAlgAuto_def Clock.k_frontier_def
  by simp

(*

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

*)

definition
  "ClockAutoDFS ≡ λagents jkbp envInit envAction envTrans envVal envObs. λa.
    alg_dfs acts_MapOps
            trans_MapOps
            (clock_simObs envObs a)
            (clock_simTrans agents jkbp envAction envTrans envVal envObs a)
            (clock_simAction jkbp envVal envObs a)
            (map (clock_simInit envInit envObs a ∘ envObs a) envInit)"

lemma (in FiniteLinorderEnvironment)
  "mkClockAuto agents jkbp envInit envAction envTrans envVal envObs
 = (λa. alg_mk_auto acts_MapOps trans_MapOps (clock_simInit a) (ClockAutoDFS agents jkbp envInit envAction envTrans envVal envObs a))"
  unfolding mkClockAuto_def ClockAutoDFS_def mkAlgAuto_def alg_mk_auto_def by (simp add: Let_def)

(*>*)
text‹

  discuss the clock semantics further in \S\ref{sec:kbps-alg-clock}.

 ›

(*<*)
end
(*>*)