nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:d19bfc6e7631
+:5f3387b7474f
 This function is bijective, the identity on all atoms except
 @{text a} and @{text b}, and sort respecting. Therefore it is
 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}
 @{thm swap_commute[no_vars]}\hspace{10mm}
 @{text "(a a) = id"}
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \end{isabelle}
 \noindent
-whereby @{text "\<beta>"} is a generic type for @{text x}. The definition of this operation will be
+whereby @{text "\<beta>"} 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:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \end{isabelle}
 \end{proof}
 \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 "\<pi> \<bullet> (f x) ="}
 @{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]}
 \hfill\numbered{permutefunapp}
 \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}.
 The main benefit of the use of type classes is that it allows us to delegate
 much of the routine resoning involved in determining whether the permutation properties
 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 \<Rightarrow> (atom set * nat)"}, satisfies the
 permutation properties.  For this we define the notion of a
 \emph{permutation type}:
 \begin{definition}[Permutation type]
 A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
 @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"}
 \hfill\numbered{holterms}
 \end{isabelle}
 \noindent
-where @{text c} stands for constants and @{text x} for
+where @{text c} stands for constants and @{text x} for variables.
-variables.
+We assume HOL-terms are fully typed, but for the sake of greater
-We assume HOL-terms are fully typed, but for the sake of
+legibility we leave the typing information implicit.  We also assume
-greater legibility we leave the typing information implicit.  We
+the usual notions for free and bound variables of a HOL-term.
-also assume the usual notions for free and bound variables of a
+Furthermore, HOL-terms are regarded as equal modulo alpha-, beta-
-HOL-term.  Furthermore, it is custom in HOL to regard terms as equal
+and eta-equivalence.  Statements in HOL are HOL-terms of type @{text
-modulo alpha-, beta- and eta-equivalence.
+"bool"}.
 An \emph{equivariant} HOL-term is one that is invariant under the
 permutation operation. This can be defined in Isabelle/HOL
 as follows:
 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 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
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \end{isabelle}
 \noindent
 for all @{text a}, @{text b} and @{text \<pi>}. Also the booleans
 @{const True} and @{const False} are equivariant by the definition
-of the permutation operation for booleans. It is easy to see
+of the permutation operation for booleans. Given this definition, it
-that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text
+is also easy to see that the boolean operators, like @{text "\<and>"},
-"\<not>"} and @{text "\<longrightarrow>"}, are equivariant too; for example we have
+@{text "\<or>"}, @{text "\<longrightarrow>"} and  @{text "\<not>"} are equivariant too:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}lcl}
 @{text "\<pi> \<bullet> (A \<and> B) = (\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\
+@{text "\<pi> \<bullet> (A \<or> B) = (\<pi> \<bullet> A) \<or> (\<pi> \<bullet> B)"}\\
 @{text "\<pi> \<bullet> (A \<longrightarrow> B) = (\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\
+@{text "\<pi> \<bullet> (\<not>A) = \<not>(\<pi> \<bullet> 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
+it leads to rewrite system that allows us to
-towards the leaves of a HOL-term (i.e.~constants and
+`push' a permutation towards the leaves of a HOL-term
-variables).  Then the permutation disappears in cases where the
+(i.e.~constants and variables).  Then the permutation disappears in
-constants are equivariant. We have implemented this rewrite system
+cases where the constants are equivariant. This can be stated more
-as a simplification tactic on the ML-level of Isabelle/HOL.  Having this tactic
+formally as the following \emph{equivariance principle}:
-at our disposal, together with a collection of constants for which
-equivariance is already established, we can automatically establish
+\begin{theorem}[Equivariance Principle]\label{eqvtprin}
-equivariance of a constant for which equivariance is not yet known. For this we only have to
+Suppose a HOL-term @{text t} whose constants are all equivariant. For any
-make sure that the definiens of this constant
+permutation @{text \<pi>}, let @{text t'} be the HOL-term @{text t} except every
-is a HOL-term whose constants are all equivariant.  In what follows
+free variable @{text x} in @{term t} is replaced by @{text "\<pi> \<bullet> x"}, then
-we shall specify this tactic and argue that it terminates and
+@{text "\<pi> \<bullet> t = t'"}.
-is correct (in the sense of pushing a
+\end{theorem}
-permutation @{text "\<pi>"} inside a term and the only remaining
-instances of @{text "\<pi>"} are in front of the term's free variables).
+\noindent
+The significance of this principle is that we can automatically establish
-The simplifiaction tactic is a rewrite systems consisting of four `oriented'
+the equivariance of a constant for which equivariance is not yet
-equations. We will first give a naive version of this tactic, which however
+known. For this we only have to make sure that the definiens of this
-is in some cornercases incorrect and does not terminate, and then modify
+constant is a HOL-term whose constants are all equivariant. For example
-it in order to obtain the desired properties. A permutation @{text \<pi>} can
+the universal quantifier @{text "All"}, also written @{text "\<forall>"}, is
-be pushed into applications and abstractions as follows
+of type @{text "(\<alpha> \<Rightarrow> bool) \<Rightarrow> 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 "\<pi> \<bullet> (All P)   \<equiv>   \<pi> \<bullet> (P = (\<lambda>x. True))   =   ((\<pi> \<bullet> P) = (\<lambda>x. True))   \<equiv>   All (\<pi> \<bullet> P)"}
+\end{isabelle}
+\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 "\<exists>"}, 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 "\<forall>"} and @{text "\<longrightarrow>"}). 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 "\<pi> \<cdot> t = ... = t'"}
+\end{isabelle}
+\noindent
+that establish the equality between @{term "\<pi> \<bullet> 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 "\<pi>"} inside a
+term and the only remaining instances of @{text "\<pi>"} 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 \<pi>} can be pushed into
+applications and abstractions as follows
 \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])"}\\
 property \emph{equivariance principle} (book ref ???). In our
 setting the precise statement of this property is a slightly more
 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 \<pi>}, let @{text t'}
-be the HOL-term @{text t} except every free variable @{text x} in @{term t} is
-replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> t = t'"}.
-\end{theorem}
 With these definitions in place we can define the notion of an \emph{equivariant}
 HOL-term

changeset 2775	5f3387b7474f
parent 2772	c3ff26204d2a
child 2776	8e0f0b2b51dd