1 (*<*)

     2 theory SlidesA

     3 imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   %% was \begin{colormixin}{20!averagebackgroundcolor}

    15   %% 

    16   %% is \begin{colormixin}{50!averagebackgroundcolor}

    17   \renewcommand{\slidecaption}{Warsaw, 9 February 2012}

    18   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    19   \mode<presentation>{

    20   \begin{frame}

    21   \frametitle{%

    22   \begin{tabular}{@ {}c@ {}}

    23   \Huge Nominal Techniques\\[0mm]

    24   \Huge in Isabelle\\

    25   \Large or, How Not to be Intimidated by the\\[-3mm]

    26   \Large Variable Convention\\[-5mm]

    27   \end{tabular}}

    28   

    29   \begin{center}

    30   Christian Urban\\[1mm]

    31   King's College London\\[-6mm]\mbox{}

    32   \end{center}

    33  

    34   \begin{center}

    35   \begin{block}{}

    36   \color{gray}

    37   \small

    38   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 

    39   If $M_1,\ldots,M_n$ occur in a certain mathematical context

    40   (e.g. definition, proof), then in these terms all bound variables 

    41   are chosen to be different from the free variables.\\[2mm]

    42   

    43   \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

    44   \end{block}

    45   \end{center}

    46 

    47   \end{frame}}

    48   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    49 

    50 *}

    51 

    52 text_raw {*

    53   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    54   \mode<presentation>{

    55   \begin{frame}<1->[c]

    56   \frametitle{Nominal Techniques}

    57 

    58   \begin{itemize}

    59   \item Andy Pitts found out that permutations\\ preserve $\alpha$-equivalence:

    60   \begin{center}

    61   \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 

    62   \end{center}

    63 

    64   \item also permutations and substitutions commute, if you suspend permutations

    65   in front of variables

    66   \begin{center}

    67   \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}

    68   \end{center}\medskip\medskip

    69 

    70   \item this allowed us to define Nominal Unification\medskip

    71   \begin{center}

    72   \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}

    73   \smath{\nabla \vdash a \fresh^? t}

    74   \end{center}

    75   \end{itemize}

    76 

    77   \begin{textblock}{3}(13.1,1.1)

    78   \includegraphics[scale=0.26]{andrewpitts.jpg}

    79   \end{textblock}

    80 

    81   \end{frame}}

    82   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    83 *}

    84 

    85 text_raw {*

    86   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    87   \mode<presentation>{

    88   \begin{frame}[c]

    89   \frametitle{Nominal Isabelle}

    90 

    91   \begin{itemize}

    92   \item a theory about atoms and permutations\medskip

    93 

    94   \item support and freshness

    95   \begin{center}

    96   \smath{\text{supp}(x) \dn \{ a \mid \text{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}

    97   \end{center}\bigskip\pause

    98 

    99   \item $\alpha$-equivalence

   100   \begin{center}

   101   \begin{tabular}{l}

   102   \smath{as.x \approx_\alpha bs.y \dn}\\[2mm]

   103   \hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 

   104   \hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\

   105   \hspace{2cm}\smath{\;\wedge\; \pi \act x = y}

   106   \end{tabular}

   107   \end{center}

   108   \end{itemize}

   109 

   110   \end{frame}}

   111   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   112 *}

   113 

   114 text_raw {*

   115   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   116   \mode<presentation>{

   117   \begin{frame}<1-6>

   118   \frametitle{New Types in HOL}

   119 

   120    \begin{center}

   121   \begin{tikzpicture}[scale=1.5]

   122   %%%\draw[step=2mm] (-4,-1) grid (4,1);

   123   

   124   \onslide<2-4,6>{\draw[very thick] (0.7,0.4) circle (4.25mm);}

   125   \onslide<1-4,6>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}

   126   \onslide<3-5,6>{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}

   127   

   128   \onslide<3-4,6>{\draw (-2.0, 0.845) --  (0.7,0.845);}

   129   \onslide<3-4,6>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}

   130 

   131   \onslide<4-4,6>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}

   132   \onslide<4-5,6>{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}

   133   \onslide<1-4,6>{\draw (1.8, 0.48) node[right=-0.1mm]

   134     {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6>{\alert{(sets of raw terms)}}\end{tabular}};}

   135   \onslide<2-4,6>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}

   136   \onslide<3-5,6>{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}

   137   

   138   \onslide<3-4,6>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}

   139   \onslide<3-4,6>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}

   140 

   141   \onslide<6>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}

   142   \end{tikzpicture}

   143   \end{center}

   144   

   145   \begin{center}

   146   \textcolor{red}{\large\bf\onslide<6>{define $\alpha$-equivalence}}

   147   \end{center}

   148 

   149   \end{frame}}

   150   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   151 *}

   152 

   153 text_raw {*

   154   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   155   \mode<presentation>{

   156   \begin{frame}<1-3>[c]

   157   \frametitle{HOL vs.~Nominal}

   158 

   159   \begin{itemize}

   160   \item Nominal logic / nominal sets by Pitts are incompatible 

   161   with choice principles\medskip

   162 

   163   \item HOL includes Hilbert's epsilon\pause\bigskip

   164 

   165   \item Solution: Do not require that everything has finite support\medskip

   166 

   167   \begin{center}

   168   \smath{\onslide<1-2>{\text{finite}(\text{supp}(x))  \quad\Rightarrow\quad} a \fresh a.x}

   169   \end{center}

   170   \end{itemize}

   171 

   172   \end{frame}}

   173   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   174 *}

   175 

   176 text_raw {*

   177   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   178   \mode<presentation>{

   179   \begin{frame}[c]

   180   \frametitle{}

   181 

   182   \begin{tabular}{c@ {\hspace{2mm}}c}

   183   \\[6mm]

   184   \begin{tabular}{c}

   185   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

   186   {\footnotesize Bob Harper}\\[-2.5mm]

   187   {\footnotesize (CMU)}

   188   \end{tabular}

   189   \begin{tabular}{c}

   190   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

   191   {\footnotesize Frank Pfenning}\\[-2.5mm]

   192   {\footnotesize (CMU)}

   193   \end{tabular} &

   194 

   195   \begin{tabular}{p{6cm}}

   196   \raggedright

   197   \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,

   198   $\sim$31pp}

   199   \end{tabular}\\

   200 

   201   \pause

   202   \\[0mm]

   203   

   204   \begin{tabular}{c}

   205   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   206   {\footnotesize Andrew Appel}\\[-2.5mm]

   207   {\footnotesize (Princeton)}

   208   \end{tabular} &

   209 

   210   \begin{tabular}{p{6cm}}

   211   \raggedright

   212   \color{gray}{relied on their proof in a\\ {\bf security} critical application}

   213   \end{tabular}

   214   \end{tabular}\medskip\pause

   215 

   216   \small

   217   \begin{minipage}{1.0\textwidth}

   218   (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination

   219   examined by Henk Barendregt and Andy Pitts.)

   220   \end{minipage}

   221 

   222   \end{frame}}

   223   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   224 *}

   225 

   226 

   227 

   228 text_raw {*

   229 

   230   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   231   \mode<presentation>{

   232   \begin{frame}<1,2,3,4>[squeeze]

   233   \frametitle{Formalisation of LF} 

   234   

   235   

   236   \begin{center}

   237   \begin{tabular}{@ {\hspace{-16mm}}lc}

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

   239 

   240   \textcolor{white}{\raisebox{4mm}{1.~Solution}} &

   241   \begin{tikzpicture}

   242   [node distance=25mm,

   243    text height=1.5ex,

   244    text depth=.25ex,

   245    node1/.style={

   246      rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   247      draw=black!50, top color=white, bottom color=black!20},

   248   ]

   249 

   250   \node (proof) [node1] {\large Proof};

   251   \node (def)   [node1, left of=proof] {\large$\,\;\dn\;\,$};

   252   \node (alg)  [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};

   253   

   254   \draw[->,black!50,line width=2mm] (proof) -- (def);

   255   \draw[->,black!50,line width=2mm] (proof) -- (alg);

   256 

   257   \onslide<2->{\draw[white,line width=1mm] (0.1,0.6) -- (-0.1,0.25) -- (0.1,-0.25) -- (-0.1,-0.6);} 

   258   \end{tikzpicture}

   259   \\[2mm]

   260 

   261   \onslide<3->{%

   262   \raisebox{4mm}{\textcolor{white}{1st Solution}} &

   263   \begin{tikzpicture}

   264   [node distance=25mm,

   265    text height=1.5ex,

   266    text depth=.25ex,

   267    node1/.style={

   268      rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   269      draw=black!50, top color=white, bottom color=black!20},

   270    node2/.style={

   271      rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   272      draw=red!70, top color=white, bottom color=red!50!black!20}

   273   ]

   274 

   275   \node (proof) [node1] {\large Proof};

   276   \node (def)   [node2, left of=proof] {\large$\dn{}\!\!^\text{+ex}$};

   277   \node (alg)   [node1, right of=proof] {\large\hspace{1mm}Alg.\hspace{1mm}\mbox{}};

   278   

   279   \draw[->,black!50,line width=2mm] (proof) -- (def);

   280   \draw[->,black!50,line width=2mm] (proof) -- (alg);

   281 

   282   \end{tikzpicture}

   283   \\[2mm]}

   284 

   285   \end{tabular}

   286   \end{center}

   287 

   288   \begin{textblock}{3}(13.2,5.1)

   289   \onslide<3->{

   290   \begin{tikzpicture}

   291   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   292   \end{tikzpicture}

   293   }

   294   \end{textblock}

   295 

   296   

   297   \begin{textblock}{11}(1.4,14.3)

   298   \only<1->{\footnotesize (one needs to check $\sim$31pp~of informal paper proofs from 

   299             ACM Transactions on Computational Logic, 2005)}

   300   \end{textblock}

   301 

   302   \only<4->{

   303   \begin{textblock}{9}(10,11.5)

   304   \begin{tikzpicture}[remember picture, overlay]

   305   \draw (0,0) node[fill=cream, text width=5.3cm, thick, draw=red, rounded corners=1mm] (n2)

   306   {\raggedright I also found \mbox{(fixable)} mistakes in my Ph.D.~thesis. 

   307   };

   308   \end{tikzpicture}

   309   \end{textblock}}

   310 

   311   \end{frame}}

   312   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   313 

   314 *}

   315 

   316 text_raw {*

   317 

   318   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   319   \mode<presentation>{

   320   \begin{frame}[c]

   321   \frametitle{\LARGE\begin{tabular}{c}Nominal Isabelle\end{tabular}}

   322   

   323 

   324   \begin{itemize}

   325   \item \ldots{}is a tool on top of the theorem prover

   326   Isabelle; bound variables have names (no de Bruijn 

   327   indices).\medskip

   328 

   329   \item It can be used to, for example, represent lambda terms

   330 

   331   \begin{center}

   332   \smath{M ::= x\;\mid\; M\,N \;\mid\; \lambda x.M}

   333   \end{center}

   334   \end{itemize}

   335   

   336   \end{frame}}

   337   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   338 

   339 *}

   340 

   341 text_raw {* 

   342   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   343   \mode<presentation>{

   344   \begin{frame}

   345   \small

   346   \begin{beamercolorbox}[sep=1mm, wd=11cm]{boxcolor}

   347   {\bf Substitution Lemma:} 

   348   If \smath{x\not\equiv y} and

   349   \smath{x\not\in \text{fv}(L)}, then\\

   350   \mbox{}\hspace{5mm}\smath{M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]}

   351   \end{beamercolorbox}

   352 

   353   {\bf Proof:} \alert<4>{By induction on the structure of \smath{M}.}

   354   \begin{itemize}

   355   \item {\bf Case 1:} \smath{M} is a variable.

   356 

   357   \begin{tabular}{@ {}l@ {\hspace{1mm}}p{9cm}@ {}}

   358    Case 1.1. & \smath{M\equiv x}. Then both sides \alert<3,4>{equal} 

   359                \smath{N[y:=L]} since \smath{x\not\equiv y}.\\[1mm] 

   360    Case 1.2. & \smath{M\equiv y}. Then both sides \alert<3,4>{equal}

   361                \smath{L}, for \smath{x\not\in \text{fv}(L)}\\

   362              & implies \smath{L[x:=\ldots]\equiv L}.\\[1mm]

   363    Case 1.3. & \smath{M\equiv z\not\equiv x,y}. Then both sides \alert<3,4>{equal} \smath{z}.\\[1mm]

   364   \end{tabular}

   365 

   366   \item {\bf Case 2:} \smath{M\equiv \lambda z.M_1}. 

   367   \alert<2>{By the variable convention we may assume that \smath{z\not\equiv x,y} 

   368   and \smath{z} is not free in \smath{N,L}.}

   369 

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

   371   \smath{(\lambda z.M_1)[x\!:=\!N][y\!:=\!L]} 

   372   \smath{\equiv} & \smath{\lambda z.(M_1[x\!:=\!N][y\!:=\!L])}\\

   373   \smath{\equiv} & \smath{\lambda z.(M_1[y\!:=\!L][x\!:=\!N[y\!:=\!L]])}\\

   374   \smath{\equiv} & \smath{(\lambda z.M_1)[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}.\\

   375   \end{tabular}

   376   

   377   \item {\bf Case 3:} \smath{M\equiv M_1 M_2}. 

   378   The statement follows again from the induction hypothesis. \hfill$\,\Box\,$

   379   \end{itemize}

   380 

   381   \begin{textblock}{11}(4,3)

   382   \begin{block}<5>{}

   383   Remember only if \smath{y\not=x} and \smath{x\not\in \text{fv}(N)} then\\[2mm]

   384   \smath{\quad(\lambda y.M)[x:=N]=\lambda y.(M[x:=N])}\\[4mm]

   385   

   386           \begin{tabular}{c@ {\hspace{2mm}}l@ {\hspace{2mm}}l@ {}}

   387             & \smath{(\lambda z.M_1)[x:=N][y:=L]}\\[1.3mm]

   388             \smath{\equiv} & \smath{(\lambda z.(M_1[x:=N]))[y:=L]} & $\stackrel{1}{\leftarrow}$\\[1.3mm]

   389             \smath{\equiv} & \smath{\lambda z.(M_1[x:=N][y:=L])} & $\stackrel{2}{\leftarrow}$\\[1.3mm]

   390             \smath{\equiv} & \smath{\lambda z.(M_1[y:=L][x:=N[y:=L]])} & IH\\[1.3mm] 

   391             \smath{\equiv} & \smath{(\lambda z.(M_1[y:=L]))[x:=N[y:=L]])} 

   392                                  & $\stackrel{2}{\rightarrow}$ \alert{\bf\;!}\\[1.3mm] 

   393             \smath{\equiv} & \smath{(\lambda z.M_1)[y:=L][x:=N[y:=L]]}. & 

   394                                                              $\stackrel{1}{\rightarrow}$\\[1.3mm]

   395           \end{tabular}

   396   \end{block}

   397   \end{textblock}

   398 

   399   \end{frame}}

   400   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   401 *}

   402 

   403 text_raw {*

   404 

   405   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   406   \mode<presentation>{

   407   \begin{frame}

   408   \frametitle{Nominal Isabelle} 

   409 

   410   \begin{itemize}

   411   \item Define lambda-terms as:

   412   \end{itemize}

   413 *}

   414       

   415  atom_decl name   text_raw {*\medskip\isanewline *}

   416 	nominal_datatype lam =

   417 	    Var "name"

   418 	  | App "lam" "lam" 

   419 	  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam _._")

   420 

   421 

   422 text_raw {*

   423   \mbox{}\bigskip

   424 

   425   \begin{itemize}

   426   \item These are \underline{\bf named} alpha-equivalence classes, for example

   427   \end{itemize}

   428 

   429   \begin{center}

   430   \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}

   431   \end{center}

   432 

   433   \end{frame}}

   434   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   435 

   436 *}

   437 

   438 (*<*)

   439 

   440 nominal_primrec

   441   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)

   442 where

   443   "(Var x)[y::=s] = (if x=y then s else (Var x))"

   444 | "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"

   445 | "x\<sharp>(y,s) \<Longrightarrow> (SlidesA.Lam x t)[y::=s] = SlidesA.Lam x (t[y::=s])"

   446 apply(finite_guess)+

   447 apply(rule TrueI)+

   448 apply(simp add: abs_fresh)+

   449 apply(fresh_guess)+

   450 done

   451 

   452 (*>*)

   453 

   454 text_raw {*

   455 

   456   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   457   \mode<presentation>{

   458   \begin{frame}

   459   %%\frametitle{\large Formal Proof of the Substitution Lemma} 

   460 

   461   \small

   462   \begin{tabular}{@ {\hspace{-4mm}}c @ {}}

   463   \begin{minipage}{1.1\textwidth}

   464 *}

   465 

   466 lemma forget: 

   467   assumes a: "x \<sharp> L"

   468   shows "L[x::=P] = L"

   469 using a by (nominal_induct L avoiding: x P rule: lam.strong_induct)

   470                 (auto simp add: abs_fresh fresh_atm)

   471 

   472 lemma fresh_fact: 

   473   fixes z::"name"

   474   assumes a: "z \<sharp> N" "z \<sharp> L"

   475   shows "z \<sharp> N[y::=L]"

   476 using a by (nominal_induct N avoiding: z y L rule: lam.strong_induct)

   477                 (auto simp add: abs_fresh fresh_atm)

   478 

   479 lemma substitution_lemma:  

   480   assumes a: "x \<noteq> y" "x \<sharp> L" -- {* \mbox{}\hspace{-2mm}\tikz[remember picture] \node (n1) {}; *}

   481   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   482 using a 

   483 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

   484      (auto simp add: fresh_fact forget)

   485 

   486 text_raw {*

   487   \end{minipage}

   488   \end{tabular}

   489 

   490   \begin{textblock}{6}(11,9)

   491   \only<2>{

   492   \begin{tikzpicture}[remember picture, overlay]

   493   \draw (0,0) node[fill=cream, text width=5.5cm, thick, draw=red, rounded corners=1mm] (n2)

   494   {\setlength\leftmargini{6mm}%

   495    \begin{itemize}

   496    \item stands for \smath{x\not\in \text{fv}(L)}\\[-2mm]

   497    \item reads as ``\smath{x} fresh for \smath{L}'' 

   498    \end{itemize}

   499   };

   500   

   501   \path[overlay, ->, very thick, red] (n2) edge[out=-90, in=0] (n1);

   502   \end{tikzpicture}}

   503   \end{textblock}

   504 

   505   \only<1-3>{}

   506   \end{frame}}

   507   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   508 

   509 *}

   510 

   511 text_raw {*

   512 

   513   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   514   \mode<presentation>{

   515   \begin{frame}

   516   \frametitle{\LARGE (Weak) Induction Principles} 

   517 

   518   \begin{itemize}

   519   \item The usual induction principle for lambda-terms is as follows:

   520 

   521   \begin{center}

   522   \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}

   523   \centering\smath{%

   524   \infer{P\,t}

   525   {\begin{array}{l}

   526   \forall x.\;P\,x\\[2mm]

   527   \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]

   528   \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\

   529   \end{array}

   530   }}

   531   \end{beamercolorbox}

   532   \end{center}

   533 

   534   \item It requires us in the lambda-case to show the property \smath{P} for

   535   all binders \smath{x}.\smallskip\\ 

   536 

   537   (This nearly always requires renamings and they can be 

   538   tricky to automate.)

   539   \end{itemize}

   540 

   541   \end{frame}}

   542   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   543 

   544 *}

   545 

   546 

   547 text_raw {*

   548 

   549   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   550   \mode<presentation>{

   551   \begin{frame}

   552   \frametitle{\LARGE Strong Induction Principles} 

   553 

   554   \begin{itemize}

   555   \item Therefore we will use the following strong induction principle:

   556 

   557   \begin{center}

   558   \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}

   559   \centering\smath{%

   560   \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%

   561          \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%

   562          \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}

   563   {\begin{array}{l}

   564   \forall x\,c.\;P\,c\;x\\[2mm]

   565   \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)

   566   \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]

   567   \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 

   568   \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)

   569   \end{array}

   570   }}

   571   \end{beamercolorbox}

   572   \end{center}

   573   \end{itemize}

   574 

   575   \begin{textblock}{11}(0.9,10.9)

   576   \only<2>{

   577   \begin{tikzpicture}[remember picture]

   578   \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)

   579   { The variable over which the induction proceeds:\\[2mm]

   580     \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};

   581 

   582   \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);

   583   \end{tikzpicture}}

   584 

   585   \only<3>{

   586   \begin{tikzpicture}[remember picture]

   587   \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)

   588   {The {\bf context} of the induction; i.e.~what the binder should be fresh for

   589    $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]

   590    ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 

   591      and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};

   592 

   593   \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);

   594   \end{tikzpicture}}

   595 

   596   \only<4>{

   597   \begin{tikzpicture}[remember picture]

   598   \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)

   599   {The property to be proved by induction:\\[-3mm]

   600   \begin{center}\small

   601   \begin{tabular}{l}

   602   \smath{\!\!\lambda

   603   (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]

   604   \hspace{8mm}

   605   \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  

   606   \end{tabular}

   607   \end{center}};

   608 

   609   \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);

   610   \end{tikzpicture}}

   611   \end{textblock}

   612 

   613   \end{frame}}

   614   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   615 

   616 *}

   617 

   618 

   619 text_raw {*

   620 

   621   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   622   \mode<presentation>{

   623   \begin{frame}

   624   \frametitle{\LARGE Strong Induction Principles} 

   625 

   626    \begin{center}

   627   \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}

   628   \centering\smath{%

   629   \infer{P\,\alert{c}\;t}

   630   {\begin{array}{l}

   631   \forall x\,c.\;P\,c\;x\\[2mm]

   632   \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)

   633   \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]

   634   \forall x\,t\,c.\;x\fresh c \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)

   635   \end{array}

   636   }}

   637   \end{beamercolorbox}

   638   \end{center}

   639  

   640 

   641   \only<1>{

   642   \begin{textblock}{14}(1.2,9.2)

   643   \begin{itemize}

   644   \item There is a condition for when Barendregt's variable convention

   645     is applicable---it is almost always satisfied, but not always:\\[2mm]

   646     

   647     The induction context \smath{c} needs to be finitely supported 

   648     (is not allowed to mention all names as free).

   649   \end{itemize}

   650   \end{textblock}}

   651 

   652   \only<2>{

   653   \begin{itemize}

   654   \item In the case of the substitution lemma:\\[2mm]

   655 

   656   \begin{textblock}{16.5}(0.7,11.5)

   657   \small

   658 *}

   659 

   660 (*<*)

   661 lemma 

   662   assumes a: "x\<noteq>y" "x \<sharp> L"

   663   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   664 using a

   665 (*>*)

   666 proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

   667 txt_raw {* \isanewline$\ldots$ *}

   668 (*<*)oops(*>*)

   669 

   670 text_raw {*

   671   \end{textblock}

   672   \end{itemize}}

   673 

   674   \end{frame}}

   675   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   676 

   677 *}

   678 

   679 

   680 text_raw {*

   681 

   682   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   683   \mode<presentation>{

   684   \begin{frame}

   685   \frametitle{\Large \mbox{Same Problem with Rule Inductions}} 

   686 

   687   \begin{itemize}

   688   \item We can specify typing-rules for lambda-terms as:

   689 

   690   \begin{center}

   691   \begin{tabular}{@ {\hspace{-6mm}}c@ {}}

   692   \colorbox{cream}{

   693   \smath{\infer{\Gamma\vdash x:\tau}{(x\!:\!\tau)\in\Gamma\;\;\text{valid}\;\Gamma}}}

   694   \;\;

   695   \colorbox{cream}{

   696   \smath{\infer{\Gamma\vdash t_1\;t_2:\tau}

   697         {\Gamma\vdash t_1:\sigma\!\rightarrow\!\tau & \Gamma\vdash t_2:\sigma}}}\\[4mm]

   698 

   699   \colorbox{cream}{

   700   \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}

   701         {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}\\[6mm]

   702 

   703   \colorbox{cream}{

   704   \smath{\infer{\text{valid}\;[]}{}}}

   705   \;\;\;\;

   706   \colorbox{cream}{

   707   \smath{\infer{\text{valid}\;(x\!:\!\tau)\!::\!\Gamma}{x\fresh\Gamma & \text{valid}\;\Gamma}}}\\[8mm]

   708   \end{tabular}

   709   \end{center}

   710 

   711   \item If \smath{\Gamma_1\vdash t:\tau} and \smath{\text{valid}\;\Gamma_2},

   712   \smath{\Gamma_1\subseteq \Gamma_2} then \smath{\Gamma_2\vdash t:\tau}.$\!\!\!\!\!$

   713 

   714   \end{itemize}

   715 

   716   

   717   \begin{textblock}{11}(1.3,4)

   718   \only<2>{

   719   \begin{tikzpicture}

   720   \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (nn)

   721   {The proof of the weakening lemma is said to be trivial / obvious / routine 

   722    /\ldots{} in many places.\\[2mm] 

   723           

   724   (I am actually still looking for a place in the literature where a

   725   trivial / obvious / routine /\ldots{} proof is spelled out --- I know of

   726   proofs by Gallier, McKinna \& Pollack and Pitts, but I would not

   727   call them trivial / obvious / routine /\ldots)};

   728   \end{tikzpicture}}

   729   \end{textblock}

   730 

   731   \end{frame}}

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

   733 *}

   734 

   735 text_raw {*

   736 

   737   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   738   \mode<presentation>{

   739   \begin{frame}[c]

   740   \frametitle{Recall: Rule Inductions} 

   741 

   742   \begin{center}\large

   743   \colorbox{cream}{

   744   \smath{\infer[\text{rule}]{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}}

   745   \end{center}\bigskip

   746 

   747   \begin{tabular}[t]{l}

   748   Rule Inductions:\\[1mm]

   749   \begin{tabular}{l@ {\hspace{2mm}}p{8.4cm}}

   750   1.) & Assume the property for the premises. Assume the side-conditions.\\[1mm]

   751   2.) & Show the property for the conclusion.\\

   752   \end{tabular}

   753   \end{tabular}

   754 

   755   \end{frame}}

   756   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   757 

   758 *}

   759 

   760 text_raw {*

   761 

   762   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   763   \mode<presentation>{

   764   \begin{frame}

   765   \frametitle{\LARGE\mbox{Induction Principle for Typing}} 

   766 

   767   \begin{itemize}

   768   \item The induction principle that comes with the typing definition is as follows:\\[-13mm]

   769   \mbox{}

   770   \end{itemize}

   771 

   772   \begin{center}

   773   \begin{tabular}{@ {\hspace{-5mm}}c@ {}}

   774   \colorbox{cream}{

   775   \smath{

   776   \infer{\Gamma\vdash t:\tau \Rightarrow P\,\Gamma\,t\,\tau}

   777   {\begin{array}{l}

   778       \forall \Gamma\,x\,\tau.\,\;(x\!:\!\tau)\in\Gamma\wedge

   779          \text{valid}\,\Gamma\Rightarrow P\,\Gamma\,(x)\,\tau\\[4mm]

   780       \forall \Gamma\,t_1\,t_2\,\sigma\,\tau.\\

   781       P\,\Gamma\,t_1\,(\sigma\!\rightarrow\!\tau)\wedge

   782       P\,\Gamma\,t_2\,\sigma

   783       \Rightarrow P\,\Gamma\,(t_1\,t_2)\,\tau\\[4mm]

   784       \forall \Gamma\,x\,t\,\sigma\,\tau.\\

   785       x\fresh\Gamma\wedge

   786       P\,((x\!:\!\sigma)\!::\!\Gamma)\,t\,\tau

   787       \Rightarrow P\,\Gamma (\lambda x.t)\,(\sigma\!\rightarrow\!\tau)\\[2mm]

   788    \end{array}

   789   }

   790   }}

   791   \end{tabular}

   792   \end{center}

   793 

   794   \begin{textblock}{4}(9,13.8)

   795   \begin{tikzpicture}

   796   \draw (0,0) node[fill=cream, text width=3.9cm, thick, draw=red, rounded corners=1mm] (nn)

   797   {\small Note the quantifiers!};

   798   \end{tikzpicture}

   799   \end{textblock}

   800 

   801   \end{frame}}

   802   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   803 

   804 *}

   805 

   806 text_raw {*

   807 

   808   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   809   \mode<presentation>{

   810   \begin{frame}

   811   \frametitle{\LARGE \mbox{Proof of Weakening Lemma}} 

   812   \mbox{}\\[-18mm]\mbox{}

   813 

   814   \begin{center}

   815   \colorbox{cream}{

   816   \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}

   817         {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}

   818   \end{center}

   819 

   820   \begin{minipage}{1.1\textwidth}

   821   \begin{itemize}

   822   \item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then 

   823   \smath{\alert<1>{\forall \Gamma_2}.\,\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!

   824   \Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}

   825   \end{itemize}

   826 

   827   \pause

   828 

   829   \mbox{}\hspace{-5mm}

   830   \underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:

   831   

   832   \begin{itemize}

   833   \item We know:\\

   834   \smath{\forall \alert<4->{\Gamma_2}.\,\text{valid}\,\alert<4->{\Gamma_2} \wedge 

   835     (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \alert<4->{\Gamma_2} \Rightarrow \!\!

   836     \tikz[remember picture, baseline=(ea.base)] 

   837          \node (ea) {\smath{\alert<4->{\Gamma_2}}};\!\vdash\! t\!:\!\tau}\\

   838   \smath{x\fresh\Gamma_1}\\

   839   \onslide<3->{\smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2

   840                       \only<6->{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\!

   841                                             (x\!:\!\sigma)\!::\!\Gamma_2}}}\\

   842   \onslide<3->{\smath{\textcolor{white}{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2

   843           \Rightarrow} \only<7->{\;\alert{\text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2\;\;\text{\bf ???}}}}}

   844 

   845   \item We have to show:\\

   846   \only<2>{

   847   \smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge 

   848   \Gamma_1\!\subseteq\!\Gamma_2 \Rightarrow \Gamma_2\!\vdash\! 

   849   \lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}

   850   \only<3->{

   851   \smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}}

   852 

   853   \end{itemize}

   854   \end{minipage}

   855 

   856   \begin{textblock}{4}(10,6.5)

   857   \only<5->{

   858   \begin{tikzpicture}[remember picture]

   859   \draw (0,0) node[fill=cream, text width=4cm, thick, draw=red, rounded corners=1mm] (eb)

   860   {\smath{\Gamma_2\mapsto (x\!:\!\sigma)\!::\!\Gamma_2}};

   861   

   862   \path[overlay, ->, ultra thick, red] (eb) edge[out=-90, in=80] (ea);

   863   \end{tikzpicture}}

   864   \end{textblock}

   865 

   866   \end{frame}}

   867   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   868 

   869 *}

   870 

   871 text_raw {*

   872 

   873   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   874   \mode<presentation>{

   875   \begin{frame}

   876 

   877   \begin{textblock}{14.8}(0.7,0.5)

   878   \begin{itemize}

   879   \item The usual proof of strong normalisation for simply- typed lambda-terms 

   880   establishes first:\\[1mm]

   881 

   882   \colorbox{cream}{%

   883   \begin{tabular}{@ {}p{11cm}}

   884   Lemma: If for all reducible \smath{s}, \smath{t[x\!:=\!s]} is reducible, then

   885   \smath{\lambda x.t} is reducible.

   886   \end{tabular}}\smallskip

   887 

   888   \item Then one shows for a closing (simultaneous) substitution:\\[2mm]

   889 

   890   \colorbox{cream}{%

   891   \begin{tabular}{@ {}p{11cm}}

   892   Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing

   893   substitutions \smath{\theta} containing reducible terms only, 

   894   \smath{\theta(t)} is reducible.

   895   \end{tabular}}

   896 

   897   \mbox{}\\[1mm]

   898 

   899   Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)}

   900   is reducible with \smath{s} being reducible. This is equal\alert{$^*$} to

   901   \smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get \smath{\lambda

   902   x.(\theta(t))} is reducible. Because this is equal\alert{$^*$} to

   903   \smath{\theta(\lambda x.t)}, we are done.

   904   \hfill\footnotesize\alert{$^*$}you have to take a deep breath

   905   \end{itemize}

   906   \end{textblock}

   907 

   908   \end{frame}}

   909   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   910 

   911 *}

   912 

   913 

   914 text_raw {*

   915 

   916   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   917   \mode<presentation>{

   918   \begin{frame}

   919   \frametitle{\LARGE \mbox{Proof of Weakening Lemma}} 

   920   \mbox{}\\[-18mm]\mbox{}

   921 

   922   \begin{center}

   923   \colorbox{cream}{

   924   \smath{\infer{\Gamma\vdash \lambda x.t:\sigma\!\rightarrow\!\tau}

   925         {x\fresh \Gamma & (x\!:\!\sigma)\!::\!\Gamma\vdash t:\tau}}}

   926   \end{center}

   927 

   928   \begin{minipage}{1.1\textwidth}

   929   \begin{itemize}

   930   \item If \smath{\Gamma_1\!\vdash\! t\!:\!\tau} then 

   931   \smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!

   932   \Gamma_2\!\Rightarrow\! \Gamma_2\!\vdash\! t\!:\!\tau}

   933   \end{itemize}

   934 

   935   \mbox{}\hspace{-5mm}

   936   \underline{For all \smath{\Gamma_1}, \smath{x}, \smath{t}, \smath{\sigma} and \smath{\tau}}:

   937   

   938   \begin{itemize}

   939   \item We know:\\

   940   \smath{\forall \Gamma_2.\,\text{valid}\,\Gamma_2 \wedge 

   941     (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! \Gamma_2 \Rightarrow \!\!

   942     \Gamma_2\!\vdash\! t\!:\!\tau}\\

   943   \smath{x\fresh\Gamma_1}\\

   944   \begin{tabular}{@ {}ll@ {}}

   945   \smath{\text{valid}\,\Gamma_2 \wedge \Gamma_1\!\subseteq\!\Gamma_2} &

   946   \only<2->{\smath{\alert{\Rightarrow (x\!:\!\sigma)\!::\!\Gamma_1\!\subseteq\! 

   947                            (x\!:\!\sigma)\!::\!\Gamma_2}}}\\

   948   \smath{\alert{x\fresh\Gamma_2}} & 

   949   \only<2->{\smath{\alert{\Rightarrow \text{valid}\,(x\!:\!\sigma)\!::\!\Gamma_2}}}

   950   \end{tabular}

   951 

   952   \item We have to show:\\

   953   \smath{\Gamma_2\!\vdash\!\lambda x.t\!:\!\sigma\!\rightarrow\!\tau}

   954 

   955   \end{itemize}

   956   \end{minipage}

   957 

   958 

   959   \end{frame}}

   960   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   961 

   962 *}

   963 

   964 

   965 

   966 text_raw {*

   967 

   968   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   969   \mode<presentation>{

   970   \begin{frame}

   971   \frametitle{SN (Again)} 

   972   \mbox{}\\[-8mm]

   973 

   974   \colorbox{cream}{%

   975   \begin{tabular}{@ {}p{10.5cm}}

   976   Theorem: If \smath{\Gamma\vdash t:\tau}, then for all closing

   977   substitutions \smath{\theta} containing reducible terms only, 

   978   \smath{\theta(t)} is reducible.

   979   \end{tabular}}\medskip

   980 

   981   \begin{itemize}

   982   \item

   983   Since we say that the strong induction should avoid \smath{\theta}, we

   984   get the assumption \alert{$x\fresh\theta$} then:\\[2mm]

   985   

   986   \begin{tabular}{@ {}p{10.5cm}}\raggedright

   987   Lambda-Case: By ind.~we know \smath{(x\!\mapsto\! s\cup\theta)(t)} is reducible 

   988   with

   989   \smath{s} being reducible. This is {\bf equal} to

   990   \smath{(\theta(t))[x\!:=\!s]}. Therefore, we can apply the lemma and get

   991   \smath{\lambda x.(\theta(t))} is reducible. Because this is {\bf equal} to

   992   \smath{\theta(\lambda x.t)}, we are done.

   993   \end{tabular}\smallskip

   994 

   995   \begin{center}

   996   \begin{tabular}{rl}

   997   \smath{x\fresh\theta\Rightarrow} & 

   998   \smath{(x\!\mapsto\! s\cup\theta)(t) \;\alert{=}\;(\theta(t))[x\!:=\!s]}\\[1mm]

   999   &

  1000   \smath{\theta(\lambda x.t) \;\alert{=}\; \lambda x.(\theta(t))}

  1001   \end{tabular}

  1002   \end{center}

  1003   \end{itemize}

  1004 

  1005   \end{frame}}

  1006   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1007 

  1008 *}

  1009 

  1010 text_raw {*

  1011 

  1012   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1013   \mode<presentation>{

  1014   \begin{frame}

  1015   \frametitle{So Far So Good}

  1016 

  1017   \begin{itemize}

  1018   \item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}

  1019   \end{itemize}

  1020 

  1021   \begin{center}

  1022   \begin{block}{}

  1023   \color{gray}

  1024   \small%

  1025   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 

  1026   If $M_1,\ldots,M_n$ occur in a certain mathematical context

  1027   (e.g. definition, proof), then in these terms all bound variables 

  1028   are chosen to be different from the free variables.\\[2mm]

  1029   

  1030   \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''

  1031   \end{block}

  1032   \end{center}

  1033 

  1034   \mbox{}\\[-18mm]\mbox{}

  1035 

  1036   \begin{columns}

  1037   \begin{column}[t]{4.7cm}

  1038   Inductive Definitions:\\

  1039   \begin{center}

  1040   \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}

  1041   \end{center}

  1042   \end{column}

  1043   \begin{column}[t]{7cm}

  1044   Rule Inductions:\\[2mm]

  1045   \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}

  1046   1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]

  1047   2.) & Show the property for\\ & the conclusion.\\

  1048   \end{tabular}

  1049   \end{column}

  1050   \end{columns}

  1051 

  1052   \end{frame}}

  1053   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1054 

  1055 *}

  1056 

  1057 text_raw {*

  1058 

  1059   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1060   \mode<presentation>{

  1061   \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}

  1062   \begin{frame}[sqeeze]

  1063   \frametitle{Faulty Reasoning} 

  1064 

  1065   %\mbox{}

  1066 

  1067   \begin{itemize}

  1068   \item Consider the two-place relation \smath{\text{foo}}:\medskip

  1069   \begin{center}

  1070   \begin{tabular}{ccc}

  1071   \raisebox{2.5mm}{\colorbox{cream}{%

  1072   \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}

  1073   &

  1074   \raisebox{2mm}{\colorbox{cream}{%

  1075   \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}

  1076   &

  1077   \colorbox{cream}{%

  1078   \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]

  1079   \end{tabular}

  1080   \end{center}

  1081 

  1082   \pause

  1083 

  1084   \item The lemma we going to prove:\smallskip

  1085   \begin{center}

  1086   Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.

  1087   \end{center}\bigskip

  1088 

  1089   \only<3>{

  1090   \item Cases 1 and 2 are trivial:\medskip

  1091   \begin{itemize}

  1092   \item If \smath{y\fresh x} then \smath{y\fresh x}.

  1093   \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.

  1094   \end{itemize}

  1095   }

  1096 

  1097   \only<4->{

  1098   \item Case 3:

  1099   \begin{itemize}

  1100   \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; 

  1101   We have to show \smath{y\fresh t'}.$\!\!\!\!$ 

  1102   \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.

  1103   \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!

  1104   \end{itemize}

  1105   }

  1106   \end{itemize}

  1107   

  1108   \begin{textblock}{11.3}(0.7,0.6)

  1109   \only<5-7>{

  1110   \begin{tikzpicture}

  1111   \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)

  1112   {{\bf Variable Convention:}\\[2mm] 

  1113   \small

  1114    If $M_1,\ldots,M_n$ occur in a certain mathematical context

  1115    (e.g. definition, proof), then in these terms all bound variables 

  1116    are chosen to be different from the free variables.\smallskip

  1117 

  1118   \normalsize

  1119    {\bf In our case:}\\[2mm]

  1120    The free variables are \smath{y} and \smath{t'}; the bound one is 

  1121    \smath{x}.\medskip

  1122           

  1123    By the variable convention we conclude that \smath{x\not= y}.

  1124   };

  1125   \end{tikzpicture}}

  1126   \end{textblock}

  1127 

  1128   \begin{textblock}{9.2}(3.6,9)

  1129   \only<6,7>{

  1130   \begin{tikzpicture}[remember picture]

  1131   \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)

  1132   {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow

  1133           y\!\not\in\! \text{fv}(t)\!-\!\{x\}

  1134           \stackrel{x\not=y}{\Longleftrightarrow}

  1135           y\!\not\in\! \text{fv}(t)}};