Theory KBPsAlg

(*<*)
theory KBPsAlg
imports KBPsAuto DFS MapOps
begin
(*>*)

subsection‹An algorithm for automata synthesis›

text‹

\label{sec:kbps-alg}

We now show how to construct the automaton defined by @{term
"mkAutoSim"} (\S\ref{sec:kbps-automata-synthesis-alg}) using the DFS
of \S\ref{sec:dfs}.

From here on we assume that the environment consists of only a finite
set of states:

›

locale FiniteEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s ⇒ 'eAct list"
    and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's"
    and envVal :: "'s ⇒ 'p ⇒ bool"
    and envObs :: "'a ⇒ 's ⇒ 'obs"

text_raw‹
\begin{figure}[p]
\begin{isabellebody}%
›
locale Algorithm =
  FiniteEnvironment jkbp envInit envAction envTrans envVal envObs
+ AlgSimIncrEnvironment jkbp envInit envAction envTrans envVal jview envObs
               jviewInit jviewIncr
               simf simRels simVal simAbs simObs simInit simTrans simAction
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s ⇒ 'eAct list"
    and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's"
    and envVal :: "'s ⇒ 'p ⇒ bool"
    and jview :: "('a, 's, 'tobs) JointView"

    and envObs :: "'a ⇒ 's ⇒ 'obs"
    and jviewInit :: "('a, 'obs, 'tobs) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tobs) IncrJointView"

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

    and 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"

+ fixes aOps :: "('ma, 'rep, 'aAct list) MapOps"
    and tOps :: "('mt, 'rep × 'obs, 'rep) MapOps"

  assumes aOps: "MapOps simAbs jkbpSEC aOps"
      and tOps: "MapOps (λk. (simAbs (fst k), snd k)) (jkbpSEC × UNIV) tOps"
text_raw‹
  \end{isabellebody}%
  \caption{The ‹Algorithm› locale.}
  \label{fig:kbps-alg-alg-locale}
\end{figure}
›

text (in Algorithm) ‹

The @{term "Algorithm"} locale, shown in
Figure~\ref{fig:kbps-alg-alg-locale}, also extends the @{term
"AlgSimIncrEnvironment"} locale with a pair of finite map operations:
@{term "aOps"} is used to map automata states to lists of actions, and
@{term "tOps"} handles simulated transitions. In both cases the maps
are only required to work on the abstract domain of simulated
canonical traces. Note also that the space of simulated equivalence
classes of type @{typ "'ss"} must be finite, but there is no
restriction on the representation type @{typ "'rep"}.

We develop the algorithm for a single, fixed agent, which requires us
to define a new locale @{term "AlgorithmForAgent"} that extends ‹Algorithm› with an extra parameter designating the agent:

›

locale AlgorithmForAgent =
  Algorithm jkbp envInit envAction envTrans envVal jview envObs
            jviewInit jviewIncr
            simf simRels simVal simAbs simObs simInit simTrans simAction
            aOps tOps(*<*)
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s ⇒ 'eAct list"
    and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's"
    and envVal :: "'s ⇒ 'p ⇒ bool"
    and jview :: "('a, 's, 'tobs) JointView"

    and envObs :: "'a ⇒ 's ⇒ 'obs"
    and jviewInit :: "('a, 'obs, 'tobs) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tobs) IncrJointView"

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

    and 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"

    and aOps :: "('ma, 'rep, 'aAct list) MapOps"
    and tOps :: "('mt, 'rep × 'obs, 'rep) MapOps"
(*>*)

  ― ‹...›
+ fixes a :: "'a"

subsubsection‹DFS operations›

text‹

We represent the automaton under construction using a record:

›

record ('ma, 'mt) AlgState =
  aActs :: "'ma"
  aTrans :: "'mt"

context AlgorithmForAgent
begin

text‹

We instantiate the DFS theory with the following functions.

A node is an equivalence class of represented simulated traces.

›

definition k_isNode :: "'rep ⇒ bool" where
  "k_isNode ec ≡ simAbs ec ∈ sim_equiv_class a ` jkbpC"

text‹

The successors of a node are those produced by the simulated
transition function.

›

abbreviation k_succs :: "'rep ⇒ 'rep list" where
  "k_succs ≡ simTrans a"

text‹

The initial automaton has no transitions and no actions.

›

definition k_empt :: "('ma, 'mt) AlgState" where
  "k_empt ≡ ⦇ aActs = empty aOps, aTrans = empty tOps ⦈"

text‹

We use the domain of the action map to track the set of nodes the DFS
has visited.

›

definition k_memb :: "'rep ⇒ ('ma, 'mt) AlgState ⇒ bool" where
  "k_memb s A ≡ isSome (lookup aOps (aActs A) s)"

text‹

We integrate a new equivalence class into the automaton by updating
the action and transition maps:

›

definition actsUpdate :: "'rep ⇒ ('ma, 'mt) AlgState ⇒ 'ma" where
  "actsUpdate ec A ≡ update aOps ec (simAction a ec) (aActs A)"

definition transUpdate :: "'rep ⇒ 'rep ⇒ 'mt ⇒ 'mt" where
  "transUpdate ec ec' at ≡ update tOps (ec, simObs a ec') ec' at"

definition k_ins :: "'rep ⇒ ('ma, 'mt) AlgState ⇒ ('ma, 'mt) AlgState" where
  "k_ins ec A ≡ ⦇ aActs = actsUpdate ec A,
                   aTrans = foldr (transUpdate ec) (k_succs ec) (aTrans A) ⦈"

text‹

The required properties are straightforward to show.

›

(*<*)

lemma k_isNode_cong:
  "simAbs ec' = simAbs ec ⟹ k_isNode ec' ⟷ k_isNode ec"
  unfolding k_isNode_def by simp

lemma alg_MapOps_empty[simp]:
  "k_isNode ec ⟹ lookup aOps (empty aOps) ec = None"
  "k_isNode (fst k) ⟹ lookup tOps (empty tOps) k = None"
  unfolding k_isNode_def
  using MapOps_emptyD[OF _ aOps] MapOps_emptyD[OF _ tOps] by blast+

lemma alg_aOps_lookup_update[simp]:
  "⟦ k_isNode ec; k_isNode ec' ⟧ ⟹ lookup aOps (update aOps ec e M) ec' = (if simAbs ec' = simAbs ec then Some e else lookup aOps M ec')"
  unfolding k_isNode_def
  using MapOps_lookup_updateD[OF _ _ aOps] by blast

lemma alg_tOps_lookup_update[simp]:
  "⟦ k_isNode (fst k); k_isNode (fst k') ⟧ ⟹ lookup tOps (update tOps k e M) k' = (if (simAbs (fst k'), snd k') = (simAbs (fst k), snd k) then Some e else lookup tOps M k')"
  unfolding k_isNode_def
  using MapOps_lookup_updateD[OF _ _ tOps] by blast

lemma k_succs_is_node[intro, simp]:
  assumes x: "k_isNode x"
  shows "list_all k_isNode (k_succs x)"
proof -
  from x obtain t
    where tC: "t ∈ jkbpC"
      and sx: "simAbs x = sim_equiv_class a t"
    unfolding k_isNode_def by blast
  have F: "⋀y. y ∈ set (k_succs x) ⟹ simAbs y ∈ simAbs ` set (k_succs x)" by simp
  show ?thesis
    using simTrans[rule_format, where a=a and t=t] tC sx
    unfolding k_isNode_def [abs_def]
    apply (auto iff: list_all_iff)
    apply (frule F)
    apply (auto)
    done
qed

lemma k_memb_empt[simp]:
  "k_isNode x ⟹ ¬k_memb x k_empt"
  unfolding k_memb_def k_empt_def by simp

(*>*)

subsubsection‹Algorithm invariant›

text‹

The invariant for the automata construction is straightforward, viz
that at each step of the process the state represents an automaton
that concords with @{term "mkAutoSim"} on the visited equivalence
classes. We also need to know that the state has preserved the @{term
"MapOps"} invariants.

›

definition k_invariant :: "('ma, 'mt) AlgState ⇒ bool" where
  "k_invariant A ≡
      (∀ec ec'. k_isNode ec ∧ k_isNode ec' ∧ simAbs ec' = simAbs ec
        ⟶ lookup aOps (aActs A) ec = lookup aOps (aActs A) ec')
    ∧ (∀ec ec' obs. k_isNode ec ∧ k_isNode ec' ∧ simAbs ec' = simAbs ec
        ⟶ lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs))
    ∧ (∀ec. k_isNode ec ∧ k_memb ec A
        ⟶ (∃acts. lookup aOps (aActs A) ec = Some acts
                   ∧ set acts = set (simAction a ec)))
    ∧ (∀ec obs. k_isNode ec ∧ k_memb ec A
              ∧ obs ∈ simObs a ` set (simTrans a ec)
        ⟶ (∃ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
                  ∧ simAbs ec' ∈ simAbs ` set (simTrans a ec)
                  ∧ simObs a ec' = obs))"
(*<*)

lemma k_invariantI[intro]:
  "⟦ ⋀ec ec'. ⟦ k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec ⟧
       ⟹ lookup aOps (aActs A) ec = lookup aOps (aActs A) ec';
     ⋀ec ec' obs. ⟦ k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec ⟧
       ⟹ lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs);
     ⋀ec. ⟦ k_isNode ec; k_memb ec A ⟧
       ⟹ ∃acts. lookup aOps (aActs A) ec = Some acts ∧ set acts = set (simAction a ec);
     ⋀ec obs ecs'. ⟦ k_isNode ec; k_memb ec A; obs ∈ simObs a ` set (simTrans a ec) ⟧
       ⟹ ∃ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
               ∧ simAbs ec' ∈ simAbs ` set (simTrans a ec)
               ∧ simObs a ec' = obs ⟧
  ⟹ k_invariant A"
  unfolding k_invariant_def by (simp (no_asm_simp))

lemma k_invariantAOD:
  "⟦ k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec; k_invariant A ⟧
     ⟹ lookup aOps (aActs A) ec = lookup aOps (aActs A) ec'"
  unfolding k_invariant_def by blast

lemma k_invariantTOD:
  "⟦ k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec; k_invariant A ⟧
     ⟹ lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs)"
  unfolding k_invariant_def by blast

lemma k_invariantAD:
  "⟦ k_isNode ec; k_memb ec A; k_invariant A ⟧
     ⟹ ∃acts. lookup aOps (aActs A) ec = Some acts ∧ set acts = set (simAction a ec)"
  unfolding k_invariant_def by blast

lemma k_invariantTD:
  "⟦ k_isNode ec; k_memb ec A; obs ∈ simObs a ` set (simTrans a ec); k_invariant A ⟧
     ⟹ ∃ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
             ∧ simAbs ec' ∈ simAbs ` set (simTrans a ec)
             ∧ simObs a ec' = obs"
  unfolding k_invariant_def by blast

lemma k_invariant_empt[simp]:
  "k_invariant k_empt"
  apply rule
  apply auto
  apply (auto iff: k_empt_def)
  done

lemma k_invariant_step_new_aux:
  assumes X: "set X ⊆ set (k_succs x)"
      and x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "simAbs ec' ∈ simAbs ` set X"
      and S: "simAbs ec = simAbs x"
  shows "∃r. lookup tOps (foldr (transUpdate x) X Y) (ec, simObs a ec') = Some r
           ∧ simAbs r ∈ simAbs ` set (k_succs ec)
           ∧ simObs a r = simObs a ec'"
using X ec'
proof(induct X arbitrary: Y)
  case Nil thus ?case by simp
next
  case (Cons y ys) show ?case
  proof(cases "simAbs ec' = simAbs y")
    case False with x ec S Cons show ?thesis
      unfolding transUpdate_def
      apply clarsimp
      unfolding k_isNode_def
      apply (erule imageE)+
      apply (cut_tac a=a and t=ta and ec=x and ec'=ec in simTrans_simAbs_cong[symmetric])
      apply simp_all
      done
  next
    case True
    with Cons have F: "simAbs y ∈ simAbs ` set (k_succs x)"
      by auto
    from x obtain t
      where tC: "t ∈ jkbpC"
        and x': "simAbs x = sim_equiv_class a t"
      unfolding k_isNode_def by blast
    from F obtain t' s
      where "simAbs y = sim_equiv_class a (t' ↝ s)"
        and tsC: "t' ↝ s ∈ jkbpC"
        and tt': "jview a t = jview a t'"
      using simTrans[rule_format, where a=a and t=t] tC x' by auto
    with Cons.hyps[where Y11=Y] Cons(2) Cons(3) True S x ec show ?thesis
      unfolding transUpdate_def
      apply auto
      apply (subst simTrans_simAbs_cong[where t=t' and ec'=x])
       apply blast

       using x' tt'
       apply auto[1]

       apply simp

       apply (rule image_eqI[where x=y])
       apply simp
       apply simp
      using simObs[rule_format, where a=a and t="t'↝s"]
      apply simp
      done
  qed
qed

lemma k_invariant_step_new:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "ec' ∈ set (k_succs ec)"
      and S: "simAbs ec = simAbs x"
  shows "∃ec''. lookup tOps (aTrans (k_ins x A)) (ec, simObs a ec') = Some ec''
              ∧ simAbs ec'' ∈ simAbs ` set (k_succs ec)
              ∧ simObs a ec'' = simObs a ec'"
proof -
  from x ec'
  have ec': "simAbs ec' ∈ simAbs ` set (k_succs x)"
    unfolding k_isNode_def
    apply clarsimp
    apply (subst simTrans_simAbs_cong[OF _ _ S, symmetric])
    using S
    apply auto
    done
  thus ?thesis
    using k_invariant_step_new_aux[OF subset_refl x ec _ S, where ec'=ec']
    unfolding k_ins_def
    apply auto
    done
qed

lemma k_invariant_step_old_aux:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and S: "simAbs ec ≠ simAbs x"
  shows "lookup tOps (foldr (transUpdate x) X Y) (ec, obs)
       = lookup tOps Y (ec, obs)"
proof(induct X)
  case (Cons z zs) with x ec S show ?case
    by (cases "lookup tOps Y (ec, obs)") (simp_all add: transUpdate_def)
qed simp

lemma k_invariant_step_old:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and S: "simAbs ec ≠ simAbs x"
  shows "lookup tOps (aTrans (k_ins x A)) (ec, obs)
       = lookup tOps (aTrans A) (ec, obs)"
  unfolding k_ins_def
  using k_invariant_step_old_aux[OF x ec S]
  by simp

lemma k_invariant_frame:
  assumes B: "lookup tOps Y (ec, obs) = lookup tOps Y (ec', obs)"
      and x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "k_isNode ec'"
      and S: "simAbs ec' = simAbs ec"
  shows "lookup tOps (foldr (transUpdate x) X Y) (ec, obs) = lookup tOps (foldr (transUpdate x) X Y) (ec', obs)"
  apply (induct X)
  unfolding transUpdate_def
   using B
   apply simp
  using x ec ec' S
  apply simp
  done

lemma k_invariant_step[simp]:
  assumes N: "k_isNode x"
      and I: "k_invariant A"
      and M: "¬ k_memb x A"
  shows "k_invariant (k_ins x A)"
(*<*)
proof
  fix ec ec'
  assume ec: "k_isNode ec" and ec': "k_isNode ec'" and X: "simAbs ec' = simAbs ec"
  with N show "lookup aOps (aActs (k_ins x A)) ec = lookup aOps (aActs (k_ins x A)) ec'"
    unfolding k_ins_def actsUpdate_def
    using k_invariantAOD[OF ec ec' X I]
    apply simp
    done
next
  fix ec ec' obs
  assume ec: "k_isNode ec" and ec': "k_isNode ec'" and X: "simAbs ec' = simAbs ec"
  show "lookup tOps (aTrans (k_ins x A)) (ec, obs) = lookup tOps (aTrans (k_ins x A)) (ec', obs)"
    unfolding k_ins_def
    using k_invariant_frame[OF k_invariantTOD[OF ec ec' X I] N ec ec' X]
    apply simp
    done
next
  fix ec obs ecs'
  assume n: "k_isNode ec"
    and ec: "k_memb ec (k_ins x A)"
    and obs: "obs ∈ simObs a ` set (simTrans a ec)"
  show "∃ec'. lookup tOps (aTrans (k_ins x A)) (ec, obs) = Some ec'
            ∧ simAbs ec' ∈ simAbs ` set (k_succs ec)
            ∧ simObs a ec' = obs"
  proof(cases "simAbs ec = simAbs x")
    case True with N n obs show ?thesis
      using k_invariant_step_new by auto
  next
    case False with I N n ec obs show ?thesis
      apply (simp add: k_invariant_step_old)
      apply (rule k_invariantTD)
      apply simp_all
      unfolding k_ins_def k_memb_def actsUpdate_def
      apply simp
      done
  qed
next
  fix ec
  assume n: "k_isNode ec"
     and ec: "k_memb ec (k_ins x A)"
  show "∃acts. lookup aOps (aActs (k_ins x A)) ec = Some acts ∧ set acts = set (simAction a ec)"
  proof(cases "simAbs ec = simAbs x")
    case True with aOps N n show ?thesis
      unfolding k_ins_def actsUpdate_def
      apply clarsimp
      unfolding k_isNode_def
      apply clarsimp
      apply (erule jAction_simAbs_cong)
      apply auto
      done
  next
    case False with aOps N I M n ec show ?thesis
      unfolding k_ins_def actsUpdate_def
      apply simp
      apply (rule k_invariantAD)
      unfolding k_memb_def
      apply simp_all
      done
  qed
qed
(*>*)

(*>*)

text‹

Showing that the invariant holds of @{term "k_empt"} and is respected
by @{term "k_ins"} is routine.

The initial frontier is the partition of the set of initial states
under the initial observation function.

›

definition (in Algorithm) k_frontier :: "'a ⇒ 'rep list" where
  "k_frontier a ≡ map (simInit a ∘ envObs a) envInit"
(*<*)

lemma k_frontier_is_node[intro, simp]:
  "list_all k_isNode (k_frontier a)"
  unfolding k_frontier_def
  by (auto iff: simInit list_all_iff k_isNode_def jviewInit jviewIncr)
(*>*)

end (* context AlgorithmForAgent *)

text‹

We now instantiate the @{term "DFS"} locale with respect to the @{term
"AlgorithmForAgent"} locale. The instantiated lemmas are given the
mandatory prefix ‹KBPAlg› in the @{term "AlgorithmForAgent"}
locale.

›

sublocale AlgorithmForAgent
        < KBPAlg: DFS k_succs k_isNode k_invariant k_ins k_memb k_empt simAbs

(*<*)
  apply (unfold_locales)
  apply simp_all

  unfolding k_memb_def k_ins_def actsUpdate_def
  using aOps
  apply (auto iff: isSome_eq)[1]

  unfolding k_isNode_def
  apply clarsimp
  apply (erule simTrans_simAbs_cong)
  apply auto
  done
(*>*)

text_raw‹
\begin{figure}
\begin{isabellebody}%
›
definition
  alg_dfs :: "('ma, 'rep, 'aAct list) MapOps
         ⇒ ('mt, 'rep × 'obs, 'rep) MapOps
         ⇒ ('rep ⇒ 'obs)
         ⇒ ('rep ⇒ 'rep list)
         ⇒ ('rep ⇒ 'aAct list)
         ⇒ 'rep list
         ⇒ ('ma, 'mt) AlgState"
where
  "alg_dfs aOps tOps simObs simTrans simAction ≡
    let k_empt = ⦇ aActs = empty aOps, aTrans = empty tOps ⦈;
       k_memb = (λs A. isSome (lookup aOps (aActs A) s));
       k_succs = simTrans;
       actsUpdate = λec A. update aOps ec (simAction ec) (aActs A);
       transUpdate = λec ec' at. update tOps (ec, simObs ec') ec' at;
       k_ins = λec A. ⦇ aActs = actsUpdate ec A,
                         aTrans = foldr (transUpdate ec) (k_succs ec) (aTrans A) ⦈
     in gen_dfs k_succs k_ins k_memb k_empt"

text‹›

definition
  mkAlgAuto :: "('ma, 'rep, 'aAct list) MapOps
            ⇒ ('mt, 'rep × 'obs, 'rep) MapOps
            ⇒ ('a ⇒ 'rep ⇒ 'obs)
            ⇒ ('a ⇒ 'obs ⇒ 'rep)
            ⇒ ('a ⇒ 'rep ⇒ 'rep list)
            ⇒ ('a ⇒ 'rep ⇒ 'aAct list)
            ⇒ ('a ⇒ 'rep list)
            ⇒ ('a, 'obs, 'aAct, 'rep) JointProtocol"
where
  "mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier ≡ λa.
    let auto = alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a)
                       (frontier a)
     in ⦇ pInit = simInit a,
          pTrans = λobs ec. the (lookup tOps (aTrans auto) (ec, obs)),
          pAct = λec. the (lookup aOps (aActs auto) ec) ⦈"

text_raw‹
  \end{isabellebody}%
  \caption{The algorithm. The function @{term "the"} projects a value from the
    @{typ "'a option"} type, diverging on @{term "None"}.}
  \label{fig:kbps-alg-algorithm}
\end{figure}
›
(*<*)
lemma mkAutoSim_simps[simp]:
  "pInit (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a) = simInit a"
  "pTrans (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a)
 = (λobs ec. the (lookup tOps (aTrans (alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (frontier a))) (ec, obs)))"
  "pAct (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a)
 = (λec. the (lookup aOps (aActs (alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (frontier a))) ec))"
  unfolding mkAlgAuto_def
  apply (simp_all add: Let_def)
  done

(* Later we want to show that a particular DFS implementation does the
right thing. *)

definition
  alg_mk_auto :: "('ma, 'rep, 'aAct list) MapOps
                ⇒ ('mt, 'rep × 'obs, 'rep) MapOps
                ⇒ ('obs ⇒ 'rep)
                ⇒ ('ma, 'mt) AlgState
                ⇒ ('obs, 'aAct, 'rep) Protocol"
where
  "alg_mk_auto aOps tOps simInit k_dfs ≡
    ⦇ pInit = simInit,
      pTrans = λobs ec. the (lookup tOps (aTrans k_dfs) (ec, obs)),
      pAct = λec. the (lookup aOps (aActs k_dfs) ec)
    ⦈"

(*>*)
context AlgorithmForAgent
begin

text‹

The final algorithm, with the constants inlined, is shown in
Figure~\ref{fig:kbps-alg-algorithm}. The rest of this section shows
its correctness.

Firstly it follows immediately from ‹dfs_invariant› that the
invariant holds of the result of the DFS:

›
(*<*)

abbreviation
  "k_dfs ≡ KBPsAlg.alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (k_frontier a)"

(* This is a syntactic nightmare. *)

lemma k_dfs_gen_dfs_unfold[simp]:
  "k_dfs = gen_dfs k_succs k_ins k_memb k_empt (k_frontier a)"
  unfolding alg_dfs_def
  apply (fold k_empt_def k_memb_def actsUpdate_def transUpdate_def)
  apply (simp add: k_ins_def[symmetric])
  done

(*>*)
lemma k_dfs_invariant: "k_invariant k_dfs"
(*<*)
  using KBPAlg.dfs_invariant[where S="k_empt" and xs="k_frontier a"]
  by simp

(*>*)
text‹

Secondly we can see that the set of reachable equivalence classes
coincides with the partition of @{term "jkbpC"} under the simulation
and representation functions:

›

lemma k_reachable:
  "simAbs ` KBPAlg.reachable (set (k_frontier a)) = sim_equiv_class a ` jkbpC"
(*<*)(is "?lhs = ?rhs")
proof
  show "?lhs ⊆ ?rhs"
  proof
    fix sx assume "sx ∈ ?lhs"
    then obtain x
      where x: "x ∈ KBPAlg.reachable (set (k_frontier a))"
        and sx: "simAbs x = sx"
      by auto
    hence "x ∈ ({ (x, y). y ∈ set (k_succs x) })⇧*
                 `` set (map (simInit a ∘ envObs a) envInit)"
      unfolding KBPAlg.reachable_def k_frontier_def by simp
    then obtain s iobs
      where R: "(simInit a iobs, x) ∈ ({ (x, y). y ∈ set (k_succs x)})⇧*"
        and sI: "s ∈ set envInit"
        and iobs: "envObs a s = iobs"
      by auto
    from R x have "simAbs x ∈ ?rhs"
    proof(induct arbitrary: sx rule: rtrancl_induct)
      case base
      with sI iobs show ?case by (auto simp: jviewInit simInit)
    next
      case (step x y)
      with sI iobs
      have "simAbs x ∈ sim_equiv_class a ` jkbpC"
        unfolding KBPAlg.reachable_def Image_def k_frontier_def
        by auto
      then obtain t
        where tC: "t ∈ jkbpC"
          and F: "simAbs x = sim_equiv_class a t"
        by auto
      from step
      have "simAbs y ∈ simAbs ` set (k_succs x)" by auto
      thus  ?case
        using simTrans[rule_format, where a=a and t=t] tC F by auto
    qed
    with sx show "sx ∈ ?rhs" by simp
  qed
next
  show "?rhs ⊆ ?lhs"
  proof
    fix ec assume "ec ∈ ?rhs"
    then obtain t
      where tC: "t ∈ jkbpC"
        and ec: "ec = sim_equiv_class a t"
      by auto
    thus "ec ∈ ?lhs"
    proof(induct t arbitrary: ec)
      case (tInit s) thus ?case
        unfolding KBPAlg.reachable_def (* FIXME ouch this is touchy *)
        unfolding k_frontier_def
        apply simp
        apply (rule image_eqI[where x="simInit a (envObs a s)"])
         apply (simp add: simInit jviewInit)
        apply (rule ImageI[where a="simInit a (envObs a s)"])
        apply auto
        done
    next
      case (tStep t s)
      hence tsC: "t ↝ s ∈ jkbpC"
        and ec: "ec = sim_equiv_class a (t ↝ s)"
        and "sim_equiv_class a t
           ∈ simAbs ` DFS.reachable k_succs (set (k_frontier a))"
        by auto
      then obtain rect
        where rect: "rect ∈ DFS.reachable k_succs (set (k_frontier a))"
          and srect: "simAbs rect = sim_equiv_class a t"
        by auto
      from tsC ec srect
      have "ec ∈ simAbs ` set (simTrans a rect)"
        using simTrans[rule_format, where a=a and t="t" and ec="rect"] srect by auto
      then obtain rec
        where rec: "ec = simAbs rec"
          and F: "rec ∈ set (simTrans a rect)"
        by auto
      from rect obtain rec0
        where rec0: "rec0 ∈ set (k_frontier a)"
          and rec0rect: "(rec0, rect) ∈ ({ (x, y). y ∈ set (k_succs x)})⇧*"
        unfolding KBPAlg.reachable_def by auto
      show ?case
        apply -
        apply (rule image_eqI[where x="rec"])
         apply (rule rec)
        unfolding KBPAlg.reachable_def
        apply (rule ImageI[where a="rec0"])
         apply (rule rtrancl_into_rtrancl[where b="rect"])
          apply (rule rec0rect)
         apply clarsimp
         apply (rule F)
         apply (rule rec0)
         done
     qed
   qed
qed
(*>*)
text‹

Left to right follows from an induction on the reflexive, transitive
closure, and right to left by induction over canonical traces.

This result immediately yields the same result at the level of
representations:

›

lemma k_memb_rep:
  assumes N: "k_isNode rec"
  shows "k_memb rec k_dfs"
(*<*)
proof -
  from N obtain rec'
    where r: "rec' ∈ DFS.reachable k_succs (set (k_frontier a))"
      and rec': "simAbs rec = simAbs rec'"
    unfolding k_isNode_def by (auto iff: k_reachable[symmetric])

  from N k_isNode_cong[OF rec', symmetric]
  have N': "k_isNode rec'"
    unfolding k_isNode_def by auto

  show "k_memb rec k_dfs"
    using KBPAlg.reachable_imp_dfs[OF N' k_frontier_is_node r]
    apply clarsimp
    apply (subst k_memb_def)
    apply (subst (asm) k_memb_def)
    using k_invariantAOD[OF N' N rec' k_dfs_invariant, symmetric]
    apply (cut_tac ec=y' and ec'=rec' in k_invariantAOD[OF _ _ _ k_dfs_invariant, symmetric])
     apply simp_all

     apply (cut_tac ec=rec' and ec'=y' in k_isNode_cong)
     apply simp
     using N'
     apply simp
     apply (rule N')
     done
qed
(*>*)

end (* context AlgorithmForAgent *)

text‹

This concludes our agent-specific reasoning; we now show that the
algorithm works for all agents. The following command generalises all
our lemmas in the @{term "AlgorithmForAgent"} to the @{term
"Algorithm"} locale, giving them the mandatory prefix ‹KBP›:

›

sublocale Algorithm
        < KBP: AlgorithmForAgent
            jkbp envInit envAction envTrans envVal jview envObs
            jviewInit jviewIncr simf simRels simVal simAbs simObs
            simInit simTrans simAction aOps tOps a for a
(*<*)
  by unfold_locales
(*>*)

context Algorithm
begin

abbreviation
  "k_mkAlgAuto ≡
    mkAlgAuto aOps tOps simObs simInit simTrans simAction k_frontier"
(*<*)

lemma k_mkAlgAuto_mkAutoSim_equiv:
  assumes tC: "t ∈ jkbpC"
  shows "simAbs (runJP k_mkAlgAuto t a) = simAbs (runJP mkAutoSim t a)"
using tC
proof(induct t)
  case (tInit s) thus ?case by simp
next
  case (tStep t s)
  hence tC: "t ∈ jkbpC" by blast

  from tStep
  have N: "KBP.k_isNode a (runJP k_mkAlgAuto t a)"
    unfolding KBP.k_isNode_def
    by (simp only: mkAutoSim_ec) auto

  from tStep
  have ect: "simAbs (runJP k_mkAlgAuto t a) = sim_equiv_class a t"
    by (simp only: mkAutoSim_ec) auto

  from tStep
  have "sim_equiv_class a (t ↝ s) ∈ simAbs ` set (simTrans a (runJP k_mkAlgAuto t a))"
    using simTrans[rule_format, where a=a and t=t] tC ect by auto
  then obtain ec
    where ec: "ec ∈ set (simTrans a (runJP k_mkAlgAuto t a))"
      and sec: "simAbs ec = sim_equiv_class a (t ↝ s)"
    by auto

  from tStep
  have F: "envObs a s ∈ simObs a ` set (simTrans a (runJP k_mkAlgAuto t a))"
    using simObs[rule_format, where a=a and t="t↝s", symmetric] sec ec by auto
  from KBP.k_memb_rep[OF N]
  have E: "KBP.k_memb (runJP k_mkAlgAuto t a) (KBP.k_dfs a)" by blast

  have G: "simAbs (runJP k_mkAlgAuto (t ↝ s) a) = sim_equiv_class a (t ↝ s)"
    using KBP.k_invariantTD[OF N E F KBP.k_dfs_invariant]
    apply (clarsimp simp: jviewIncr)
    using simTrans[rule_format, where a=a and t=t and ec="runJP k_mkAlgAuto t a"] tC ect
    apply (subgoal_tac "simAbs x ∈ simAbs ` set (simTrans a (runJP k_mkAlgAuto t a))")
     apply (clarsimp simp: jviewIncr)
     apply (cut_tac a=a and ec=ec' and t="t'↝sa" in simObs[rule_format])
      apply (simp add: jviewIncr)
     apply simp
    apply blast
    done

  from tStep show ?case by (simp only: G mkAutoSim_ec)
qed

(*>*)
text‹

Running the automata produced by the DFS on a canonical trace @{term
"t"} yields some representation of the expected equivalence class:

›

lemma k_mkAlgAuto_ec:
  assumes tC: "t ∈ jkbpC"
  shows "simAbs (runJP k_mkAlgAuto t a) = sim_equiv_class a t"
(*<*)
  using k_mkAlgAuto_mkAutoSim_equiv[OF tC] mkAutoSim_ec[OF tC]
  by simp

(*>*)
text‹

This involves an induction over the canonical trace @{term "t"}.

That the DFS and @{term "mkAutoSim"} yield the same actions on
canonical traces follows immediately from this result and the
invariant:

›

lemma k_mkAlgAuto_mkAutoSim_act_eq:
  assumes tC: "t ∈ jkbpC"
  shows "set ∘ actJP k_mkAlgAuto t = set ∘ actJP mkAutoSim t"
(*<*)
proof
  fix a
  let ?ec = "sim_equiv_class a t"
  let ?rec = "runJP k_mkAlgAuto t a"

  from tC have E: "?ec ∈ sim_equiv_class a ` jkbpC"
    by auto

  from tC E have N: "KBP.k_isNode a (runJP k_mkAlgAuto t a)"
    unfolding KBP.k_isNode_def by (simp add: k_mkAlgAuto_ec[OF tC])

  from KBP.k_memb_rep[OF N]
  have E: "KBP.k_memb ?rec (KBP.k_dfs a)" by blast

  obtain acts
    where "lookup aOps (aActs (KBP.k_dfs a)) ?rec = Some acts"
      and "set acts = set (simAction a ?rec)"
    using KBP.k_invariantAD[OF N E KBP.k_dfs_invariant] by blast

  thus "(set ∘ actJP k_mkAlgAuto t) a = (set ∘ actJP mkAutoSim t) a"
    by (auto intro!: jAction_simAbs_cong[OF tC]
               simp: k_mkAlgAuto_ec[OF tC] mkAutoSim_ec[OF tC])
qed
(*>*)

text‹

Therefore these two constructions are behaviourally equivalent, and so
the DFS generates an implementation of @{term "jkbp"} in the given
environment:

›

theorem k_mkAlgAuto_implements: "implements k_mkAlgAuto"
(*<*)
proof -
  have "behaviourally_equiv mkAutoSim k_mkAlgAuto"
    by rule (simp only: k_mkAlgAuto_mkAutoSim_act_eq)
  with mkAutoSim_implements show ?thesis
    by (simp add: behaviourally_equiv_implements)
qed
(*>*)

end (* context Algorithm *)

text‹

Clearly the automata generated by this algorithm are large. We discuss
this issue in \S\ref{sec:kbps-alg-auto-min}.

\FloatBarrier

›

(*<*)
end
(*>*)