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

theory KBPsAuto
imports
  Extra
  KBPs
begin
(*>*)

section‹Automata Synthesis›

text‹

 label{sec:kbps-automata-synthesis}

  attention now shifts to showing how we can synthesise standard
  that \emph{implement} a JKBP under certain conditions. We
  by defining \emph{incremental views} following
 cite‹"Ron:1996"›, which provide the interface between the system and
  automata. The algorithm itself is presented in
 S\ref{sec:kbps-alg}.

 ›

subsection‹Incremental views›

text‹

 label{sec:kbps-environments}

  an agent instantaneously observes the system state, and so
  maintain her view of the system \emph{incrementally}: her new
  must be a function of her current view and some new
 . We allow this observation to be an arbitrary projection
 {term "envObs a"} of the system state for each agent @{term "a"}:

 ›

locale Environment =
  PreEnvironment jkbp envInit envAction envTrans envVal
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s → 'eAct list"
    and envTrans :: "'eAct → ('a → 'aAct) → 's → 's"
    and envVal :: "'s → 'p → bool"
+ fixes envObs :: "'a → 's → 'obs"

text‹

  incremental view therefore consists of two functions with these
 :

 ›

type_synonym ('a, 'obs, 'tv) InitialIncrJointView = "'a → 'obs → 'tv"
type_synonym ('a, 'obs,  'tv) IncrJointView = "'a → 'obs → 'tv → 'tv"

text‹

  functions are required to commute with their corresponding
 -based joint view in the obvious way:

 ›

locale IncrEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
+ PreEnvironmentJView jkbp envInit envAction envTrans envVal jview
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s → 'eAct list"
    and envTrans :: "'eAct → ('a → 'aAct) → 's → 's"
    and envVal :: "'s → 'p → bool"
    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a → 's → 'obs"
+ fixes jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
  fixes jviewIncr :: "('a, 'obs, 'tv) IncrJointView"
  assumes jviewInit: "∀a s. jviewInit a (envObs a s) = jview a (tInit s)"
  assumes jviewIncr: "∀a t s. jview a (t ↝ s)
                             = jviewIncr a (envObs a s) (jview a t)"

text‹

  with these definitions, the following sections show that there
  automata that implement a JKBP in a given environment.

 ›

subsection‹Automata›

text‹

  implementations of JKBPs take the form of deterministic Moore
 , where transitions are labelled by observation and states
  the action to be performed. We will use the term \emph{protocols}
  with automata, following the KBP literature, and adopt
 emph{joint protocols} for the assignment of one such to each agent:

 ›

record ('obs, 'aAct, 'ps) Protocol =
  pInit :: "'obs → 'ps"
  pTrans :: "'obs → 'ps → 'ps"
  pAct :: "'ps → 'aAct list"

type_synonym ('a, 'obs, 'aAct, 'ps) JointProtocol
    = "'a → ('obs, 'aAct, 'ps) Protocol"

context IncrEnvironment
begin

text‹

  ease composition with the system we adopt the function @{term
 pInit"} which maps the initial observation to an initial automaton
 .

 🚫‹"Ron:1996"› shows that even non-deterministic JKBPs can be
  with deterministic transition functions; intuitively all
  uncertainty the agent has about the system must be encoded
  each automaton state, so there is no benefit to doing this
 -deterministically. In contrast we model the non-deterministic
  of action by making @{term "pAct"} a relation.

  a protocol on a trace is entirely standard, as is running a
  protocol, and determining their actions:

 ›

fun runJP :: "('a, 'obs, 'aAct, 'ps) JointProtocol
           → 's Trace → 'a → 'ps"
where
  "runJP jp (tInit s) a = pInit (jp a) (envObs a s)"
| "runJP jp (t ↝ s) a = pTrans (jp a) (envObs a s) (runJP jp t a)"

abbreviation actJP :: "('a, 'obs, 'aAct, 'ps) JointProtocol
                    → 's Trace → 'a → 'aAct list" where
  "actJP jp ≡ λt a. pAct (jp a) (runJP jp t a)"

text ‹

  to \S\ref{sec:kbps-canonical-kripke} we will reason about
  set of traces generated by a joint protocol in a fixed
 :

 ›

inductive_set
  jpTraces :: "('a, 'obs, 'aAct, 'ps) JointProtocol → 's Trace set"
    for jp :: "('a, 'obs, 'aAct, 'ps) JointProtocol"
where
  "s ∈ set envInit ==> tInit s ∈ jpTraces jp"
| "[ t ∈ jpTraces jp; eact ∈ set (envAction (tLast t));
     ∧a. aact a ∈ set (actJP jp t a); s = envTrans eact aact (tLast t) ]
     ==> t ↝ s ∈ jpTraces jp"
(*<*)

declare jpTraces.intros[intro]

lemma jpTraces_init_inv[dest]:
  "tInit s ∈ jpTraces jp ==> s ∈ set envInit"
  by (cases rule: jpTraces.cases) auto

lemma jpTraces_step_inv[dest]:
  "t ↝ s ∈ jpTraces jp
    ==> t ∈ jpTraces jp
     ∧ (∃eact ∈ set (envAction (tLast t)).
        (∃aact. (∀a. aact a ∈ set (actJP jp t a))
          ∧ s = envTrans eact aact (tLast t)))"
  by (cases rule: jpTraces.cases) auto

lemma jpTraces_init_length_inv:
  "t ∈ jpTraces jp ==> (tLength t = 0) ⟷ (∃s. s ∈ set envInit ∧ t = tInit s)"
  by (induct t) (auto elim: jpTraces.cases)

lemma jpTraces_step_length_inv_aux:
  "t ∈ { t ∈ jpTraces jp . tLength t = Suc n }
    ==> ∃t' s. t = t' ↝ s
            ∧ t' ∈ jpTraces jp
            ∧ tLength t' = n
            ∧ (∃eact ∈ set (envAction (tLast t')).
               (∃aact. (∀a. aact a ∈ set (actJP jp t' a))
                 ∧ s = envTrans eact aact (tLast t')))"
  by (induct t arbitrary: n) auto

lemma jpTraces_step_length_inv:
  "{ t ∈ jpTraces jp . tLength t = Suc n }
 = { t ↝ s |eact aact t s. t ∈ { t ∈ jpTraces jp . tLength t = n }
              ∧ eact ∈ set (envAction (tLast t))
              ∧ (∀a. aact a ∈ set (actJP jp t a))
              ∧ s = envTrans eact aact (tLast t) }"
  apply (rule set_eqI)
  apply rule
   apply (drule jpTraces_step_length_inv_aux)
   apply auto
  done
(*>*)

end (* context IncrEnvironment *)

subsection‹The Implementation Relation›

text‹

 label{sec:kbps-implementation}

  this machinery in hand, we now relate automata with JKBPs. We say
  joint protocol @{term "jp"} \emph{implements} a JKBP when they
  the same actions on the canonical of traces. Note that the
  of @{term "jp"} on other traces is arbitrary.

 ›

context IncrEnvironment
begin

definition
  implements :: "('a, 'obs, 'aAct, 'ps) JointProtocol → bool"
where
  "implements jp ≡ (∀t ∈ jkbpC. set ∘ actJP jp t = set ∘ jAction MC t)"

text‹

  there are environments where the canonical trace set @{term
 jkbpC"} can be generated by actions that differ from those prescribed
  the JKBP. We can show that the \emph{implements} relation is a
  requirement than the mere trace-inclusion required by the
 emph{represents} relation of \S\ref{sec:kbps-canonical-kripke}.

 ›
(*<*)

lemma implementsI[intro]:
  "(∧t. t ∈ jkbpC ==> set ∘ actJP jp t = set ∘ jAction MC t)
  ==> implements jp"
  unfolding implements_def by simp

lemma implementsE[elim]:
  assumes impl: "implements jp"
      and tC: "t ∈ jkbpC"
     shows "set ∘ actJP jp t = set ∘ jAction MC t"
  using assms unfolding implements_def by simp

lemma implements_actJP_jAction:
   assumes impl: "implements jp"
       and tCn: "t ∈ jkbpCn n"
  shows "set (actJP jp t a) = set (jAction (MCn n) t a)" (is "?lhs = ?rhs")
proof -
  from tCn have tC: "t ∈ jkbpC" by blast
  hence "?lhs = (set ∘ jAction MC t) a"
    using implementsE[OF impl, symmetric] by auto
  also have "... = set (jAction (MCn n) t a)"
    by (simp add: jkbpC_jkbpCn_jAction_eq[OF tCn])
  finally show ?thesis .
qed

(*>*)
lemma implements_represents:
  assumes impl: "implements jp"
  shows "represents (jpTraces jp)"
(*<*)
proof -
  { fix n
    have "{ t ∈ jpTraces jp . tLength t = n }
        = { t ∈ jkbpC . tLength t = n }"
    proof(induct n)
      case 0 thus ?case
        by (auto dest: jpTraces_init_length_inv iff: jkbpC_traces_of_length)
    next
      case (Suc n)
      hence indhyp: "{t ∈ jpTraces jp . tLength t = n} = jkbpCn n"
        by (simp add: jkbpC_traces_of_length)

      have "{t ∈ jpTraces jp. tLength t = Suc n}
          = {t ↝ s |eact aact t s. t ∈ jkbpCn n
                      ∧ eact ∈ set (envAction (tLast t))
                      ∧ (∀a. aact a ∈ set (actJP jp t a))
                      ∧ s = envTrans eact aact (tLast t) }"
        using indhyp by (simp add: jpTraces_step_length_inv)
      also have "... = jkbpCn (Suc n)"
        apply (auto iff: Let_def)
        apply (auto iff: implements_actJP_jAction[OF impl, symmetric])
        done
      finally show ?case by (auto iff: jkbpC_traces_of_length)
    qed }
  hence R: "jpTraces jp = jkbpC" by auto
  from R jkbpC_represents
  show "represents (jpTraces jp)" by simp
qed

lemma implements_ind_jkbpC:
  assumes acts: "∧a n t.
                  [ {t ∈ jpTraces jp. tLength t = n} = jkbpCn n; t ∈ jkbpCn n ]
                  ==> actJP jp t a = jAction MC t a"
  shows "implements jp"
proof -
  let ?T = "jpTraces jp"

  from acts have acts':
      "∧n t. [ {t ∈ jpTraces jp. tLength t = n} = jkbpCn n; t ∈ jkbpCn n ]
          ==> actJP jp t = jAction (MCn n) t"
    by (simp only: jkbpC_jkbpCn_jAction_eq)

  from acts have acts':
      "∧n t. [ {t ∈ jpTraces jp. tLength t = n} = jkbpCn n; t ∈ jkbpCn n ]
          ==> actJP jp t = jAction (MCn n) t"
    apply -
    apply (rule ext)
    apply simp
    using jkbpC_jkbpCn_jAction_eq
    apply simp
    done

  { fix n
    have "{ t ∈ ?T . tLength t = n } = { t ∈ jkbpC . tLength t = n }"
    proof(induct n)
      case 0 thus ?case
        by (auto dest: jpTraces_init_length_inv iff: jkbpC_traces_of_length)
    next
      case (Suc n)
      hence indhyp: "{t ∈ ?T. tLength t = n} = jkbpCn n"
        by (simp add: jkbpC_traces_of_length)

      have "{t ∈ jpTraces jp. tLength t = Suc n}
          = {t ↝ s |eact aact t s. t ∈ jkbpCn n
                      ∧ eact ∈ set (envAction (tLast t))
                      ∧ (∀a. aact a ∈ set (actJP jp t a))
                      ∧ s = envTrans eact aact (tLast t) }"
        using indhyp by (simp add: jpTraces_step_length_inv)
      also have "... = jkbpCn (Suc n)"
        apply (auto iff: Let_def)
         apply (drule acts'[OF indhyp, symmetric])
         apply auto[1]
        apply (drule acts'[OF indhyp, symmetric])
        apply auto[1]
        done
      finally show ?case
        apply (auto iff: jkbpC_traces_of_length)
        done
    qed
    hence "∀t∈jkbpCn n. actJP jp t = jAction (MCn n) t"
      apply clarsimp
      apply (rule acts')
       apply (auto iff: jkbpC_traces_of_length)
      done
    hence "∀t∈jkbpCn n. actJP jp t = jAction MC t"
      apply clarsimp
      by ( rule sync_jview_jAction_eq[where n="n"]
         , auto iff: jkbpC_traces_of_length)
  }
  thus ?thesis
    unfolding implements_def jkbpC_def
    apply clarsimp
    done
qed

(*>*)
text‹

  proof is by a straightfoward induction over the lengths of traces
  by the joint protocol.

  final piece of technical machinery allows us to refine automata
 : we say that two joint protocols are \emph{behaviourally
 } if the actions they propose coincide for each canonical
 . The implementation relation is preserved by this relation.

 ›

definition
  behaviourally_equiv :: "('a, 'obs, 'aAct, 'ps) JointProtocol
                        → ('a, 'obs, 'aAct, 'ps') JointProtocol
                        → bool"
where
  "behaviourally_equiv jp jp' ≡ ∀t ∈ jkbpC. set ∘ actJP jp t = set ∘ actJP jp' t"

(*<*)
lemma behaviourally_equivI[intro]:
  "(∧t. t ∈ jkbpC ==> set ∘ actJP jp t = set ∘ actJP jp' t)
    ==> behaviourally_equiv jp jp'"
  unfolding behaviourally_equiv_def by simp
(*>*)

lemma behaviourally_equiv_implements:
  assumes "behaviourally_equiv jp jp'"
  shows "implements jp ⟷ implements jp'"
(*<*)
  using assms unfolding behaviourally_equiv_def implements_def by simp
(*>*)
text‹›

end (* context IncrEnvironment *)

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

subsection‹Automata using Equivalence Classes›

text‹

  now show that there is an implementation of every JKBP with respect
  every incremental synchronous view. Intuitively the states of the
  for agent @{term "a"} represent the equivalence classes of
  that @{term "a"} considers possible, and the transitions update
  sets according to her KBP.

 ›

context IncrEnvironment
begin

definition
  mkAutoEC :: "('a, 'obs, 'aAct, 's Trace set) JointProtocol"
where
  "mkAutoEC ≡ λa.
     ( pInit = λobs. { t ∈ jkbpC . jviewInit a obs = jview a t },
       pTrans = λobs ps. { t |t t'. t ∈ jkbpC ∧ t' ∈ ps
                                 ∧ jview a t = jviewIncr a obs (jview a t') },
       pAct = λps. jAction MC (SOME t. t ∈ ps) a )"

text‹

  function ‹SOME› is Hilbert's indefinite description
  @{term "ε"}, used here to choose an arbitrary trace from the
  state.

  this automaton maintains the correct equivalence class on a trace
 {term "t"} follows from an easy induction over @{term "t"}.

 ›

lemma mkAutoEC_ec:
  assumes "t ∈ jkbpC"
  shows "runJP mkAutoEC t a = { t' ∈ jkbpC . jview a t' = jview a t }"
(*<*)
  using assms
  apply (induct t)
   apply (auto simp add: mkAutoEC_def jviewInit)[1]
  apply simp
  apply (subst mkAutoEC_def)
  apply (auto iff: Let_def jviewIncr)
  done
(*>*)

text‹

  can show that the construction yields an implementation by
  to the previous lemma and showing that the @{term "pAct"}
  coincide.

 ›

lemma mkAutoEC_implements: "implements mkAutoEC"
(*<*)
  apply (rule implements_ind_jkbpC)
  apply (subst mkAutoEC_def)
  apply simp
  apply (subgoal_tac "t ∈ jkbpC")
   using mkAutoEC_ec
   apply simp
   apply (rule S5n_jAction_eq)
    apply simp_all
    apply (rule_tac a=t in someI2)
     apply simp_all
    unfolding mkM_def
    apply auto
   done
(*>*)

text‹

  definition leans on the canonical trace set jkbpC, and is indeed
 : we can enumerate all canonical traces and are sure to find
  that has the view we expect. Then it is sufficient to consider
  traces of the same length due to synchrony. We would need to do
  computation dynamically, as the automaton will (in general) have
  infinite state space.

 ›

end (* context IncrEnvironment *)

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

subsection‹Simulations›

text‹
 label{sec:kbps-theory-automata-env-sims}

  goal now is to reduce the space required by the automaton
  by @{term "mkAutoEC"} by \emph{simulating} the equivalence
  (\S\ref{sec:kripke-theory-simulations}).

  following locale captures the framework of 🚫‹"Ron:1996"›:

 ›

locale SimIncrEnvironment =
  IncrEnvironment jkbp envInit envAction envTrans envVal jview envObs
                  jviewInit jviewIncr
    for jkbp :: "('a, 'p, 'aAct) JKBP"

    and envInit :: "'s list"
    and envAction :: "'s → 'eAct list"
    and envTrans :: "'eAct → ('a → 'aAct) → 's → 's"
    and envVal :: "'s → 'p → bool"
    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a → 's → 'obs"
    and jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tv) IncrJointView"
+ fixes simf :: "'s Trace → 'ss"
  fixes simRels :: "'a → 'ss Relation"
  fixes simVal :: "'ss → 'p → bool"
  assumes simf: "sim MC (mkKripke (simf ` jkbpC) simRels simVal) simf"

context SimIncrEnvironment
begin

text‹

  that the back tick ‹`› is Isabelle/HOL's relational image
 . In context it says that @{term "simf"} must be a simulation
  @{term "jkbpC"} to its image under @{term "simf"}.

  we lift our familiar canonical trace sets and Kripke
  through the simulation.

 ›

abbreviation jkbpCSn :: "nat → 'ss set"(*<*)(\<open>jkbpCS\<^bsub>_\<^esub>\<close>)(*>*) where
  "jkbpCS ≡ simf ` jkbpC"

abbreviation jkbpCS :: "'ss set" where
  "jkbpCS ≡ simf ` jkbpC"

abbreviation MCSn :: "nat → ('a, 'p, 'ss) KripkeStructure"(*<*)(\<open>MCS\<^bsub>_\<^esub>\<close>)(*>*) where
  "MCS ≡ mkKripke jkbpCS simRels simVal"

abbreviation MCS :: "('a, 'p, 'ss) KripkeStructure" where
  "MCS ≡ mkKripke jkbpCS simRels simVal"
(*<*)
lemma jkbpCSn_jkbpCS_subset:
  "jkbpCSn n ⊆ jkbpCS"
  by (rule image_mono[OF jkbpCn_jkbpC_subset])

(*>*)
text‹

  will be often be concerned with the equivalence class of traces
  by agent @{term "a"}'s view:

 ›

abbreviation sim_equiv_class :: "'a → 's Trace → 'ss set" where
  "sim_equiv_class a t ≡ simf ` { t' ∈ jkbpC . jview a t' = jview a t }"

abbreviation jkbpSEC :: "'ss set set" where
  "jkbpSEC ≡ ∪a. sim_equiv_class a ` jkbpC"

text‹

  some effort we can show that the temporal slice of the simulated
  is adequate for determining the actions of the JKBP. The
  is tedious and routine, exploiting the sub-model property
 \S\ref{sec:generated_models}).

 ›
(*<*)

lemma sim_submodel_aux:
  assumes s: "s ∈ worlds (MCSn n)"
  shows "gen_model MCS s = gen_model (MCSn n) s"
proof(rule gen_model_subset[where T="jkbpCSn n"])
  from s show "s ∈ worlds MCS"
    by (simp add: subsetD[OF jkbpCSn_jkbpCS_subset])
  from s show "s ∈ worlds (MCSn n)" by assumption
next
  fix a
  show "relations MCS a ∩ jkbpCSn n × jkbpCSn n
      = relations (MCSn n) a ∩ jkbpCSn n × jkbpCSn n"
    by (simp add: Int_ac Int_absorb1
                  relation_mono[OF jkbpCSn_jkbpCS_subset jkbpCSn_jkbpCS_subset])
next
  from s
  show "(∪a. relations (MCSn n) a)^* `` {s} ⊆ jkbpCSn n"
    apply (clarsimp simp del: mkKripke_simps)
    apply (erule kripke_rels_trc_worlds)
    apply auto
    done
next
  from s obtain t
    where st: "s = simf t"
      and tCn: "t ∈ jkbpCn n"
    by fastforce
  from tCn have tC: "t ∈ jkbpC" by blast
  { fix t'
    assume tt': "(t, t') ∈ (∪a. relations MC a)<sup>*</sup>"
    from tC tt' have t'C: "t' ∈ jkbpC"
      by - (erule kripke_rels_trc_worlds, simp_all)
    from tCn tt' have t'Len: "tLength t' = n"
      by (auto dest: sync_tLength_eq_trc[where as=UNIV])
    from t'C t'Len have "t' ∈ jkbpCn n"
      by - (erule jkbpC_tLength_inv) }
  hence "(∪a. relations MC a)<sup>*</sup> `` {t} ⊆ jkbpCn n"
    by clarsimp
  hence "simf ` ((∪a. relations MC a)^* `` {t}) ⊆ jkbpCSn n"
    by (rule image_mono)
  with st tC
  show "(∪a. relations MCS a)<sup>*</sup> `` {s} ⊆ jkbpCSn n"
    using sim_trc_commute[OF _ simf, where t=t]
    by simp
qed simp_all
(*>*)

lemma jkbpC_jkbpCSn_jAction_eq:
  assumes tCn: "t ∈ jkbpCn n"
  shows "jAction MC t = jAction (MCSn n) (simf t)"
(*<*) (is "?lhs = ?rhs")
proof -
  have "?lhs = jAction MCS (simf t)"
    by (simp add: simulation_jAction_eq simf jkbpCn_jkbpC_inc[OF tCn])
  also have "... = ?rhs"
    using tCn
    by - ( rule gen_model_jAction_eq[OF sim_submodel_aux, where w="simf t"]
         , auto intro: gen_model_world_refl )
  finally show ?thesis .
qed
(*>*)

end (* context SimIncrEnvironment *)

text‹

  can be shown that a suitable simulation into a finite structure is
  to establish the existence of finite-state implementations
 🚫‹‹Theorem~2› in "Ron:1996"›: essentially we apply the simulation to
  states of @{term "mkAutoEC"}. However this result does not make it
  how the transition function can be incrementally
 . One approach is to maintain @{term "jkbpC"} while
  the automaton, which is quite space inefficient.

  we would like to compute the possible @{term
 sim_equiv_class"} successors of a given @{term "sim_equiv_class"}
  reference to @{term "jkbpC"}, and this should be possible as
  reachable simulated worlds must contain enough information to
  themselves from every other simulated world (reachable
  not) that represents a trace that is observationally distinct to
  own.

  leads us to asking for some extra functionality of our
 , which we do in the following section.

 ›

subsection‹Automata using simulations›

text_raw‹
 label{sec:kbps-automata-synthesis-alg}

 begin{figure}[hp]
 begin{isabellebody}%
 ›
locale AlgSimIncrEnvironment =
  SimIncrEnvironment jkbp envInit envAction envTrans envVal
                     jview envObs jviewInit jviewIncr simf simRels simVal
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s → 'eAct list"
    and envTrans :: "'eAct → ('a → 'aAct) → 's → 's"
    and envVal :: "'s → 'p → bool"

    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a → 's → 'obs"
    and jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tv) IncrJointView"

    and simf :: "'s Trace → 'ss"
    and simRels :: "'a → 'ss Relation"
    and simVal :: "'ss → 'p → bool"

+ fixes simAbs :: "'rep → 'ss set"

    and simObs :: "'a → 'rep → 'obs"
    and simInit :: "'a → 'obs → 'rep"
    and simTrans :: "'a → 'rep → 'rep list"
    and simAction :: "'a → 'rep → 'aAct list"

  assumes simInit:
            "∀a iobs. iobs ∈ envObs a ` set envInit
                   ⟶ simAbs (simInit a iobs)
                     = simf ` { t' ∈ jkbpC. jview a t' = jviewInit a iobs }"
      and simObs:
            "∀a ec t. t ∈ jkbpC ∧ simAbs ec = sim_equiv_class a t
                   ⟶ simObs a ec = envObs a (tLast t)"
      and simAction:
            "∀a ec t. t ∈ jkbpC ∧ simAbs ec = sim_equiv_class a t
                   ⟶ set (simAction a ec) = set (jAction MC t a)"
      and simTrans:
            "∀a ec t. t ∈ jkbpC ∧ simAbs ec = sim_equiv_class a t
                   ⟶ simAbs ` set (simTrans a ec)
                     = { sim_equiv_class a (t' ↝ s)
                         |t' s. t' ↝ s ∈ jkbpC ∧ jview a t' = jview a t }"
text_raw‹
 end{isabellebody}%
 begin{isamarkuptext}%
 caption{The ‹SimEnvironment› locale extends the @{term
 Environment"} locale with simulation and algorithmic operations. The
  ‹`› is Isabelle/HOL's image-of-a-set-under-a-function
 .}
 label{fig:kbps-theory-auto-SimEnvironment}
 end{isamarkuptext}%
 end{figure}
 ›

text‹

  locale in Figure~\ref{fig:kbps-theory-auto-SimEnvironment} captures
  extra requirements of a simulation.

  we relate the concrete representation @{typ "'rep"} of
  classes under simulation to differ from the abstract
  @{typ "'ss set"} using the abstraction function @{term
 simAbs"} 🚫‹"EdR:cup98"›; there is no one-size-fits-all concrete
 , as we will see.

  we ask for a function @{term "simInit a iobs"} that
  generates a representation of the equivalence class of
  initial states that are possible for agent @{term "a"} given
  valid initial observation @{term "iobs"}.

  the @{term "simObs"} function allows us to partition the
  of @{term "simTrans"} according to the recurrent observation
  agent @{term "a"} makes of the equivalence class.

 , the function @{term "simAction"} computes a list of actions
  by the JKBP on a state that concretely represents a canonical
  class.

  we expect to compute the list of represented @{term
 sim_equiv_class"} successors of a given @{term "sim_equiv_class"}
  @{term "simTrans"}.

  that these definitions are stated relative to the environment and
  JKBP, allowing us to treat specialised cases such as broadcast
 \S\ref{sec:kbps-theory-spr-deterministic-protocols} and
 S\ref{sec:kbps-theory-spr-non-deterministic-protocols}).

  these functions in hand, we can define our desired automaton:

 ›

definition (in AlgSimIncrEnvironment)
  mkAutoSim :: "('a, 'obs, 'aAct, 'rep) JointProtocol"
where
  "mkAutoSim ≡ λa.
     ( pInit = simInit a,
       pTrans = λobs ec. (SOME ec'. ec' ∈ set (simTrans a ec)
                                  ∧ simObs a ec' = obs),
       pAct = simAction a )"
(*<*)

context AlgSimIncrEnvironment
begin

lemma jAction_simAbs_cong:
  assumes tC: "t ∈ jkbpC"
      and ec: "simAbs ec = sim_equiv_class a t"
      and ec': "simAbs ec = simAbs ec'"
  shows "set (simAction a ec) = set (simAction a ec')"
  using assms simAction[rule_format, where a=a and t=t] tC by simp

lemma simTrans_simAbs_cong:
  assumes tC: "t ∈ jkbpC"
      and ec: "simAbs ec = sim_equiv_class a t"
      and ec': "simAbs ec = simAbs ec'"
  shows "simAbs ` set (simTrans a ec) = simAbs ` set (simTrans a ec')"
  using assms simTrans[rule_format, where a=a and t=t] tC by simp

lemma mkAutoSim_simps[simp]:
  "pInit (mkAutoSim a) = simInit a"
  "pTrans (mkAutoSim a) = (λobs ec. (SOME ec'. ec' ∈ set (simTrans a ec) ∧ simObs a ec' = obs))"
  "pAct (mkAutoSim a) = simAction a"
  unfolding mkAutoSim_def by simp_all

end (* context AlgSimIncrEnvironment *)

(*>*)
text‹

  automaton faithfully constructs the simulated equivalence class of
  given trace:

 ›

lemma (in AlgSimIncrEnvironment) mkAutoSim_ec:
  assumes tC: "t ∈ jkbpC"
  shows "simAbs (runJP mkAutoSim t a) = sim_equiv_class a t"
(*<*)
using tC
proof(induct t)
  case (tInit s) thus ?case
    by (simp add: jviewInit[rule_format, symmetric] simInit)
next
  case (tStep t s)
  hence tC: "t ∈ jkbpC" by blast

      from tC tStep
      have F: "simAbs ` set (simTrans a (runJP mkAutoSim t a))
             = { sim_equiv_class a (t' ↝ s)
                 |t' s. t' ↝ s ∈ jkbpC ∧ jview a t' = jview a t}"
        using simTrans[rule_format, where a=a and t=t and ec="runJP mkAutoSim t a"]
        apply clarsimp
        done

      from tStep
      have G: "sim_equiv_class a (t ↝ s)
             ∈ { sim_equiv_class a (t' ↝ s)
                |t' s. t' ↝ s ∈ jkbpC ∧ jview a t' = jview a t}"
        by auto

      from F G
      have H: "sim_equiv_class a (t ↝ s) ∈ simAbs ` set (simTrans a (runJP mkAutoSim t a))"
        by simp

      then obtain r
        where R: "r ∈ set (simTrans a (runJP mkAutoSim t a))"
        and S: "simAbs r = sim_equiv_class a (t ↝ s)"
        by auto

  show ?case
  proof(simp, rule someI2)
    from R S tStep tC
    show "r ∈ set (simTrans a (runJP mkAutoSim t a)) ∧ simObs a r = envObs a s"
      using simObs[rule_format, where t="t↝s" and a=a]
      apply clarsimp
      done
  next
    fix x assume x: "x ∈ set (simTrans a (runJP mkAutoSim t a)) ∧ simObs a x = envObs a s"

    from x
    have A: "simObs a x = envObs a s" by simp

    from x
    have "simAbs x ∈ simAbs ` set (simTrans a (runJP mkAutoSim t a))" by simp
    with tStep tC
    have "simAbs x ∈ { sim_equiv_class a (t' ↝ s)
                         |t' s. t' ↝ s ∈ jkbpC ∧ jview a t' = jview a t}"
      using simTrans[rule_format, where a=a and t=t] by simp
    then obtain t' s'
      where X: "simAbs x = sim_equiv_class a (t' ↝ s')"
          and Y: "t' ↝ s' ∈ jkbpC"
          and Z: "jview a t' = jview a t"
      by auto

    from A X Y Z
    show "simAbs x = sim_equiv_class a (t ↝ s)"
      using simObs[rule_format, where a=a and t="t'↝s'", symmetric]
      by (simp add: jviewIncr)
  qed
qed

(*>*)
text‹

  follows from a simple induction on @{term "t"}.

  following is a version of the Theorem 2 of 🚫‹"Ron:1996"›.

 ›

theorem (in AlgSimIncrEnvironment) mkAutoSim_implements:
  "implements mkAutoSim"
(*<*)
  apply rule
  apply rule
  apply (auto dest: jkbpCn_jkbpC_inc iff: mkAutoSim_ec simAction)
  done
(*>*)

text‹

  reader may care to contrast these structures with the
 emph{progression structures} of 🚫‹"Ron:1997"›, where states
  entire Kripke structures, and expanding the automaton is
  with bisimulation reduction to ensure termination when a
 -state implementation exists (see \S\ref{sec:kbps-alg-auto-min})
  also use simulations in Appendix~\ref{ch:complexity} to show the
  of some related model checking problems.

  now review a simple \emph{depth-first search} (DFS) theory, and an
  of finite maps, before presenting the algorithm for KBP
 .

 FloatBarrier

 ›

(*<*)
end
(*>*)