# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269358126 -3600
# Node ID b37e8e85d0973326f7acc361b3cc7b764e37a9cf
# Parent  0ea578c6dae3d00545b71766fe722bd32fa3f3a1# Parent  b7e19f16bcd04fa7b6771630f606868e387340c7
merge

diff -r 0ea578c6dae3 -r b37e8e85d097 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 23 16:28:29 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 16:28:46 2010 +0100
@@ -522,28 +522,84 @@
 section {* Alpha-Equivalence and Free Variables *}
 
 text {*
-  A specification of a term-calculus in Nominal Isabelle is a collection
-  of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ 
+  The syntax of a specification for a term-calculus in Nominal Isabelle is
+  heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a
+  collection of (possibly mutual recursive) type declarations, say
+  $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
+  collection of associated binding function declarations, say
+  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically 
   written as follows:
 
   \begin{center}
-  \begin{tabular}{l}
-  \isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\
-  \isacommand{and} $ty_{\alpha{}2} =$\\
+  \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
+  types \mbox{declaration part} &
+  $\begin{cases}
+  \mbox{\begin{tabular}{l}
+  \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
+  \isacommand{and} $ty_{\alpha{}2} = \ldots$\\
   $\ldots$\\ 
-  \isacommand{and} $ty_{\alpha{}}n =$\\ 
+  \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ 
+  \end{tabular}}
+  \end{cases}$\\
+  binding \mbox{functions part} &
+  $\begin{cases}
+  \mbox{\begin{tabular}{l}
+  \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
   $\ldots$\\
-  \isacommand{with}\\
+  \isacommand{where}\\
   $\ldots$\\
+  \end{tabular}}
+  \end{cases}$\\
   \end{tabular}
   \end{center}
 
   \noindent
-  The section below the \isacommand{with} are binding functions, which
-  will be explained below.
+  Each type declaration $ty_{\alpha{}i}$ consists of a collection of 
+  term-constructors, each of which comes with a list of labelled 
+  types that indicate the types of the arguments of the term-constructor,
+  like 
+
+  \begin{center}
+  $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ 
+  \end{center}
   
+  \noindent
+  The labels are optional and can be used in the (possibly empty) list of binding clauses.
+  These clauses indicate the binders and the scope of the binders in a term-constructor. They
+  are of the form
 
+  \begin{center}
+  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label} 
+  \end{center}
 
+  \noindent
+  whereby we distinguish between \emph{shallow} binders and \emph{deep} binders.
+  Shallow binders are just of the form \isacommand{bind}\; {\it label}\; 
+  \isacommand{in}\; {\it another\_label}. The only restriction on shallow binders
+  is that the {\it label} must refer to either a type which is single atom or
+  to a type which is a finite set of atoms. For example the specification of 
+  lambda-terms and type-schemes use them:
+
+  \begin{center}
+  \begin{tabular}{@ {}cc@ {}}
+  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+  \isacommand{nominal\_datatype} {\it lam} =\\
+  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+  \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
+  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
+  \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \end{tabular} &
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{nominal\_datatype} {\it ty} =\\
+  \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
+  \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
+  \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+  \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+
+  \noindent
   A specification of a term-calculus in Nominal Isabell is very similar to 
   the usual datatype definition of Isabelle/HOL: 
 
diff -r 0ea578c6dae3 -r b37e8e85d097 Paper/document/root.bib
--- a/Paper/document/root.bib	Tue Mar 23 16:28:29 2010 +0100
+++ b/Paper/document/root.bib	Tue Mar 23 16:28:46 2010 +0100
@@ -2,7 +2,7 @@
 @Unpublished{Pitts04,
   author = 	 {Andrew Pitts},
   title = 	 {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},
-  note = 	 {bla},
+  note = 	 {Notes for an invited talk given at CTCS},
   year = 	 {2004}
 }