diff -r d19bfc6e7631 -r 5f3387b7474f Slides/Slides7.thy
--- a/Slides/Slides7.thy	Mon May 02 13:01:02 2011 +0800
+++ b/Slides/Slides7.thy	Wed May 04 15:27:04 2011 +0800
@@ -12,7 +12,7 @@
 (*>*)
 
 text_raw {*
-  \renewcommand{\slidecaption}{Hefei, 15.~April 2011}
+  \renewcommand{\slidecaption}{Beijing, 29.~April 2011}
 
   \newcommand{\abst}[2]{#1.#2}% atom-abstraction
   \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
@@ -90,7 +90,7 @@
   \item Theorem provers can prevent mistakes, {\bf if} the problem
   is formulated so that it is suitable for theorem provers.\bigskip
   \item This re-formulation can be done, even in domains where
-  we do not expect it.
+  we least expect it.
   \end{itemize}
 
   \end{frame}}
@@ -237,7 +237,7 @@
   \end{center}
  
   \onslide<3->
-  {looks OK \ldots let's ship it to customers\hspace{5mm} 
+  {Looks OK \ldots let's ship it to customers\hspace{5mm} 
    \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
   
   \end{frame}}
@@ -329,7 +329,7 @@
   \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
   \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
-       &          & \bl{\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
+       &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
 
   \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
@@ -383,7 +383,7 @@
   \end{tabular}
   \end{center}
   \pause\pause\bigskip
-  ??? By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
+  By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
 
   \begin{tabular}{lrcl}
   Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
@@ -524,7 +524,7 @@
   My point:\bigskip\\
 
   The theory about regular languages can be reformulated 
-  to be more suitable for theorem proving.
+  to be more\\ suitable for theorem proving.
   \end{tabular}
   \end{center}
   \end{frame}}
@@ -614,7 +614,7 @@
   \begin{center}
   \begin{tabular}{l}
   finite $\Rightarrow$ regular\\
-  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r. L = \mathbb{L}(r)}\\[3mm]
+  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_L) \Rightarrow \exists r.\; L = \mathbb{L}(r)}\\[3mm]
   regular $\Rightarrow$ finite\\
   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
   \end{tabular}
@@ -631,15 +631,16 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\LARGE Final States}
+  \frametitle{\LARGE Final Equiv.~Classes}
 
   \mbox{}\\[3cm]
 
   \begin{itemize}
-  \item ??? \smath{\text{final}_L\,X \dn \{[|s|]_\approx\;|\; s \in X\}}\\
+  \item \smath{\text{finals}\,L \dn 
+     \{{\lbrack\mkern-2mu\lbrack{s}\rbrack\mkern-2mu\rbrack}_\approx\;|\; s \in L\}}\\
   \medskip
 
-  \item we can prove: \smath{L = \bigcup \{X\;|\;\text{final}_L\,X\}}
+  \item we can prove: \smath{L = \bigcup (\text{finals}\,L)}
 
   \end{itemize}
 
@@ -651,7 +652,7 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\LARGE Transitions between\\[-3mm] Equivalence Classes}
+  \frametitle{\LARGE Transitions between ECs}
 
   \smath{L = \{[c]\}}
 
@@ -725,9 +726,9 @@
   & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
   \onslide<3->{we can prove} 
   & \onslide<3->{\smath{R_1}} & \onslide<3->{\smath{=}} 
-      & \onslide<3->{\smath{R_1; \mathbb{L}(b) \,\cup\, R_2;\mathbb{L}(b) \,\cup\, \{[]\};\{[]\}}}\\
+      & \onslide<3->{\smath{R_1;; \mathbb{L}(b) \,\cup\, R_2;;\mathbb{L}(b) \,\cup\, \{[]\}}}\\
   & \onslide<3->{\smath{R_2}} & \onslide<3->{\smath{=}}    
-      & \onslide<3->{\smath{R_1; \mathbb{L}(a) \,\cup\, R_2;\mathbb{L}(a)}}\\
+      & \onslide<3->{\smath{R_1;; \mathbb{L}(a) \,\cup\, R_2;;\mathbb{L}(a)}}\\
   \end{tabular}
   \end{center}
 
@@ -928,23 +929,45 @@
 *}
 
 
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\LARGE Other Direction}
-
+  \frametitle{\LARGE The Other Direction}
+  
   One has to prove
 
   \begin{center}
   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}
   \end{center}
 
-  by induction on \smath{r}. Not trivial, but after a bit 
-  of thinking, one can prove that if
+  by induction on \smath{r}. This is straightforward for \\the base cases:\small
 
   \begin{center}
-  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{5mm}
+  \begin{tabular}{l@ {\hspace{1mm}}l}
+  \smath{U\!N\!IV /\!/ \!\approx_{\emptyset}} & \smath{= \{U\!N\!IV\}}\smallskip\\
+  \smath{U\!N\!IV /\!/ \!\approx_{\{[]\}}} & \smath{\subseteq \{\{[]\}, U\!N\!IV - \{[]\}\}}\smallskip\\
+  \smath{U\!N\!IV /\!/ \!\approx_{\{[c]\}}} & \smath{\subseteq \{\{[]\}, \{[c]\}, U\!N\!IV - \{[], [c]\}\}}
+  \end{tabular}
+  \end{center}
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE The Other Direction}
+
+  More complicated are the inductive cases:\\ one needs to prove that if
+
+  \begin{center}
+  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1)})}\hspace{3mm}
   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
   \end{center}
 
@@ -954,12 +977,149 @@
   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_1) \,\cup\, \mathbb{L}(r_2)})}
   \end{center}
   
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE Helper Lemma}
+
+  \begin{center}
+  \begin{tabular}{p{10cm}}
+  %If \smath{\text{finite} (f\;' A)} and \smath{f} is injective 
+  %(on \smath{A}),\\ then \smath{\text{finite}\,A}.
+  Given two equivalence relations \smath{R_1} and \smath{R_2} with
+  \smath{R_1} refining \smath{R_2} (\smath{R_1 \subseteq R_2}).\\ 
+  Then\medskip\\
+  \smath{\;\;\text{finite} (U\!N\!IV /\!/ R_1) \Rightarrow \text{finite} (U\!N\!IV /\!/ R_2)}
+  \end{tabular}
+  \end{center}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\Large Derivatives and Left-Quotients}
+  \small
+  Work by Brozowski ('64) and Antimirov ('96):\pause\smallskip
+
+
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \multicolumn{4}{@ {}l}{Left-Quotient:}\\
+  \multicolumn{4}{@ {}l}{\bl{$\text{Ders}\;\text{s}\,A \dn \{\text{s'} \;|\; \text{s @ s'} \in A\}$}}\bigskip\\
+
+  \multicolumn{4}{@ {}l}{Derivative:}\\
+  \bl{der c ($\varnothing$)}       & \bl{$=$} & \bl{$\varnothing$} & \\
+  \bl{der c ([])}                  & \bl{$=$} & \bl{$\varnothing$} & \\
+  \bl{der c (d)}                   & \bl{$=$} & \bl{if c = d then [] else $\varnothing$} & \\
+  \bl{der c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\
+  \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$)} & \\
+       &          & \bl{\;\;\;\;+ (if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\
+  \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ r$^*$} &\smallskip\\
+
+  \bl{ders [] r}     & \bl{$=$} & \bl{r} & \\
+  \bl{ders (s @ [c]) r} & \bl{$=$} & \bl{der c (ders s r)} & \\
+  \end{tabular}\pause
+
+  \begin{center}
+  \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \mathbb{L} (\text{ders s r})}
+  \end{center}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Left-Quotients and MN-Rels}
+
+  \begin{itemize}
+  \item \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}\medskip
+  \item \bl{$\text{Ders}\;s\,A \dn \{s' \;|\; s @ s' \in A\}$}
+  \end{itemize}\bigskip
+
+  \begin{center}
+  \smath{x \approx_A y  \Longleftrightarrow \text{Ders}\;x\;A = \text{Ders}\;y\;A}
+  \end{center}\bigskip\pause\small
+
+  which means
+
+  \begin{center}
+  \smath{x \approx_{\mathbb{L}(r)} y  \Longleftrightarrow 
+  \mathbb{L}(\text{ders}\;x\;r) = \mathbb{L}(\text{ders}\;y\;r)}
+  \end{center}\pause
+
+  \hspace{8.8mm}or
+  \smath{\;x \approx_{\mathbb{L}(r)} y  \Longleftarrow 
+  \text{ders}\;x\;r = \text{ders}\;y\;r}
+
   
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Partial Derivatives}
+
+  Antimirov: \bl{pder : rexp $\Rightarrow$ rexp set}\bigskip
+
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{pder c ($\varnothing$)}       & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
+  \bl{pder c ([])}                  & \bl{$=$} & \bl{\{$\varnothing$\}} & \\
+  \bl{pder c (d)}                   & \bl{$=$} & \bl{if c = d then \{[]\} else \{$\varnothing$\}} & \\
+  \bl{pder c (r$_1$ + r$_2$)}       & \bl{$=$} & \bl{(pder c r$_1$) $\cup$ (pder c r$_2$)} & \\
+  \bl{pder c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(pder c r$_1$) $\odot$ r$_2$} & \\
+       &          & \bl{\hspace{-10mm}$\cup$ (if nullable r$_1$ then pder c r$_2$ else $\varnothing$)}\\
+  \bl{pder c (r$^*$)}          & \bl{$=$} & \bl{(pder c r) $\odot$ r$^*$} &\smallskip\\
+  \end{tabular}
+
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{pders [] r}     & \bl{$=$} & \bl{r} & \\
+  \bl{pders (s @ [c]) r} & \bl{$=$} & \bl{pder c (pders s r)} & \\
+  \end{tabular}\pause
+
+  \begin{center}
+  \alert{$\Rightarrow$}\smath{\;\;\text{Ders}\,\text{s}\,(\mathbb{L}(\text{r})) = \bigcup (\mathbb{L}\;`\; (\text{pders s r}))}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE Final Result}
+  
+  \mbox{}\\[7mm]
+
+  \begin{itemize}
+  \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}}
+            {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 
+        refines \bl{x $\approx_{\mathbb{L}(\text{r})}$ y}\pause
+  \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
+  \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r)})}. Qed.
+  \end{itemize}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%