[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
  Peter





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