(*<*)
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
(*>*)