(*<*)
theory SlidesA
imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
begin
notation (latex output)
set ("_") and
Cons ("_::/_" [66,65] 65)
(*>*)
text_raw {*
%% was \begin{colormixin}{20!averagebackgroundcolor}
%%
%% is \begin{colormixin}{50!averagebackgroundcolor}
\renewcommand{\slidecaption}{Warsaw, 9 February 2012}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\Huge Nominal Techniques\\[0mm]
\Huge in Isabelle\\
\Large or, How Not to be Intimidated by the\\[-3mm]
\Large 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 Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
\end{block}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1->[c]
\frametitle{Nominal Techniques}
\begin{itemize}
\item Andy Pitts found out 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 Nominal Unification\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.1)
\includegraphics[scale=0.26]{andrewpitts.jpg}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Nominal Isabelle}
\begin{itemize}
\item a theory about atoms and permutations\medskip
\item support and freshness
\begin{center}
\smath{\text{supp}(x) \dn \{ a \mid \text{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}
\end{center}\bigskip\pause
\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-6>
\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 $\alpha$-equivalence}}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1-3>[c]
\frametitle{HOL vs.~Nominal}
\begin{itemize}
\item Nominal logic / nominal sets by Pitts are incompatible
with choice principles\medskip
\item HOL includes Hilbert's epsilon\pause\bigskip
\item Solution: Do not require that everything has finite support\medskip
\begin{center}
\smath{\onslide<1-2>{\text{finite}(\text{supp}(x)) \quad\Rightarrow\quad} a \fresh a.x}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{}
\begin{tabular}{c@ {\hspace{2mm}}c}
\\[6mm]
\begin{tabular}{c}
\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
{\footnotesize Bob Harper}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular}
\begin{tabular}{c}
\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
{\footnotesize Frank Pfenning}\\[-2.5mm]
{\footnotesize (CMU)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright
\color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
$\sim$31pp}
\end{tabular}\\
\pause
\\[0mm]
\begin{tabular}{c}
\includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
{\footnotesize Andrew Appel}\\[-2.5mm]
{\footnotesize (Princeton)}
\end{tabular} &
\begin{tabular}{p{6cm}}
\raggedright
\color{gray}{relied on their proof in a\\ {\bf security} critical application}
\end{tabular}
\end{tabular}\medskip\pause
\small
\begin{minipage}{1.0\textwidth}
(I also found an {\bf error} in my Ph.D.-thesis about cut-elimination
examined by Henk Barendregt and Andy Pitts.)
\end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<1,2,3,4>[squeeze]
\frametitle{Formalisation of LF}
\begin{center}
\begin{tabular}{@ {\hspace{-16mm}}lc}
\mbox{}\\[-6mm]
\textcolor{white}{\raisebox{4mm}{1.~Solution}} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
]
\node (proof) [node1] {\large Proof};
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);}
\end{tikzpicture}
\\[2mm]
\onslide<3->{%
\raisebox{4mm}{\textcolor{white}{1st Solution}} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
node2/.style={
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20}
]
\node (proof) [node1] {\large Proof};
\node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$};
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\end{tikzpicture}
\\[2mm]}
\end{tabular}
\end{center}
\begin{textblock}{3}(13.2,5.1)
\onslide<3->{
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
\end{tikzpicture}
}
\end{textblock}
\begin{textblock}{11}(1.4,14.3)
\only<1->{\footnotesize (one needs to check $\sim$31pp~of informal paper proofs from
ACM Transactions on Computational Logic, 2005)}
\end{textblock}
\only<4->{
\begin{textblock}{9}(10,11.5)
\begin{tikzpicture}[remember picture, overlay]
\draw (0,0) node[fill=cream, text width=5.3cm, thick, draw=red, rounded corners=1mm] (n2)
{\raggedright I also found \mbox{(fixable)} mistakes in my Ph.D.~thesis.
};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{\LARGE\begin{tabular}{c}Nominal Isabelle\end{tabular}}
\begin{itemize}
\item \ldots{}is a tool on top of the theorem prover
Isabelle; bound variables have names (no de Bruijn
indices).\medskip
\item It can be used to, for example, represent lambda terms
\begin{center}
\smath{M ::= x\;\mid\; M\,N \;\mid\; \lambda x.M}
\end{center}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\small
\begin{beamercolorbox}[sep=1mm, wd=11cm]{boxcolor}
{\bf Substitution Lemma:}
If \smath{x\not\equiv y} and
\smath{x\not\in \text{fv}(L)}, then\\
\mbox{}\hspace{5mm}\smath{M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]}
\end{beamercolorbox}
{\bf Proof:} \alert<4>{By induction on the structure of \smath{M}.}
\begin{itemize}
\item {\bf Case 1:} \smath{M} is a variable.
\begin{tabular}{@ {}l@ {\hspace{1mm}}p{9cm}@ {}}
Case 1.1. & \smath{M\equiv x}. Then both sides \alert<3,4>{equal}
\smath{N[y:=L]} since \smath{x\not\equiv y}.\\[1mm]
Case 1.2. & \smath{M\equiv y}. Then both sides \alert<3,4>{equal}
\smath{L}, for \smath{x\not\in \text{fv}(L)}\\
& implies \smath{L[x:=\ldots]\equiv L}.\\[1mm]
Case 1.3. & \smath{M\equiv z\not\equiv x,y}. Then both sides \alert<3,4>{equal} \smath{z}.\\[1mm]
\end{tabular}
\item {\bf Case 2:} \smath{M\equiv \lambda z.M_1}.
\alert<2>{By the variable convention we may assume that \smath{z\not\equiv x,y}
and \smath{z} is not free in \smath{N,L}.}
\begin{tabular}{@ {}r@ {\hspace{1mm}}l@ {}}
\smath{(\lambda z.M_1)[x\!:=\!N][y\!:=\!L]}
\smath{\equiv} & \smath{\lambda z.(M_1[x\!:=\!N][y\!:=\!L])}\\
\smath{\equiv} & \smath{\lambda z.(M_1[y\!:=\!L][x\!:=\!N[y\!:=\!L]])}\\
\smath{\equiv} & \smath{(\lambda z.M_1)[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}.\\
\end{tabular}
\item {\bf Case 3:} \smath{M\equiv M_1 M_2}.
The statement follows again from the induction hypothesis. \hfill$\,\Box\,$
\end{itemize}
\begin{textblock}{11}(4,3)
\begin{block}<5>{}
Remember only if \smath{y\not=x} and \smath{x\not\in \text{fv}(N)} then\\[2mm]
\smath{\quad(\lambda y.M)[x:=N]=\lambda y.(M[x:=N])}\\[4mm]
\begin{tabular}{c@ {\hspace{2mm}}l@ {\hspace{2mm}}l@ {}}
& \smath{(\lambda z.M_1)[x:=N][y:=L]}\\[1.3mm]
\smath{\equiv} & \smath{(\lambda z.(M_1[x:=N]))[y:=L]} & $\stackrel{1}{\leftarrow}$\\[1.3mm]
\smath{\equiv} & \smath{\lambda z.(M_1[x:=N][y:=L])} & $\stackrel{2}{\leftarrow}$\\[1.3mm]
\smath{\equiv} & \smath{\lambda z.(M_1[y:=L][x:=N[y:=L]])} & IH\\[1.3mm]
\smath{\equiv} & \smath{(\lambda z.(M_1[y:=L]))[x:=N[y:=L]])}
& $\stackrel{2}{\rightarrow}$ \alert{\bf\;!}\\[1.3mm]
\smath{\equiv} & \smath{(\lambda z.M_1)[y:=L][x:=N[y:=L]]}. &
$\stackrel{1}{\rightarrow}$\\[1.3mm]
\end{tabular}
\end{block}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Nominal Isabelle}
\begin{itemize}
\item Define lambda-terms as:
\end{itemize}
*}
atom_decl name text_raw {*\medskip\isanewline *}
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam "\<guillemotleft>name\<guillemotright>lam" ("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}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
(*<*)
nominal_primrec
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
where
"(Var x)[y::=s] = (if x=y then s else (Var x))"
| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
| "x\<sharp>(y,s) \<Longrightarrow> (SlidesA.Lam x t)[y::=s] = SlidesA.Lam x (t[y::=s])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess)+
done
(*>*)
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
%%\frametitle{\large Formal Proof of the Substitution Lemma}
\small
\begin{tabular}{@ {\hspace{-4mm}}c @ {}}
\begin{minipage}{1.1\textwidth}
*}
lemma forget:
assumes a: "x \<sharp> L"
shows "L[x::=P] = L"
using a by (nominal_induct L avoiding: x P rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
lemma fresh_fact:
fixes z::"name"
assumes a: "z \<sharp> N" "z \<sharp> L"
shows "z \<sharp> N[y::=L]"
using a by (nominal_induct N avoiding: z y L rule: lam.strong_induct)
(auto simp add: abs_fresh fresh_atm)
lemma substitution_lemma:
assumes a: "x \<noteq> y" "x \<sharp> L" -- {* \mbox{}\hspace{-2mm}\tikz[remember picture] \node (n1) {}; *}
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
(auto simp add: fresh_fact forget)
text_raw {*
\end{minipage}
\end{tabular}
\begin{textblock}{6}(11,9)
\only<2>{
\begin{tikzpicture}[remember picture, overlay]
\draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (n2)
{\setlength\leftmargini{6mm}%
\begin{itemize}
\item stands for \smath{x\not\in \text{fv}(L)}\\[-2mm]
\item reads as ``\smath{x} fresh for \smath{L}''
\end{itemize}
};
\path[overlay, ->, very thick, red] (n2) edge[out=-90, in=0] (n1);
\end{tikzpicture}}
\end{textblock}
\only<1-3>{}
\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 will use 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}
\frametitle{\LARGE Strong Induction Principles}
\begin{center}
\mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
\centering\smath{%
\infer{P\,\alert{c}\;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.\;x\fresh c \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
\end{array}
}}
\end{beamercolorbox}
\end{center}
\only<1>{
\begin{textblock}{14}(1.2,9.2)
\begin{itemize}
\item There is a condition for when Barendregt's variable convention
is applicable---it is almost always satisfied, but not always:\\[2mm]
The induction context \smath{c} needs to be finitely supported
(is not allowed to mention all names as free).
\end{itemize}
\end{textblock}}
\only<2>{
\begin{itemize}
\item In the case of the substitution lemma:\\[2mm]
\begin{textblock}{16.5}(0.7,11.5)
\small
*}
(*<*)
lemma
assumes a: "x\<noteq>y" "x \<sharp> L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a
(*>*)
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
txt_raw {* \isanewline$\ldots$ *}
(*<*)oops(*>*)
text_raw {*
\end{textblock}
\end{itemize}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\Large \mbox{Same Problem with Rule Inductions}}
\begin{itemize}
\item We can specify typing-rules for lambda-terms as:
\begin{center}
\begin{tabular}{@ {\hspace{-6mm}}c@ {}}
\colorbox{cream}{
\smath{\infer{\Gamma\vdash x:\tau}{(x\!:\!\tau)\in\Gamma\;\;\text{valid}\;\Gamma}}}
\;\;
\colorbox{cream}{
\smath{\infer{\Gamma\vdash t_1\;t_2:\tau}
{\Gamma\vdash t_1:\sigma\!\rightarrow\!\tau & \Gamma\vdash t_2:\sigma}}}\\[4mm]
\colorbox{cream}{
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}\\[6mm]
\colorbox{cream}{
\smath{\infer{\text{valid}\;[]}{}}}
\;\;\;\;
\colorbox{cream}{
\smath{\infer{\text{valid}\;(x\!:\!\tau)\!::\!\Gamma}{x\fresh\Gamma & \text{valid}\;\Gamma}}}\\[8mm]
\end{tabular}
\end{center}
\item If \smath{\Gamma_1\vdash t:\tau} and \smath{\text{valid}\;\Gamma_2},
\smath{\Gamma_1\subseteq \Gamma_2} then \smath{\Gamma_2\vdash t:\tau}.$\!\!\!\!\!$
\end{itemize}
\begin{textblock}{11}(1.3,4)
\only<2>{
\begin{tikzpicture}
\draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (nn)
{The proof of the weakening lemma is said to be trivial / obvious / routine
/\ldots{} in many places.\\[2mm]
(I am actually still looking for a place in the literature where a
trivial / obvious / routine /\ldots{} proof is spelled out --- I know of
proofs by Gallier, McKinna \& Pollack and Pitts, but I would not
call them trivial / obvious / routine /\ldots)};
\end{tikzpicture}}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Recall: Rule Inductions}
\begin{center}\large
\colorbox{cream}{
\smath{\infer[\text{rule}]{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}}
\end{center}\bigskip
\begin{tabular}[t]{l}
Rule Inductions:\\[1mm]
\begin{tabular}{l@ {\hspace{2mm}}p{8.4cm}}
1.) & Assume the property for the premises. Assume the side-conditions.\\[1mm]
2.) & Show the property for the conclusion.\\
\end{tabular}
\end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\LARGE\mbox{Induction Principle for Typing}}
\begin{itemize}
\item The induction principle that comes with the typing definition is as follows:\\[-13mm]
\mbox{}
\end{itemize}
\begin{center}
\begin{tabular}{@ {\hspace{-5mm}}c@ {}}
\colorbox{cream}{
\smath{
\infer{\Gamma\vdash t:\tau \Rightarrow P\,\Gamma\,t\,\tau}
{\begin{array}{l}
\forall \Gamma\,x\,\tau.\,\;(x\!:\!\tau)\in\Gamma\wedge
\text{valid}\,\Gamma\Rightarrow P\,\Gamma\,(x)\,\tau\\[4mm]
\forall \Gamma\,t_1\,t_2\,\sigma\,\tau.\\
P\,\Gamma\,t_1\,(\sigma\!\rightarrow\!\tau)\wedge
P\,\Gamma\,t_2\,\sigma
\Rightarrow P\,\Gamma\,(t_1\,t_2)\,\tau\\[4mm]
\forall \Gamma\,x\,t\,\sigma\,\tau.\\
x\fresh\Gamma\wedge
P\,((x\!:\!\sigma)\!::\!\Gamma)\,t\,\tau
\Rightarrow P\,\Gamma (\lambda x.t)\,(\sigma\!\rightarrow\!\tau)\\[2mm]
\end{array}
}
}}
\end{tabular}
\end{center}
\begin{textblock}{4}(9,13.8)
\begin{tikzpicture}
\draw (0,0) node[fill=cream, text width=3.9cm, thick, draw=red, rounded corners=1mm] (nn)
{\small Note the quantifiers!};
\end{tikzpicture}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\LARGE \mbox{Proof of Weakening Lemma}}
\mbox{}\\[-18mm]\mbox{}
\begin{center}
\colorbox{cream}{
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}
\end{center}
\begin{minipage}{1.1\textwidth}
\begin{itemize}
\item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then
\smath{\alert<1>{\forall \Gamma_2}.\,\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!
\Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}
\end{itemize}
\pause
\mbox{}\hspace{-5mm}
\underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:
\begin{itemize}
\item We know:\\
\smath{\forall \alert<4->{\Gamma_2}.\,\text{valid}\,\alert<4->{\Gamma_2} \wedge
(x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \alert<4->{\Gamma_2} \Rightarrow \!\!
\tikz[remember picture, baseline=(ea.base)]
\node (ea) {\smath{\alert<4->{\Gamma_2}}};\!\vdash\! t\!:\!\tau}\\
\smath{x\fresh\Gamma_1}\\
\onslide<3->{\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2
\only<6->{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\!
(x\!:\!\sigma)\!::\!\Gamma_2}}}\\
\onslide<3->{\smath{\textcolor{white}{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2
\Rightarrow} \only<7->{\;\alert{\text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2\;\;\text{\bf ???}}}}}
\item We have to show:\\
\only<2>{
\smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge
\Gamma_1\!\subseteq\!\Gamma_2 \Rightarrow \Gamma_2\!\vdash\!
\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}
\only<3->{
\smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}
\end{itemize}
\end{minipage}
\begin{textblock}{4}(10,6.5)
\only<5->{
\begin{tikzpicture}[remember picture]
\draw (0,0) node[fill=cream, text width=4cm, thick, draw=red, rounded corners=1mm] (eb)
{\smath{\Gamma_2\mapsto (x\!:\!\sigma)\!::\!\Gamma_2}};
\path[overlay, ->, ultra thick, red] (eb) edge[out=-90, in=80] (ea);
\end{tikzpicture}}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\begin{textblock}{14.8}(0.7,0.5)
\begin{itemize}
\item The usual proof of strong normalisation for simply- typed lambda-terms
establishes first:\\[1mm]
\colorbox{cream}{%
\begin{tabular}{@ {}p{11cm}}
Lemma: If for all reducible \smath{s}, \smath{t[x\!:=\!s]} is reducible, then
\smath{\lambda x.t} is reducible.
\end{tabular}}\smallskip
\item Then one shows for a closing (simultaneous) substitution:\\[2mm]
\colorbox{cream}{%
\begin{tabular}{@ {}p{11cm}}
Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing
substitutions \smath{\theta} containing reducible terms only,
\smath{\theta(t)} is reducible.
\end{tabular}}
\mbox{}\\[1mm]
Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)}
is reducible with \smath{s} being reducible. This is equal\alert{$^*$} to
\smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get \smath{\lambda
x.(\theta(t))} is reducible. Because this is equal\alert{$^*$} to
\smath{\theta(\lambda x.t)}, we are done.
\hfill\footnotesize\alert{$^*$}you have to take a deep breath
\end{itemize}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\LARGE \mbox{Proof of Weakening Lemma}}
\mbox{}\\[-18mm]\mbox{}
\begin{center}
\colorbox{cream}{
\smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}
{x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}
\end{center}
\begin{minipage}{1.1\textwidth}
\begin{itemize}
\item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then
\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!
\Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}
\end{itemize}
\mbox{}\hspace{-5mm}
\underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:
\begin{itemize}
\item We know:\\
\smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge
(x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \Gamma_2 \Rightarrow \!\!
\Gamma_2\!\vdash\! t\!:\!\tau}\\
\smath{x\fresh\Gamma_1}\\
\begin{tabular}{@ {}ll@ {}}
\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2} &
\only<2->{\smath{\alert{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\!
(x\!:\!\sigma)\!::\!\Gamma_2}}}\\
\smath{\alert{x\fresh\Gamma_2}} &
\only<2->{\smath{\alert{\Rightarrow \text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2}}}
\end{tabular}
\item We have to show:\\
\smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}
\end{itemize}
\end{minipage}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{SN (Again)}
\mbox{}\\[-8mm]
\colorbox{cream}{%
\begin{tabular}{@ {}p{10.5cm}}
Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing
substitutions \smath{\theta} containing reducible terms only,
\smath{\theta(t)} is reducible.
\end{tabular}}\medskip
\begin{itemize}
\item
Since we say that the strong induction should avoid \smath{\theta}, we
get the assumption \alert{$x\fresh\theta$} then:\\[2mm]
\begin{tabular}{@ {}p{10.5cm}}\raggedright
Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)} is reducible
with
\smath{s} being reducible. This is {\bf equal} to
\smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get
\smath{\lambda x.(\theta(t))} is reducible. Because this is {\bf equal} to
\smath{\theta(\lambda x.t)}, we are done.
\end{tabular}\smallskip
\begin{center}
\begin{tabular}{rl}
\smath{x\fresh\theta\Rightarrow} &
\smath{(x\!\mapsto\! s\cup\theta)(t) \;\alert{=}\;(\theta(t))[x\!:=\!s]}\\[1mm]
&
\smath{\theta(\lambda x.t) \;\alert{=}\; \lambda x.(\theta(t))}
\end{tabular}
\end{center}
\end{itemize}
\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>{
\setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
\begin{frame}
\frametitle{VC-Compatibility}
\begin{itemize}
\item We introduced two conditions that make the VC safe to use in rule inductions:
\begin{itemize}
\item the relation needs to be \alert{\bf equivariant}, and
\item the binder is not allowed to occur in the \alert{\bf support} of
the conclusion (not free in the conclusion)\bigskip
\end{itemize}
\item Once a relation satisfies these two conditions, then Nominal
Isabelle derives the strong induction principle automatically.
\end{itemize}
\begin{textblock}{11.3}(0.7,6)
\only<2>{
\begin{tikzpicture}
\draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (nn)
{A relation \smath{R} is {\bf equivariant} iff
%
\begin{center}
\smath{%
\begin{array}[t]{l}
\forall \pi\,t_1\ldots t_n\\[1mm]
\;\;\;\;R\,t_1\ldots t_n \Rightarrow R (\pi\act t_1)\ldots(\pi\act t_n)
\end{array}}
\end{center}
%
This means the relation has to be invariant under permutative renaming of
variables.\smallskip
\small
(This property can be checked automatically if the inductive definition is composed of
equivariant ``things''.)
};
\end{tikzpicture}}
\end{textblock}
\only<3>{}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\mbox{Honest Toil, No Theft!}}
\begin{itemize}
\item The \underline{sacred} principle of HOL:
\begin{block}{}
``The method of `postulating' what we want has many advantages; they are
the same as the advantages of theft over honest toil.''\\[2mm]
\hfill{}\footnotesize B.~Russell, Introduction of Mathematical Philosophy
\end{block}\bigskip\medskip
\item I will show next that the \underline{weak} structural induction
principle implies the \underline{strong} structural induction principle.\\[3mm]
\textcolor{gray}{(I am only going to show the lambda-case.)}
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Permutations}
A permutation \alert{\bf acts} on variable names as follows:
\begin{center}
\begin{tabular}{rcl}
$\smath{{[]}\act a}$ & $\smath{\dn}$ & $\smath{a}$\\
$\smath{(\swap{a_1}{a_2}\!::\!\pi)\act a}$ & $\smath{\dn}$ &
$\smath{\begin{cases}
a_1 &\text{if $\pi\act a = a_2$}\\
a_2 &\text{if $\pi\act a = a_1$}\\
\pi\act a &\text{otherwise}
\end{cases}}$
\end{tabular}
\end{center}
\begin{itemize}
\item $\smath{[]}$ stands for the empty list (the identity permutation), and\smallskip
\item $\smath{\swap{a_1}{a_2}\!::\!\pi}$ stands for the permutation $\smath{\pi}$
followed by the swapping $\smath{\swap{a_1}{a_2}}$.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\Large\mbox{Permutations on Lambda-Terms}}
\begin{itemize}
\item Permutations act on lambda-terms as follows:
\begin{center}
\begin{tabular}{rcl}
$\smath{\pi\act\,x}$ & $\smath{\dn}$ & ``action on variables''\\
$\smath{\pi\act\, (t_1~t_2)}$ & $\smath{\dn}$ & $\smath{(\pi\act t_1)~(\pi\act t_2)}$\\
$\smath{\pi\act(\lambda x.t)}$ & $\smath{\dn}$ & $\smath{\lambda (\pi\act x).(\pi\act t)}$\\
\end{tabular}
\end{center}\medskip
\item Alpha-equivalence can be defined as:
\begin{center}
\begin{tabular}{c}
\colorbox{cream}{\smath{\infer{\lambda x.t_1 = \lambda x.t_2}{t_1=t_2}}}\\[3mm]
\colorbox{cream}{\smath{\infer{\lambda x.t_1
\tikz[baseline=-3pt,remember picture] \node (e1) {\alert<2>{$=$}};
\lambda y.t_2}
{x\not=y & t_1 = \swap{x}{y}\act t_2 & x\fresh t_2}}}
\end{tabular}
\end{center}
\end{itemize}
\begin{textblock}{4}(8.3,14.2)
\only<2>{
\begin{tikzpicture}[remember picture]
\draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (e2)
{\small Notice, I wrote equality here!};
\path[overlay, ->, ultra thick, red] (e2) edge[out=180, in=-90] (e1);
\end{tikzpicture}}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{My Claim}
\begin{center}
\colorbox{cream}{%
\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}
}}}\medskip
\begin{tikzpicture}
\node at (0,0) [single arrow, single arrow tip angle=140,
shape border rotate=270, fill=red,text=white]{implies};
\end{tikzpicture}\medskip
\colorbox{cream}{%
\smath{%
\infer{P c\,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.\;
x\fresh c \wedge (\forall d.\,P d\,t)\Rightarrow P c\,(\lambda x.t)
\end{array}}}}
\end{center}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{\large\mbox{Proof for the Strong Induction Principle}}
\begin{textblock}{14}(1.2,1.7)
\begin{itemize}
\item<1-> We prove \alt<1>{\smath{P c\,t}}{\smath{\forall \pi\,c.\;P c\,(\pi\act t)}}
by induction on \smath{t}.
\item<3-> I.e., we have to show \alt<3>{\smath{P c\,(\pi\act(\lambda x.t))}}
{\smath{P c\,\lambda(\pi\act x).(\pi\act t)}}.
\item<5-> We have \smath{\forall \pi\,c.\;P c\,(\pi\act t)} by induction.
\item<6-> Our weaker precondition says that:\\
\begin{center}
\smath{\forall x\,t\,c.\,x\fresh c \wedge (\forall c.\,P c\,t) \Rightarrow P c\,(\lambda x.t)}
\end{center}
\item<7-> We choose a fresh \smath{y} such that \smath{y\fresh (\pi\act x,\pi\act t,c)}.
\item<8-> Now we can use
\alt<8>{\smath{\forall c.\;P c\,((\swap{y}{\,\pi\act x}\!::\!\pi)\act t)}}
{\smath{\forall c.\;P c\,(\swap{y}{\,\pi\act x}\act\pi\act t)}} \only<10->{to infer}
\only<10->{
\begin{center}
\smath{P\,c\,\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t)}
\end{center}}
\item<11-> However
\begin{center}
\smath{\lambda y.(\swap{y}{\,\pi\act x}\act\pi\act t)
\textcolor{red}{\;=\;}\lambda (\pi\act x).(\pi\act t)}
\end{center}
\item<12> Therefore \smath{P\,c\,\lambda (\pi\act x).(\pi\act t)} and we are done.
\end{itemize}
\end{textblock}
\only<11->{
\begin{textblock}{9}(7,6)
\begin{tikzpicture}[remember picture, overlay]
\draw (0,0) node[fill=cream, text width=7cm, thick, draw=red, rounded corners=1mm] (n2)
{\centering
\smath{\infer{\lambda y.t_1=\lambda x.t_2}{x\not=y & t_1=\swap{x}{y}\act t_2 &
y\fresh t_2}}
};
\end{tikzpicture}
\end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}<3->[squeeze]
\frametitle{Formalisation of LF}
\begin{center}
\begin{tabular}{@ {\hspace{-16mm}}lc}
\mbox{}\\[-6mm]
\textcolor{white}{\raisebox{4mm}{1.~Solution}} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
]
\node (proof) [node1] {\large Proof};
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);}
\end{tikzpicture}
\\[2mm]
\onslide<3->{%
\raisebox{4mm}{1st Solution} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
node2/.style={
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20}
]
\node (proof) [node1] {\large Proof};
\node (def) [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$};
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\end{tikzpicture}
\\[2mm]}
\onslide<4->{%
\raisebox{4mm}{\hspace{-1mm}2nd Solution} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
node2/.style={
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20}
]
\node (proof) [node1] {\large Proof};
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
\node (alg) [node2, right of=proof] {\large Alg.$\!^\text{-ex}$};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\end{tikzpicture}
\\[2mm]}
\onslide<5->{%
\raisebox{4mm}{\hspace{-1mm}3rd Solution} &
\begin{tikzpicture}
[node distance=25mm,
text height=1.5ex,
text depth=.25ex,
node1/.style={
rectangle, minimum size=10mm, rounded corners=3mm, very thick,
draw=black!50, top color=white, bottom color=black!20},
node2/.style={
rectangle, minimum size=12mm, rounded corners=3mm, very thick,
draw=red!70, top color=white, bottom color=red!50!black!20}
]
\node (proof) [node2] {\large Proof};
\node (def) [node1, left of=proof] {\large$\,\;\dn\;\,$};
\node (alg) [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};
\draw[->,black!50,line width=2mm] (proof) -- (def);
\draw[->,black!50,line width=2mm] (proof) -- (alg);
\end{tikzpicture}
\\}
\end{tabular}
\end{center}
\begin{textblock}{3}(13.2,5.1)
\onslide<3->{
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
\end{tikzpicture}
}
\end{textblock}
\begin{textblock}{13}(1.4,15)
\only<3->{\footnotesize (each time one needs to check $\sim$31pp~of informal paper proofs)}
\end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Conclusions}
\begin{itemize}
\item The Nominal Isabelle automatically derives the strong structural
induction principle for \underline{\bf all} nominal datatypes (not just the
lambda-calculus);
\item also for rule inductions (though they have to satisfy the vc-condition).
\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}
\frametitle{\begin{tabular}{c}Nominal Meets\\[-2mm] Automata Theory\end{tabular}}
\begin{itemize}
\item<1-> So what?\bigskip\medskip
\item<2-> I can give you a good argument why regular expressions
are much, much better than automata. \textcolor{darkgray}{(over dinner?)}\medskip
\item<3-> Nominal automata?\bigskip\bigskip\medskip
\end{itemize}
\onslide<2->{
\footnotesize\textcolor{darkgray}{A Formalisation of the Myhill-Nerode Theorem based on
Regular Expressions (by Wu, Zhang and Urban)}
}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}
\frametitle{Quiz}
%%%\small
\mbox{}\\[-9mm]
Imagine\ldots\\[2mm]
\begin{tabular}{@ {\hspace{1cm}}l}
\textcolor{blue}{Var\;``name''} \\
\textcolor{blue}{App\;``lam''\;''lam''}\\
\textcolor{blue}{Lam\;``\flqq{}name\frqq{}lam''} \\
\textcolor{red}{Foo\;``\flqq{}name\frqq{}\flqq{}name\frqq{}lam''\;``
\flqq{}name\frqq{}\flqq{}name\frqq{}lam''}\\[2mm]
\end{tabular}
That means roughly:\\[2mm]
\begin{tabular}{@ {\hspace{1cm}}l}
\alert{Foo\;($\lambda x.y.t_1$)\;($\lambda z.u.t_2$)}
\end{tabular}
\begin{itemize}
\item What does the variable convention look like for \alert{Foo}?
\item What does the clause for capture-avoiding substitution look like?
\end{itemize}
\footnotesize
Answers: Download Nominal Isabelle and try it out\\
\textcolor{white}{Answers:} http://isabelle.in.tum.de/nominal\\
\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
(*>*)