
diff -r 0865caafbfe6 -r 3890483c674f Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Jan 03 16:21:12 2011 +0000
+++ b/Paper/Paper.thy	Tue Jan 04 13:47:38 2011 +0000
@@ -23,7 +23,7 @@
   If  ("if _ then _ else _" 10) and
   alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
-  alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fa'(_')" [100] 100) and
@@ -32,7 +32,7 @@
   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
-  Abs_res ("[_]\<^bsub>res\<^esub>._") and
+  Abs_res ("[_]\<^bsub>set+\<^esub>._") and
   Abs_print ("_\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
   supp_set ("aux _" [1000] 10) and
@@ -104,7 +104,7 @@
   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"}\hspace{10mm}
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}
   \end{equation}
   %
@@ -138,7 +138,7 @@
   \eqref{one} as $\alpha$-equivalent with
   %
   \begin{center}
-  @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
+  @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
   \end{center}
   %
   \noindent
@@ -318,7 +318,7 @@
   The problem with introducing a new type in Isabelle/HOL is that in order to
   be useful, a reasoning infrastructure needs to be ``lifted'' from the
   underlying subset to the new type. This is usually a tricky and arduous
-  task. To ease it, we re-implemented in Isabelle/HOL the quotient package
+  task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package
   described by Homeier \cite{Homeier05} for the HOL4 system. This package
   allows us to lift definitions and theorems involving raw terms to
   definitions and theorems involving $\alpha$-equated terms. For example if we
@@ -729,12 +729,12 @@
   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
+  $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to
   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
   since there is no permutation that makes the lists @{text "[x, y]"} and
   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
-  unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
+  unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{set+}}$
   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
@@ -751,13 +751,13 @@
   \end{equation}
   
   \noindent
-  (similarly for $\approx_{\,\textit{abs\_res}}$ 
+  (similarly for $\approx_{\,\textit{abs\_set+}}$ 
   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
   relations. %% and equivariant.
 
   \begin{lemma}\label{alphaeq} 
   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
-  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if 
+  and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 
   %@{term "abs_set (as, x) (bs, y)"} then also 
   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
   \end{lemma}
@@ -772,7 +772,7 @@
 
   \noindent
   This lemma allows us to use our quotient package for introducing 
-  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+  new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
   representing $\alpha$-equivalence classes of pairs of type 
   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
   (in the third case). 
@@ -797,8 +797,8 @@
   \begin{tabular}{l}
   @{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]}
+  @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$
+  @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}
   \end{tabular}
   \end{center}
   \end{theorem}
@@ -950,9 +950,9 @@
   %
   \begin{center}
   \begin{tabular}{@ {}l@ {}}
-  \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\;
-  \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\;
-  \isacommand{bind (res)} {\it binders} \isacommand{in} {\it bodies}
+  \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
+  \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\,
+  \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies}
   \end{tabular}
   \end{center}
   %
@@ -981,7 +981,7 @@
   \noindent
   %Similarly for the other binding modes. 
   %Interestingly, in case of \isacommand{bind (set)}
-  %and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics
+  %and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics
   %of the specifications (the corresponding $\alpha$-equivalence will differ). We will 
   %show this later with an example.
   
@@ -998,7 +998,7 @@
   For binders we distinguish between
   \emph{shallow} and \emph{deep} binders.  Shallow binders are just
   labels. The restriction we need to impose on them is that in case of
-  \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
+  \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either
   refer to atom types or to sets of atom types; in case of \isacommand{bind}
   the labels must refer to atom types or lists of atom types. Two examples for
   the use of shallow binders are the specification of lambda-terms, where a
@@ -1018,7 +1018,7 @@
   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~%
-  \isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
+  \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -1037,7 +1037,7 @@
   other arguments and also in the same argument (we will call such binders
   \emph{recursive}, see below). The binding functions are
   expected to return either a set of atoms (for \isacommand{bind (set)} and
-  \isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can
+  \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can
   be defined by recursion over the corresponding type; the equations
   must be given in the binding function part of the scheme shown in
   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
@@ -1487,7 +1487,7 @@
   \noindent
   In this case we define a premise @{text P} using the relation
   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
-  $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
+  $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other
   binding modes). This premise defines $\alpha$-equivalence of two abstractions
   involving multiple binders. As above, we first build the tuples @{text "D"} and
   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
@@ -1641,7 +1641,7 @@
   \begin{proof} 
   The proof is by mutual induction over the definitions. The non-trivial
   cases involve premises built up by $\approx_{\textit{set}}$, 
-  $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They 
+  $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 
   can be dealt with as in Lemma~\ref{alphaeq}.
   \end{proof}
 
@@ -1761,7 +1761,7 @@
 
   Finally we can add to our infrastructure a cases lemma (explained in the next section)
   and a structural induction principle 
-  for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
+  for the types @{text "ty\<AL>"}$_{1..n}$. The conclusion of the induction principle is
   of the form
   %
   %\begin{equation}\label{weakinduct}
@@ -1794,7 +1794,7 @@
   \end{center}
   %
   \noindent
-  These properties can be established using the induction principle.
+  These properties can be established using the induction principle for the types @{text "ty\<AL>"}$_{1..n}$.
   %%in \eqref{weakinduct}.
   Having these equivariant properties established, we can
   show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
@@ -1954,7 +1954,7 @@
   %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} 
+  a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} 
   this lemma is of the form
   %
   \begin{equation}\label{weakcases}
@@ -1974,7 +1974,7 @@
   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
   in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 
   \emph{all} @{text Let}-terms. 
-  What we need instead is a cases rule where we only have to consider terms that have 
+  What we need instead is a cases lemma where we only have to consider terms that have 
   binders that are fresh w.r.t.~a context @{text "c"}. This gives the implications
   %
   \begin{center}
@@ -2257,7 +2257,7 @@
   binding clauses. In Ott you specify binding clauses with a single body; we 
   allow more than one. We have to do this, because this makes a difference 
   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 
-  \isacommand{bind (res)}. 
+  \isacommand{bind (set+)}. 
   %
   %Consider the examples
   %
@@ -2312,7 +2312,7 @@
   
   In a slightly different domain (programming with dependent types), the 
   paper \cite{Altenkirch10} presents a calculus with a notion of 
-  $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
+  $\alpha$-equivalence related to our binding mode \isacommand{bind (set+)}.
   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
   has a more operational flavour and calculates a partial (renaming) map. 
   In this way, the definition can deal with vacuous binders. However, to our
@@ -2330,7 +2330,7 @@
   To specify general binders we used the specifications from Ott, but extended them 
   in some places and restricted
   them in others so that they make sense in the context of $\alpha$-equated terms. 
-  We also introduced two binding modes (set and res) that do not 
+  We also introduced two binding modes (set and set+) that do not 
   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 




