(*<*)

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}