--- 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