--- a/Slides/Slides2.thy Sat May 12 21:05:59 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,449 +0,0 @@
-(*<*)
-theory Slides2
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
-begin
-
-notation (latex output)
- set ("_") and
- Cons ("_::/_" [66,65] 65)
-
-(*>*)
-
-
-text_raw {*
- \renewcommand{\slidecaption}{Edinburgh, 11.~July 2010}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>[t]
- \frametitle{%
- \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
- \\
- \LARGE Proof Pearl:\\[-0mm]
- \LARGE A New Foundation for\\[-2mm]
- \LARGE Nominal Isabelle\\[12mm]
- \end{tabular}}
- \begin{center}
- Brian Huf\!fman and {\bf Christian Urban}\\[0mm]
- \end{center}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-2>[c]
- \frametitle{Nominal Isabelle}
-
- \begin{itemize}
- \item \ldots is a definitional extension of Isabelle/HOL
- (let-polymorphism and type classes)\medskip
-
- \item \ldots provides a convenient reasoning infrastructure for
- terms involving binders (e.g.~lambda calculus, variable convention)\medskip
-
- \item<2-> \ldots mainly used to find errors in my own
- (published) paper proofs and in those of others \alert{\bf ;o)}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-3>[c]
- \frametitle{Nominal Theory}
-
- \ldots by Pitts; at its core are:\bigskip
-
- \begin{itemize}
- \item sorted atoms and
- \item sort-respecting permutations
- \end{itemize}
-
- \onslide<2->{
- \begin{textblock}{8}(4,11)
- \onslide<3->{$\text{inv\_of\_}\pi \,\act\, ($}\onslide<2->{$\pi \,\act\, x$}%
- \onslide<3->{$) \,=\, x$}
- \end{textblock}}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>[t]
- \frametitle{The ``Old Way''}
-
- \begin{itemize}
- \item sorted atoms\\ \alert{$\quad\mapsto$ separate types}\; (``copies'' of nat)\bigskip
- \item sort-respecting permutations\\ \alert{$\quad\mapsto$ lists of pairs of atoms (list swappings)}
- \onslide<2->{
- \begin{center}
- \begin{tabular}{c@ {\hspace{7mm}}c}
- $\text{[]} \,\act\, c = c$ &
- $\swap{a}{b}\!::\!\pi \,\act\, c =
- \begin{cases}
- b & \text{if}\, \pi\act c = a\\
- a & \text{if}\, \pi\act c = b\\
- \pi\act c & \text{otherwise}
- \end{cases}$
- \end{tabular}
- \end{center}}
- \end{itemize}
-
- \only<3>{
- \begin{textblock}{14}(1,12.5)
- \alert{The big benefit:} the type system takes care of the sort-respecting requirement.
- \end{textblock}}
- \only<4>{
- \begin{textblock}{14}(1,12.5)
- \alert{A small benefit:} permutation composition is \alert{list append}
- and permutation inversion is \alert{list reversal}.
- \end{textblock}
- }
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{Problems}
-
- \begin{itemize}
- \item @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}\bigskip
-
- \item @{text "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-
- \begin{center}
- $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots
- $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$
- \end{center}\bigskip
-
- \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip
-
- \item type-classes
- \onslide<3>{\small\hspace{5mm}can only have \alert{\bf one} type parameter}
- \begin{itemize}
- \item<2-> $\text{[]}\,\act\, x = x$
- \item<2-> $(\pi_1 @ \pi_2) \,\act \, x = \pi_1 \,\act\,(\pi_2 \,\act\, x)$
- \item<2-> if $\pi_1 \sim \pi_2$ then $\pi_1 \,\act\, x = \pi_2 \,\act\, x$
- \item<2-> if $\pi_1$, $\pi_2$ have dif$\!$f.~type, then
- $\pi_1 \act (\pi_2 \act x) = \pi_2 \act (\pi_1 \act x)$
- \end{itemize}
- \end{itemize}
-
- \only<4->{
- \begin{textblock}{9}(3,7)\begin{tikzpicture}
- \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
- {\normalsize\color{darkgray}
- \begin{quote}
- \begin{itemize}
- \item \alert{lots} of ML-code
- \item \alert{not} pretty
- \item \alert{not a {\bf proof pearl}} :o(
- \end{itemize}
- \end{quote}};
- \end{tikzpicture}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{A Better Way}
-*}
-datatype atom = Atom string nat
-
-text_raw {*
- \mbox{}\bigskip
- \begin{itemize}
- \item<2-> permutations are (restricted) bijective functions from @{text "atom \<Rightarrow> atom"}
-
- \begin{itemize}
- \item sort-respecting \hspace{5mm}($\,\forall a.\;\text{sort}(\pi a) = \text{sort}(a)$)
- \item finite domain \hspace{5mm}($\text{finite} \{a.\;\pi a \not= a\}$)
- \end{itemize}\medskip
-
- \item<3-> \alert{What about {\bf swappings}?}
- \small
- \[
- \begin{array}{l@ {\hspace{1mm}}l}
- (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\
- & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\;
- \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\
- & \text{else}\;\only<3>{\raisebox{-5mm}{\textcolor{red}{\huge\bf $?$}}}
- \only<4->{\text{\alert{\bf id}}}
- \end{array}
- \]
- \end{itemize}
-
- \only<2>{
- \begin{textblock}{7}(4,11)
- @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- \end{textblock}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-7>
- \frametitle{A Smoother Nominal Theory}
-
- From there it is essentially plain sailing:\bigskip
-
- \begin{itemize}
- \item<2-> $(a\;b) = (b\;a) \onslide<4->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip
-
- \item<3-> permutations are an instance of Isabelle's\\
- group\_add ($0$, $\pi_1 + \pi_2$, $- \pi$)\bigskip
-
- \item<6-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip
-
- \begin{itemize}
- \item $0\;\act\;x = x$\\
- \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$
- \end{itemize}\medskip
-
- \onslide<7->{\alert{$\;\mapsto\;$}only one type class needed, $\text{finite}(\text{supp}\;x)$,\\
- \hspace{9mm}$\forall \pi. P$}
- \end{itemize}
-
- \only<5>{
- \begin{textblock}{6}(2.5,11)
- \begin{tikzpicture}
- \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
- {\normalsize\color{darkgray}
- \begin{minipage}{8cm}\raggedright
- This is slightly odd, since in general:
- \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center}
- \end{minipage}};
- \end{tikzpicture}
- \end{textblock}}
-
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>[c]
- \frametitle{One Snatch}
-*}
-
-datatype \<iota>atom = \<iota>Atom string nat
-
-
-text_raw {*
- \isanewline\isanewline
- \begin{itemize}
- \item You like to get the advantages of the old way back: you
- \alert{cannot mix} atoms of dif$\!$ferent sort:\bigskip
-
- \small
- e.g.~LF-objects:
- \begin{center}
- $\quad M ::= c \mid x \mid \lambda x\!:\!A. M \mid M_1\;M_2$
- \end{center}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-2>
- \frametitle{Our Solution}
-
-
- \begin{itemize}
- \item \underline{concrete} atoms:
- \end{itemize}
-*}
-(*<*)
-consts sort :: "atom \<Rightarrow> string"
-(*>*)
-
-typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*)
-typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*)
-
-text_raw {*
- \mbox{}\bigskip\bigskip
- \begin{itemize}
- \item they are a ``subtype'' of the generic atom type
- \item there is an overloaded function \alert{\bf atom}, which injects concrete
- atoms into generic ones\medskip
- \begin{center}
- \begin{tabular}{l}
- $\text{atom}(a) \fresh x$\\
- $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$
- \end{tabular}
- \end{center}
- \pause
- One would like to have $a \fresh x$, $\swap{a}{b}$, \ldots
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{Sorts Reloaded}
-*}
-datatype atom\<iota> = Atom\<iota> string nat
-
-text_raw {*
- \isanewline\isanewline
- \pause
- \alert{Problem}: HOL-binders or Church-style lambda-terms
- \begin{center}
- $\lambda x_\alpha.\, x_\alpha\;x_\beta$
- \end{center}
- \pause
- \isanewline\isanewline
-
-\isacommand{datatype} ty = TVar string $\mid$ ty $\rightarrow$ ty\\
-\isacommand{datatype} var = Var name ty\\
-\pause
-$(x \leftrightarrow y) \,\act\, (x_\alpha, x_\beta) = (y_\alpha, y_\beta)$
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-2>
- \frametitle{Non-Working Solution}
-
-Instead of\isanewline\isanewline
-*}
- datatype atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-
-text_raw {*
-\isanewline\isanewline
-have
-\isanewline\isanewline
-*}
-
- datatype 'a atom\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota> 'a nat
-text_raw {*
- \pause
- \isanewline\isanewline
- But then
- \begin{center}
- @{text "_ \<bullet> _ :: \<alpha> perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- \end{center}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-(*<*)
-hide_const sort
-(*>*)
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>
- \frametitle{A Working Solution}
-
-*}
- datatype sort = Sort string "sort list"
- datatype atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
-(*<*)
-consts sort_ty :: "nat \<Rightarrow> sort"
-(*>*)
-text_raw {*
- \pause
- \isanewline
-
- {\small\begin{tabular}{rcl}
- @{text "sort_ty (TVar x)"} & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
- @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\
- \end{tabular}}
- \pause
- \isanewline\isanewline
- \isacommand{typedef} @{text "var = {a :: atom. sort a \<in> range sort_ty}"}
- \pause
- \isanewline\isanewline
- \small
- \begin{minipage}{12cm}
- @{text "Var x \<tau> \<equiv> \<lceil> Atom (sort_ty \<tau>) x \<rceil>"}\isanewline
-
- @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau> = Var y \<tau>"}\\
- @{text "(Var x \<tau> \<leftrightarrow> Var y \<tau>) \<bullet> Var x \<tau>' = Var x \<tau>'"}\\
- \end{minipage}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1-4>[c]
- \frametitle{Conclusion}
- \mbox{}\\[-3mm]
-
- \begin{itemize}
- \item the formalised version of the nominal theory is now much nicer to
- work with (sorts are occasionally explicit, \alert{$\forall \pi. P$})\medskip
-
- \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\medskip
-
- \item the crucial insight: allow sort-disrespecting swappings%
- \onslide<2->{ \ldots just define them as the identity}\\%
- \onslide<3->{ (a referee called this a \alert{``hack''})}\medskip
-
- \item<4-> there will be a hands-on tutorial about Nominal Isabelle at \alert{POPL'11}
- in Austin Texas
- \end{itemize}
-
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}<1>[c]
- \frametitle{
- \begin{tabular}{c}
- \mbox{}\\[23mm]
- \alert{\LARGE Thank you very much}\\
- \alert{\Large Questions?}
- \end{tabular}}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-(*<*)
-end
-(*>*)
\ No newline at end of file