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@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