--- a/LMCS-Paper/Paper.thy Thu Sep 15 01:01:43 2011 +0200
+++ b/LMCS-Paper/Paper.thy Fri Sep 16 08:00:15 2011 +0200
@@ -874,7 +874,7 @@
\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
+ 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)"}.
@@ -1039,7 +1039,7 @@
There are also some restrictions we need to impose on our binding clauses in
comparison to the ones of Ott. The main idea behind these restrictions is
- that we obtain a sensible notion of alpha-equivalence where it is ensured
+ that we obtain a notion of alpha-equivalence where it is ensured
that within a given scope an atom occurrence cannot be both bound and free
at the same time. The first restriction is that a body can only occur in
\emph{one} binding clause of a term constructor. So for example
@@ -1215,15 +1215,16 @@
\noindent
In this example the term constructor @{text "ACons'"} has four arguments with
- a binding clause for two of them. This constructor is also used in the definition
+ a binding clause involving two of them. This constructor is also used in the definition
of the binding function. The restriction we have to impose is that the
- binding function can only return free atoms, that is the ones that are not
+ binding function can only return free atoms, that is the ones that are \emph{not}
mentioned in a binding clause. Therefore @{text "y"} cannot be used in the
binding function @{text "bn"} (since it is bound in @{text "ACons'"} by the
binding clause), but @{text x} can (since it is a free atom). This
restriction is sufficient for lifting the binding function to alpha-equated
- terms. If we would permit that @{text "bn"} can also return @{text "y"},
- then it would not be respectful and therefore cannot be lifted.
+ terms. If we would permit @{text "bn"} to return @{text "y"},
+ then it would not be respectful and therefore cannot be lifted to
+ alpha-equated lambda-terms.
In the version of Nominal Isabelle described here, we also adopted the
restriction from the Ott-tool that binding functions can only return: the
@@ -1281,7 +1282,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 on the ``raw'' type @{text "ty"}.
+ @{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>"}.
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
@@ -1323,7 +1325,7 @@
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
- bound, as we saw in the example with ``plain'' @{text Let}s. We need
+ bound, as we saw in \eqref{letrecs} with the example of ``plain'' @{text Let}s. We need
therefore functions that calculate those free atoms in deep binders.
While the idea behind these free-atom functions is simple (they just
@@ -1687,7 +1689,7 @@
Again let us take a look at a concrete example for these definitions. For
the specification given in \eqref{letrecs}
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
- $\approx_{\textit{bn}}$ with the following clauses:
+ $\approx_{\textit{bn}}$ with the following rules:
\begin{equation}\label{rawalpha}\mbox{
\begin{tabular}{@ {}c @ {}}
@@ -1723,10 +1725,11 @@
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 (e.g.~in the @{text "Let_rec"}-case)
+ Note also that in case of more than one body (that is in the @{text "Let_rec"}-case)
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.
+ corresponding binding clause specifies a binder with two bodies, namely
+ @{text "as"} and @{text "t"}.
*}
section {* Establishing the Reasoning Infrastructure *}
@@ -1768,7 +1771,7 @@
\end{lem}
\begin{proof}
- The proof is by induction over the definitions. The non-trivial
+ The proofs are by induction. The non-trivial
cases involve premises built up by $\approx_{\textit{set}}$,
$\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They
can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
@@ -1843,11 +1846,30 @@
"bn"}$_{1..m}$ so that they return bound atoms and in this case the third
implication is \emph{not} true. A result is that in general the lifting of the
corresponding binding functions in Ott to alpha-equated terms is impossible.
-
Having established respectfulness for the ``raw'' term-constructors, the
quotient package is able to automatically deduce \eqref{distinctalpha} from
- \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
- also lift properties that characterise when two ``raw'' terms of the form
+ \eqref{distinctraw}.
+
+ Next we can lift the permutation operations defined in \eqref{ceqvt}. In
+ order to make this lifting to go through, we have to show that the
+ permutation operations are respectful. This amounts to showing that the
+ alpha-equivalence relations are equivariant, which
+ we already established in Lemma~\ref{equiv}. As a result we can add the
+ equations
+
+ \begin{equation}\label{calphaeqvt}
+ @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
+ \end{equation}\smallskip
+
+ \noindent
+ to our infrastructure. In a similar fashion we can lift the defining equations
+ of the free-atom functions @{text "fa_ty\<AL>"}$_{1..n}$ and
+ @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
+ "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
+ The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
+ by the datatype package of Isabelle/HOL.
+
+ We also need to lift the properties that characterise when two ``raw'' terms of the form
\[
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
@@ -1862,11 +1884,13 @@
\]\smallskip
\noindent
- We call these conditions as \emph{quasi-injectivity}. They correspond to
- the premises in our alpha-equiva\-lence relations, with the exception that
- in case of binders the relations @{text "\<approx>ty"}$_{1..n}$ are all replaced
- by equality. Recall the alpha-equivalence rules for @{text "Let"} and @{text "Let_rec"}
- shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"} we have
+ We call these conditions as \emph{quasi-injectivity}. They correspond to the
+ premises in our alpha-equiva\-lence relations, with the exception 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
+ @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and
+ @{text "Let_rec\<^sup>\<alpha>"} we have
\begin{equation}\label{alphalift}\mbox{
\begin{tabular}{@ {}c @ {}}
@@ -1879,30 +1903,7 @@
\end{tabular}}
\end{equation}\smallskip
- \noindent
- where @{text "\<approx>\<^bsub>trm\<^esub>"} and @{text "\<approx>\<^bsub>assn\<^esub>"} are replaced by @{text "="} (and similarly
- the free-atom and binding functions are replaced by their lifted counterparts).
-
- Next we can lift the permutation operations defined in \eqref{ceqvt}. In
- order to make this lifting to go through, we have to show that the
- permutation operations are respectful. This amounts to showing that the
- alpha-equivalence relations are equivariant, which
- we already established in Lemma~\ref{equiv}. As a result we can add the
- equations
-
- \begin{equation}\label{calphaeqvt}
- @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
- \end{equation}\smallskip
-
- \noindent
- to our infrastructure. In a similar fashion we can lift the defining equations
- of the free-atom functions @{text "fn_ty\<AL>"}$_{1..n}$ and
- @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
- "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.
- The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$
- by the datatype package of Isabelle/HOL.
-
- Finally we can add to our infrastructure cases lemmas and a (mutual)
+ We can also add to our infrastructure cases lemmas and a (mutual)
induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
lemmas allow the user to deduce a property @{text "P"} by exhaustively
analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be
@@ -1938,7 +1939,7 @@
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
- premise of the form
+ 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)"}}
@@ -1956,18 +1957,18 @@
on the right):
\begin{equation}\label{inductex}\mbox{
- \begin{tabular}{c@ {\hspace{10mm}}c}
+ \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {}}
\begin{tabular}{@ {}c@ {}}
\infer{@{text "P\<^bsub>trm\<^esub>"}}
- {\begin{array}{l}
+ {\begin{array}{@ {}l@ {}}
@{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
- @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+ @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
\end{array}}\medskip\\
\infer{@{text "P\<^bsub>pat\<^esub>"}}
- {\begin{array}{l}
+ {\begin{array}{@ {}l@ {}}
@{text "y = PNil\<^sup>\<alpha> \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
@{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
@@ -1977,11 +1978,11 @@
\begin{tabular}{@ {}c@ {}}
\infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}
- {\begin{array}{l}
+ {\begin{array}{@ {}l@ {}}
@{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
- @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
@{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
@{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
@@ -2022,13 +2023,13 @@
in terms of support and freshness, but also provides evidence that our
notions of free-atoms and alpha-equivalence ``match up''.
- \begin{thm}
+ \begin{thm}\label{suppfa}
For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
\end{thm}
\begin{proof}
- The proof is by induction. In each case
+ The proof is by induction on @{text "x"}$_{1..n}$. In each case
we unfold the definition of @{text "supp"}, move the swapping inside the
term-constructors and then use the quasi-injectivity lemmas in order to complete the
proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},
@@ -2052,9 +2053,11 @@
\]\smallskip
\noindent
- Taking the fact into account that @{term "equ2"} and @{term "supp2"} are
- by definition equal to @{term "equal"} and @{term "supp"}, respectively,
- the above rules simplify even further to
+ Taking the fact 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
+
\[\mbox{
\begin{tabular}{@ {}c @ {}}
@@ -2068,10 +2071,11 @@
\]\smallskip
\noindent
- which means we can characterise equality between term-constructors in terms
- of equality between the abstractions defined in Section~\ref{sec:binders}. From this
- we can derive the support for @{text "Let\<^sup>\<alpha>"} and
- @{text "Let_rec\<^sup>\<alpha>"}, namely
+ which means we can characterise equality between term-constructors (on the
+ alpha-equated level) in terms of equality between the abstractions defined
+ in Section~\ref{sec:binders}. From this we can deduce the support for @{text
+ "Let\<^sup>\<alpha>"} and @{text "Let_rec\<^sup>\<alpha>"}, namely
+
\[\mbox{
\begin{tabular}{l@ {\hspace{2mm}}l@ {\hspace{2mm}}l}
@@ -2096,32 +2100,31 @@
text {*
In the previous section we derived induction principles for alpha-equated
- terms (see \eqref{induct} and \eqref{inductex}). This was done by lifting
- the corresponding inductions principles for ``raw'' terms. We already
- employed these induction principles in order to derive several facts for
- 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 any assumptions about the atoms that are
- bound, and we have to potentially rename them. This renaming has to be
- done manually and is often very cumbersome (especially in the case for
+ terms (see \eqref{induct} for the general form and \eqref{inductex} for an
+ instance). 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
+ 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
+ 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
multiple bound atoms).
+
For the older versions of Nominal Isabelle we introduced in
\cite{UrbanTasson05} a method for automatically strengthening weak induction
- principles in case of single binders. These stronger induction principles
- allow the user to make additional assumptions about bound atoms. The main
- point is that these additional assumptions amount to a formal version of the
- informal variable convention for binders and nearly always make manual
- renaming of binders 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
+ 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:
\begin{equation}\label{stronginduct}
\mbox{
@@ -2130,8 +2133,9 @@
{\begin{array}{l}
@{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
- @{text "\<forall>x\<^isub>1 x\<^isub>2 c. {atom x\<^isub>1} #\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
- @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\
+ \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
@{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
@{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
@{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
@@ -2141,45 +2145,122 @@
\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\<^sup>\<alpha>"} cases (these are the cases
- where the user specified some binding clauses).
+ 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\<^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\<^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.
In what follows we will show that the induction principle in
- \eqref{inductex} implies \eqref{stronginduct}. This fact was established in
- \cite{UrbanTasson05} 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 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 each type
- @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction step and the
- other is that we have covered all cases.
+ \eqref{inductex} implies \eqref{stronginduct}. This fact was established for
+ single binders in \cite{UrbanTasson05} 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
+ 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
+ each type @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction
+ step and the other is that we have covered all cases. 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.
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
- is straightforward to establish that these measures decrease in every
+ is straightforward to establish that the sizes decrease in every
induction step. What is left to show is that we covered all cases.
- To do so, we use a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat}
- this lemma is of the form
-
- \begin{equation}\label{weakcases}
+ To do so, we have to derive stronger cases lemmas, which look in our
+ running example as follows:
+
+ \[\mbox{
+ \begin{tabular}{@ {}c@ {\hspace{6mm}}c@ {}}
\infer{@{text "P\<^bsub>trm\<^esub>"}}
- {\begin{array}{l@ {\hspace{9mm}}l}
- @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
- @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
- \end{array}}\\[-1mm]
- \end{equation}
-
- where we have a premise for each term-constructor.
- The idea behind such cases lemmas is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
- provided we can show that this property holds if we substitute for @{text "t"} all
- possible term-constructors.
+ {\begin{array}{@ {}l@ {}}
+ @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+ \end{array}} &
+
+ \infer{@{text "P\<^bsub>pat\<^esub>"}}
+ {\begin{array}{@ {}l@ {}}
+ @{text "y = PNil\<^sup>\<alpha> \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+ @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
+ \end{array}}
+ \end{tabular}}
+ \]\smallskip
+
+ \noindent
+ 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 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\<^sup>\<alpha>"}. There the
+ stronger cases lemma allow us to assume that the bound atoms avoid the context @{text "c"}
+ (which is assumed to be finitely supported).
+
+ Let us show first establish the simpler 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 implication
+
+ \begin{equation}\label{imp}
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. atom x\<^isub>1 # c \<and> y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}
+ \end{equation}\smallskip
+
+ \noindent
+ which we can 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
+ 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
+ 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"}. We can use this in the assumption
+ \eqref{assm} and then use \eqref{imp} to conclude this case.
+
+ The @{text "Let\<^sup>\<alpha>"}-case involving a (non-recursive) deep binder is more complicated.
+ We have the assumption
+
+ \begin{equation}\label{assm}
+ @{text "y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3"}
+ \end{equation}\smallskip
+
+ \noindent
+ and as implication
+
+ \[
+
+ \]\smallskip
+
+
+ The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+ because @{text p} might contain names bound by @{text bn}, but also some that are
+ free. To solve this problem we have to introduce a permutation function that only
+ permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
+ by lifting. For a
+ clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
+
+
+ {\bf NOT DONE YET}
+
+ {\it
The only remaining difficulty is that in order to derive the stronger induction
principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
@@ -2187,31 +2268,8 @@
\emph{all} @{text Let}-terms.
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}
- \begin{tabular}{l}
- @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
- @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\[-2mm]
- \end{tabular}
- \end{center}
+
- \noindent
- which however can be relatively easily be derived from the implications in \eqref{weakcases}
- by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
- that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with
- a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and
- @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
- By using Property \ref{supppermeq}, we can infer from the latter
- that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
- and we are done with this case.
-
- The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
- The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
- because @{text p} might contain names bound by @{text bn}, but also some that are
- free. To solve this problem we have to introduce a permutation function that only
- permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
- by lifting. For a
- 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
@@ -2242,12 +2300,6 @@
principle.
-
- A natural question is
- whether we can also strengthen the weak induction principles involving
- the general binders presented here. We will indeed be able to so, but for this we need an
- additional notion for permuting deep binders.
-
Given a binding function @{text "bn"} we define an auxiliary permutation
operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
Assuming a clause of @{text bn} is given as
@@ -2311,88 +2363,10 @@
This fact will be crucial when establishing the strong induction principles below.
- In our running example about @{text "Let"}, the strong induction
- principle means that instead
- of establishing the implication
-
- \begin{center}
- @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
- \end{center}
-
- \noindent
- it is sufficient to establish the following implication
-
- \begin{equation}\label{strong}
- \mbox{\begin{tabular}{l}
- @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
- \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
- \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
- \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
- \end{tabular}}
- \end{equation}
-
- \noindent
- While this implication contains an additional argument, namely @{text c}, and
- also additional universal quantifications, it is usually easier to establish.
- The reason is that we have the freshness
- assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
- chosen by the user as long as it has finite support.
-
- Let us now show how we derive the strong induction principles from the
- weak ones. In case of the @{text "Let"}-example we derive by the weak
- induction the following two properties
-
- \begin{equation}\label{hyps}
- @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
- @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
- \end{equation}
-
- \noindent
- For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
- assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
- By Property~\ref{avoiding} we
- obtain a permutation @{text "r"} such that
-
- \begin{equation}\label{rprops}
- @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
- @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
- \end{equation}
-
- \noindent
- hold. The latter fact and \eqref{renaming} give us
-
- \begin{center}
- \begin{tabular}{l}
- @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
- \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
- \end{tabular}
- \end{center}
-
- \noindent
- So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
- establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
- To do so, we will use the implication \eqref{strong} of the strong induction
- principle, which requires us to discharge
- the following four proof obligations:
-
- \begin{center}
- \begin{tabular}{rl}
- {\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
- {\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
- {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
- {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
- others from the induction hypotheses in \eqref{hyps} (in the fourth case
- we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
-
- Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
- we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
+
This completes the proof showing that the weak induction principles imply
the strong induction principles.
+ }
*}