--- a/Slides/Slides8.thy Sun May 22 10:20:18 2011 +0200
+++ b/Slides/Slides8.thy Tue May 24 19:39:38 2011 +0200
@@ -1,6 +1,6 @@
(*<*)
theory Slides8
-imports "~~/src/HOL/Library/LaTeXsugar" "Main"
+imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
begin
declare [[show_question_marks = false]]
@@ -384,6 +384,53 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Lesson Learned}
+
+ \begin{textblock}{11.5}(1.2,5)
+ \begin{minipage}{10.5cm}
+ \begin{block}{}
+ Theorem provers can keep large proofs and definitions consistent and
+ make them modifiable.
+ \end{block}
+ \end{minipage}
+ \end{textblock}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{}
+
+ \begin{textblock}{11.5}(0.8,2.3)
+ \begin{minipage}{11.2cm}
+ In most papers/books:
+ \begin{block}{}
+ \color{darkgray}
+ ``\ldots this necessary hygienic discipline is somewhat swept under the carpet via
+ the so-called `{\bf variable convention}' \ldots
+ The {\color{black}{\bf belief}} that this is {\bf sound} came from the calculus
+ with nameless binders in de Bruijn''
+ \end{block}\medskip
+ \end{minipage}
+ \end{textblock}
+
+ \begin{textblock}{11.5}(0.8,10)
+ \includegraphics[scale=0.25]{LambdaBook.jpg}\hspace{-3mm}\includegraphics[scale=0.3]{barendregt.jpg}
+ \end{textblock}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
\begin{frame}<1->[t]
\frametitle{Regular Expressions}
@@ -564,13 +611,11 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1->[t]
+ \begin{frame}<1->[c]
\frametitle{Testing}
\begin{itemize}
- \item While testing is an important part in the process of programming development\pause\ldots
-
- \item we can only test a {\bf finite} amount of examples.\bigskip\pause
+ \item We can only test a {\bf finite} amount of examples:\bigskip
\begin{center}
\colorbox{cream}
@@ -1214,44 +1259,24 @@
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{\LARGE The Other Direction}
-
+ \frametitle{\LARGE 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}. This is straightforward for \\the base cases:\small
+ by induction on \smath{r}. Not trivial, but after a bit
+ of thinking, one can prove that if
\begin{center}
- \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_1)})}\hspace{5mm}
\smath{\text{finite} (U\!N\!IV /\!/ \approx_{\mathbb{L}(r_2)})}
\end{center}
@@ -1261,148 +1286,12 @@
\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 {*