--- a/Slides/Slides1.thy Wed Jun 02 11:37:51 2010 +0200
+++ b/Slides/Slides1.thy Thu Jun 03 11:48:44 2010 +0200
@@ -11,7 +11,7 @@
text_raw {*
- \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
+ \renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1>[t]
@@ -20,10 +20,13 @@
\\
\huge Nominal 2\\[-2mm]
\large Or, How to Reason Conveniently with\\[-5mm]
- \large General Bindings in Isabelle\\[15mm]
+ \large General Bindings in Isabelle/HOL\\[5mm]
\end{tabular}}
\begin{center}
- joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm]
+ Christian Urban
+ \end{center}
+ \begin{center}
+ joint work with {\bf Cezary Kaliszyk}\\[0mm]
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -34,197 +37,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1-2>
- \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item sorted atoms and sort-respecting permutations\medskip
-
- \onslide<2->{
- \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip
-
- \begin{center}
- \begin{tabular}{c@ {\hspace{7mm}}c}
- $[]\;\act\;c \dn c$ &
- $(a\;b)\!::\!\pi\;\act\;c \dn$
- $\begin{cases}
- b & \text{if}\; \pi \act c = a\\
- a & \text{if}\; \pi \act c = b\\
- \pi \act c & \text{otherwise}
- \end{cases}$
- \end{tabular}
- \end{center}}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>
- \frametitle{\begin{tabular}{c}Problems\end{tabular}}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
-
- \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
- \begin{center}
- $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots
- $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$
- \end{center}\bigskip
-
- \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip
-
- \item type-classes
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}}
- \mbox{}\\[-3mm]
-*}
-datatype atom = Atom string nat
-
-text_raw {*
- \mbox{}\bigskip
- \begin{itemize}
- \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
-
- \begin{itemize}
- \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$)
- \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$)
- \end{itemize}\medskip
-
- \item<3-> swappings:
- \small
- \[
- \begin{array}{l@ {\hspace{1mm}}l}
- (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
- & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
- \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
- & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}}
- \end{array}
- \]
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-6>
- \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip
-
- \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip
-
- \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip
-
- \begin{itemize}
- \item $0\;\act\;x = x$\\
- \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
- \end{itemize}
-
- \small
- \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}
- \end{itemize}
-
- \only<4>{
- \begin{textblock}{6}(2.5,11)
- \begin{tikzpicture}
- \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
- {\normalsize\color{darkgray}
- \begin{minipage}{8cm}\raggedright
- This is slightly odd, since in general:
- \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center}
- \end{minipage}};
- \end{tikzpicture}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-3>
- \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item \underline{concrete} atoms:
- \end{itemize}
-*}
-(*<*)
-consts sort :: "atom \<Rightarrow> string"
-(*>*)
-
-typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*)
-typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)
-
-text_raw {*
- \mbox{}\bigskip\bigskip
- \begin{itemize}
- \item<2-> there is an overloaded function \underline{atom}, which injects concrete
- atoms into generic ones\medskip
- \begin{center}
- \begin{tabular}{l}
- $\text{atom}(a) \fresh x$\\
- $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
- \end{tabular}
- \end{center}\bigskip\medskip
-
- \onslide<3->
- {I would like to have $a \fresh x$, $(a\; b)$, \ldots}
-
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-2>[c]
- \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item the formalised version of the nominal theory is now much nicer to
- work with (sorts are occasionally explicit)\bigskip
-
- \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip
-
- \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity}
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-2>
- \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}}
+ \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}}
\mbox{}\\[-6mm]
\begin{itemize}
@@ -240,7 +53,8 @@
$\forall\{a_1,\ldots,a_n\}.\; T$
\end{center}\medskip
- with single binders is a \alert{major} pain; take my word for it!
+ with single binders and reasoning about it is a \alert{\bf major} pain;
+ take my word for it!
\end{itemize}
\only<1>{
@@ -250,6 +64,7 @@
\begin{tabular}{l@ {\hspace{2mm}}l}
\pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
\pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
+ \pgfuseshading{smallspherered} & Barendregt style reasoning about bound variables\\
\end{tabular}
\end{textblock}}
@@ -362,10 +177,10 @@
\begin{itemize}
\item the order does not matter and alpha-equivelence is preserved under
- vacuous binders (restriction)\medskip
+ vacuous binders \textcolor{gray}{(restriction)}\medskip
\item the order does not matter, but the cardinality of the binders
- must be the same (abstraction)\medskip
+ must be the same \textcolor{gray}{(abstraction)}\medskip
\item the order does matter
\end{itemize}
@@ -401,8 +216,8 @@
\multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
\multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
- \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $\varnothing$}}\\
- \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\
+ \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\
+ \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\
\end{tabular}
@@ -414,33 +229,65 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{\begin{tabular}{c}Ott\end{tabular}}
+ \begin{frame}<1-5>
+ \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}}
\mbox{}\\[-3mm]
\begin{itemize}
- \item this way of specifying binding is pretty much stolen from
- Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip
+ \item this way of specifying binding is inspired by
+ Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip
+
+ \only<2>{
\begin{itemize}
- \item<2-> Ott allows specifications like\smallskip
+ \item Ott allows specifications like\smallskip
\begin{center}
$t ::= t\;t\; |\;\lambda x.t$
- \end{center}\medskip
+ \end{center}
+ \end{itemize}}
- \item<3-> whether something is bound can depend on other bound things\smallskip
+ \only<3-4>{
+ \begin{itemize}
+ \item whether something is bound can depend in Ott on other bound things\smallskip
\begin{center}
- Foo $(\lambda x. t)\; s$
- \end{center}\medskip
- \onslide<4->{this might make sense for ``raw'' terms, but not at all
+ \begin{tikzpicture}
+ \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$};
+ \node (B) at ( 1.1,1) {$s$};
+ \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};}
+ \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);}
+ \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);}
+ \end{tikzpicture}
+ \end{center}
+ \onslide<4>{this might make sense for ``raw'' terms, but not at all
for $\alpha$-equated terms}
- \end{itemize}
+ \end{itemize}}
+
+ \only<5>{
+ \begin{itemize}
+ \item we allow multiple binders and bodies\smallskip
+ \begin{center}
+ \isacommand{bind} a b c \isacommand{in} x y z
+ \end{center}\bigskip\medskip
+ the reason is that in general
+ \begin{center}
+ \begin{tabular}{rcl}
+ \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
+ \begin{tabular}{@ {}l}
+ \isacommand{bind\_res} as \isacommand{in} x,\\
+ \isacommand{bind\_res} as \isacommand{in} y
+ \end{tabular}
+ \end{tabular}
+ \end{center}\smallskip
+
+ same with \isacommand{bind\_set}
+ \end{itemize}}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -449,13 +296,13 @@
\mbox{}\\[-3mm]
\begin{itemize}
- \item in old Nominal we represented single binders as partial functions:\bigskip
+ \item in old Nominal, we represented single binders as partial functions:\bigskip
\begin{center}
\begin{tabular}{l}
- Lam [$a$].$t$ $\;\dn$\\[2mm]
+ Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm]
\;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\
- \phantom{\;\;\;\;$\lambda b.$\;\;\;}$\text{if}\;b \fresh t\;
+ \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\;
\text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$
\end{tabular}
\end{center}
@@ -471,6 +318,66 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
+ \begin{frame}<1->
+ \frametitle{\begin{tabular}{c}New Design\end{tabular}}
+ \mbox{}\\[4mm]
+
+ \begin{center}
+ \begin{tikzpicture}
+ \alt<2>
+ {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};}
+ {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
+
+ \alt<3>
+ {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};}
+ {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
+
+ \alt<4>
+ {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
+ {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
+
+ \alt<5>
+ {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};}
+ {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
+
+ \alt<6>
+ {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};}
+ {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
+
+ \alt<7>
+ {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
+ (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};}
+ {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
+
+ \draw[->,white!50,line width=1mm] (A) -- (B);
+ \draw[->,white!50,line width=1mm] (B) -- (C);
+ \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+ (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
+ \draw[->,white!50,line width=1mm] (D) -- (E);
+ \draw[->,white!50,line width=1mm] (E) -- (F);
+ \end{tikzpicture}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
\begin{frame}<1-9>
\frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
\mbox{}\\[-3mm]
@@ -815,8 +722,6 @@
\multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
\end{tabular}
-
-
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -896,7 +801,7 @@
\]
\footnotesize
- where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\times\text{fv}$
+ where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -988,6 +893,83 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
+ \begin{frame}<1>[t]
+ \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}}
+ \mbox{}\\[-7mm]\mbox{}
+
+ \footnotesize
+ \begin{center}
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
+
+ \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
+
+ \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
+
+ \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
+
+ \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
+
+ \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
+
+ \draw[->,white!50,line width=1mm] (A) -- (B);
+ \draw[->,white!50,line width=1mm] (B) -- (C);
+ \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+ (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
+ \draw[->,white!50,line width=1mm] (D) -- (E);
+ \draw[->,white!50,line width=1mm] (E) -- (F);
+ \end{tikzpicture}
+ \end{center}
+
+ \begin{itemize}
+ \item Core Haskell: 11 types, 49 term-constructors,
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->
+ \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \small
+ \mbox{}\hspace{10mm}
+ \begin{tabular}{ll}
+ \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
+ \hspace{5mm}\phantom{$|$} Var name\\
+ \hspace{5mm}$|$ App trm trm\\
+ \hspace{5mm}$|$ Lam x::name t::trm
+ & \isacommand{bind} x \isacommand{in} t\\
+ \hspace{5mm}$|$ Let as::assn t::trm
+ & \isacommand{bind} bn(as) \isacommand{in} t\\
+ \multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+ \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+ \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
+ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
+ \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
+ \end{tabular}\bigskip\medskip
+
+ we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
\begin{frame}<1->
\frametitle{\begin{tabular}{c}Conclusion\end{tabular}}
\mbox{}\\[-6mm]
@@ -995,14 +977,14 @@
\begin{itemize}
\item the user does not see anything of the raw level\medskip
\only<1>{\begin{center}
- Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)
+ Lam a (Var a) \alert{$=$} Lam b (Var b)
\end{center}\bigskip}
\item<2-> we have not yet done function definitions (will come soon and
we hope to make improvements over the old way there too)\medskip
- \item<3-> it took quite some time to get here, but it seems worthwhile (POPL 2011 tutorial)\medskip
- \item<4-> Thanks goes to Cezary!\\
- \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!}
+ \item<3-> it took quite some time to get here, but it seems worthwhile
+ (Barendregt's variable convention is unsound in general,
+ found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip
\end{itemize}