header {* Finite State Machines *}

(*<*)theory FSM_ex imports Main
begin
(*>*)

text{*
A nondeterministic \emph{finite state machine}, as formalised below, has
a set of initial states (where the machine may start execution),
a set of final states (indicating acceptance of a string)
and finally a next state relation.

Type @{typ"'a"} denotes the set of states, while type @{typ"'b"} represents the alphabet.
The next state relation represents labelled transitions, $s\xrightarrow{\;c\;} s'$.
It holds whenever it is possible
to go from state $s$ to state $s'$ reading the character~$c$.
*}
record ('a,'b) fsm = init  :: "'a set"
                     final :: "'a set"
                     nxt :: "'a  => 'b => 'a => bool"
text{*The definition above uses Isabelle records, which have not been covered in the course.
As used here, they are very simple.
A field of a record @{term r} is designated using the field name as a function,
as in \hbox{@{term "init r"}}.
Records are further described in the Tutorial (section 8.2),
but it is permissible to replace the record by a 3-tuple in this exercise.
*}

(*<*)consts  reaches :: "[('a,'b) fsm, 'a, 'b list, 'a] => bool"(*>*)

text {*\begin{task}
Define an Isabelle function @{term"reaches"} of type @{typ"[('a,'b) fsm, 'a, 'b list, 'a] => bool"}
generalising the next state relation to the that of \emph{reachability},
$s\xrightarrow{\;l\;}^* s'$, where $l$ is a list of characters.
Therefore  @{term"reaches"} should satisfy
\begin{itemize}
  \item $s\xrightarrow{\;[]\;}^* s$ (with the empty list, a state $s$ is reachable from itself), and
  \item $s\xrightarrow{\;(c\#l)\;}^* s'$ if $s\xrightarrow{\;c\;} s''$ and $s''\xrightarrow{\;l\;}^* s'$
        for som intermediate state $s''$.
\end{itemize}
(Note that a string of characters has type @{typ"'b"}.)\marks{5}
\end{task}
*}

text {*\begin{task}
Prove the following theorem.\marks{5}
\end{task}
*}
lemma reaches_append_iff:
     "reaches fsm s (xs@ys) s' \<longleftrightarrow>
        (\<exists>s''. reaches fsm s xs s'' \<and> reaches fsm s'' ys s')"
(*<*) oops (*>*)

text{*A finite state machine \emph{accepts} a given string provided
some final state is reachable from some initial state via that string.
*}
definition accepts :: "('a,'b) fsm => 'b list => bool"  where
  "accepts fsm xs ==
    \<exists>s s'. reaches fsm s xs s' \<and> s \<in> init fsm \<and> s' \<in> final fsm"

text{*For example, we can define a trivial finite state machine that does not accept any strings.
The proof of the theorem is trivial. This example also illustrates the syntax for writing record expressions.
Note the special brackets used to enclose the record fields.
*}
definition Null where
  "Null = \<lparr>init = {}, final = {}, nxt = \<lambda>st x st'. False\<rparr>"

lemma accepts_empty:  "~ accepts Null l"
(*<*) oops (*>*)


text{*\begin{task}
Prove the following theorem, for a suitable definition of the function @{term SingStr}.
This should create a machine that accepts only a string consisting of the given single character.\marks{10}
\end{task}*}
(*<*)consts SingStr :: "'b => ('a,'b) fsm"(*>*)

lemma accepts_singstr: "accepts (SingStr a) l \<longleftrightarrow> l = [a]"
(*<*) oops (*>*)

text{*\begin{task}
Prove the following theorem, for a suitable definition of the function @{term Reverse}.
This should create a machine that reverses the direction of all transitions
in a given machine. (You may find it helpful to prove a lemma relating the functions
@{term reaches} and @{term Reverse}.)
\marks{12}
\end{task}*}
(*<*)consts Reverse :: "('a,'b) fsm => ('a,'b) fsm"(*>*)

lemma accepts_rev: "accepts fsm l \<Longrightarrow> accepts (Reverse fsm) (rev l)"
(*<*) oops (*>*)

text{*\begin{task}
Prove the following theorem, for a suitable definition of the function @{term Times}.
This should create a machine that runs to other given machines in parallel. Each state of this machine should be an ordered pair.
The point of this construction is to define the intersection of two languages.
(You will probably need Isabelle's operator for forming the Cartesian product of two sets, written @{term"A\<times>B"}.
.)
\marks{18}
\end{task}*}

(*<*)consts Times :: "('a1,'b) fsm => ('a2,'b) fsm => ('a1*'a2,'b) fsm"(*>*)

lemma accepts_Times_iff:
    "accepts (Times fsm1 fsm2) xs \<longleftrightarrow>
     accepts fsm1 xs \<and> accepts fsm2 xs"
(*<*) oops (*>*)

text{*\emph{Remark}: This material represents part of a development of the theory of regular languages.
In fact it needs much work before it can be useful in that guise. A regular language is normally defined to be
any language accepted by some finite state machine. Unfortunately, with our definitions,
the set of states of a machine affects its type. So the relevant definition cannot be expressed.
To develop this material further requires a different treatment of machine states.*}
(*<*)end(*>*)