--- a/Myhill.thy	Mon Feb 07 11:12:36 2011 +0000
+++ b/Myhill.thy	Mon Feb 07 13:08:09 2011 +0000
@@ -2,7 +2,9 @@
   imports Myhill_2
 begin
 
-section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
+section {* Preliminaries *}
+
+subsection {* Finite automata and \mht  \label{sec_fa_mh} *}
 
 text {*
 
@@ -51,19 +53,20 @@
 It can be proved that the the partition induced by $\approx_M$ also has $|Q_M|$ equivalent classes.
 It is also easy to show that: if $x \approx_M y$, then $x \approx_{L(M)} y$, and this means
 $\approx_M$ is a more refined equivalent relation than $\approx_{L(M)}$. Since partition induced by
-$\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite. Now, we get one direction
-of \mht:
-\begin{Lem}[\mht , Direction one]
+$\approx_M$ is finite, the one induced by $\approx_{L(M)}$ must also be finite, and this is 
+one of the two directions of \mht:
+\begin{Lem}[\mht , Direction two]
   If a language $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$), then 
   the partition induced by $\approx_\Lang$ is finite.
 \end{Lem}
 
 The other direction is:
-\begin{Lem}[\mht , Direction two]\label{auto_mh_d2}
+\begin{Lem}[\mht , Direction one]\label{auto_mh_d1}
   If  the partition induced by $\approx_\Lang$ is finite, then
   $\Lang$ is regular (i.e. $\Lang = L(M)$ for some DFA $M$).
 \end{Lem}
-To prove this lemma, a DFA $M_\Lang$ is constructed out of $\approx_\Lang$ with:
+The $M$ we are seeking when prove lemma \ref{auto_mh_d2} can be constructed out of $\approx_\Lang$,
+denoted $M_\Lang$ and defined as the following:
 \begin{subequations}
 \begin{eqnarray}
   Q_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}\\
@@ -73,14 +76,62 @@
   F_{M_\Lang} ~ & \equiv & ~ \{ \cls{x}{\approx_\Lang}~|~ x \in \Lang \}
 \end{eqnarray}
 \end{subequations}
-From the assumption of lemma \ref{auto_mh_d2}, we have that $\{ \cls{x}{\approx_\Lang}~|~ x \in \Sigma^* \}$
-is finite
-It can be proved that $\Lang = L(M_\Lang)$.
+It can be proved that $Q_{M_\Lang}$ is indeed finite and $\Lang = L(M_\Lang)$, so lemma \ref{auto_mh_d1} holds.
+It can also be proved that $M_\Lang$ is the minimal DFA (therefore unique) which recoginzes $\Lang$.
+
+
 
 *}
 
+subsection {* The objective and the underlying intuition *}
+
 text {*
+  It is now obvious from section \ref{sec_fa_mh} that \mht\ can be established easily when
+  {\em reglar languages} are defined as ones recognized by finite automata. 
+  Under the context where the use of finite automata is forbiden, the situation is quite different.
+  The theorem now has to be expressed as:
+  \begin{Thm}[\mht , Regular expression version]
+      A language $\Lang$ is regular (i.e. $\Lang = L(\re)$ for some {\em regular expression} $\re$)
+      iff. the partition induced by $\approx_\Lang$ is finite.
+  \end{Thm}
+  The proof of this version consists of two directions (if the use of automata are not allowed):
+  \begin{description}
+    \item [Direction one:] 
+      generating a regular expression $\re$ out of the finite partition induced by $\approx_\Lang$,
+      such that $\Lang = L(\re)$.
+    \item [Direction two:]
+          showing the finiteness of the partition induced by $\approx_\Lang$, under the assmption
+          that $\Lang$ is recognized by some regular expression $\re$ (i.e. $\Lang = L(\re)$).
+  \end{description}
+  The development of these two directions consititutes the body of this paper.
 
+*}
+
+section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
+
+text {*
+  Although not used explicitly, the notion of finite autotmata and its relationship with 
+  language partition, as outlined in section \ref{sec_fa_mh}, still servers as important intuitive 
+  guides in the development of this paper.
+  For example, {\em Direction one} follows the {\em Brzozowski algebraic method}
+  used to convert finite autotmata to regular expressions, under the intuition that every 
+  partition member $\cls{x}{\approx_\Lang}$ is a state in the DFA $M_\Lang$  constructed to prove 
+  lemma \ref{auto_mh_d1} of section \ref{sec_fa_mh}.
+
+  The basic idea of Brzozowski method is to set aside an unknown for every DFA state and 
+  describe the state-trasition relationship by charateristic equations. 
+  By solving the equational system such obtained, regular expressions 
+  characterizing DFA states are obtained. There are choices of 
+  how DFA states can be characterized.  The first is to characterize a DFA state by the set of 
+  striings leading from the state in question into accepting states. 
+  The other choice is to characterize a DFA state by the set of strings leading from initial state 
+  into the state in question. For the first choice, the lauguage recognized by a DFA can 
+  be characterized by the regular expression characterizing initial state, while 
+  in the second choice, the languaged of the DFA can be characterized by the summation of
+  regular expressions of all accepting states.
+*}
+
+text {*
 \begin{figure}[h!]
 \centering
 \begin{minipage}{0.5\textwidth}
@@ -112,4 +163,5 @@
 
   *}
 
+
 end

--- a/tphols-2011/document/root.tex	Mon Feb 07 11:12:36 2011 +0000
+++ b/tphols-2011/document/root.tex	Mon Feb 07 13:08:09 2011 +0000
@@ -47,10 +47,12 @@
 %\renewcommand{\isastyle}{\isastyleminor}
 
 {\theoremstyle{break} \newtheorem{Lem}{Lemma}}
+{\theoremstyle{break} \newtheorem{Thm}{Theorem}}
 
 \newcommand{\dfa}[1]{\hat{\delta}_{#1}}
 \newcommand{\Lang}{\mathcal{L}}
-\newcommand{\mht}{Myhill-Nerode Theorem}
+\newcommand{\re}{e}
+\newcommand{\mht}{Myhill-Nerode theorem}
 \newcommand{\qnt}[2]{{#1}//{#2}}
 \newcommand{\cls}[2]{\llbracket{#1}\rrbracket_{#2}}