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 defined by (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,
Cristiano Longo
Alle 07:25, venerdì 24 agosto 2007, Nguyen Van Tang ha scritto:
Hi all,

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 MHonArc.