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.

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,
>
>
>
> 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(simp add:ACCEPT_DEF RUN_DEF)
apply blast
done

lemma "accept [ONE, ONE, ONE, ZERO, ONE, ZERO, ONE]"
apply(simp add:ACCEPT_DEF RUN_DEF)
apply blast
done

lemma "accept [ONE, ZERO, ONE, ZERO]"
apply(simp add:ACCEPT_DEF RUN_DEF)
apply blast
done


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


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