*To*: Cristiano Longo <cristiano.longo at tvblob.com>*Subject*: Re: [isabelle] please, help me !*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 26 Aug 2007 13:16:55 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <200708241246.08580.cristiano.longo@tvblob.com>*References*: <0JN9005U0J2ALB@mailproxy-in1.jaist.ac.jp> <200708241246.08580.cristiano.longo@tvblob.com>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

http://afp.sourceforge.net/entries/Functional-Automata.shtml Tobias Cristiano Longo schrieb:

Hi, I used the definition of Non Deterministic Finite State Automaton to builda "model" for Automaton with a not finite state set. Such automaton can bedefined 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 setThe run function in NonDeterministicAutomata.thy compute the final state setof a such defined machine given the initial state, transition function and alist of symbols.Note the use of option datatype to extends the symbol set with epsilon(None).ExampleNA.thy implements the automata shown inhttp://en.wikipedia.org/wiki/Nondeterministic_finite_state_machine.The transition function is defined as an inductive set. Using this techniqueis 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 isrecognized by this automata using quicksearch, and blast loops on some tryngto chek some string, for example 001010.I would be happy to receive suggestions about transition function definitions. Please my english,Cristiano LongoAlle 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, Bests, Tang.

**References**:**[isabelle] please, help me !***From:*Nguyen Van Tang

**Re: [isabelle] please, help me !***From:*Cristiano Longo

- Previous by Date: Re: [isabelle] please, help me !
- Next by Date: [isabelle] Simultaneous rule induction
- Previous by Thread: Re: [isabelle] please, help me !
- Next by Thread: [isabelle] Simultaneous rule induction
- Cl-isabelle-users August 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list