diff -r d19bfc6e7631 -r 5f3387b7474f Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Mon May 02 13:01:02 2011 +0800 +++ b/Pearl-jv/Paper.thy Wed May 04 15:27:04 2011 +0800 @@ -290,7 +290,7 @@ a function in @{typ perm}. One advantage of using functions as a representation for - permutations is that it is unique. For example the swappings + permutations is that it is a unique representation. For example the swappings \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -352,7 +352,7 @@ \end{isabelle} \noindent - whereby @{text "\"} is a generic type for @{text x}. The definition of this operation will be + whereby @{text "\"} is a generic type for the object @{text x}. 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, such as atoms, permutations, booleans and natural numbers: @@ -435,7 +435,7 @@ \noindent Note that the permutation operation for functions is defined so that - we have for applications the property + we have for applications the equation \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "\ \ (f x) ="} @@ -444,7 +444,7 @@ \end{isabelle} \noindent - whenever the permutation properties hold for @{text x}. This property can + whenever the permutation properties hold for @{text x}. This equation can be easily shown by unfolding the permutation operation for functions on the right-hand side, simplifying the beta-redex and eliminating the permutations in front of @{text x} using \eqref{cancel}. @@ -454,7 +454,7 @@ are satisfied to Isabelle/HOL's type system: we only have to establish that base types satisfy them and that type-constructors preserve them. Isabelle/HOL will use this information and determine - whether an object @{text x} with a compound type satisfies the + whether an object @{text x} with a compound type, like @{typ "atom \ (atom set * nat)"}, satisfies the permutation properties. For this we define the notion of a \emph{permutation type}: @@ -506,13 +506,13 @@ \end{isabelle} \noindent - where @{text c} stands for constants and @{text x} for - variables. - We assume HOL-terms are fully typed, but for the sake of - greater legibility we leave the typing information implicit. We - also assume the usual notions for free and bound variables of a - HOL-term. Furthermore, it is custom in HOL to regard terms as equal - modulo alpha-, beta- and eta-equivalence. + where @{text c} stands for constants and @{text x} for variables. + We assume HOL-terms are fully typed, but for the sake of greater + 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. Statements in HOL are HOL-terms of type @{text + "bool"}. An \emph{equivariant} HOL-term is one that is invariant under the permutation operation. This can be defined in Isabelle/HOL @@ -546,11 +546,11 @@ \eqref{cancel}. To see the other direction, we use \eqref{permutefunapp}. Similarly for HOL-terms that take more than one argument. The point to note is that equivariance and equivariance in fully - applied form are (for permutation types) always interderivable. + applied form are always interderivable (for permutation types). Both formulations of equivariance have their advantages and disadvantages: \eqref{altequivariance} is usually more convenient to - establish, since statements in Isabelle/HOL are commonly given in a + establish, since statements in HOL are commonly given in a form where functions are fully applied. For example we can easily show that equality is equivariant @@ -579,41 +579,91 @@ \noindent for all @{text a}, @{text b} and @{text \}. Also the booleans @{const True} and @{const False} are equivariant by the definition - of the permutation operation for booleans. It is easy to see - that the boolean operators, like @{text "\"}, @{text "\"}, @{text - "\"} and @{text "\"}, are equivariant too; for example we have + of the permutation operation for booleans. Given this definition, it + is also easy to see that the boolean operators, like @{text "\"}, + @{text "\"}, @{text "\"} and @{text "\"} are equivariant too: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lcl} @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ + @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ @{text "\ \ (A \ B) = (\ \ A) \ (\ \ B)"}\\ + @{text "\ \ (\A) = \(\ \ A)"}\\ \end{tabular} \end{isabelle} - - \noindent - by the definition of the permutation operation acting on booleans. In contrast, the advantage of Definition \ref{equivariance} is that - it leads to a relatively simple rewrite system that allows us to `push' a permutation - towards the leaves of a HOL-term (i.e.~constants and - variables). Then the permutation disappears in cases where the - constants are equivariant. We have implemented this rewrite system - as a simplification tactic on the ML-level of Isabelle/HOL. Having this tactic - at our disposal, together with a collection of constants for which - equivariance is already established, we can automatically establish - equivariance of a constant for which equivariance is not yet known. For this we only have to - make sure that the definiens of this constant - is a HOL-term whose constants are all equivariant. In what follows - we shall specify this tactic and argue that it terminates and - is correct (in the sense of pushing a - permutation @{text "\"} inside a term and the only remaining - instances of @{text "\"} are in front of the term's free variables). + it leads to rewrite system that allows us to + `push' a permutation towards the leaves of a HOL-term + (i.e.~constants and variables). Then the permutation disappears in + cases where the constants are equivariant. This can be stated more + formally as the following \emph{equivariance principle}: + + \begin{theorem}[Equivariance Principle]\label{eqvtprin} + Suppose a HOL-term @{text t} whose constants are all equivariant. For any + permutation @{text \}, let @{text t'} be the HOL-term @{text t} except every + free variable @{text x} in @{term t} is replaced by @{text "\ \ x"}, then + @{text "\ \ t = t'"}. + \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 + constant is a HOL-term whose constants are all equivariant. For example + the universal quantifier @{text "All"}, also written @{text "\"}, is + of type @{text "(\ \ bool) \ bool"} and in HOL is definied as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm All_def[no_vars]} + \end{isabelle} + + \noindent + Now @{text All} must be equivariant, because by the equivariance + principle we only have to test whether the contants in the HOL-term + @{thm (rhs) All_def[no_vars]}, namely @{text "="} and @{text + "True"}, are equivariant. We shown this above. Taking all equations + together, we can establish + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\ \ (All P) \ \ \ (P = (\x. True)) = ((\ \ P) = (\x. True)) \ All (\ \ P)"} + \end{isabelle} - The simplifiaction tactic is a rewrite systems consisting of four `oriented' - equations. We will first give a naive version of this tactic, which however - is in some cornercases incorrect and does not terminate, and then modify - it in order to obtain the desired properties. A permutation @{text \} can - be pushed into applications and abstractions as follows + \noindent + where the equation in the `middle' is given by Theorem~\ref{eqvtprin}. + As a consequence, the constant @{text "All"} is equivariant. Given this + fact we can further show that the existential quantifier @{text Ex}, + written also as @{text "\"}, is equivariant, since it is defined as + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{thm Ex_def[no_vars]} + \end{isabelle} + + \noindent + and the HOL-term on the right-hand side contains equivariant constants only + (namely @{text "\"} and @{text "\"}). In this way we can establish step by step + equivariance for constants in HOL. + + In order to establish Theorem~\ref{eqvtprin}, we use a rewrite system + consisting of a series of equalities + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "\ \ t = ... = t'"} + \end{isabelle} + + \noindent + that establish the equality between @{term "\ \ t"} and @{text + "t'"}. We have implemented this rewrite system as a conversion + tactic on the ML-level of Isabelle/HOL. + We shall next specify this tactic and show that it terminates and is + correct (in the sense of pushing a permutation @{text "\"} inside a + term and the only remaining instances of @{text "\"} are in front of + the term's free variables). The tactic applies four `oriented' + equations. We will first give a naive version of this tactic, which + however in some cornercases produces incorrect resolts or does not + terminate. We then give a modification it in order to obtain the + desired properties. A permutation @{text \} can be pushed into + applications and abstractions as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l} @@ -732,12 +782,6 @@ involved because of the fact that @{text unpermutes} needs to be treated specially. - \begin{theorem}[Equivariance Principle] - Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all - its constants are equivariant. For any permutation @{text \}, let @{text t'} - be the HOL-term @{text t} except every free variable @{text x} in @{term t} is - replaced by @{text "\ \ x"}, then @{text "\ \ t = t'"}. - \end{theorem}