--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/SlidesB.thy Sun Oct 13 23:09:21 2013 +0200
@@ -0,0 +1,735 @@
+(*<*)
+theory SlidesB
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+
+text_raw {*
+ %% was \begin{colormixin}{20!averagebackgroundcolor}
+ %%
+ %% is \begin{colormixin}{50!averagebackgroundcolor}
+ \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \Huge Nominal Isabelle\\[0mm]
+ \Large or, How Not to be Intimidated by\\[-3mm]
+ \Large the Variable Convention\\[-5mm]
+ \end{tabular}}
+
+ \begin{center}
+ Christian Urban\\[1mm]
+ King's College London\\[-6mm]\mbox{}
+ \end{center}
+
+ \begin{center}
+ \begin{block}{}
+ \color{gray}
+ \small
+ {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm]
+ If $M_1,\ldots,M_n$ occur in a certain mathematical context
+ (e.g. definition, proof), then in these terms all bound variables
+ are chosen to be different from the free variables.\\[2mm]
+
+ \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+ \end{block}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{}
+
+ \begin{itemize}
+ \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
+ \end{itemize}
+
+ \begin{center}
+ \begin{block}{}
+ \color{gray}
+ \footnotesize
+ {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm]
+ If $M_1,\ldots,M_n$ occur in a certain mathematical context
+ (e.g. definition, proof), then in these terms all bound variables
+ are chosen to be different from the free variables.\hfill ---Henk Barendregt
+ \end{block}
+ \end{center}\pause
+
+ \mbox{}\\[-19mm]\mbox{}
+
+ \begin{itemize}
+ \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning
+ about LF (and fixed it in three ways)
+ \item found also fixable errors in my Ph.D.-thesis about cut-elimination
+ (examined by Henk Barendregt and Andy Pitts)
+ \item found the variable convention can in principle be used for proving false
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Nominal Techniques}
+
+ \begin{itemize}
+ \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:
+ \begin{center}
+ \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2}
+ \end{center}
+
+ \item also permutations and substitutions commute, if you suspend permutations
+ in front of variables
+ \begin{center}
+ \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}
+ \end{center}\medskip\medskip
+
+ \item this allowed us to define as simple Nominal Unification algorithm\medskip
+ \begin{center}
+ \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}
+ \smath{\nabla \vdash a \fresh^? t}
+ \end{center}
+ \end{itemize}
+
+ %\begin{textblock}{3}(13.1,1.3)
+ %\includegraphics[scale=0.26]{andrewpitts.jpg}
+ %\end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Nominal Isabelle}
+
+ \begin{itemize}
+ \item a general theory about atoms and permutations\medskip
+ \begin{itemize}
+ \item sorted atoms and
+ \item sort-respecting permutations
+ \end{itemize}
+
+ \item support and freshness
+ \begin{center}
+ \begin{tabular}{l}
+ \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\
+ \smath{a \fresh x \dn a \notin \textit{supp}(x)}
+ \end{tabular}
+ \end{center}\bigskip\pause
+
+ \item allow users to reason about alpha-equivalence classes like about
+ syntax trees
+ %
+ %\item $\alpha$-equivalence
+ %\begin{center}
+ %\begin{tabular}{l}
+ %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]
+ %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\
+ %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\
+ %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}
+ %\end{tabular}
+ %\end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-7>
+ \frametitle{New Types in HOL}
+
+ \begin{center}
+ \begin{tikzpicture}[scale=1.5]
+ %%%\draw[step=2mm] (-4,-1) grid (4,1);
+
+ \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+ \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+ \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+
+ \onslide<3-4,6->{\draw (-2.0, 0.845) -- (0.7,0.845);}
+ \onslide<3-4,6->{\draw (-2.0,-0.045) -- (0.7,-0.045);}
+
+ \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+ \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+ \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]
+ {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}
+ \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+ \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+
+ \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+ \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+
+ \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+ \end{tikzpicture}
+ \end{center}
+
+ \begin{center}
+ \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}
+ \end{center}
+
+ \begin{textblock}{9}(2.8,12.5)
+ \only<7>{
+ \begin{tikzpicture}
+ \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn)
+ {The ``new types'' are the reason why there is no Nominal Coq.};
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-3>[c]
+ \frametitle{HOL vs.~Nominal}
+
+ \begin{itemize}
+ \item Nominal logic by Pitts are incompatible
+ with choice principles\medskip
+
+ \item HOL includes Hilbert's epsilon\pause\bigskip
+
+ \item The solution: Do not require that everything has finite support\medskip
+
+ \begin{center}
+ \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-5>
+ \frametitle{\begin{tabular}{c}Our Work\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \begin{center}
+ \begin{tikzpicture}[scale=1.5]
+ %%%\draw[step=2mm] (-4,-1) grid (4,1);
+
+ \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+ \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+ \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+
+ \onslide<1>{\draw (-2.0, 0.845) -- (0.7,0.845);}
+ \onslide<1>{\draw (-2.0,-0.045) -- (0.7,-0.045);}
+
+ \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+ \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+ \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]
+ {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}
+ \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+ \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+
+ \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+ \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+
+ \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+ \end{tikzpicture}
+ \end{center}
+
+ \begin{textblock}{9.5}(6,3.5)
+ \begin{itemize}
+ \item<1-> defined fv and $\alpha$
+ \item<2-> built quotient / new type
+ \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots)
+ \item<4-> derive a {\bf stronger} cases lemma
+ \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
+ \begin{center}
+ \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)}
+ \end{center}
+ \end{itemize}
+ \end{textblock}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{Nominal Isabelle}
+
+ \begin{itemize}
+ \item Users can define lambda-terms as:
+ \end{itemize}
+*}
+
+ atom_decl name text_raw {*\medskip\isanewline *}
+ nominal_datatype lam =
+ Var "name"
+ | App "lam" "lam"
+ | Lam x::"name" t::"lam" binds x in t ("Lam _. _")
+
+
+text_raw {*
+ \mbox{}\bigskip
+
+ \begin{itemize}
+ \item These are \underline{\bf named} alpha-equivalence classes, for example
+ \end{itemize}
+
+ \begin{center}
+ \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{\Large (Weak) Induction Principles}
+
+ \begin{itemize}
+ \item The usual induction principle for lambda-terms is as follows:
+
+ \begin{center}
+ \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}
+ \centering\smath{%
+ \infer{P\,t}
+ {\begin{array}{l}
+ \forall x.\;P\,x\\[2mm]
+ \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]
+ \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\
+ \end{array}
+ }}
+ \end{beamercolorbox}
+ \end{center}
+
+ \item It requires us in the lambda-case to show the property \smath{P} for
+ all binders \smath{x}.\smallskip\\
+
+ (This nearly always requires renamings and they can be
+ tricky to automate.)
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{\Large Strong Induction Principles}
+
+ \begin{itemize}
+ \item Therefore we introduced the following strong induction principle:
+
+ \begin{center}
+ \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
+ \centering\smath{%
+ \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%
+ \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%
+ \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}
+ {\begin{array}{l}
+ \forall x\,c.\;P\,c\;x\\[2mm]
+ \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
+ \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
+ \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}}
+ \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
+ \end{array}
+ }}
+ \end{beamercolorbox}
+ \end{center}
+ \end{itemize}
+
+ \begin{textblock}{11}(0.9,10.9)
+ \only<2>{
+ \begin{tikzpicture}[remember picture]
+ \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)
+ { The variable over which the induction proceeds:\\[2mm]
+ \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};
+
+ \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);
+ \end{tikzpicture}}
+
+ \only<3>{
+ \begin{tikzpicture}[remember picture]
+ \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)
+ {The {\bf context} of the induction; i.e.~what the binder should be fresh for
+ $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]
+ ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}}
+ and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};
+
+ \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);
+ \end{tikzpicture}}
+
+ \only<4>{
+ \begin{tikzpicture}[remember picture]
+ \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)
+ {The property to be proved by induction:\\[-3mm]
+ \begin{center}\small
+ \begin{tabular}{l}
+ \smath{\!\!\lambda
+ (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]
+ \hspace{8mm}
+ \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}
+ \end{tabular}
+ \end{center}};
+
+ \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-4>
+ \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item binding sets of names has some interesting properties:\medskip
+
+ \begin{center}
+ \begin{tabular}{l}
+ \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}
+ \bigskip\smallskip\\
+
+ \onslide<2->{%
+ \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}
+ }\bigskip\smallskip\\
+
+ \onslide<3->{%
+ \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}
+ }\medskip\\
+ \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \begin{textblock}{8}(2,14.5)
+ \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct
+ \end{textblock}
+
+ \only<4>{
+ \begin{textblock}{6}(2.5,4)
+ \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
+ For type-schemes the order of bound names does not matter, and
+ $\alpha$-equivalence is preserved under \alert{vacuous} binders.
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-3>
+ \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item alpha-equivalence being preserved under vacuous binders is \underline{not} always
+ wanted:\bigskip\bigskip\normalsize
+
+ \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+ $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\
+ \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}
+ \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}
+ \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}
+ \end{tabular}}
+
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>
+ \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}
+ \mbox{}\\[-3mm]
+
+ \begin{itemize}
+ \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip
+
+ \begin{center}
+ \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+ $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\
+ $\;\;\;\not\approx_\alpha
+ \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$
+ \end{tabular}}
+ \end{center}
+
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<2-3>
+ \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \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 \only<2->{x::}name \only<2->{t::}trm
+ & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
+ \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
+ & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
+ \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
+ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+ \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
+ \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
+ \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}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{So Far So Good}
+
+ \begin{itemize}
+ \item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}
+ \end{itemize}
+
+ \begin{center}
+ \begin{block}{}
+ \color{gray}
+ \small%
+ {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm]
+ If $M_1,\ldots,M_n$ occur in a certain mathematical context
+ (e.g. definition, proof), then in these terms all bound variables
+ are chosen to be different from the free variables.\\[2mm]
+
+ \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+ \end{block}
+ \end{center}
+
+ \mbox{}\\[-18mm]\mbox{}
+
+ \begin{columns}
+ \begin{column}[t]{4.7cm}
+ Inductive Definitions:\\
+ \begin{center}
+ \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}
+ \end{center}
+ \end{column}
+ \begin{column}[t]{7cm}
+ Rule Inductions:\\[2mm]
+ \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}
+ 1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]
+ 2.) & Show the property for\\ & the conclusion.\\
+ \end{tabular}
+ \end{column}
+ \end{columns}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
+ \begin{frame}[sqeeze]
+ \frametitle{Faulty Reasoning}
+
+ %\mbox{}
+
+ \begin{itemize}
+ \item Consider the two-place relation \smath{\text{foo}}:\medskip
+ \begin{center}
+ \begin{tabular}{ccc}
+ \raisebox{2.5mm}{\colorbox{cream}{%
+ \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}
+ &
+ \raisebox{2mm}{\colorbox{cream}{%
+ \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}
+ &
+ \colorbox{cream}{%
+ \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]
+ \end{tabular}
+ \end{center}
+
+ \pause
+
+ \item The lemma we going to prove:\smallskip
+ \begin{center}
+ Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.
+ \end{center}\bigskip
+
+ \only<3>{
+ \item Cases 1 and 2 are trivial:\medskip
+ \begin{itemize}
+ \item If \smath{y\fresh x} then \smath{y\fresh x}.
+ \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.
+ \end{itemize}
+ }
+
+ \only<4->{
+ \item Case 3:
+ \begin{itemize}
+ \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.};
+ We have to show \smath{y\fresh t'}.$\!\!\!\!$
+ \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.
+ \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!
+ \end{itemize}
+ }
+ \end{itemize}
+
+ \begin{textblock}{11.3}(0.7,0.6)
+ \only<5-7>{
+ \begin{tikzpicture}
+ \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)
+ {{\bf Variable Convention:}\\[2mm]
+ \small
+ If $M_1,\ldots,M_n$ occur in a certain mathematical context
+ (e.g. definition, proof), then in these terms all bound variables
+ are chosen to be different from the free variables.\smallskip
+
+ \normalsize
+ {\bf In our case:}\\[2mm]
+ The free variables are \smath{y} and \smath{t'}; the bound one is
+ \smath{x}.\medskip
+
+ By the variable convention we conclude that \smath{x\not= y}.
+ };
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \begin{textblock}{9.2}(3.6,9)
+ \only<6,7>{
+ \begin{tikzpicture}[remember picture]
+ \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)
+ {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow
+ y\!\not\in\! \text{fv}(t)\!-\!\{x\}
+ \stackrel{x\not=y}{\Longleftrightarrow}
+ y\!\not\in\! \text{fv}(t)}};
+
+ \path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{Conclusions}
+
+ \begin{itemize}
+ \item The user does not see anything of the ``raw'' level.
+ \item The Nominal Isabelle automatically derives the strong structural
+ induction principle for \underline{\bf all} nominal datatypes (not just the
+ lambda-calculus)
+
+ \item They are easy to use: you just have to think carefully what the variable
+ convention should be.
+
+ \item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners
+ of the variable convention: when and where it can be used safely.
+
+ \item<2> \alert{\bf Main Point:} Actually these proofs using the
+ variable convention are all trivial / obvious / routine\ldots {\bf provided}
+ you use Nominal Isabelle. ;o)
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[b]
+ \frametitle{
+ \begin{tabular}{c}
+ \mbox{}\\[13mm]
+ \alert{\LARGE Thank you very much!}\\
+ \alert{\Large Questions?}
+ \end{tabular}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file