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

subsection‹An algorithm for automata synthesis›

text‹

 label{sec:kbps-alg}

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

  here on we assume that the environment consists of only a finite
  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) ‹

  @{term "Algorithm"} locale, shown in
 ~\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
  only required to work on the abstract domain of simulated
  traces. Note also that the space of simulated equivalence
  of type @{typ "'ss"} must be finite, but there is no
  on the representation type @{typ "'rep"}.

  develop the algorithm for a single, fixed agent, which requires us
  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‹

  represent the automaton under construction using a record:

 ›

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

context AlgorithmForAgent
begin

text‹

  instantiate the DFS theory with the following functions.

  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‹

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

 ›

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

text‹

  initial automaton has no transitions and no actions.

 ›

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

text‹

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

 ›

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

text‹

  integrate a new equivalence class into the automaton by updating
  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‹

  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‹

  invariant for the automata construction is straightforward, viz
  at each step of the process the state represents an automaton
  concords with @{term "mkAutoSim"} on the visited equivalence
 . 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‹

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

  initial frontier is the partition of the set of initial states
  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‹

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

 ›

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‹

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

  it follows immediately from ‹dfs_invariant› that the
  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‹

  we can see that the set of reachable equivalence classes
  with the partition of @{term "jkbpC"} under the simulation
  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‹

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

  result immediately yields the same result at the level of
 :

 ›

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‹

  concludes our agent-specific reasoning; we now show that the
  works for all agents. The following command generalises all
  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‹

  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‹

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

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

 ›

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‹

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

 ›

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‹

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

 FloatBarrier

 ›

(*<*)
end
(*>*)