diff -r 77e1d9f2925e -r c7d4bd9e89e0 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Mon Jun 06 13:11:04 2011 +0100 +++ b/Pearl-jv/Paper.thy Tue Jun 07 08:52:59 2011 +0100 @@ -80,7 +80,7 @@ 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 @@ -323,7 +323,7 @@ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} - i)~~@{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\\ + i)~~@{thm add_assoc[where a="\\<^isub>1" and b="\\<^isub>2" and c="\\<^isub>3"]}\smallskip\\ ii)~~@{thm monoid_add_class.add_0_left[where a="\::perm"]} \hspace{9mm} iii)~~@{thm monoid_add_class.add_0_right[where a="\::perm"]} \hspace{9mm} iv)~~@{thm group_add_class.left_minus[where a="\::perm"]} @@ -357,7 +357,7 @@ \noindent whereby @{text "\"} is a generic type for the object @{text - x}.\footnote{We will use the standard notation @{text "((op \) \) + x}.\footnote{We will write @{text "((op \) \) 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 @@ -506,7 +506,8 @@ \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 @@ -518,8 +519,8 @@ @{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 + There are a number of equivalent formulations for equivariance. + For example, assuming @{text f} is a function of permutation type @{text "\ \ \"}, then equivariance of @{text f} can also be stated as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -529,7 +530,7 @@ \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 @@ -602,8 +603,8 @@ 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 - formally as follows: + and eta-equivalence. The equivariance principle can now + be stated formally as follows: \begin{theorem}[Equivariance Principle]\label{eqvtprin} Suppose a HOL-term @{text t} whose constants are all equivariant. For any @@ -615,9 +616,20 @@ \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 "\"} is definied in HOL as + known. For this we only have to establish that the definiens of this + constant is a HOL-term whose constants are all equivariant. + 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 "\"} is definied in HOL as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "\x. P x \ "}~@{thm (rhs) All_def[no_vars]} @@ -629,7 +641,11 @@ the equivariance principle gives us \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "\ \ (\x. P x) \ \ \ (P = (\x. True)) = ((\ \ P) = (\x. True)) \ \x. (\ \ P) x"} + \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{text "\ \ (\x. P x)"} & @{text "\"} & @{text "\ \ (P = (\x. True))"}\\ + & @{text "="} & @{text "(\ \ P) = (\x. True)"}\\ + & @{text "\"} & @{text "\x. (\ \ P) x"} + \end{tabular} \end{isabelle} \noindent @@ -653,7 +669,8 @@ \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 @@ -670,14 +687,15 @@ 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 "\"} 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 + "\"} are in front of the term's free variables). + + 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}\ \ \ \ \ \ \ \ \ \ %%% @@ -697,10 +715,9 @@ 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 - \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \) \') t"}.\footnote{Note we - 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 + 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 \) \') t"}. + Recall that we established in Lemma \ref{permutecompose} that the constant @{text "(op \)"} is equivariant and consider the infinite reduction sequence @@ -716,7 +733,7 @@ \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 @@ -726,8 +743,8 @@ iii)} can `overlap'. For this note that the term @{term "\ \(\x. x)"} reduces by {\it ii)} to @{term "\x. \ \ (- \) \ x"}, to which we can apply rule {\it iii)} in order to obtain @{term - "\x. x"}, as is desired---since there is no free variable in the original - term. the permutation should completely vanish. However, the + "\x. x"}, as is desired: since there is no free variable in the original + term, the permutation should completely vanish. However, the subterm @{text "(- \) \ x"} is also an application. Consequently, the term @{term "\x. \ \ (- \) \x"} can also reduce to @{text "\x. (- (\ \ \)) \ (\ \ x)"} using {\it i)}. Given our strategy, we cannot @@ -1222,11 +1239,11 @@ representation for permutations (for example @{term "(a \ b)"} and @{term "(b \ a)"} are equal permutations), this representation does not come automatically with an induction principle. Such an - induction principle is however handy for generalising - Lemma~\ref{swapfreshfresh} from swappings to permutations + induction principle is however useful for generalising + 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="\", no_vars]} \end{lemma} \noindent @@ -1238,7 +1255,7 @@ Using a the property from \cite{???} \begin{lemma}\label{smallersupp} - @{thm [mode=IfThen] smaller_supp[no_vars]} + @{thm [mode=IfThen] smaller_supp[where p="\", no_vars]} \end{lemma} *}