--- a/LMCS-Paper/Paper.thy Tue Sep 13 09:30:34 2011 +0200
+++ b/LMCS-Paper/Paper.thy Tue Sep 13 16:14:32 2011 +0200
@@ -1716,11 +1716,11 @@
establishing the reasoning infrastructure for the alpha-equated types @{text
"ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We
give in this section and the next the proofs we need for establishing this
- infrastructure. One main point of our work is that we have completely
+ infrastructure. One point of our work is that we have completely
automated these proofs in Isabelle/HOL.
First we establish that the free-variable functions, the binding functions and the
- alpha-equivalences are equivariant.
+ alpha-equi\-va\-lences are equivariant.
\begin{lem}\mbox{}\\
@{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and
@@ -1730,15 +1730,16 @@
\end{lem}
\begin{proof}
- The function package of Isabelle/HOL allows us to prove the first part is by mutual
- induction over the definitions of the functions. The second is by a straightforward
- induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using
- the first part.
+ The function package of Isabelle/HOL allows us to prove the first part is by
+ mutual induction over the definitions of the functions (we know that they
+ are terminating functions, from which an induction principle can be
+ derived). The second is by a straightforward induction over the rules of
+ @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using the first part.
\end{proof}
\noindent
Next we establish that the alpha-equivalence relations defined in the
- previous section are equivalence relations.
+ previous section are indeed equivalence relations.
\begin{lem}\label{equiv}
The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
@@ -1746,7 +1747,7 @@
\end{lem}
\begin{proof}
- The proof is by mutual induction over the definitions. The non-trivial
+ The proof is by induction over the definitions. 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
@@ -1754,106 +1755,78 @@
\end{proof}
\noindent
- We can feed this lemma into our quotient package and obtain new types @{text
- "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$.
-
- We also obtain definitions for the term-constructors @{text
- "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$,
- and similar definitions for the free-atom functions @{text
+ We can feed the last lemma into our quotient package and obtain new types
+ @{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
+ @{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
+ @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+ "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
"fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
- binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show
- by induction over the definitions of alpha-equivalences that the ``raw''
- functions are respectful. This means we need to establish that
-
- \[\mbox{
- \begin{tabular}{lll}
- @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
- @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
- @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
- \end{tabular}
- }\]\smallskip
-
- \noindent
- holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A
- similar property is needed for the constructors @{text "C"}$_{1..k}$. In order
- to establish it we need to prove that
-
- \[\mbox{
- \begin{tabular}{lll}
- @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
- \end{tabular}
- }\]\smallskip
-
- \noindent
- The respectfulness properties are crucial, ... ???
- However, these definitions are not really useful to the
- user, since they are given in terms of the isomorphisms we obtained by
- creating new types in Isabelle/HOL (recall the picture shown in the
- Introduction).
+ binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
+ are not really useful to the user, since they are given in terms of the
+ isomorphisms we obtained by creating new types in Isabelle/HOL (recall the
+ picture shown in the Introduction).
The first useful property for the user is the fact that distinct
- term-constructors are not
- equal, that is
+ term-constructors are not equal, that is the property
- \[\label{distinctalpha}
+ \begin{equation}\label{distinctalpha}
\mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~%
@{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}}
- \]\smallskip
+ \end{equation}\smallskip
\noindent
whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
- In order to derive this fact, we use the definition of alpha-equivalence
+ In order to derive this property, we use the definition of alpha-equivalence
and establish that
- \[\label{distinctraw}
+ \begin{equation}\label{distinctraw}
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
- \]\smallskip
+ \end{equation}\smallskip
\noindent
holds for the corresponding raw term-constructors.
In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
- Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
+ Given, for example, @{text "C"} is of type @{text "ty"} with argument types
@{text "ty"}$_{1..r}$, respectfulness amounts to showing that
- \begin{center}
+ \[\mbox{
@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
- \end{center}
+ }\]\smallskip
\noindent
- holds under the assumptions that we have \mbox{@{text
+ holds under the assumptions \mbox{@{text
"x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
- @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
- implication by applying the corresponding rule in our alpha-equivalence
- definition and by establishing the following auxiliary implications %facts
- %
- \begin{equation}\label{fnresp}
- \mbox{%
- \begin{tabular}{ll@ {\hspace{7mm}}ll}
- \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
- \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+ @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments
+ (similarly for @{text "D"}). For this we have to show
+ by induction over the definitions of alpha-equivalences the following
+ auxiliary implications
- \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
- \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
- \end{tabular}}
- \end{equation}
-
+ \begin{equation}\label{fnresp}\mbox{
+ \begin{tabular}{lll}
+ @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
+ \end{tabular}
+ }\end{equation}\smallskip
+
\noindent
- They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
- second and last implication are true by how we stated our definitions, the
- third \emph{only} holds because of our restriction
- imposed on the form of the binding functions---namely \emph{not} returning
- any bound atoms. In Ott, in contrast, the user may
- define @{text "bn"}$_{1..m}$ so that they return bound
- atoms and in this case the third implication is \emph{not} true. A
- result is that the lifting of the corresponding binding functions in Ott to alpha-equated
- terms is impossible.
+ whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}
+ is defined. These implications can be established by induction on @{text
+ "\<approx>ty"}$_{1..n}$. Whereas the first, second and last implication are true by
+ how we stated our definitions, the third \emph{only} holds because of our
+ restriction imposed on the form of the binding functions---namely \emph{not}
+ returning any bound atoms. In Ott, in contrast, the user may define @{text
+ "bn"}$_{1..m}$ so that they return bound atoms and in this case the third
+ implication is \emph{not} true. A result is that 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
+ \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
also lift properties that characterise when two raw terms of the form
\[
@@ -1870,16 +1843,14 @@
\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to
- the premises in our alpha-equivalence relations.
+ the premises in our alpha-equiva\-lence relations.
- 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 \cite{HuffmanUrban10}.
- , which we already established
- in Lemma~\ref{equiv}.
- As a result we can add the equations
+ 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)"}
@@ -1893,19 +1864,43 @@
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 a cases lemma (explained in the next section)
- and a structural induction principle
- for the types @{text "ty\<AL>"}$_{1..n}$. The conclusion of the induction principle is
- of the form
-
- \begin{equation}\label{weakinduct}
- \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
- \end{equation} \smallskip
-
+ Finally we can add to our infrastructure cases lemmas and a structural
+ 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 all cases how the elements in a type @{text "ty\<AL>"}$_i$ can
+ be constructed (that means one case for each of term-constructors @{text "C\<AL>"}$_{1..m}$
+ of type @{text "ty\<AL>"}$_i\,$). These are lifted versions of the cases
+ lemma over the raw type @{text "ty"}$_i$ and schematically look as
+ follows
+
+ \[
+ \infer{P}
+ {\begin{array}{l}
+ @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
+ \hspace{5mm}\ldots\\
+ @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
+ \end{array}}
+ \]\smallskip
+
\noindent
- whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$
- have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
- term constructor @{text "C"}$^\alpha$ a premise of the form
+ where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the
+ property that is established by the case analysis. Similarly, we have an induction
+ principle for the types @{text "ty\<AL>"}$_{1..n}$, which is
+
+ \[
+ \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
+ {\begin{array}{l}
+ @{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>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
+ \hspace{5mm}\ldots\\
+ @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
+ \end{array}}
+ \]\smallskip
+
+ \noindent
+ whereby the @{text P}$_{1..n}$ are the properties established by induction
+ and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$.
+ This induction principle has for all term constructors @{text "C"}$^\alpha$
+ a premise of the form
\begin{equation}\label{weakprem}
\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
@@ -1913,7 +1908,26 @@
\noindent
in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
- the recursive arguments of @{text "C\<AL>"}.
+ the recursive arguments of the term constructor. In case of the lambda-calculus,
+ the cases lemma and the induction principle boil down to the following:
+
+ \[\mbox{
+ \begin{tabular}{c@ {\hspace{10mm}}c}
+ \infer{@{text "P"}}
+ {\begin{array}{l}
+ @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}
+ \end{array}} &
+
+ \infer{@{text "P y"}}
+ {\begin{array}{l}
+ @{text "\<forall>x. P (Var\<^sup>\<alpha> x)"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>1 \<and> P x\<^isub>2 \<Rightarrow> P (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
+ @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
+ \end{array}}
+ \end{tabular}}
+ \]\smallskip
By working now completely on the alpha-equated level, we
can first show that the free-atom functions and binding functions are
@@ -1925,12 +1939,12 @@
@{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
@{text "\<pi> \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
\end{tabular}}
- \]
+ \]\smallskip
\noindent
These properties can be established using the induction principle for the
- types @{text "ty\<AL>"}$_{1..n}$. in \eqref{weakinduct}. Having these
+ types @{text "ty\<AL>"}$_{1..n}$. Having these
equivariant properties established, we can show that the support of
term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
arguments, that means
@@ -1940,14 +1954,13 @@
\]\smallskip
\noindent
- holds. This allows us to prove by induction that
- every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported.
- This can be again shown by induction
- over @{text "ty\<AL>"}$_{1..n}$.
- 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 a nominal setting, but also provides evidence
- that our notions of free-atoms and alpha-equivalence are correct.
+ holds. This allows us to prove by induction that every @{text x} of type
+ @{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by
+ induction over @{text "ty\<AL>"}$_{1..n}$. 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, but
+ also provides evidence that our notions of free-atoms and alpha-equivalence
+ are sensible.
\begin{thm}
For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have