Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
theory Myhill imports Myhill_2beginsection {* Direction @{text "regular language \<Rightarrow>finite partition"} *}text {*The intuition behind our treatment is still automata. Taking the automaton in Fig.\ref{fig_origin_auto} as an example, like any automaton, itrepresents the vehicle used to recognize a certain regular language.For any given string, the process starts from the left most and proceed character by character to the right, driving the state transtion of automaton starting from the initial state (the one marked by an short arrow). There couldbe three outcomes: \begin{enumerate} \item The process finally reaches the end of the string and the automaton is at an accepting state, in which case the string is considered a member of the language. For the automaton in Fig.\ref{fig_origin_auto}, @{text "a, ab, abb, abc, abbcc, b, baa"} are such kind of strings. \item The process finally reaches the end of the string but the automaton is at an non-accepting state, in which case, the string is considered a non-member of the language. For the automaton in Fig.\ref{fig_origin_auto}, @{text "ad, abbd, adbd, bdabbccd"} are such kind of strings. \label{case_end_reject} \item \label{case_stuck} The process get stuck at the middle of the string, in which case, the string is considered a non-member of the lauguage. For the automaton in Fig.\ref{fig_origin_auto}, @{text "c, acb, bbacd, aaccd"} are such kind of strings. \end{enumerate}To avoid the situation \ref{case_stuck} above, we can augment a normal automaton with a ``absorbing state'',as the state $X_3$ in Fig.\ref{fig_extended_auto}. In an auguments automaton, the process of strings neverget stuck: whenever a string is recognized as not belonging to the language, the augmented automatonis transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, in which case, the string is rejected by situation \ref{case_end_reject} above.Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}corresponds to the state reached by processing @{text "x"} with the augmented automaton. \begin{figure}[h!]\centering\subfigure[Original automaton]{\label{fig_origin_auto}\begin{minipage}{0.4\textwidth}\scalebox{0.8}{\begin{tikzpicture}[ultra thick,>=latex] \node[draw,circle,initial] (start) {$X_0$}; \node[draw,circle,accepting] at ($(start) + (3.5cm,2cm)$) (ac1) {$X_1$}; \node[draw,circle,accepting] at ($(start) + (3.5cm,-2cm)$) (ac2) {$X_2$}; \path[->] (start) edge [bend left] node [midway, above] {$a$} (ac1); \path[->] (start) edge [bend right] node [midway, below] {$b$} (ac2); \path[->] (ac1) edge [loop above] node [midway, above] {$b$} (ac1); \path[->] (ac2) edge [loop below] node [midway, below] {$a$} (ac2); \path[->] (ac1) edge [bend right] node [midway, left] {$c$} (ac2); \path[->] (ac2) edge [bend right] node [midway, right] {$c$} (ac1); \path[->] (ac1) edge node [midway, sloped, above] {$d$} (start); \path[->] (ac2) edge node [midway, sloped, above] {$d$} (start);\end{tikzpicture}}\end{minipage}}\subfigure[Extended automaton]{\label{fig_extended_auto}\begin{minipage}{0.5\textwidth}\scalebox{0.8}{\begin{tikzpicture}[ultra thick,>=latex] \node[draw,circle,initial] (start) {$X_0$}; \node[draw,circle,accepting] at ($(start) + (3.5cm,2cm)$) (ac1) {$X_1$}; \node[draw,circle,accepting] at ($(start) + (3.5cm,-2cm)$) (ac2) {$X_2$}; \node[draw,circle] at ($(start) + (6.5cm,0cm)$) (ab) {$X_3$}; \path[->] (start) edge [bend left] node [midway, above] {$a$} (ac1); \path[->] (start) edge [bend right] node [midway, below] {$b$} (ac2); \path[->] (ac1) edge [loop above] node [midway, above] {$b$} (ac1); \path[->] (ac2) edge [loop below] node [midway, below] {$a$} (ac2); \path[->] (ac1) edge [bend right] node [midway, left] {$c$} (ac2); \path[->] (ac2) edge [bend right] node [midway, right] {$c$} (ac1); \path[->] (ac1) edge node [midway, sloped, above] {$d$} (start); \path[->] (ac2) edge node [midway, sloped, above] {$d$} (start); \path [draw, rounded corners,->,dashed] (start) -- ($(start) + (0cm, 3.7cm)$) -- ($(ab) + (0cm, 3.7cm)$) node[midway,above,sloped]{$\Sigma - \{a, b\}$} -- (ab); \path[->,dashed] (ac1) edge node [midway, above, sloped] {$\Sigma - \{b,c,d\}$} (ab); \path[->,dashed] (ac2) edge node [midway, below, sloped] {$\Sigma - \{a,c,d\}$} (ab); \path[->,dashed] (ab) edge [loop right] node [midway, right] {$\Sigma$} (ab);\end{tikzpicture}}\end{minipage}}\caption{The relationship between automata and finite partition}\label{fig_auto_part_rel}\end{figure} *}end