--- a/Paper/Paper.thy Fri Apr 02 13:12:10 2010 +0200
+++ b/Paper/Paper.thy Fri Apr 02 15:28:55 2010 +0200
@@ -213,7 +213,7 @@
The scope of the binding is indicated by labels given to the types, for
example @{text "s::trm"}, and a binding clause, in this case
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
- clause states to bind in @{text s} all the names the function call @{text
+ clause states to bind in @{text s} all the names the function @{text
"bn(as)"} returns. This style of specifying terms and bindings is heavily
inspired by the syntax of the Ott-tool \cite{ott-jfp}.
@@ -554,7 +554,13 @@
\noindent
From property \eqref{equivariancedef} and the definition of @{text supp}, we
- can be easily deduce that equivariant functions have empty support.
+ can be easily deduce that equivariant functions have empty support. There is
+ also a similar notion for equivariant relations, say @{text R}, namely the property
+ that
+ %
+ \begin{center}
+ @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+ \end{center}
Finally, the nominal logic work provides us with convenient means to rename
binders. While in the older version of Nominal Isabelle, we used extensively
@@ -925,9 +931,9 @@
\begin{center}
\begin{tabular}{l}
- \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
\end{tabular}
\end{center}
@@ -1114,10 +1120,10 @@
The datatype definition can be obtained by stripping off the
- binding clauses and the labels on the types. We also have to invent
+ binding clauses and the labels from the types. We also have to invent
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
- But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate
+ But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
that a notion is defined over alpha-equivalence classes and leave it out
for the corresponding notion defined on the ``raw'' level. So for example
we have
@@ -1143,12 +1149,6 @@
@{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}
\end{equation}
- % TODO: we did not define permutation types
- %\noindent
- %From this definition we can easily show that the raw datatypes are
- %all permutation types (Def ??) by a simple structural induction over
- %the @{text "ty"}s.
-
The first non-trivial step we have to perform is the generation free-variable
functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
we need to define free-variable functions
@@ -1160,7 +1160,7 @@
\noindent
We define them together with auxiliary free-variable functions for
the binding functions. Given binding functions
- @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
+ @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
%
\begin{center}
@{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
@@ -1168,7 +1168,7 @@
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
- bound, as we shall see in an example below. We need therefore a function
+ bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
that calculates those unbound atoms.
While the idea behind these
@@ -1177,7 +1177,7 @@
somewhat involved.
Given a term-constructor @{text "C"} of type @{text ty} with argument types
\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
- @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
+ @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},
calculated below for each argument.
First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
we can determine whether the argument is a shallow or deep
@@ -1187,10 +1187,10 @@
\begin{equation}\label{deepbinder}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
- $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+ $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\
+ $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
non-recursive binder with the auxiliary binding function @{text "bn"}\\
- $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
+ $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
a deep recursive binder with the auxiliary binding function @{text "bn"}
\end{tabular}}
\end{equation}
@@ -1215,14 +1215,14 @@
\begin{equation}\label{deepbody}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
- $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
- $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
- $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
+ $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+ $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+ $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+ $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes
corresponding to the types specified by the user\\
% $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
% with a free-variable function @{text "fv\<^isup>\<alpha>"}\\
- $\bullet$ & @{term "{}"} otherwise
+ $\bullet$ & @{term "v = {}"} otherwise
\end{tabular}}
\end{equation}
@@ -1249,9 +1249,9 @@
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
+ $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
recursive call @{text "bn x\<^isub>i"}\medskip\\
- $\bullet$ & @{term "{}"} provided @{text "rhs"} contains
+ $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains
@{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
\end{tabular}
\end{center}
@@ -1438,7 +1438,7 @@
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
- {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}\medskip\\
+ {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
\end{tabular}
\end{center}
@@ -1446,7 +1446,7 @@
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
- {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\medskip\\
+ {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
\end{tabular}
\end{center}
@@ -1455,7 +1455,7 @@
$\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
the components in an assignment that are \emph{not} bound. Therefore we have
a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
- a non-recursive binder). The reason is that the terms inside an assignment are not meant
+ a non-recursive binder). 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 everything from the assignment is under the binder.
*}
@@ -1541,21 +1541,21 @@
In fact we can from now on lift facts from the raw level to the alpha-equated level
as long as they contain raw term-constructors only. The
induction principles derived by the datatype package in Isabelle/HOL for the types @{text
- "ty\<AL>\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+ "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
induction principles that establish
\begin{center}
- @{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
+ @{text "P\<^bsub>ty\<AL>\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^isub>n\<^esub> y\<^isub>n "}
\end{center}
\noindent
- for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<^isub>i\<^esub>"} stand for properties
+ for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^isub>i\<^esub>"} stand for properties
defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of
these induction principles look
as follows
\begin{center}
- @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+ @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<AL>\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<AL>\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<AL>\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
\end{center}
\noindent
@@ -1606,7 +1606,7 @@
\noindent
are alpha-equivalent. This gives us conditions when the corresponding
- alpha-equated terms are equal, namely
+ alpha-equated terms are \emph{equal}, namely
\begin{center}
@{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
@@ -1617,7 +1617,7 @@
we have to lift in the next section, we completed
the lifting part of establishing the reasoning infrastructure.
- Working bow completely on the alpha-equated level, we can first show that
+ By working now completely on the alpha-equated level, we can first show that
the free-variable functions and binding functions
are equivariant, namely
@@ -1763,17 +1763,17 @@
\noindent
where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
The problem with this implication is that in general it is not easy to establish it.
- The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"}
+ The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}
(for example we cannot assume the variable convention for them).
In \cite{UrbanTasson05} we introduced a method for automatically
strengthening weak induction principles for terms containing single
binders. These stronger induction principles allow the user to make additional
- assumptions about binders when proving the induction hypotheses.
+ assumptions about binders.
These additional assumptions amount to a formal
version of the informal variable convention for binders. A natural question is
whether we can also strengthen the weak induction principles involving
- general binders. We will indeed be able to so, but for this we need an
+ 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
@@ -1796,7 +1796,7 @@
\end{center}
\noindent
- Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
+ Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
alpha-equated terms. We can then prove the following two facts
\begin{lemma}\label{permutebn}
@@ -1806,7 +1806,7 @@
\end{lemma}
\begin{proof}
- By induction on @{text x}. The equation follow by simple unfolding
+ By induction on @{text x}. The equations follow by simple unfolding
of the definitions.
\end{proof}
@@ -1822,19 +1822,19 @@
\eqref{letpat} this means for a permutation @{text "r"}:
%
\begin{equation}\label{renaming}
- \mbox{if @{term "supp (Abs_lst (bn p) t) \<sharp>* r"}
- then @{text "Let p t = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (r \<bullet> t)"}}
+ \begin{array}{l}
+ \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
+ \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+ \end{array}
\end{equation}
\noindent
- This fact will be used when establishing the strong induction principles.
-
-
+ This fact will be crucial when establishing the strong induction principles.
In our running example about @{text "Let"}, they state that instead
of establishing the implication
\begin{center}
- @{text "\<forall>p t. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t)"}
+ @{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
@@ -1842,9 +1842,10 @@
%
\begin{equation}\label{strong}
\mbox{\begin{tabular}{l}
- @{text "\<forall>p t c."}\\
- \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t)"}\\
- \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+ @{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}
@@ -1865,54 +1866,59 @@
\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)"}
- assuming \eqref{hyps} as induction hypotheses. By Property~\ref{avoiding} we
+ 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)) \<sharp>* r"}
+ @{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}
- @{text "Let (q \<bullet> p) (q \<bullet> t) = Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t))"}
+ \begin{tabular}{l}
+ @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
+ \hspace{15mm}@{text "Let (r \<bullet>\<^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)"}, we are can equally
+ So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally
establish
\begin{center}
- @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (r \<bullet> (q \<bullet> t)))"}
+ @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}
\end{center}
\noindent
To do so, we will use the implication \eqref{strong} of the strong induction
principle, which requires us to discharge
- the following three proof obligations:
+ the following four proof obligations:
\begin{center}
\begin{tabular}{rl}
{\it i)} & @{text "set (bn (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
{\it ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
- {\it iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t))"}\\
+ {\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
- second and third from the induction hypotheses in \eqref{hyps} (in the latter case
- we have to use the fact that @{term "(r \<bullet> (q \<bullet> t)) = (r + q) \<bullet> t"}).
+ 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 strong induction principle derives from
the weak induction principle. At the moment we can derive the difficult cases of
the strong induction principles only by hand, but they are very schematically
- so that with little effort we can even derive the strong induction principle for
+ so that with little effort we can even derive them for
Core-Haskell given in Figure~\ref{nominalcorehas}.
*}
@@ -1930,8 +1936,8 @@
approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist
of two numbers, one referring to the place where a variable is bound and the
other to which variable is bound. The reasoning infrastructure for both
- representations of bindings comes for free in the theorem provers Isabelle/HOL and
- Coq, for example, as the corresponding term-calculi can be implemented as ``normal''
+ representations of bindings comes for free in the theorem provers, like Isabelle/HOL or
+ Coq, as the corresponding term-calculi can be implemented as ``normal''
datatypes. However, in both approaches it seems difficult to achieve our
fine-grained control over the ``semantics'' of bindings (i.e.~whether the
order of binders should matter, or vacuous binders should be taken into
@@ -1980,7 +1986,7 @@
Because of how we set up our definitions, we had to impose restrictions,
like excluding overlapping deep binders, that are not present in Ott. Our
expectation is that we can still cover many interesting term-calculi from
- programming language research, for example Core-Haskell. For prviding support
+ programming language research, for example Core-Haskell. For providing support
of neat features in Ott, such as subgrammars, the existing datatype
infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the
other hand, we are not aware that Ott can make the distinction between our
@@ -2058,7 +2064,7 @@
This suggest there should be an approriate notion of alpha-equivalence.
Another interesting line of investigation is whether we can go beyond the
- simple-minded form of binding function we adopted from Ott. At the moment, binding
+ simple-minded form for binding functions that we adopted from Ott. At the moment, binding
functions can only return the empty set, a singleton atom set or unions
of atom sets (similarly for lists). It remains to be seen whether
properties like \eqref{bnprop} provide us with means to support more interesting