nominal2: comparison Slides/Slides5.thy

equal deleted inserted replaced

-:7cf2d79d8d5e
+:43283267737c
 (*>*)
 text_raw {*
+%% shallow, deep, and recursive binders
+%%
 %%\renewcommand{\slidecaption}{Cambridge, 8.~June 2010}
 %%\renewcommand{\slidecaption}{Uppsala, 3.~March 2011}
 \renewcommand{\slidecaption}{Saarbrücken, 31.~March 2011}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1>[t]
 \frametitle{%
 \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
 \\
-\huge General Bindings and Alpha-Equivalence in Nominal Isabelle\\[-2mm]
+\LARGE General Bindings and\\
-\large Or, Nominal 2\\[-5mm]
+\LARGE Alpha-Equivalence\\
+\LARGE in Nominal Isabelle\\[3mm]
+\Large Or, Nominal Isabelle 2\\[-5mm]
 \end{tabular}}
 \begin{center}
 Christian Urban
 \end{center}
 \begin{center}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1-2>
+\frametitle{New Types in HOL}
+picture
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
 \begin{frame}<1-4>
 \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}
 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
 \hspace{5mm}\phantom{$|$} Var name\\
 \hspace{5mm}$|$ App trm trm\\
 \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm
 & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
-\hspace{5mm}$|$ Let \only<2->{as::}assn \only<2->{t::}trm
+\hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
 & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
-\multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
 \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\
 \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\
 \end{tabular}
 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
 \hspace{5mm}\phantom{$|$} Var name\\
 \hspace{5mm}$|$ App trm trm\\
 \hspace{5mm}$|$ Lam x::name t::trm
 & \isacommand{bind} x \isacommand{in} t\\
-\hspace{5mm}$|$ Let as::assn t::trm
+\hspace{5mm}$|$ Let as::assns t::trm
 & \isacommand{bind} bn(as) \isacommand{in} t\\
-\multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
 \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
 \end{tabular}
 \begin{tabular}{ll}
 \multicolumn{2}{l}{\isacommand{datatype} trm $=$}\\
 \hspace{5mm}\phantom{$|$} Var name\\
 \hspace{5mm}$|$ App trm trm\\
 \hspace{5mm}$|$ Lam name trm\\
-\hspace{5mm}$|$ Let assn trm\\
+\hspace{5mm}$|$ Let assns trm\\
-\multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\[5mm]
+\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\[5mm]
 \multicolumn{2}{l}{\isacommand{function} bn \isacommand{where}}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
 \end{tabular}
 \begin{frame}<1-2>
 \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
 \mbox{}\\[6mm]
 \begin{center}
-Let as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\
+Let as::assns t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t\\
 \end{center}
 \[
 \infer[\text{Let-}\!\approx_\alpha]
 \begin{frame}<1>
 \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}}
 \mbox{}\\[6mm]
 \begin{center}
-LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
+LetRec as::assns t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\
 \end{center}
 \[\mbox{}\hspace{-4mm}
 \infer[\text{LetRec-}\!\approx_\alpha]
 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
 \hspace{5mm}\phantom{$|$} Var name\\
 \hspace{5mm}$|$ App trm trm\\
 \hspace{5mm}$|$ Lam x::name t::trm
 & \isacommand{bind} x \isacommand{in} t\\
-\hspace{5mm}$|$ Let as::assn t::trm
+\hspace{5mm}$|$ Let as::assns t::trm
 & \isacommand{bind} bn(as) \isacommand{in} t\\
-\multicolumn{2}{l}{\isacommand{and} assn $=$}\\
+\multicolumn{2}{l}{\isacommand{and} assns $=$}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
-\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\
+\multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
 \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\
 \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\
 \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\
 \end{tabular}\bigskip\medskip
-we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+we cannot quotient assns: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
 \only<1->{
 \begin{textblock}{8}(0.2,7.3)
 \alert{\begin{tabular}{p{2.6cm}}
-\raggedright\footnotesize{}Should a ``naked'' assn be quotient?
+\raggedright\footnotesize{}Should a ``naked'' assns be quotient?
 \end{tabular}\hspace{-3mm}
 $\begin{cases}
 \mbox{} \\ \mbox{}
 \end{cases}$}
 \end{textblock}}

changeset 2750	43283267737c
parent 2748	6f38e357b337
child 2751	3b8232f56941