diff -r a6f3e1b08494 -r b6873d123f9b Slides/Slides2.thy
--- 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