nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:2cb34b1e7e19
+:8412c7e503d4
 @{text "For a finite set of atoms S, there exists an atom a such that
 sort a = s and a \<notin> S"}.
 \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
 identity on all atoms, except a finite number of them; and map
 each atom to one of the same sort. These properties can be conveniently stated
 @{text x} is a constant, but of course there is no way in
 Isabelle/HOL to restrict this definition to just these cases.
 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}
 @{text "\<forall>\<pi> x.  \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
 \end{tabular}\hfill\numbered{altequivariance}
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "\<pi> \<bullet> (\<forall>x. P x)  \<equiv>  \<pi> \<bullet> (P = (\<lambda>x. True))  =  ((\<pi> \<bullet> P) = (\<lambda>x. True))  \<equiv>  \<forall>x. (\<pi> \<bullet> P) x"}
 \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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "\<exists>x. P x \<equiv> "}~@{thm (rhs) Ex_def[no_vars]}
 \noindent
 with all constants on the right-hand side being equivariant. With this kind
 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'"}
 \end{isabelle}
 four `oriented' equations. We will first give a naive version of
 this tactic, which however in some cornercases produces incorrect
 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}
 i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
 ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & \rrh & @{text "\<lambda>x. \<pi> \<bullet> (t[x :=  (-\<pi>) \<bullet> x])"}\\
 {\rm @{term "c"}\hspace{6mm}provided @{text c} is equivariant}\\
 \end{tabular}\hfill\numbered{rewriteapplam}
 \end{isabelle}
 \noindent
-A permutation @{text \<pi>} can be pushed into applications and abstractions as follows
+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 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
+The third is a consequence of \eqref{cancel} and the fourth from
-following two equations
+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
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we
-\begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
+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
-\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
 constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
 reduction sequence
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \end{tabular}
 \end{isabelle}
 \noindent
-The last term is again an instance of rewrite rule {\it i}), but the term
+where the last term is again an instance of rewrite rule {\it i}), but bigger.
-is bigger.  To avoid this loop we need to apply our rewrite rule
+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.
 Another problem we have to avoid is that the rules {\it i)} and {\it
 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
+"\<lambda>x. x"}, as is desired---since there is no free variable in the original
-term and so the permutation should completely vanish. However, the
+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>
+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
+\<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
+apply rule {\it iii)} anymore in order to eliminate the permutation.
-introduce shortly increased. On the other hand, if we had started
+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
+completely and thus violating our correctness property. The problem is that
-instances where the variable is to bound; for free variables we want
+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
 the way how conversion tactics are implemented in Isabelle/HOL.
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}
 \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}
 i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & \rrh &
 @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\
 \hspace{6mm}{\rm provided @{text c} is equivariant}\\
 \end{tabular}
 \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
 of a term (counting terms of the form @{text "unpermute \<pi> x"} as
 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 _"}.
+in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
-We need the following technical notion characterising a \emph{@{text "\<pi>"}-proper} HOL-term
+We need the following technical notion characterising \emph{@{text "\<pi>"}-proper} HOL-terms
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}ll}
 $\bullet$ & variables and constants are @{text \<pi>}-proper,\\
 $\bullet$ & @{term "unpermute \<pi> x"} is @{text \<pi>}-proper,\\

changeset 2783	8412c7e503d4
parent 2776	8e0f0b2b51dd
child 2821	c7d4bd9e89e0