[isabelle] Automata library

Hi all,

I'm looking for an Isabelle-formalization of nondeterministic finite
automata, that also generates executable code.

In particular, I need the following operations:
  Membership query (directly on nondet. automata, without converting to
det. automata first)
  Union, Intersection,
  Substitution, in its general case, i.e. by a function :: \Sigma ->
\Gamma fsm

Especially the substitution operation seems tricky with the
Functional-Automata  formalization in afp, because it stores no explicit
information about the alphabet.

Are there other formalizations of FSMs out there, from which I could start ?
Or can I extend the Functional-Automata in that direction ?

Regards, and thanks in advance for any suggestions

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.