# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306258778 -7200
# Node ID bccda961a61253372b074dcdf8e40f3d36512bc8
# Parent  c63ffe1735ebee06d6b37b882583ddee0b2d3a0b
more on slides

diff -r c63ffe1735eb -r bccda961a612 IsaMakefile
--- a/IsaMakefile	Sun May 22 10:20:18 2011 +0200
+++ b/IsaMakefile	Tue May 24 19:39:38 2011 +0200
@@ -142,7 +142,7 @@
 session8: Slides/ROOT8.ML \
          Slides/document/root* \
          Slides/Slides6.thy
-	@$(USEDIR) -D generated8 -f ROOT8.ML HOL Slides
+	@$(USEDIR) -D generated8 -f ROOT8.ML HOL-Nominal Slides
 
 slides8: session8
 	rm -f Slides/generated8/*.aux # otherwise latex will fall over                                      
diff -r c63ffe1735eb -r bccda961a612 Slides/Slides8.thy
--- 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 {*