nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:77e1d9f2925e
+:c7d4bd9e89e0
 many proofs. There are a two main design choices to be made. One is
 how to represent sorted atoms. We opt here for a single unified atom
 type to represent atoms of different sorts. The other is how to
 present sort-respecting permutations. For them we use the standard
 technique of HOL-formalisations of introducing an appropriate
-substype of functions from atoms to atoms.
+subtype of functions from atoms to atoms.
 The nominal logic work has been the starting point for a number of proving
 infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
 Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban
 and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very
 \noindent
 and verify the four simple properties
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\smallskip\\
 ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
 iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
 iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]}
 \end{tabular}\hfill\numbered{grouplaws}
 \end{isabelle}
 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \end{isabelle}
 \noindent
 whereby @{text "\<beta>"} is a generic type for the object @{text
-x}.\footnote{We will use the standard notation @{text "((op \<bullet>) \<pi>)
+x}.\footnote{We will write @{text "((op \<bullet>) \<pi>)
 x"} for this operation in the few cases where we need to indicate
 that it is a function applied with two arguments.}  The definition
 of this operation will be given by in terms of `induction' over this
 generic type. The type-class mechanism of Isabelle/HOL
 \cite{Wenzel04} allows us to give a definition for `base' types,
 text {*
 Two important notions in the nominal logic work are what Pitts calls
 \emph{equivariance} and the \emph{equivariance principle}.  These
 notions allows us to characterise how permutations act upon compound
 statements in HOL by analysing how these statements are constructed.
-The notion of equivariance can defined as follows:
+The notion of equivariance means that an object is invariant under
+any permutations. This can be defined as follows:
 \begin{definition}[Equivariance]\label{equivariance}
 An object @{text "x"} of permutation type is \emph{equivariant} provided
 for all permutations @{text "\<pi>"}, \mbox{@{term "\<pi> \<bullet> x = x"}} holds.
 \end{definition}
 \noindent
 In what follows we will primarily be interested in the cases where
 @{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
+There are a number of equivalent formulations for equivariance.
-property.  For example, assuming @{text f} is a function of permutation
+For example, assuming @{text f} is a function of permutation
 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}
 \end{isabelle}
 \noindent
-We will call this formulation of equivariance in \emph{fully applied form}.
+We will say this formulation of equivariance is in \emph{fully applied form}.
 To see that this formulation implies the definition, we just unfold
 the definition of the permutation operation for functions and
 simplify with the equation and the cancellation property shown in
 \eqref{cancel}. To see the other direction, we use
 \eqref{permutefunapp}. Similarly for functions that take more than
 where @{text c} stands for constants and @{text x} for variables.
 We assume HOL-terms are fully typed, but for the sake of better
 legibility we leave the typing information implicit.  We also assume
 the usual notions for free and bound variables of a HOL-term.
 Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
-and eta-equivalence. The equivariance principle can now be stated
+and eta-equivalence. The equivariance principle can now
-formally as follows:
+be stated formally as follows:
 \begin{theorem}[Equivariance Principle]\label{eqvtprin}
 Suppose a HOL-term @{text t} whose constants are all equivariant. For any
 permutation @{text \<pi>}, let @{text t'} be @{text t} except every
 free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then
 \end{theorem}
 \noindent
 The significance of this principle is that we can automatically establish
 the equivariance of a constant for which equivariance is not yet
-known. For this we only have to make sure that the definiens of this
+known. For this we only have to establish that the definiens of this
-constant is a HOL-term whose constants are all equivariant. For example
+constant is a HOL-term whose constants are all equivariant.
-the universal quantifier @{text "\<forall>"} is definied in HOL as
+This meshes well with how HOL is designed: except for a few axioms, every constant
+is defined in terms of existing constants. For example an alternative way
+to deduce that @{term True} is equivariant is to look at its
+definition
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+@{thm True_def}
+\end{isabelle}
+\noindent
+and observing that the only constant in the definiens, namely @{text "="}, is
+equivariant. Similarly, the universal quantifier @{text "\<forall>"} is definied in HOL as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "\<forall>x. P x \<equiv> "}~@{thm (rhs) All_def[no_vars]}
 \end{isabelle}
 The constants in the definiens @{thm (rhs) All_def[no_vars]}, namely @{text "="}
 and @{text "True"}, are equivariant (we shown this above). Therefore
 the equivariance principle gives us
 \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"}
+\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{text "\<pi> \<bullet> (\<forall>x. P x)"} & @{text "\<equiv>"} & @{text "\<pi> \<bullet> (P = (\<lambda>x. True))"}\\
+& @{text "="} & @{text "(\<pi> \<bullet> P) = (\<lambda>x. True)"}\\
+& @{text "\<equiv>"} & @{text "\<forall>x. (\<pi> \<bullet> P) x"}
+\end{tabular}
 \end{isabelle}
 \noindent
 which means the constant @{text "\<forall>"} must be equivariant. From this
 we can deduce that the existential quantifier @{text "\<exists>"} is equivariant.
 @{text "\<exists>!x. P x \<equiv> "}~@{thm (rhs) Ex1_def[no_vars]}
 \end{isabelle}
 \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.
+of reasoning we can build up a database of equivariant constants, which will
+be handy for more complex calculations later on.
 Before we proceed, let us give a justification for the equivariance principle.
 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
 that establish the equality between @{term "\<pi> \<bullet> t"} and
 @{text "t'"}. The idea of the rewrite system is to push the
 permutation inside the term @{text t}. We have implemented this as a
 conversion tactic on the ML-level of Isabelle/HOL.  In what follows,
 we will show that this tactic produces only finitely many equations
-and also show that is correct (in the sense of pushing a permutation
+and also show that it is correct (in the sense of pushing a permutation
 @{text "\<pi>"} inside a term and the only remaining instances of @{text
-"\<pi>"} are in front of the term's free variables).  The tactic applies
+"\<pi>"} are in front of the term's free variables).
-four `oriented' equations. We will first give a naive version of
-this tactic, which however in some cornercases produces incorrect
+The tactic applies four `oriented' equations.
+We will first give a naive version of
+our tactic, which however in some corner cases produces incorrect
 results or does not terminate.  We then give a modification in order
 to obtain the desired properties.
 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)"}\\
 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.
 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
+the rules {\it i)} and {\it iv}) since they can lead to loops whenever
-\mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we
+\mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.
-deviate here from our usual convention of writing the permutation operation infix,
+Recall that we established in Lemma \ref{permutecompose} that the
-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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \end{tabular}
 \end{isabelle}
 \noindent
-where the last term is again an instance of rewrite rule {\it i}), but bigger.
+where the last term is again an instance of rewrite rule {\it i}), but larger.
 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---since there is no free variable in the original
+"\<lambda>x. x"}, as is desired: since there is no free variable in the original
-term. 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 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
 text {*
 While the use of functions as permutation provides us with a unique
 representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and
 @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation does
 not come automatically with an induction principle.  Such an
-induction principle is however handy for generalising
+induction principle is however useful for generalising
-Lemma~\ref{swapfreshfresh} from swappings to permutations
+Lemma~\ref{swapfreshfresh} from swappings to permutations, namely
 \begin{lemma}
-@{thm [mode=IfThen] perm_supp_eq[no_vars]}
+@{thm [mode=IfThen] perm_supp_eq[where p="\<pi>", no_vars]}
 \end{lemma}
 \noindent
 In this section we will establish an induction principle for permutations
 with which this lemma can be easily proved. It is not too difficult to derive
 permutations having a finite support.
 Using a the property from \cite{???}
 \begin{lemma}\label{smallersupp}
-@{thm [mode=IfThen] smaller_supp[no_vars]}
+@{thm [mode=IfThen] smaller_supp[where p="\<pi>", no_vars]}
 \end{lemma}
 *}
 section {* An Abstraction Type *}

changeset 2821	c7d4bd9e89e0
parent 2783	8412c7e503d4
child 2949	adf22ee09738