# Re: [isabelle] please, help me !

```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
http://en.wikipedia.org/wiki/Nondeterministic_finite_state_machine.

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.

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) ?
>
>
>
>
>
>
>
>
>
> Bests,
>
> Tang.
```
```theory NonDeterministicAutomata imports Main begin

types ('state,'symbol)transitionFunction = "'state \<Rightarrow> 'symbol option \<Rightarrow> 'state set"

consts
runND :: "('state,'symbol)transitionFunction \<Rightarrow> 'state set  \<Rightarrow> 'symbol list \<Rightarrow> 'state set"

primrec
"runND t S [] = S"
"runND t S (x#xl) = (\<Union>s\<in>runND t S xl. (t s (Some x) \<union> t s None))"

lemma [simp]:"runND P S (xs at ys) = runND P (runND P S ys) xs"
apply(induct_tac xs, auto)
done

constdefs
run :: "('state, 'symbol)transitionFunction \<Rightarrow> 'state => 'symbol list \<Rightarrow> 'state set"
RUN_DEF:"run t s l == runND t {s} (rev l)"

end
```
```theory ExampleNa imports NonDeterministicAutomata begin

(* see http://en.wikipedia.org/wiki/Nondeterministic_finite_state_machine *)
datatype state = S0 | S1 | S2 | S3 | S4
datatype symbol = ZERO | ONE

(* transitions definition *)
consts T :: "(state, symbol)transitionFunction"

inductive "T s x"
intros
[intro]:"\<lbrakk>s=S0; x=None\<rbrakk> \<Longrightarrow> S1 \<in> T s x"
[intro]:"\<lbrakk>s=S0; x=None\<rbrakk> \<Longrightarrow> S3 \<in> T s x"
[intro]:"\<lbrakk>s=S1;x=Some ZERO\<rbrakk> \<Longrightarrow> S2 \<in> T s x"
[intro]:"\<lbrakk>s=S1;x=Some ONE\<rbrakk> \<Longrightarrow> S1 \<in> T s x"
[intro]:"\<lbrakk>s=S2;x=Some ZERO\<rbrakk> \<Longrightarrow> S1 \<in> T s x"
[intro]:"\<lbrakk>s=S2;x=Some ONE\<rbrakk> \<Longrightarrow> S2 \<in> T s x"
[intro]:"\<lbrakk>s=S3;x=Some ZERO\<rbrakk> \<Longrightarrow> S3 \<in> T s x"
[intro]:"\<lbrakk>s=S3;x=Some ONE\<rbrakk> \<Longrightarrow> S4 \<in> T s x"
[intro]:"\<lbrakk>s=S4;x=Some ZERO\<rbrakk> \<Longrightarrow> S4 \<in> T s x"
[intro]:"\<lbrakk>s=S4;x=Some ONE\<rbrakk> \<Longrightarrow> S3 \<in> T s x"

constdefs
accept :: "symbol list \<Rightarrow> bool"
ACCEPT_DEF:"accept cl == S1 \<in> run T S1 cl \<or> S3 \<in> run T S1 cl"

lemma "accept [ONE]"
apply blast
done

lemma "accept [ONE, ONE, ONE, ZERO, ONE, ZERO, ONE]"
apply blast
done

lemma "accept [ONE, ZERO, ONE, ZERO]"