nominal2: comparison Slides/Slides1.thy

equal deleted inserted replaced

-:ad03df7e8056
+:25d2cdf7d7e4
 \mode<presentation>{
 \begin{frame}<1>[t]
 \frametitle{%
 \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
 \\
-\huge Nominal 2\\[-2mm]
+\huge Nominal Isabelle 2\\[-2mm]
-\large Or, How to Reason Conveniently with\\[-5mm]
+\large Or, How to Reason Conveniently\\[-5mm]
-\large General Bindings in Isabelle/HOL\\[5mm]
+\large with General Bindings\\[5mm]
 \end{tabular}}
 \begin{center}
 Christian Urban
 \end{center}
 \begin{center}
 vacuous binders \textcolor{gray}{(restriction)}\medskip
 \item the order does not matter, but the cardinality of the binders
 must be the same \textcolor{gray}{(abstraction)}\medskip
-\item the order does matter
+\item the order does matter \textcolor{gray}{(iterated single binders)}
 \end{itemize}
 \onslide<2->{
 \begin{center}
 \isacommand{bind\_res}\hspace{6mm}
 \only<5>{
 \begin{itemize}
 \item we allow multiple ``binders'' and ``bodies''\smallskip
 \begin{center}
-\isacommand{bind} a b c \isacommand{in} x y z
+\begin{tabular}{l}
+\isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\
+\isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\
+\isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots
+\end{tabular}
 \end{center}\bigskip\medskip
-the reason is that with our definitions of $\alpha$-equivalence
+the reason is that with our definition of $\alpha$-equivalence\medskip
 \begin{center}
-\begin{tabular}{rcl}
+\begin{tabular}{l}
-\isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
+\isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\
-\begin{tabular}{@ {}l}
+\hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y
-\isacommand{bind\_res} as \isacommand{in} x,\\
+\end{tabular}
-\isacommand{bind\_res} as \isacommand{in} y
+\end{center}\medskip
-\end{tabular}
-\end{tabular}
-\end{center}\smallskip
 same with \isacommand{bind\_set}
 \end{itemize}}
 \end{itemize}
 \frametitle{\begin{tabular}{c}New Design\end{tabular}}
 \mbox{}\\[4mm]
 \begin{center}
 \begin{tikzpicture}
+{\draw (0,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+(A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
+{\draw (3,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
+(B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
 \alt<2>
-{\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};}
-{\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
-(A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
-\alt<3>
-{\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};}
-{\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
-(B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
-\alt<4>
 {\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
 (C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
-{\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+{\draw (6,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
 (C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
-\alt<5>
+{\draw (0,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-{\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};}
-{\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
 (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
-\alt<6>
+{\draw (3,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-{\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};}
-{\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
 (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
-\alt<7>
+{\draw (6,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
-{\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
-(F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};}
-{\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
 (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
-\draw[->,white!50,line width=1mm] (A) -- (B);
+\draw[->,fg!50,line width=1mm] (A) -- (B);
-\draw[->,white!50,line width=1mm] (B) -- (C);
+\draw[->,fg!50,line width=1mm] (B) -- (C);
-\draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+\draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
 (C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
-\draw[->,white!50,line width=1mm] (D) -- (E);
+\draw[->,fg!50,line width=1mm] (D) -- (E);
-\draw[->,white!50,line width=1mm] (E) -- (F);
+\draw[->,fg!50,line width=1mm] (E) -- (F);
 \end{tikzpicture}
 \end{center}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \mode<presentation>{
-\begin{frame}<1-9>
+\begin{frame}<1-8>
 \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
 \mbox{}\\[-3mm]
 \begin{itemize}
 \item lets first look at pairs\bigskip\medskip
 \begin{tabular}{@ {\hspace{1cm}}l}
-$(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}%
+$(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}%
-\only<8>{${}_{\text{\alert{list}}}$}%
+\only<7>{${}_{\text{\alert{list}}}$}%
-\only<9>{${}_{\text{\alert{res}}}$}}%
+\only<8>{${}_{\text{\alert{res}}}$}}%
 \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
 \end{tabular}\bigskip
 \end{itemize}
 \only<1>{
 \begin{textblock}{8}(3,8.5)
 \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
 \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
-\pgfuseshading{smallspherered} & $x$ is the body\\
+\pgfuseshading{smallspherered} & $x$ is the body (might be a tuple)\\
 \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality
 of the binders has to be the same\\
 \end{tabular}
 \end{textblock}}
 \only<4->{
 \begin{textblock}{12}(5,8)
 \begin{tabular}{ll@ {\hspace{1mm}}l}
 $\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm]
 & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm]
-& \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm]
+& \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x)\;R\;y$}\\[1mm]
-& \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\
+& \onslide<6-7>{$\;\;\;\wedge$} & \onslide<6-7>{$\pi \act as = bs$}\\
 \end{tabular}
 \end{textblock}}
-\only<8>{
+\only<7>{
-\begin{textblock}{8}(3,13.8)
+\begin{textblock}{7}(3,13.8)
 \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 \mbox{}\\[-7mm]\mbox{}
 \footnotesize
 \begin{center}
 \begin{tikzpicture}
-\draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (0,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
-\draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (2,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
-\draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (4,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
-\draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (0,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
-\draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (2,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
-\draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+\draw (4,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
 (F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
-\draw[->,white!50,line width=1mm] (A) -- (B);
+\draw[->,fg!50,line width=1mm] (A) -- (B);
-\draw[->,white!50,line width=1mm] (B) -- (C);
+\draw[->,fg!50,line width=1mm] (B) -- (C);
-\draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+\draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
 (C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
-\draw[->,white!50,line width=1mm] (D) -- (E);
+\draw[->,fg!50,line width=1mm] (D) -- (E);
-\draw[->,white!50,line width=1mm] (E) -- (F);
+\draw[->,fg!50,line width=1mm] (E) -- (F);
 \end{tikzpicture}
 \end{center}
 \begin{itemize}
 \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions
 \begin{frame}<1->
 \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}}
 \mbox{}\\[-6mm]
 \small
-\mbox{}\hspace{10mm}
+\mbox{}\hspace{20mm}
 \begin{tabular}{ll}
 \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
 \hspace{5mm}\phantom{$|$} Var name\\
 \hspace{5mm}$|$ App trm trm\\
 \hspace{5mm}$|$ Lam x::name t::trm
 \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
+\only<1->{
+\begin{textblock}{8}(0.2,7.3)
+\alert{\begin{tabular}{p{2.6cm}}
+\raggedright\footnotesize{}Should a ``naked'' assn be quotient?
+\end{tabular}\hspace{-3mm}
+$\begin{cases}
+\mbox{} \\ \mbox{}
+\end{cases}$}
+\end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
 text_raw {*
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 *}
+text_raw {*
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\begin{frame}<1-2>[c]
+\frametitle{\begin{tabular}{c}Examples\end{tabular}}
+\mbox{}\\[-6mm]
+\begin{center}
+$(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, a \rightarrow b)$
+$(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, b \rightarrow a)$
+\end{center}
+\begin{center}
+$(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\
+\hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$
+\end{center}
+\onslide<2->
+{1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$,
+\isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip
+2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$
+}
+\end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
 (*<*)
 end
 (*>*)

changeset 2313	25d2cdf7d7e4
parent 2311	4da5c5c29009
child 2348	09b476c20fe1