Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Slides/Slides1.thy
changeset 2313 25d2cdf7d7e4
parent 2311 4da5c5c29009
child 2348 09b476c20fe1 
--- a/Slides/Slides1.thy	Mon Jun 07 11:46:26 2010 +0200
+++ b/Slides/Slides1.thy	Wed Jun 09 15:14:16 2010 +0200
@@ -18,9 +18,9 @@
   \frametitle{%
   \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
   \\
-  \huge Nominal 2\\[-2mm] 
-  \large Or, How to Reason Conveniently with\\[-5mm]
-  \large General Bindings in Isabelle/HOL\\[5mm]
+  \huge Nominal Isabelle 2\\[-2mm] 
+  \large Or, How to Reason Conveniently\\[-5mm]
+  \large with General Bindings\\[5mm]
   \end{tabular}}
   \begin{center}
   Christian Urban
@@ -182,7 +182,7 @@
   \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->{
@@ -266,18 +266,19 @@
   \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}
-  \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
-  \begin{tabular}{@ {}l}
-  \isacommand{bind\_res} as \isacommand{in} x,\\
-  \isacommand{bind\_res} as \isacommand{in} y
+  \begin{tabular}{l}
+  \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\ 
+  \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y
   \end{tabular}
-  \end{tabular}
-  \end{center}\smallskip
+  \end{center}\medskip
 
   same with \isacommand{bind\_set}
   \end{itemize}}
@@ -324,48 +325,33 @@
 
   \begin{center}
   \begin{tikzpicture}
-  \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]
+  {\draw (0,0) node[inner sep=3mm, ultra thick, draw=fg, 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]
+  {\draw (3,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
   (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
 
-  \alt<4>
+  \alt<2>
   {\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=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]
+  {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
   (D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
 
-  \alt<6>
-  {\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]
+  {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
   (E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
 
-  \alt<7>
-  {\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]
+  {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
   (F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
   
-  \draw[->,white!50,line width=1mm] (A) -- (B);
-  \draw[->,white!50,line width=1mm] (B) -- (C);
-  \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] 
+  \draw[->,fg!50,line width=1mm] (A) -- (B);
+  \draw[->,fg!50,line width=1mm] (B) -- (C);
+  \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[->,white!50,line width=1mm] (E) -- (F);
+  \draw[->,fg!50,line width=1mm] (D) -- (E);
+  \draw[->,fg!50,line width=1mm] (E) -- (F);
   \end{tikzpicture}
   \end{center}
 
@@ -378,7 +364,7 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1-9>
+  \begin{frame}<1-8>
   \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
   \mbox{}\\[-3mm]
 
@@ -386,9 +372,9 @@
   \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}}$}%
-           \only<8>{${}_{\text{\alert{list}}}$}%
-           \only<9>{${}_{\text{\alert{res}}}$}}%
+  $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}%
+           \only<7>{${}_{\text{\alert{list}}}$}%
+           \only<8>{${}_{\text{\alert{res}}}$}}%
            \onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
   \end{tabular}\bigskip
   \end{itemize}
@@ -397,7 +383,7 @@
   \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}
@@ -408,13 +394,13 @@
   \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<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\
+        & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x)\;R\;y$}\\[1mm]
+        & \onslide<6-7>{$\;\;\;\wedge$} & \onslide<6-7>{$\pi \act as = bs$}\\
   \end{tabular}
   \end{textblock}}
   
-  \only<8>{
-  \begin{textblock}{8}(3,13.8)
+  \only<7>{
+  \begin{textblock}{7}(3,13.8)
   \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names 
   \end{textblock}}
   \end{frame}}
@@ -965,30 +951,30 @@
   \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[->,white!50,line width=1mm] (B) -- (C);
-  \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm] 
+  \draw[->,fg!50,line width=1mm] (A) -- (B);
+  \draw[->,fg!50,line width=1mm] (B) -- (C);
+  \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[->,white!50,line width=1mm] (E) -- (F);
+  \draw[->,fg!50,line width=1mm] (D) -- (E);
+  \draw[->,fg!50,line width=1mm] (E) -- (F);
   \end{tikzpicture}
   \end{center}
 
@@ -1012,7 +998,7 @@
   \mbox{}\\[-6mm]
 
   \small
-  \mbox{}\hspace{10mm}
+  \mbox{}\hspace{20mm}
   \begin{tabular}{ll}
   \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
   \hspace{5mm}\phantom{$|$} Var name\\
@@ -1031,6 +1017,15 @@
 
   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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -1075,6 +1070,34 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+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
 (*>*)
\ No newline at end of file
nominal2