
diff -r 90779aefbf1a -r 431cf4e6a7e2 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Dec 08 17:07:08 2010 +0000
+++ b/Paper/Paper.thy	Thu Dec 09 17:10:08 2010 +0000
@@ -99,18 +99,13 @@
   Binding multiple variables has interesting properties that cannot be captured
   easily by iterating single binders. For example in the case of type-schemes we do not
   want to make a distinction about the order of the bound variables. Therefore
-  we would like to regard the following two type-schemes as $\alpha$-equivalent
+  we would like to regard the first pair of type-schemes as $\alpha$-equivalent,
+  but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
+  the second pair should \emph{not} be $\alpha$-equivalent:
   %
   \begin{equation}\label{ex1}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"} 
-  \end{equation}
-  %
-  \noindent
-  but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
-  the following two should \emph{not} be $\alpha$-equivalent
-  %
-  \begin{equation}\label{ex2}
-  @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"}\hspace{10mm}
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
   \end{equation}
   %
   \noindent
@@ -139,7 +134,7 @@
 
   \noindent
   we might not care in which order the assignments @{text "x = 3"} and
-  \mbox{@{text "y = 2"}} are given, but it would be unusual to regard
+  \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard
   \eqref{one} as $\alpha$-equivalent with
   %
   \begin{center}
@@ -382,7 +377,7 @@
   The main improvement over Ott is that we introduce three binding modes
   (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and 
   for free variables of our terms, and also derive a reasoning infrastructure
-  for our specifications inside Isabelle/HOL from ``first principles''.
+  for our specifications from ``first principles''.
 
 
   %\begin{figure}
@@ -440,8 +435,8 @@
   sort-respecting permutations of atoms. We will use the letters @{text "a,
   b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
   permutations. The purpose of atoms is to represent variables, be they bound or free. 
-  The sorts of atoms can be used to represent different kinds of
-  variables, such as the term-, coercion- and type-variables in Core-Haskell.
+  %The sorts of atoms can be used to represent different kinds of
+  %variables, such as the term-, coercion- and type-variables in Core-Haskell.
   It is assumed that there is an infinite supply of atoms for each
   sort. In the interest of brevity, we shall restrict ourselves 
   in what follows to only one sort of atoms.
@@ -731,7 +726,7 @@
   \end{center}
 
   \noindent
-  Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
+  Now recall the examples shown in \eqref{ex1} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
   @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to
@@ -800,9 +795,10 @@
 
   \begin{center}
   \begin{tabular}{l}
-  @{thm (lhs) supp_Abs(1)[no_vars]} $=$
-  @{thm supp_Abs(2)[no_vars]}, and\\
-  @{thm supp_Abs(3)[where bs="as", no_vars]}
+  @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$
+  @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\
+  @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} $\;\;=\;\;$
+  @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
   \end{theorem}
@@ -810,7 +806,7 @@
   \noindent
   This theorem states that the bound names do not appear in the support.
   For brevity we omit the proof and again refer the reader to
-  our formalisation in Isabelle/HOL (or the appendix).
+  our formalisation in Isabelle/HOL.
 
   %\noindent
   %Below we will show the first equation. The others 
@@ -1010,20 +1006,19 @@
   bound:
 
   \begin{center}\small
-  \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}
   \begin{tabular}{@ {}l}
   \isacommand{nominal\_datatype} @{text lam} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
-  \hspace{5mm}$\mid$~@{text "App lam lam"}\\
-  \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
-  \hspace{24mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+  \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
+  \hspace{2mm}$\mid$~@{text "App lam lam"}\\
+  \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
   \end{tabular} &
   \begin{tabular}{@ {}l@ {}}
   \isacommand{nominal\_datatype}~@{text ty} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
-  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
-  \hspace{29mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
+  \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
+  \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -1118,7 +1113,7 @@
   same time, we cannot have more than one binding function for a deep binder. 
   Consequently we exclude specifications such as
   %
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
   @{text "Baz\<^isub>1 p::pat t::trm"} & 
      \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
@@ -1921,13 +1916,13 @@
   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
   the induction hypothesis requires us to establish the implications \eqref{weakprem}.
   The problem with these implications is that in general they are difficult to establish.
-  The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}. 
+  The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 
   %%(for example we cannot assume the variable convention for them).
 
   In \cite{UrbanTasson05} we introduced a method for automatically
   strengthening weak induction principles for terms containing single
   binders. These stronger induction principles allow the user to make additional
-  assumptions about binders. 
+  assumptions about bound atoms. 
   %These additional assumptions amount to a formal
   %version of the informal variable convention for binders. 
   To sketch how this strengthening extends to the case of multiple binders, we use as
@@ -1947,7 +1942,7 @@
 
   In \cite{UrbanTasson05} we showed how the weaker induction principles imply
   the stronger ones. This was done by some quite complicated, nevertheless automated,
-  induction proofs. In this paper we simplify this work by leveraging the automated proof
+  induction proof. In this paper we simplify this work by leveraging the automated proof
   methods from the function package of Isabelle/HOL. 
   The reasoning principle these methods employ is well-founded induction. 
   To use them in our setting, we have to discharge
@@ -1956,8 +1951,8 @@
   every induction step and the other is that we have covered all cases. 
   As measures we use the size functions 
   @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 
-  all well-founded. It is straightforward to establish that these measures decrease 
-  in every induction step.
+  all well-founded. %It is straightforward to establish that these measures decrease 
+  %in every induction step.
   
   What is left to show is that we covered all cases. To do so, we use 
   a cases lemma derived for each type. For the terms in \eqref{letpat} 
@@ -2009,7 +2004,7 @@
   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
   %
   \begin{center}
-  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} \;\; with
+  @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}  with
   $\begin{cases}
   \text{@{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}}\\
   \text{@{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}}\\
@@ -2248,13 +2243,13 @@
   this tool have also put forward (on paper) a definition for
   $\alpha$-equivalence of terms that can be specified in Ott.  This definition is
   rather different from ours, not using any nominal techniques.  To our
-  knowledge there is also no concrete mathematical result concerning this
+  knowledge there is no concrete mathematical result concerning this
   notion of $\alpha$-equivalence.  Also the definition for the 
   notion of free variables
   is work in progress.
 
   Although we were heavily inspired by the syntax of Ott,
-  its definition of $\alpha$-equivalence is unsuitable for our extension of
+  its definition of $\alpha$-equi\-valence is unsuitable for our extension of
   Nominal Isabelle. First, it is far too complicated to be a basis for
   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
   covers cases of binders depending on other binders, which just do not make
@@ -2340,18 +2335,19 @@
   exist in Ott. 
   We have tried out the extension with calculi such as Core-Haskell, type-schemes 
   and approximately a  dozen of other typical examples from programming 
-  language research~\cite{SewellBestiary}. The code
-  will eventually become part of the next Isabelle distribution.\footnote{For the moment
-  it can be downloaded from the Mercurial repository linked at
-  \href{http://isabelle.in.tum.de/nominal/download}
-  {http://isabelle.in.tum.de/nominal/download}.}
+  language research~\cite{SewellBestiary}. 
+  %The code
+  %will eventually become part of the next Isabelle distribution.\footnote{For the moment
+  %it can be downloaded from the Mercurial repository linked at
+  %\href{http://isabelle.in.tum.de/nominal/download}
+  %{http://isabelle.in.tum.de/nominal/download}.}
 
   We have left out a discussion about how functions can be defined over
   $\alpha$-equated terms involving general binders. In earlier versions of Nominal
-  Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We
+  Isabelle this turned out to be a thorny issue.  We
   hope to do better this time by using the function package that has recently
   been implemented in Isabelle/HOL and also by restricting function
-  definitions to equivariant functions (for such functions we can
+  definitions to equivariant functions (for them we can
   provide more automation).
 
   %There are some restrictions we imposed in this paper that we would like to lift in
@@ -2386,7 +2382,7 @@
   %many discussions about Nominal Isabelle. 
   We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
-  also for patiently explaining some of the finer points of the work on the Ott-tool.
+  also for patiently explaining some of the finer points of the Ott-tool.\\[-7mm]    
   %Stephanie Weirich suggested to separate the subgrammars
   %of kinds and types in our Core-Haskell example. \\[-6mm] 
 *}




