--- a/LMCS-Paper/Paper.thy Sun Aug 28 14:50:13 2011 +0100
+++ b/LMCS-Paper/Paper.thy Tue Sep 06 12:18:02 2011 +0100
@@ -101,7 +101,7 @@
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 first pair of type-schemes as alpha-equivalent,
+ we would like to regard below 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:
@@ -226,9 +226,9 @@
is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
extends Ott in several aspects: one is that we support three binding
modes---Ott has only one, namely the one where the order of binders matters.
- Another is that our reasoning infrastructure, like the notion of support and
- strong induction principles, is derived from first principles within the
- Isabelle/HOL theorem prover.
+ Another is that our reasoning infrastructure, like strong induction principles
+ and the notion of free variables, is derived from first principles within
+ the Isabelle/HOL theorem prover.
However, we will not be able to cope with all specifications that are
allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
@@ -331,7 +331,7 @@
\noindent
then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
- operating on quotients, or alpha-equivalence classes of lambda-terms. This
+ operating on quotients, that is alpha-equivalence classes of lambda-terms. This
lifted function is characterised by the equations
\[
@@ -361,8 +361,8 @@
Figure~\ref{corehas}). This term language involves patterns that have lists
of type-, coercion- and term-variables, all of which are bound in @{text
"\<CASE>"}-expressions. In these patterns we do not know in advance how many
- variables need to be bound. Another example is the specification of SML,
- which includes includes bindings as in type-schemes.\medskip
+ variables need to be bound. Another example is the algorithm W
+ which includes multiple binders in type-schemes.\medskip
\noindent
{\bf Contributions:} We provide three new definitions for when terms
@@ -432,7 +432,7 @@
Two central notions in the nominal logic work are sorted atoms and
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
+ b, c, \<dots>"} to stand for atoms and @{text "\<pi>, \<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.
@@ -447,8 +447,8 @@
where the generic type @{text "\<beta>"} is the type of the object
over which the permutation
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
- the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
- and the inverse permutation of @{term p} as @{text "- p"}. The permutation
+ the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}},
+ and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
operation is defined over the type-hierarchy \cite{HuffmanUrban10};
for example permutations acting on products, lists, sets, functions and booleans are
given by:
@@ -456,43 +456,26 @@
\begin{equation}\label{permute}
\mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
\begin{tabular}{@ {}l@ {}}
- @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
- @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
- @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
+ @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\[2mm]
+ @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
- @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
- @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
- @{thm permute_bool_def[no_vars, THEN eq_reflection]}
+ @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f (- \<pi> \<bullet> x))"}\\
+ @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}
\end{tabular}
\end{tabular}}
- \end{equation}
+ \end{equation}\smallskip
- \begin{center}
- \mbox{\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {\hspace{4mm}}c@ {}}
- \begin{tabular}{@ {}l@ {}}
- @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\
- @{thm permute_bool_def[no_vars, THEN eq_reflection]}
- \end{tabular} &
- \begin{tabular}{@ {}l@ {}}
- @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
- @{thm permute_list.simps(2)[no_vars, THEN eq_reflection]}\\
- \end{tabular} &
- \begin{tabular}{@ {}l@ {}}
- @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
- @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
- \end{tabular}
- \end{tabular}}
- \end{center}
-
\noindent
Concrete permutations in Nominal Isabelle are built up from swappings,
written as \mbox{@{text "(a b)"}}, which are permutations that behave
as follows:
- \begin{center}
+ \[
@{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
- \end{center}
+ \]\smallskip
The most original aspect of the nominal logic work of Pitts is a general
definition for the notion of the ``set of free variables of an object @{text
@@ -508,25 +491,31 @@
\noindent
There is also the derived notion for when an atom @{text a} is \emph{fresh}
- for an @{text x}, defined as @{thm fresh_def[no_vars]}.
+ for an @{text x}, defined as
+
+ \[
+ @{thm fresh_def[no_vars]}
+ \]\smallskip
+
+ \noindent
We use for sets of atoms the abbreviation
@{thm (lhs) fresh_star_def[no_vars]}, defined as
@{thm (rhs) fresh_star_def[no_vars]}.
A striking consequence of these definitions is that we can prove
without knowing anything about the structure of @{term x} that
swapping two fresh atoms, say @{text a} and @{text b}, leaves
- @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
- then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+ @{text x} unchanged, namely
\begin{prop}\label{swapfreshfresh}
- @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+ If @{thm (prem 1) swap_fresh_fresh[no_vars]} and @{thm (prem 2) swap_fresh_fresh[no_vars]}
+ then @{thm (concl) swap_fresh_fresh[no_vars]}
\end{prop}
While often the support of an object can be relatively easily
described, for example for atoms, products, lists, function applications,
booleans and permutations as follows
- \begin{center}
+ \[\mbox{
\begin{tabular}{c@ {\hspace{10mm}}c}
\begin{tabular}{rcl}
@{term "supp a"} & $=$ & @{term "{a}"}\\
@@ -538,18 +527,16 @@
\begin{tabular}{rcl}
@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
@{term "supp b"} & $=$ & @{term "{}"}\\
- @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+ @{term "supp \<pi>"} & $=$ & @{term "{a. \<pi> \<bullet> a \<noteq> a}"}
\end{tabular}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
in some cases it can be difficult to characterise the support precisely, and
- only an approximation can be established (as for functions above).
-
- Reasoning about
- such approximations can be simplified with the notion \emph{supports}, defined
- as follows:
+ only an approximation can be established (as for function applications
+ above). Reasoning about such approximations can be simplified with the
+ notion \emph{supports}, defined as follows:
\begin{defi}
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}