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