23   \large General Bindings\\[15mm]

    23   \large General Bindings in Isabelle\\[15mm]

   127   \begin{frame}<1-4>

   127   \begin{frame}<1-6>

   132   \item<1-> $(a\;b) = (b\;a)$\bigskip  

   132   \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip  

   136   \item<3-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip

   136   \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip

   144    \onslide<4->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}

   144    \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$}

   145   \end{itemize}

   145   \end{itemize}

   146 

   147   \only<4>{

   148   \begin{textblock}{6}(2.5,11)

   149   \begin{tikzpicture}

   150   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   151   {\normalsize\color{darkgray}

   152   \begin{minipage}{8cm}\raggedright

   153   This is slightly odd, since in general: 

   154   \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center}

   155   \end{minipage}};

   156   \end{tikzpicture}

   157   \end{textblock}}

   166 typedef name = "{a :: atom. sort a = ''name''}"

   178 typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*)

   167 (*<*)sorry(*>*)

   179 typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)

   172   \item<2-> there is a function \underline{atom}, which injects concrete atoms into generic atoms\medskip 

   184   \item<2-> there is an overloaded  function \underline{atom}, which injects concrete 

   185   atoms into generic ones\medskip 

   197   \item the formalised version of the nominal theory is much nicer to 

   210   \item the formalised version of the nominal theory is now much nicer to 

   198   work with (no assumptions, just two type classes; sorts are occasionally 

   211   work with (sorts are occasionally explicit)\bigskip

   199   explicit)\bigskip

   216   \mbox{}\\[-3mm]

   228   \mbox{}\\[-6mm]

   217 

   229 

   218   \begin{itemize}

   230   \begin{itemize}

   219   \item old Nominal provided single binders

   231   \item old Nominal provided a reasoning infrastructure for single binders\medskip

   232   

   224   \item<2-> representing 

   237   \item<2-> but representing 

   238 

   227   \end{center}

   241   \end{center}\medskip

   228   is a major pain, take my word for it

   242 

   229   \end{itemize}

   243   with single binders is a \alert{major} pain; take my word for it!

   230   

   244   \end{itemize}

   231   \end{frame}}

   245 

   232   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   246   \only<1>{

   233 *}

   247   \begin{textblock}{6}(1.5,11)

   234 

   248   \small

   235 

   249   for example\\

   250   \begin{tabular}{l@ {\hspace{2mm}}l}

   251   \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\

   252   \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\

   253   \end{tabular}

   254   \end{textblock}}

   255   

   256   \end{frame}}

   257   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   258 *}

   259 

   260 text_raw {*

   261   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   262   \mode<presentation>{

   263   \begin{frame}<1-4>

   264   \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}

   265   \mbox{}\\[-3mm]

   266 

   267   \begin{itemize}

   268   \item binding sets of names has some interesting properties:\medskip

   269   

   270   \begin{center}

   271   \begin{tabular}{l}

   272   $\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$

   273   \bigskip\smallskip\\

   274 

   275   \onslide<2->{%

   276   $\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$

   277   }\bigskip\smallskip\\

   278 

   279   \onslide<3->{%

   280   $\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$

   281   }\medskip\\

   282   \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}

   283   \end{tabular}

   284   \end{center}

   285   \end{itemize}

   286   

   287   \begin{textblock}{8}(2,14.5)

   288   \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct

   289   \end{textblock}

   290 

   291   \only<4>{

   292   \begin{textblock}{6}(2.5,4)

   293   \begin{tikzpicture}

   294   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   295   {\normalsize\color{darkgray}

   296   \begin{minipage}{8cm}\raggedright

   297   For type-schemes the order of bound names does not matter, and

   298   alpha-equivalence is preserved under \alert{vacuous} binders.

   299   \end{minipage}};

   300   \end{tikzpicture}

   301   \end{textblock}}

   302   \end{frame}}

   303   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   304 *}

   305 

   306 text_raw {*

   307   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   308   \mode<presentation>{

   309   \begin{frame}<1-3>

   310   \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}

   311   \mbox{}\\[-3mm]

   312 

   313   \begin{itemize}

   314   \item alpha-equivalence being preserved under vacuous binders is \underline{not} always

   315   wanted:\bigskip\bigskip\normalsize

   316   

   317   \begin{tabular}{@ {\hspace{-8mm}}l}

   318   $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\

   319   \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}

   320    \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}

   321     \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}

   322   \end{tabular}

   323   

   324 

   325   \end{itemize}

   326 

   327   \end{frame}}

   328   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   329 *}

   330 

   331 text_raw {*

   332   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   333   \mode<presentation>{

   334   \begin{frame}<1>

   335   \frametitle{\begin{tabular}{c}\LARGE{}Even Another Binding Mode\end{tabular}}

   336   \mbox{}\\[-3mm]

   337 

   338   \begin{itemize}

   339   \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip

   340   

   341   \begin{center}

   342   \begin{tabular}{@ {\hspace{-8mm}}l}

   343   $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\

   344   $\;\;\;\not\approx_\alpha

   345    \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$

   346   \end{tabular}

   347   \end{center}

   348   

   349 

   350   \end{itemize}

   351 

   352   \end{frame}}

   353   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   354 *}

   355 

   356 text_raw {*

   357   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   358   \mode<presentation>{

   359   \begin{frame}<1-2>

   360   \frametitle{\begin{tabular}{c}\LARGE{}Three Binding Modes\end{tabular}}

   361   \mbox{}\\[-3mm]

   362 

   363   \begin{itemize}

   364   \item the order does not matter and alpha-equivelence is preserved under

   365   vacuous binders (restriction)\medskip

   366   

   367   \item the order does not matter, but the cardinality of the binders 

   368   must be the same (abstraction)\medskip

   369 

   370   \item the order does matter

   371   \end{itemize}

   372 

   373   \onslide<2->{

   374   \begin{center}

   375   \isacommand{bind\_res}\hspace{6mm}

   376   \isacommand{bind\_set}\hspace{6mm}

   377   \isacommand{bind}

   378   \end{center}}

   379 

   380   \end{frame}}

   381   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   382 *}

   383 

   384 text_raw {*

   385   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   386   \mode<presentation>{

   387   \begin{frame}<1-3>

   388   \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}

   389   \mbox{}\\[-6mm]

   390 

   391   \mbox{}\hspace{10mm}

   392   \begin{tabular}{ll}

   393   \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\

   394   \hspace{5mm}\phantom{$|$} Var name\\

   395   \hspace{5mm}$|$ App trm trm\\

   396   \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm

   397   & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\

   398   \hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm

   399   & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\

   400   \multicolumn{2}{l}{\isacommand{and} assn $=$}\\

   401   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\

   402   \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\

   403   \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\

   404   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $\varnothing$}}\\

   405   \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\

   406   \end{tabular}

   407 

   408 

   409 

   410   \end{frame}}

   411   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   412 *}

   413 

   414 text_raw {*

   415   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   416   \mode<presentation>{

   417   \begin{frame}<1-4>

   418   \frametitle{\begin{tabular}{c}Ott\end{tabular}}

   419   \mbox{}\\[-3mm]

   420 

   421   \begin{itemize}

   422   \item this way of specifying binding is pretty much stolen from 

   423   Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip

   424 

   425   \begin{itemize}

   426   \item<2-> Ott allows specifications like\smallskip

   427   \begin{center}

   428   $t ::= t\;t\; |\;\lambda x.t$

   429   \end{center}\medskip

   430 

   431   \item<3-> whether something is bound can depend on other bound things\smallskip

   432   \begin{center}

   433   Foo $(\lambda x. t)\; s$ 

   434   \end{center}\medskip

   435   \onslide<4->{this might make sense for ``raw'' terms, but not at all 

   436   for $\alpha$-equated terms}

   437   \end{itemize}

   438   \end{itemize}

   439 

   440 

   441   \end{frame}}

   442   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   443 *}

   444 text_raw {*

   445   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   446   \mode<presentation>{

   447   \begin{frame}<1>

   448   \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}

   449   \mbox{}\\[-3mm]

   450 

   451   \begin{itemize}

   452   \item in old Nominal we represented single binders as partial functions:\bigskip

   453   

   454   \begin{center}

   455   \begin{tabular}{l}

   456   Lam [$a$].$t$ $\;\dn$\\[2mm]

   457   \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\

   458   \phantom{\;\;\;\;$\lambda b.$\;\;\;}$\text{if}\;b \fresh t\;

   459   \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ 

   460   \end{tabular}

   461   \end{center}

   462   \end{itemize}

   463 

   464   \begin{textblock}{10}(2,14)

   465   \footnotesize $^*$ alpha-equality coincides with equality on functions

   466   \end{textblock}

   467   \end{frame}}

   468   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   469 *}

   470 

   471 text_raw {*

   472   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   473   \mode<presentation>{

   474   \begin{frame}<1-9>

   475   \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}

   476   \mbox{}\\[-3mm]

   477 

   478   \begin{itemize}

   479   \item lets first look at pairs\bigskip\medskip

   480 

   481   \begin{tabular}{@ {\hspace{1cm}}l}

   482   $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}%

   483            \only<8>{${}_{\text{\alert{list}}}$}%

   484            \only<9>{${}_{\text{\alert{res}}}$}}%

   485            \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$

   486   \end{tabular}\bigskip

   487   \end{itemize}

   488 

   489   \only<1>{

   490   \begin{textblock}{8}(3,8.5)

   491   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}

   492   \pgfuseshading{smallspherered} & $as$ is a set of atoms\ldots the binders\\

   493   \pgfuseshading{smallspherered} & $x$ is the body\\

   494   \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality 

   495   of the binders has to be the same\\

   496   \end{tabular}

   497   \end{textblock}}

   498 

   499   \only<4->{

   500   \begin{textblock}{12}(5,8)

   501   \begin{tabular}{ll@ {\hspace{1mm}}l}

   502   $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm]

   503         & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm]

   504         & \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm]

   505         & \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\

   506   \end{tabular}

   507   \end{textblock}}

   508   

   509   \only<8>{

   510   \begin{textblock}{8}(3,13.8)

   511   \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms 

   512   \end{textblock}}

   513   \end{frame}}

   514   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   515 *}

   516 

   517 text_raw {*

   518   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   519   \mode<presentation>{

   520   \begin{frame}<1-2>

   521   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

   522   \mbox{}\\[-3mm]

   523 

   524   \begin{itemize}

   525   \item lets look at ``type-schemes'':\medskip\medskip

   526 

   527   \begin{center}

   528   $(as, x) \approx\!\makebox[0mm][l]{${}_{\text{set}}$}\only<1>{{}^{R,\text{fv}}}\only<2->{{}^{\alert{=},\alert{\text{fv}}}} (bs, y)$

   529   \end{center}\medskip

   530 

   531   \onslide<2->{

   532   \begin{center}

   533   \begin{tabular}{l}

   534   $\text{fv}(x) = \{x\}$\\[1mm]

   535   $\text{fv}(T_1 \rightarrow T_2) = \text{fv}(T_1) \cup \text{fv}(T_2)$\\

   536   \end{tabular}

   537   \end{center}}

   538   \end{itemize}

   539 

   540   

   541   \only<2->{

   542   \begin{textblock}{4}(0.3,12)

   543   \begin{tikzpicture}

   544   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   545   {\tiny\color{darkgray}

   546   \begin{minipage}{3.4cm}\raggedright

   547   \begin{tabular}{r@ {\hspace{1mm}}l}

   548   \multicolumn{2}{@ {}l}{res:}\\

   549   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   550   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   551   $\wedge$ & $\pi \cdot x = y$\\

   552   \\

   553   \end{tabular}

   554   \end{minipage}};

   555   \end{tikzpicture}

   556   \end{textblock}}

   557   \only<2->{

   558   \begin{textblock}{4}(5.2,12)

   559   \begin{tikzpicture}

   560   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   561   {\tiny\color{darkgray}

   562   \begin{minipage}{3.4cm}\raggedright

   563   \begin{tabular}{r@ {\hspace{1mm}}l}

   564   \multicolumn{2}{@ {}l}{set:}\\

   565   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   566   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   567   $\wedge$ & $\pi \cdot x = y$\\

   568   $\wedge$ & $\pi \cdot as = bs$\\

   569   \end{tabular}

   570   \end{minipage}};

   571   \end{tikzpicture}

   572   \end{textblock}}

   573   \only<2->{

   574   \begin{textblock}{4}(10.2,12)

   575   \begin{tikzpicture}

   576   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   577   {\tiny\color{darkgray}

   578   \begin{minipage}{3.4cm}\raggedright

   579   \begin{tabular}{r@ {\hspace{1mm}}l}

   580   \multicolumn{2}{@ {}l}{list:}\\

   581   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   582   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   583   $\wedge$ & $\pi \cdot x = y$\\

   584   $\wedge$ & $\pi \cdot as = bs$\\

   585   \end{tabular}

   586   \end{minipage}};

   587   \end{tikzpicture}

   588   \end{textblock}}

   589 

   590   \end{frame}}

   591   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   592 *}

   593 

   594 text_raw {*

   595   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   596   \mode<presentation>{

   597   \begin{frame}<1-2>

   598   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

   599   \mbox{}\\[-3mm]

   600 

   601   \begin{center}

   602   \only<1>{$(\{x, y\}, x \rightarrow y) \approx_? (\{x, y\}, y \rightarrow x)$}

   603   \only<2>{$([x, y], x \rightarrow y) \approx_? ([x, y], y \rightarrow x)$}

   604   \end{center}

   605 

   606   \begin{itemize}

   607   \item $\approx_{\text{res}}$, $\approx_{\text{set}}$% 

   608   \only<2>{, \alert{$\not\approx_{\text{list}}$}}

   609   \end{itemize}

   610 

   611   

   612   \only<1->{

   613   \begin{textblock}{4}(0.3,12)

   614   \begin{tikzpicture}

   615   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   616   {\tiny\color{darkgray}

   617   \begin{minipage}{3.4cm}\raggedright

   618   \begin{tabular}{r@ {\hspace{1mm}}l}

   619   \multicolumn{2}{@ {}l}{res:}\\

   620   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   621   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   622   $\wedge$ & $\pi \cdot x = y$\\

   623   \\

   624   \end{tabular}

   625   \end{minipage}};

   626   \end{tikzpicture}

   627   \end{textblock}}

   628   \only<1->{

   629   \begin{textblock}{4}(5.2,12)

   630   \begin{tikzpicture}

   631   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   632   {\tiny\color{darkgray}

   633   \begin{minipage}{3.4cm}\raggedright

   634   \begin{tabular}{r@ {\hspace{1mm}}l}

   635   \multicolumn{2}{@ {}l}{set:}\\

   636   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   637   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   638   $\wedge$ & $\pi \cdot x = y$\\

   639   $\wedge$ & $\pi \cdot as = bs$\\

   640   \end{tabular}

   641   \end{minipage}};

   642   \end{tikzpicture}

   643   \end{textblock}}

   644   \only<1->{

   645   \begin{textblock}{4}(10.2,12)

   646   \begin{tikzpicture}

   647   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   648   {\tiny\color{darkgray}

   649   \begin{minipage}{3.4cm}\raggedright

   650   \begin{tabular}{r@ {\hspace{1mm}}l}

   651   \multicolumn{2}{@ {}l}{list:}\\

   652   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   653   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   654   $\wedge$ & $\pi \cdot x = y$\\

   655   $\wedge$ & $\pi \cdot as = bs$\\

   656   \end{tabular}

   657   \end{minipage}};

   658   \end{tikzpicture}

   659   \end{textblock}}

   660 

   661   \end{frame}}

   662   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   663 *}

   664 

   665 text_raw {*

   666   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   667   \mode<presentation>{

   668   \begin{frame}<1>

   669   \frametitle{\begin{tabular}{c}Examples\end{tabular}}

   670   \mbox{}\\[-3mm]

   671 

   672   \begin{center}

   673   \only<1>{$(\{x\}, x) \approx_? (\{x, y\}, x)$}

   674   \end{center}

   675 

   676   \begin{itemize}

   677   \item $\approx_{\text{res}}$, $\not\approx_{\text{set}}$,

   678         $\not\approx_{\text{list}}$

   679   \end{itemize}

   680 

   681   

   682   \only<1->{

   683   \begin{textblock}{4}(0.3,12)

   684   \begin{tikzpicture}

   685   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   686   {\tiny\color{darkgray}

   687   \begin{minipage}{3.4cm}\raggedright

   688   \begin{tabular}{r@ {\hspace{1mm}}l}

   689   \multicolumn{2}{@ {}l}{res:}\\

   690   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   691   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   692   $\wedge$ & $\pi \cdot x = y$\\

   693   \\

   694   \end{tabular}

   695   \end{minipage}};

   696   \end{tikzpicture}

   697   \end{textblock}}

   698   \only<1->{

   699   \begin{textblock}{4}(5.2,12)

   700   \begin{tikzpicture}

   701   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   702   {\tiny\color{darkgray}

   703   \begin{minipage}{3.4cm}\raggedright

   704   \begin{tabular}{r@ {\hspace{1mm}}l}

   705   \multicolumn{2}{@ {}l}{set:}\\

   706   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   707   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   708   $\wedge$ & $\pi \cdot x = y$\\

   709   $\wedge$ & $\pi \cdot as = bs$\\

   710   \end{tabular}

   711   \end{minipage}};

   712   \end{tikzpicture}

   713   \end{textblock}}

   714   \only<1->{

   715   \begin{textblock}{4}(10.2,12)

   716   \begin{tikzpicture}

   717   \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   718   {\tiny\color{darkgray}

   719   \begin{minipage}{3.4cm}\raggedright

   720   \begin{tabular}{r@ {\hspace{1mm}}l}

   721   \multicolumn{2}{@ {}l}{list:}\\

   722   $\exists\pi.$ & $\text{fv}(x) - as = \text{fv}(y) - bs$\\

   723   $\wedge$ & $\text{fv}(x) - as \fresh^* \pi$\\

   724   $\wedge$ & $\pi \cdot x = y$\\

   725   $\wedge$ & $\pi \cdot as = bs$\\

   726   \end{tabular}

   727   \end{minipage}};

   728   \end{tikzpicture}

   729   \end{textblock}}

   730 

   731   \end{frame}}

   732   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   733 *}

   734 

   735 text_raw {*

   736   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   737   \mode<presentation>{

   738   \begin{frame}<1-3>

   739   \frametitle{\begin{tabular}{c}General Abstractions\end{tabular}}

   740   \mbox{}\\[-7mm]

   741 

   742   \begin{itemize}

   743   \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip

   744   \item they are equivalence relations\medskip

   745   \item we can therefore use the quotient package to introduce the 

   746   types $\beta\;\text{abs}_\star$\bigskip

   747   \begin{center}

   748   \only<1>{$[as].\,x$}

   749   \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$}

   750   \only<3>{%

   751   \begin{tabular}{r@ {\hspace{1mm}}l}

   752   \multicolumn{2}{@ {\hspace{-7mm}}l}{$[as]. x \alert{=}  [bs].y\;\;\;\text{if\!f}$}\\[2mm]

   753   $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\

   754   $\wedge$       & $\text{supp}(x) - as \fresh^* \pi$\\

   755   $\wedge$       & $\pi \act x = y $\\

   756   $(\wedge$       & $\pi \act as = bs)\;^\star$\\

   757   \end{tabular}}

   758   \end{center}

   759   \end{itemize}

   760 

   761   

   762   \end{frame}}

   763   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   764 *}

   765 

   766 text_raw {*

   767   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   768   \mode<presentation>{

   769   \begin{frame}<1>

   770   \frametitle{\begin{tabular}{c}One Problem\end{tabular}}

   771   \mbox{}\\[-3mm]

   772 

   773   \begin{center}

   774   $\text{let}\;x_1=t_1 \ldots x_n=t_n\;\text{in}\;s$

   775   \end{center}

   776 

   777   \begin{itemize}

   778   \item we cannot represent this as\medskip

   779   \begin{center}

   780   $\text{let}\;[x_1,\ldots,x_n]\alert{.}s\;\;[t_1,\ldots,t_n]$

   781   \end{center}\bigskip

   782 

   783   because\medskip

   784   \begin{center}

   785   $\text{let}\;[x].s\;\;[t_1,t_2]$

   786   \end{center}

   787   \end{itemize}

   788 

   789   

   790   \end{frame}}

   791   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   792 *}

   793 

   794 text_raw {*

   795   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   796   \mode<presentation>{

   797   \begin{frame}<1->

   798   \frametitle{\begin{tabular}{c}Our Specifications\end{tabular}}

   799   \mbox{}\\[-6mm]

   800 

   801   \mbox{}\hspace{10mm}

   802   \begin{tabular}{ll}

   803   \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\

   804   \hspace{5mm}\phantom{$|$} Var name\\

   805   \hspace{5mm}$|$ App trm trm\\

   806   \hspace{5mm}$|$ Lam x::name t::trm

   807   & \isacommand{bind} x \isacommand{in} t\\

   808   \hspace{5mm}$|$ Let as::assn t::trm

   809   & \isacommand{bind} bn(as) \isacommand{in} t\\

   810   \multicolumn{2}{l}{\isacommand{and} assn $=$}\\

   811   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\

   812   \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\

   813   \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\

   814   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\

   815   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\

   816   \end{tabular}

   817 

   818 

   819 

   820   \end{frame}}

   821   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   822 *}

   823 

   824 text_raw {*

   825   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   826   \mode<presentation>{

   827   \begin{frame}<1-2>

   828   \frametitle{\begin{tabular}{c}``Raw'' Definitions\end{tabular}}

   829   \mbox{}\\[-6mm]

   830 

   831   \mbox{}\hspace{10mm}

   832   \begin{tabular}{ll}

   833   \multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\

   834   \hspace{5mm}\phantom{$|$} Var name\\

   835   \hspace{5mm}$|$ App trm trm\\

   836   \hspace{5mm}$|$ Lam name trm\\

   837   \hspace{5mm}$|$ Let assn trm\\

   838   \multicolumn{2}{l}{\isacommand{and} assn $=$}\\

   839   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\

   840   \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm]

   841   \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\

   842   \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\

   843   \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\

   844   \end{tabular}

   845 

   846   \only<2>{

   847   \begin{textblock}{5}(10,5)

   848   $+$ \begin{tabular}{l}automatically\\ 

   849   generate fv's\end{tabular}

   850   \end{textblock}}

   851   \end{frame}}

   852   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   853 *}

   854 

   855 text_raw {*

   856   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   857   \mode<presentation>{

   858   \begin{frame}<1>

   859   \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}

   860   \mbox{}\\[6mm]

   861 

   862   \begin{center}

   863   Lam x::name t::trm \hspace{10mm}\isacommand{bind} x \isacommand{in} t\\

   864   \end{center}

   865 

   866 

   867   \[

   868   \infer[\text{Lam-}\!\approx_\alpha]

   869   {\text{Lam}\;x\;t \approx_\alpha \text{Lam}\;x'\;t'}

   870   {([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}

   871     ^{\approx_\alpha,\text{fv}} ([x'], t')}

   872   \]

   873 

   874 

   875   \end{frame}}

   876   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   877 *}

   878 

   879 text_raw {*

   880   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   881   \mode<presentation>{

   882   \begin{frame}<1>

   883   \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}

   884   \mbox{}\\[6mm]

   885 

   886   \begin{center}

   887   Lam x::name y::name t::trm s::trm \hspace{5mm}\isacommand{bind} x y \isacommand{in} t s\\

   888   \end{center}

   889 

   890 

   891   \[

   892   \infer[\text{Lam-}\!\approx_\alpha]

   893   {\text{Lam}\;x\;y\;t\;s \approx_\alpha \text{Lam}\;x'\;y'\;t'\;s'}

   894   {([x, y], (t, s)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}

   895     ^{R, fv} ([x', y'], (t', s'))}

   896   \]

   897 

   898   \footnotesize

   899   where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\times\text{fv}$

   900 

   901   \end{frame}}

   902   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   903 *}

   904 

   905 text_raw {*

   906   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   907   \mode<presentation>{

   908   \begin{frame}<1-2>

   909   \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}

   910   \mbox{}\\[6mm]

   911 

   912   \begin{center}

   913   Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\

   914   \end{center}

   915 

   916 

   917   \[

   918   \infer[\text{Let-}\!\approx_\alpha]

   919   {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'}

   920   {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}

   921     ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') &

   922    \onslide<2>{as \approx_\alpha^{\text{bn}} as'}}

   923   \]

   924 

   925 

   926   \end{frame}}

   927   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   928 *}

   929 

   930 text_raw {*

   931   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   932   \mode<presentation>{

   933   \begin{frame}<1->

   934   \frametitle{\begin{tabular}{c}\LARGE{}$\alpha$ for Binding Functions\end{tabular}}

   935   \mbox{}\\[-6mm]

   936 

   937   \mbox{}\hspace{10mm}

   938   \begin{tabular}{l}

   939   \ldots\\

   940   \isacommand{binder} bn \isacommand{where}\\

   941   \phantom{$|$} bn(ANil) $=$ $[]$\\

   942   $|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)\\

   943   \end{tabular}\bigskip

   944 

   945   \begin{center}

   946   \mbox{\infer{\text{ANil} \approx_\alpha^{\text{bn}} \text{ANil}}{}}\bigskip

   947 

   948   \mbox{\infer{\text{ACons}\;a\;t\;as \approx_\alpha^{\text{bn}} \text{ACons}\;a'\;t'\;as'}

   949   {t \approx_\alpha t' & as \approx_\alpha^{bn} as'}}

   950   \end{center}

   951 

   952 

   953   \end{frame}}

   954   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   955 *}

   956 

   957 text_raw {*

   958   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   959   \mode<presentation>{

   960   \begin{frame}<1->

   961   \frametitle{\begin{tabular}{c}Automatic Proofs\end{tabular}}

   962   \mbox{}\\[-6mm]

   963 

   964   \begin{itemize}

   965   \item we can show that $\alpha$'s are equivalence relations\medskip

   966   \item as a result we can use the quotient package to introduce the type(s)

   967   of $\alpha$-equated terms

   968 

   969   \[

   970   \infer

   971   {\text{Lam}\;x\;t \alert{=} \text{Lam}\;x'\;t'}

   972   {\only<1>{([x], t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$}

   973     ^{=,\text{supp}} ([x'], t')}%

   974    \only<2>{[x].t = [x'].t'}}

   975   \]

   976 

   977 

   978   \item the properties for support are implied by the properties of $[\_].\_$

   979   \item we can derive strong induction principles (almost automatic---just a matter of

   980   another week or two)

   981   \end{itemize}

   982 

   983 

   984   \end{frame}}

   985   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   986 *}

   987 

   988 text_raw {*

   989   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   990   \mode<presentation>{

   991   \begin{frame}<1->

   992   \frametitle{\begin{tabular}{c}Conclusion\end{tabular}}

   993   \mbox{}\\[-6mm]

   994 

   995   \begin{itemize}

   996   \item the user does not see anything of the raw level\medskip

   997   \only<1>{\begin{center}

   998   Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)

   999   \end{center}\bigskip}

  1000 

  1001   \item<2-> we have not yet done function definitions (will come soon and

  1002   we hope to make improvements over the old way there too)\medskip

  1003   \item<3-> it took quite some time to get here, but it seems worthwhile (POPL 2011 tutorial)\medskip

  1004   \item<4-> Thanks goes to Cezary!\\ 

  1005   \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!} 

  1006   \end{itemize}

  1007 

  1008 

  1009   \end{frame}}

  1010   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1011 *}