--- a/Pearl-jv/Paper.thy Tue May 10 17:10:22 2011 +0100
+++ b/Pearl-jv/Paper.thy Fri May 13 14:50:17 2011 +0100
@@ -223,7 +223,7 @@
\end{proposition}
\noindent
- This property will be used later on whenever we have to chose a `fresh' atom.
+ This property will be used later whenever we have to chose a `fresh' atom.
For implementing sort-respecting permutations, we use functions of type @{typ
"atom => atom"} that are bijective; are the
@@ -520,7 +520,7 @@
There are a number of equivalent formulations for the equivariance
property. For example, assuming @{text f} is a function of permutation
- type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance can also be stated as
+ type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} can also be stated as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -633,7 +633,7 @@
\end{isabelle}
\noindent
- and consequently, the constant @{text "\<forall>"} must be equivariant. From this
+ which means the constant @{text "\<forall>"} must be equivariant. From this
we can deduce that the existential quantifier @{text "\<exists>"} is equivariant.
Its definition in HOL is
@@ -656,7 +656,9 @@
of reasoning we can build up a database of equivariant constants.
Before we proceed, let us give a justification for the equivariance principle.
- For this we will use a rewrite system consisting of a series of equalities
+ This justification cannot be given directly inside Isabelle/HOL since we cannot
+ prove any statement about HOL-terms. Instead, we will use a rewrite
+ system consisting of a series of equalities
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "\<pi> \<cdot> t = ... = t'"}
@@ -676,7 +678,7 @@
results or does not terminate. We then give a modification in order
to obtain the desired properties.
- Consider the following oriented equations
+ Consider the following for oriented equations
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
@@ -689,27 +691,16 @@
\end{isabelle}
\noindent
- A permutation @{text \<pi>} can be pushed into applications and abstractions as follows
-
- The first equation we established in \eqref{permutefunapp};
+ These equation are oriented in the sense of being applied in the left-to-right
+ direction. The first equation we established in \eqref{permutefunapp};
the second follows from the definition of permutations acting on functions
and the fact that HOL-terms are equal modulo beta-equivalence.
- Once the permutations are pushed towards the leaves, we need the
- following two equations
-
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
-
- \end{tabular}\hfill\numbered{rewriteother}
- \end{isabelle}
-
- \noindent
- in order to remove permuations in front of bound variables and
- equivariant constants. Unfortunately, we have to be careful with
- the rules {\it i)} and {\it iv}): they can lead to a loop whenever
- \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}, where
- we do not write the permutation operation infix, as usual, but
- as an application. Recall that we established in Lemma \ref{permutecompose} that the
+ The third is a consequence of \eqref{cancel} and the fourth from
+ Definition~\ref{equivariance}. Unfortunately, we have to be careful with
+ the rules {\it i)} and {\it iv}) since they can lead to a loop whenever
+ \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we
+ deviate here from our usual convention of writing the permutation operation infix,
+ instead as an application.} Recall that we established in Lemma \ref{permutecompose} that the
constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
reduction sequence
@@ -725,8 +716,8 @@
\end{isabelle}
\noindent
- The last term is again an instance of rewrite rule {\it i}), but the term
- is bigger. To avoid this loop we need to apply our rewrite rule
+ where the last term is again an instance of rewrite rule {\it i}), but bigger.
+ To avoid this loop we will apply the rewrite rule
using an `outside to inside' strategy. This strategy is sufficient
since we are only interested of rewriting terms of the form @{term
"\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.
@@ -735,18 +726,20 @@
iii)} can `overlap'. For this note that the term @{term "\<pi>
\<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to
which we can apply rule {\it iii)} in order to obtain @{term
- "\<lambda>x. x"}, as is desired---there is no free variable in the original
- term and so the permutation should completely vanish. However, the
+ "\<lambda>x. x"}, as is desired---since there is no free variable in the original
+ term. the permutation should completely vanish. However, the
subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,
- the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi>
- \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}. Given our strategy we cannot
- apply rule {\it iii)} anymore and even worse the measure we will
- introduce shortly increased. On the other hand, if we had started
+ the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can also reduce to @{text "\<lambda>x. (- (\<pi>
+ \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}. Given our strategy, we cannot
+ apply rule {\it iii)} anymore in order to eliminate the permutation.
+ In contrast, if we start
with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"} where @{text \<pi>} and @{text
x} are free variables, then we \emph{do} want to apply rule {\it i)}
+ in order to obtain @{text "(\<pi> \<bullet> (- \<pi>)) \<bullet> (\<pi> \<bullet> x)"}
and not rule {\it iii)}. The latter would eliminate @{text \<pi>}
- completely. The problem is that rule {\it iii)} should only apply to
- instances where the variable is to bound; for free variables we want
+ completely and thus violating our correctness property. The problem is that
+ rule {\it iii)} should only apply to
+ instances where the corresponding variable is to bound; for free variables we want
to use {\it ii)}. In order to distinguish these cases we have to
maintain the information which variable is bound when inductively
taking a term `apart'. This, unfortunately, does not mesh well with
@@ -761,7 +754,7 @@
\end{isabelle}
\noindent
- The point is that now we can formulate the rewrite rules as follows
+ The point is that now we can re-formulate the rewrite rules as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lrcl}
@@ -776,9 +769,10 @@
\end{isabelle}
\noindent
- and @{text unpermutes} are only generated in case of bound variables.
+ where @{text unpermutes} are only generated in case of bound variables.
Clearly none of these rules overlap. Moreover, given our
- outside-to-inside strategy, they terminate. To see this, notice that
+ outside-to-inside strategy, applying them repeatedly must terminate.
+To see this, notice that
the permutation on the right-hand side of the rewrite rules is
always applied to a smaller term, provided we take the measure consisting
of lexicographically ordered pairs whose first component is the size
@@ -786,15 +780,15 @@
leaves) and the second is the number of occurences of @{text
"unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.
- With the rules of the conversions tactic in place, we can
+ With the rewrite rules of the conversions tactic in place, we can
establish its correctness. The property we are after is that
for a HOL-term @{text t} whose constants are all equivariant the
term \mbox{@{text "\<pi> \<bullet> t"}} is equal to @{text "t'"} with @{text "t'"}
being equal to @{text t} except that every free variable @{text x}
in @{text t} is replaced by \mbox{@{text "\<pi> \<bullet> x"}}. Let us call
a variable @{text x} \emph{really free}, if it is free and not occuring
- in an unpermute, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
- We need the following technical notion characterising a \emph{@{text "\<pi>"}-proper} HOL-term
+ in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
+ We need the following technical notion characterising \emph{@{text "\<pi>"}-proper} HOL-terms
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}ll}