# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1302305380 -3600 # Node ID cdc96d79bbba589fc6b804743f35d4279b1f31b3 # Parent a6b4d9629b1c9c953faa2c028dd1c3527becfb8a# Parent 2ef9f2d61b148a6d36be360355a62e8215d4eea5 tuned paper diff -r 2ef9f2d61b14 -r cdc96d79bbba Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Sat Apr 09 02:10:49 2011 +0800 +++ b/Pearl-jv/Paper.thy Sat Apr 09 00:29:40 2011 +0100 @@ -473,8 +473,9 @@ text {* An important notion in the nominal logic work is - \emph{equivariance}. To give a definition for this notion, let us - define \emph{HOL-terms}. They are given by the grammar + \emph{equivariance}. In order to prove properties about this notion, + let us first define \emph{HOL-terms}. They are given + by the grammar \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"} @@ -482,22 +483,23 @@ \end{isabelle} \noindent - whereby @{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. + whereby @{text c} stands for constant symbols, or short 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. An equivariant HOL-term is one that is invariant under the - permutation operation. This notion can be defined as follows: + permutation operation. This notion can be defined in Isabelle/HOL + as follows: \begin{definition}[Equivariance]\label{equivariance} - A HOL-term @{text t} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> t = t"}. + A HOL-term @{text t} with permutation type is \emph{equivariant} provided + @{term "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}. \end{definition} \noindent There are a number of equivalent formulations for the equivariance - property. For example, assuming @{text t} is of type @{text "\<alpha> \<Rightarrow> + property. For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance can also be stated as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -528,7 +530,8 @@ \noindent using the permutation operation on booleans and property - \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the + \eqref{permuteequ}. + Lemma~\ref{permutecompose} establishes that the permutation operation is equivariant. The permutation operation for lists and products, shown in \eqref{permdefs}, state that the constructors for products, @{text "Nil"} and @{text Cons} are @@ -546,7 +549,7 @@ @{const True} and @{const False} are equivariant by the definition of the permutation operation for booleans. It is also easy to see that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text - "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. + "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro) In contrast, the advantage of Definition \ref{equivariance} is that it leads to a simple rewrite system. Consider the following oriented