Re: [isabelle] please, help me !
Now that we have got on to the subject of (finite) automata, the
following theories from the Archive of Formal Proofs may be of interest:
Cristiano Longo schrieb:
Hi, I used the definition of Non Deterministic Finite State Automaton to build
a "model" for Automaton with a not finite state set. Such automaton can be
(1) a data type for states
(2) a data type for symbols + a special simbol Epsilon
(3) a transition function (state, symbol Un Epsilon) => state set
The run function in NonDeterministicAutomata.thy compute the final state set
of a such defined machine given the initial state, transition function and a
list of symbols.
Note the use of option datatype to extends the symbol set with epsilon(None).
ExampleNA.thy implements the automata shown in
The transition function is defined as an inductive set. Using this technique
is simpler and clearer that using primrec. But probably is not correct,
because it is not an inductive set.
I have done some experiment. I am not able to understand if a string is
recognized by this automata using quicksearch, and blast loops on some tryng
to chek some string, for example 001010.
I would be happy to receive suggestions about transition function definitions.
Please my english,
Alle 07:25, venerdì 24 agosto 2007, Nguyen Van Tang ha scritto:
I am studying Isabelle/HOL. I would like to have one question. Can we use
Isabelle to formalize "finite paths" of a transition system (or formalize
finite run of a finite automaton) ?
Please help me if you have a solution on this problem?
Thank you in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and