--- a/LMCS-Paper/Paper.thy Fri Sep 16 11:24:53 2011 +0200
+++ b/LMCS-Paper/Paper.thy Sun Sep 18 19:38:19 2011 +0200
@@ -45,8 +45,8 @@
alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and
alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and
Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
- Abs_lst ("[_]\<^bsub>list\<^esub>._") and
- Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
+ Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and
+ Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) and
Abs_res ("[_]\<^bsub>set+\<^esub>._") and
Abs_print ("_\<^bsub>set\<^esub>._") and
Cons ("_::_" [78,77] 73) and
@@ -282,7 +282,7 @@
easier than reasoning with raw terms. The fundamental reason for this is
that the HOL-logic underlying Nominal Isabelle allows us to replace
``equals-by-equals''. In contrast, replacing
- ``alpha-equals-by-alpha-equals'' in a representation based on raw terms
+ ``alpha-equals-by-alpha-equals'' in a representation based on ``raw'' terms
requires a lot of extra reasoning work.
Although in informal settings a reasoning infrastructure for alpha-equated
@@ -387,23 +387,25 @@
which includes multiple binders in type-schemes.\medskip
\noindent
- {\bf Contributions:} We provide three new definitions for when terms
+ {\bf Contributions:} We provide three new definitions for when terms
involving general binders are alpha-equivalent. These definitions are
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
- proofs, we establish a reasoning infrastructure for alpha-equated
- terms, including properties about support, freshness and equality
- conditions for alpha-equated terms. We are also able to derive strong
+ proofs, we establish a reasoning infrastructure for alpha-equated terms,
+ including properties about support, freshness and equality conditions for
+ alpha-equated terms. We are also able to automatically derive strong
induction principles that have the variable convention already built in.
- The method behind our specification of general binders is taken
- from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
- that our specifications make sense for reasoning about alpha-equated terms.
- 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 this we simplify the earlier automated proofs by using the proof tools
+ from the function package~\cite{Krauss09} of Isabelle/HOL. The method
+ behind our specification of general binders is taken from the Ott-tool, but
+ we introduce crucial restrictions, and also extensions, so that our
+ specifications make sense for reasoning about alpha-equated terms. 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 from ``first principles'' inside a theorem prover.
- \begin{figure}
+ \begin{figure}[t]
\begin{boxedminipage}{\linewidth}
\begin{center}
\begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
@@ -638,7 +640,7 @@
Note that @{term "supp x \<sharp>* \<pi>"}
is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also formulate
- Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the
+ Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the
reasoning infrastructure of Nominal Isabelle is set up so that it provides more
automation for the formulation given above.
@@ -721,8 +723,8 @@
and @{text bs} are lists of atoms).
If we do not want to make any difference between the order of binders \emph{and}
- also allow vacuous binders, that means according to Pitts \emph{restrict} names
- \cite{Pitts04}, then we keep sets of binders, but drop
+ also allow vacuous binders, that means according to Pitts~\cite{Pitts04}
+ \emph{restrict} names, then we keep sets of binders, but drop
condition {\it (iv)} in Definition~\ref{alphaset}:
\begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
@@ -764,10 +766,10 @@
shown that all three notions of alpha-equivalence coincide, if we only
abstract a single atom.
- In the rest of this section we are going to show that the alpha-equivalences really
- lead to abstractions where some atoms are bound (more precisely removed from the
- support). For this we are going to introduce
- three abstraction types that are quotients of the relations
+ In the rest of this section we are going to show that the alpha-equivalences
+ really lead to abstractions where some atoms are bound (more precisely
+ removed from the support). For this we will consider three abstraction
+ types that are quotients of the relations
\begin{equation}
\begin{array}{r}
@@ -841,7 +843,7 @@
\noindent
In effect, this theorem states that the atoms @{text "as"} are bound in the
- abstraction. As stated earlier, this can be seen as test that our
+ abstraction. As stated earlier, this can be seen as litmus test that our
Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
idea of alpha-equivalence relations. Below we will give the proof for the
first equation of Theorem \ref{suppabs}. The others follow by similar
@@ -874,10 +876,10 @@
\begin{proof}
If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
- Also in the other case it is straightforward using \eqref{abseqiff} and
- observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
- (supp x - as)"}. We therefore can use as permutation the swapping @{term
- "(a \<rightleftharpoons> b)"}.
+ Also in the other case the lemma is straightforward using \eqref{abseqiff}
+ and observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
+ (supp x - as)"}. We therefore can use the swapping @{term "(a \<rightleftharpoons> b)"}. as
+ the permutation fpr the proof obligation.
\end{proof}
\noindent
@@ -922,7 +924,7 @@
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
the first equation of Theorem~\ref{suppabs}.
- Recall the definition of support in \eqref{suppdef}, and note the difference between
+ Recall the definition of support given in \eqref{suppdef}, and note the difference between
the support of a ``raw'' pair and an abstraction
\[
@@ -933,7 +935,9 @@
\noindent
While the permutation operations behave in both cases the same (a permutation
is just moved to the arguments), the notion of equality is different for pairs and
- abstractions. Therefore we have different supports.
+ abstractions. Therefore we have different supports. In case of abstractions,
+ we have established that bound atoms are removed from the support of the
+ abstractions' bodies.
The method of first considering abstractions of the form @{term "Abs_set as
x"} etc is motivated by the fact that we can conveniently establish at the
@@ -1282,8 +1286,8 @@
for the corresponding notion given on the ``raw'' level. So for example
we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
where @{term ty} is the type used in the quotient construction for
- @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor in the ``raw'' type @{text "ty"},
- respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor in @{text "ty\<^sup>\<alpha>"}.
+ @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"},
+ respectively @{text "C\<^sup>\<alpha>"} is the corresponding term-constructor of @{text "ty\<^sup>\<alpha>"}.
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
non-empty and the types in the constructors only occur in positive
@@ -1299,7 +1303,7 @@
\end{equation}\smallskip
\noindent
- We need this operation later when we define the notion of alpha-equivalence.
+ We will need this operation later when we define the notion of alpha-equivalence.
The first non-trivial step we have to perform is the generation of
\emph{free-atom functions} from the specifications.\footnote{Admittedly, the
@@ -1366,9 +1370,9 @@
\noindent
where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
- we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason
+ we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i \<equiv> supp"}}. The reason
for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and
- we assume @{text supp} is the generic notion that characterises the free variables of
+ we assume @{text supp} is the generic function that characterises the free variables of
a type (in fact in the next section we will show that the free-variable functions we
define here, are equal to the support once lifted to alpha-equivalence classes).
@@ -1595,8 +1599,7 @@
$\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly
$\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and
$\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ 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
+ binding modes). As above, we first build the tuples @{text "D"} and
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
For $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ we also need
@@ -1630,7 +1633,7 @@
inside the structure of these binders. An example is @{text "Let"} where we
have to make sure the right-hand sides of assignments are
alpha-equivalent. For this we use relations @{text "\<approx>bn"}$_{1..m}$ (which we
- will formally define shortly). Let us assume the non-recursive deep binders
+ will define shortly). Let us assume the non-recursive deep binders
in @{text "bc\<^isub>i"} are
\[
@@ -1687,7 +1690,7 @@
for the existentially quantified permutation).
Again let us take a look at a concrete example for these definitions. For
- the specification given in \eqref{letrecs}
+ the specification shown in \eqref{letrecs}
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following rules:
@@ -1725,7 +1728,7 @@
The underlying reason is that the terms inside an assignment are not meant
to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
because there all components of an assignment are ``under'' the binder.
- Note also that in case of more than one body (that is in the @{text "Let_rec"}-case)
+ Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above)
we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
equivalence relation and a compound free-atom function. This is because the
corresponding binding clause specifies a binder with two bodies, namely
@@ -1885,7 +1888,7 @@
\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to the
- premises in our alpha-equiva\-lence relations, with the exception that the
+ premises in our alpha-equiva\-lence relations, except that the
relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly
the free-atom and binding functions are replaced by their lifted
counterparts). Recall the alpha-equivalence rules for @{text "Let"} and
@@ -1936,10 +1939,10 @@
\end{equation}\smallskip
\noindent
- whereby the @{text P}$_{1..n}$ are the properties established by the induction
- and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. Note that
- the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a
- hypothesis of the form
+ whereby the @{text P}$_{1..n}$ are the properties established by the
+ induction, and the @{text y}$_{1..n}$ are of type @{text
+ "ty\<AL>"}$_{1..n}$. Note that for the term constructors @{text
+ "C"}$^\alpha_1$ the induction principle has a hypothesis of the form
\[
\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}}
@@ -1952,7 +1955,7 @@
Recall the lambda-calculus with @{text "Let"}-patterns shown in
\eqref{letpat}. The cases lemmas and the induction principle shown in
- \eqref{cases} and \eqref{induct} boil down to the following three inference
+ \eqref{cases} and \eqref{induct} boil down in this example to the following three inference
rules (the cases lemmas are on the left-hand side; the induction principle
on the right):
@@ -2001,7 +2004,7 @@
\noindent
This allows us to prove using the induction principle for @{text "ty\<AL>"}$_{1..n}$
that every element of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported
- (using Prop.~\ref{supportsprop}{\it (i)}).
+ (using Proposition~\ref{supportsprop}{\it (i)}).
Similarly, we can establish by induction that the free-atom functions and binding
functions are equivariant, namely
@@ -2016,10 +2019,11 @@
\noindent
Lastly, we can show that the support of elements in @{text
- "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$. This fact
- is important in the nominal setting where the general theory is formulated
- in terms of support and freshness, but also provides evidence that our
- notions of free-atoms and alpha-equivalence ``match up''.
+ "ty\<AL>"}$_{1..n}$ is the same as the free atom functions @{text
+ "fa_ty\<AL>"}$_{1..n}$. This fact is important in the nominal setting where
+ the general theory is formulated in terms of support and freshness, but also
+ provides evidence that our notions of free-atoms and alpha-equivalence
+ ``match up'' correctly.
\begin{thm}\label{suppfa}
For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@@ -2036,8 +2040,9 @@
\end{proof}
\noindent
- Consequently we can simplify the quasi-injection lemmas, for example the ones
- given in \eqref{alphalift} for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} to
+ Consequently, we can replace the free atom functions by @{text "supp"} in
+ our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance,
+ we obtain for @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}
\[\mbox{
\begin{tabular}{@ {}c @ {}}
@@ -2051,11 +2056,10 @@
\]\smallskip
\noindent
- Taking the fact into account that the compound equivalence relation @{term
+ Taking into account that the compound equivalence relation @{term
"equ2"} and the compound free-atom function @{term "supp2"} are by
definition equal to @{term "equal"} and @{term "supp"}, respectively, the
- above rules simplify even further to
-
+ above rules simplify further to
\[\mbox{
\begin{tabular}{@ {}c @ {}}
@@ -2085,8 +2089,7 @@
\noindent
using the support of abstractions derived in Theorem~\ref{suppabs}.
-
- To sum up this section, we can establish a reasoning infrastructure for the
+ To sum up this section, we have established a reasoning infrastructure for the
types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the
``raw'' level to the quotient level and then by proving facts about
these lifted definitions. All necessary proofs are generated automatically
@@ -2099,30 +2102,29 @@
text {*
In the previous section we derived induction principles for alpha-equated
terms (see \eqref{induct} for the general form and \eqref{inductex} for an
- instance). This was done by lifting the corresponding inductions principles
+ example). This was done by lifting the corresponding inductions principles
for ``raw'' terms. We already employed these induction principles for
- deriving several facts for alpha-equated terms, including the property that
+ deriving several facts about alpha-equated terms, including the property that
the free-variable functions and the notion of support coincide. Still, we
call these induction principles \emph{weak}, because for a term-constructor,
say \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction
hypothesis requires us to establish (under some assumptions) a property
@{text "P (C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text
- "x"}$_{1..r}$. The problem is that in the presence of binders we cannot make
+ "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make
any assumptions about the atoms that are bound. One obvious way around this
problem is to rename them. Unfortunately, this leads to very clunky proofs
- and makes formalisations grievous experiences (especially in the case for
+ and makes formalisations grievous experiences (especially in the context of
multiple bound atoms).
-
- For the older versions of Nominal Isabelle we described in
- \cite{Urban08} a method for automatically strengthening weak induction
- principles. These stronger induction principles allow the user to make
- additional assumptions about bound atoms. The advantage of these assumptions
- is that they make in most cases any renaming of bound atoms unnecessary. To
- explain how the strengthening works in the presence of multiple binders, we
- use as running example the lambda-calculus with @{text "Let"}-patterns shown
- in \eqref{letpat}. Its weak induction principle is given in
- \eqref{inductex}. The stronger induction principle is as follows:
+ For the older versions of Nominal Isabelle we described in \cite{Urban08} a
+ method for automatically strengthening weak induction principles. These
+ stronger induction principles allow the user to make additional assumptions
+ about bound atoms. The advantage of these assumptions is that they make in
+ most cases any renaming of bound atoms unnecessary. To explain how the
+ strengthening works, we use as running example the lambda-calculus with
+ @{text "Let"}-patterns shown in \eqref{letpat}. Its weak induction principle
+ is given in \eqref{inductex}. The stronger induction principle is as
+ follows:
\begin{equation}\label{stronginduct}
\mbox{
@@ -2143,25 +2145,27 @@
\noindent
- Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub>
- y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the
- stronger induction principle establishes the properties @{text "
- P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in
- which the additional parameter @{text c} is assumed to be of finite
- support. The purpose of @{text "c"} is to ``control'' which freshness
- assumptions the binders should satisfy in the @{text "Lam\<^sup>\<alpha>"} and
- @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text "Lam\<^sup>\<alpha>"} we can assume the
- bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text
- "Let_pat\<^sup>\<alpha>"} we can assume all bound atoms from an assignment are fresh
- for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can
- mimic the ``pencil-and-paper'' reasoning employing the usual variable
- convention \cite{Urban08}.
+ Notice that instead of establishing two properties of the form @{text "
+ P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}, as the
+ weak one does, the stronger induction principle establishes the properties
+ of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \<and>
+ P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text
+ c} is assumed to be of finite support. The purpose of @{text "c"} is to
+ ``control'' which freshness assumptions the binders should satisfy in the
+ @{text "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases: for @{text
+ "Lam\<^sup>\<alpha>"} we can assume the bound atom @{text "x\<^isub>1"} is fresh
+ for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
+ all bound atoms from an assignment are fresh for @{text "c"} (fourth
+ line). If @{text "c"} is instantiated appropriately in the strong induction
+ principle, the user can mimic the usual ``pencil-and-paper'' reasoning
+ employing the variable convention about bound and free variables being
+ distinct \cite{Urban08}.
- In what follows we will show that the induction principle in
- \eqref{inductex} implies \eqref{stronginduct}. This fact was established for
+ In what follows we will show that the weak induction principle in
+ \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
single binders in \cite{Urban08} by some quite involved, nevertheless
automated, induction proof. In this paper we simplify the proof by
- leveraging the automated proof methods from the function package of
+ leveraging the automated proving methods from the function package of
Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods
is well-founded induction. To use them in our setting, we have to discharge
two proof obligations: one is that we have well-founded measures (one for
@@ -2169,9 +2173,8 @@
step and the other is that we have covered all cases in the induction
principle. Once these two proof obligations are discharged, the reasoning
infrastructure in the function package will automatically derive the
- stronger induction principle. This considerably simplifies the work we have
- to do here.
-
+ stronger induction principle. This way of establishing the stronger induction
+ principle is considerably simpler than the work presented \cite{Urban08}.
As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,
which we lifted in the previous section and which are all well-founded. It
@@ -2200,25 +2203,25 @@
\]\smallskip
\noindent
- They are stronger in the sense that they allow us to assume that the bound
- atoms avoid a context @{text "c"} (which is assumed to be finitely
- supported). This is similar with the stronger induction principles.
+ They are stronger in the sense that they allow us to assume in the @{text
+ "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms
+ avoid a context @{text "c"} (which is assumed to be finitely supported).
These stronger cases lemmas need to be derived from the `weak' cases lemmas
given in \eqref{inductex}. This is trivial in case of patterns (the one on
the right-hand side) since the weak and strong cases lemma coincide (there
is no binding in patterns). Interesting are only the cases for @{text
"Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"}, where we have some binders and
- therefore have an addition assumption. Let us show first establish the case
- for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma \eqref{inductex} we can
- assume that
+ therefore have an addition assumption about avoiding @{text "c"}. Let us
+ first establish the case for @{text "Lam\<^sup>\<alpha>"}. By the weak cases lemma
+ \eqref{inductex} we can assume that
\begin{equation}\label{assm}
@{text "y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
\end{equation}\smallskip
\noindent
- holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the
+ holds, and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the
corresponding implication
\begin{equation}\label{imp}
@@ -2226,19 +2229,25 @@
\end{equation}\smallskip
\noindent
- which we can use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
+ which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot
use this implication directly, because we have no information whether @{text
"x\<^isub>1"} is fresh for @{text "c"}. However, we can use Properties
- \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: We know
+ \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know
by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\<alpha>
x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 -
- {atom x\<^isub>1}"}). Property \ref{avoiding} provides us therefore with a
+ {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a
permutation @{text "\<pi>"}, such that @{text "{atom (\<pi> \<bullet> x\<^isub>1)} #\<^sup>*
c"} and \mbox{@{text "supp (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2) #\<^sup>* \<pi>"}} hold.
- By using Property \ref{supppermeq}, we can infer from the latter that @{text
- "Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"} holds. We can use this equation in
- the assumption \eqref{assm} and then use \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
- and @{text "\<pi> \<bullet> x\<^isub>2"} in order to conclude this case.
+ By using Property \ref{supppermeq}, we can infer from the latter that
+
+ \[
+ @{text "Lam\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) (\<pi> \<bullet> x\<^isub>2) = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2"}
+ \]\smallskip
+
+ \noindent
+ holds. We can use this equation in the assumption \eqref{assm}, and hence
+ use the implication \eqref{imp} with the renamed @{text "\<pi> \<bullet> x\<^isub>1"}
+ and @{text "\<pi> \<bullet> x\<^isub>2"} for concluding this case.
The @{text "Let_pat\<^sup>\<alpha>"}-case involving a deep binder is slightly more complicated.
We have the assumption
@@ -2248,11 +2257,11 @@
\end{equation}\smallskip
\noindent
- and the implication
+ and the implication from the stronger cases lemma
- \[
+ \begin{equation}\label{impletpat}
@{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
- \]\smallskip
+ \end{equation}\smallskip
\noindent
The reason that this case is more complicated is that we cannot apply directly Property
@@ -2265,13 +2274,14 @@
\]\smallskip
\noindent
- Although @{text x} and @{text y} are bound in this term, they are also free
- in the assignment. We can, however, obtain obtain such a renaming
- permutation, say @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al
- x\<^isub>1) x\<^isub>3"}. So we have \mbox{@{term "set (bn_al (\<pi> \<bullet>
- x\<^isub>1)) \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet>
- x\<^isub>3) = Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text "bn\<^sup>\<alpha>"} are equivariant).
- Now the quasi-injective property for @{text "Let_pat\<^sup>\<alpha>"} states
+ where @{text x} and @{text y} are bound in the term, but they are also free
+ in the assignment. We can, however, obtain such a renaming permutation, say
+ @{text "\<pi>"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1)
+ x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\<pi> \<bullet> x\<^isub>1))
+ \<sharp>* c"}} and @{term "Abs_lst (bn_al (\<pi> \<bullet> x\<^isub>1)) (\<pi> \<bullet> x\<^isub>3) =
+ Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text
+ "bn\<^sup>\<alpha>"} are equivariant). Now the quasi-injective property for @{text
+ "Let_pat\<^sup>\<alpha>"} states that
\[
\infer{@{text "Let_pat\<^sup>\<alpha> p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\<alpha> p\<PRIME> t\<PRIME>\<^isub>1 t\<PRIME>\<^isub>2"}}
@@ -2280,31 +2290,30 @@
\]\smallskip
\noindent
- Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}
- (hence @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}), we can infer the
- equation
+ Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\<alpha>"}, we can infer
+ @{text "(\<pi> \<bullet> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\<pi>"}. Therefore we have that
\[
@{text "Let_pat\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) x\<^isub>2 (\<pi> \<bullet> x\<^isub>3) = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
\]\smallskip
\noindent
- Taking the left-hand side as our assumption in \eqref{assmtwo}, we can use
- the implication from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
+ Taking the left-hand side in the assumption from \eqref{assmtwo}, we can use
+ the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed.
The remaining difficulty is when a deep binder contains atoms that are
- bound, but also atoms that are free. An example is @{text "Let\<^sup>\<alpha>"} in \eqref{}.
- Then @{text "(\<pi> \<bullet> x\<^isub>1)
- \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. In such
- cases, however, we only want to rename binders that will become bound, which
- does not affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. The problem is that the
- permutation operation @{text "\<bullet>"} permutes all of them. The remedy is to
- introduce an auxiliary permutation operation, written @{text "_
- \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permute bound atoms and
- leaves the other atoms unchanged. Like the @{text
- "fa_bn"}$_{1..m}$-functions, we can define this operation over raw terms
- analysing how the @{text "bn"}$_{1..m}$-functions are defined and then lift
- them to alpha-equivalent terms. Assuming the user specified a clause
+ bound, but also some that are free. An example is @{text "Let\<^sup>\<alpha>"} in
+ the example \eqref{letrecs}. In such cases @{text "(\<pi> \<bullet> x\<^isub>1)
+ \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea is
+ that we only want to rename binders that will become bound. This does not
+ affect @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. However, the problem is that the
+ permutation operation @{text "_ \<bullet> _"} applies to all of them. To avoid this
+ we introduce an auxiliary permutation operations, written @{text "_
+ \<bullet>\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or
+ more precisely the atoms specified by the @{text "bn"}-functions) and leaves
+ the other atoms unchanged. Like the @{text "fa_bn"}$_{1..m}$-functions, we
+ can define these operations over raw terms analysing how the @{text
+ "bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause
\[
@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}
@@ -2326,25 +2335,26 @@
alpha-equated terms. Moreover we can prove the following two properties
\begin{lem}\label{permutebn}
- Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\\
+ Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text "\<pi>"}\smallskip\\
{\it (i)} @{text "\<pi> \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and\\
{\it (ii)} @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x) \<approx>\<AL>\<^bsub>bn\<^esub> x"}.
\end{lem}
\begin{proof}
- By induction on @{text x}. The properties follow by simple unfolding
- of the definitions.
+ By induction on @{text x}. The properties follow by unfolding of the
+ definitions.
\end{proof}
\noindent
- The first property states that a permutation applied to a binding function is
- equivalent to first permuting the binders and then calculating the bound
- atoms. The main point of the auxiliary permutation
- functions is that it allows us to rename just the binders in a term,
- without changing anything else.
+ The first property states that a permutation applied to a binding function
+ is equivalent to first permuting the binders and then calculating the bound
+ atoms. The second states that @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} preserves
+ @{text "\<approx>\<AL>\<^bsub>bn\<^esub>"}. The main point of the auxiliary
+ permutation functions is that they allow us to rename just the binders in a
+ term, without changing anything else.
Having the auxiliary permutation function in place, we can now solve all remaining cases.
- For @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding}
+ For the @{text "Let\<^sup>\<alpha>"} term-constructor, for example, we can by Property \ref{avoiding}
obtain a @{text "\<pi>"} such that
\[
@@ -2356,7 +2366,7 @@
hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this
to @{text "set (bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and
@{text "[bn\<^sup>\<alpha> (\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\<pi> \<bullet> x\<^isub>2) = [bn\<^sup>\<alpha> x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since
- @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)}
+ @{text "(\<pi> \<bullet>\<AL>\<^bsub>bn\<^esub> x\<^isub>1) \<approx>\<AL>\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)},
we can infer that
\[
@@ -2364,16 +2374,12 @@
\]\smallskip
\noindent
- are alpha-equivalent. This allows us to use the implication from the strong cases
- lemma and we can discharge all proof-obligations to do with having covered all
- cases.
+ holds. This allows us to use the implication from the strong cases
+ lemma.
- This completes the proof showing that the weak induction principles imply
- the strong induction principles. We have automated the reasoning for all
- term-calculi the user might specify. The feature of the function package
- by Krauss \cite{Krauss09} that allows us to establish an induction principle
- by just finding decreasing measures and showing that the induction principle
- covers all cases, tremendously helped us in implementing the automation.
+ Conseqently, we can discharge all proof-obligations to do with having covered all
+ cases. This completes the proof showing that the weak induction principles imply
+ the strong induction principles.
*}
@@ -2503,7 +2509,7 @@
cover many interesting term-calculi from programming language research, for
example Core-Haskell (see Figure~\ref{nominalcorehas}).
- \begin{figure}[p!]
+ \begin{figure}[t]
\begin{boxedminipage}{\linewidth}
\small
\begin{tabular}{l}
@@ -2555,7 +2561,7 @@
lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the
declaration follows closely the original in Figure~\ref{corehas}. The
point of our work is that having made such a declaration in Nominal Isabelle,
- one obtains automatically a reasoning infrastructure for Core-Haskell.
+ one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip
\label{nominalcorehas}}
\end{figure}