# HG changeset patch # User Christian Urban # Date 1300146039 -3600 # Node ID 56b8d977d1c00041ce00454e306c0cf3a2979cb6 # Parent 7085ab735de77a94cc35bd01bcd37e6bcefc73b0 more on the pearl paper diff -r 7085ab735de7 -r 56b8d977d1c0 Nominal/Atoms.thy --- a/Nominal/Atoms.thy Mon Mar 14 16:35:59 2011 +0100 +++ b/Nominal/Atoms.thy Tue Mar 15 00:40:39 2011 +0100 @@ -80,6 +80,25 @@ This does not work for multi-sorted atoms. *} +(* fixme +lemma supp_of_finite_name_set: + fixes S::"name set" + assumes "infinte S" "infinite (UNIV - S)" + shows "supp S = UNIV" +proof - + { fix a + have "a \ supp S" + proof (cases "a \ atom ` S") + assume "a \ atom ` S" + then have "\b \ UNIV - S. (a \ atom b) \ S \ S" + apply(clarify) + + show "a \ supp S" + } + then show "supp S = UNIV" by auto +qed +*) + section {* Automatic instantiation of class @{text at}. *} diff -r 7085ab735de7 -r 56b8d977d1c0 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Mon Mar 14 16:35:59 2011 +0100 +++ b/Pearl-jv/Paper.thy Tue Mar 15 00:40:39 2011 +0100 @@ -90,8 +90,7 @@ by applying the inverse permutation. A corresponding inverse substitution might not always exist, since renaming substitutions are in general only injective. Another reason is that permutations preserve many constructions when reasoning about syntax. - For example the validity of a typing context is preserved under any permutation. - Suppose a typing context @{text "\"} of the form + For example, suppose a typing context @{text "\"} of the form \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "x\<^isub>1:\\<^isub>1, \, x\<^isub>n:\\<^isub>n"} @@ -99,9 +98,9 @@ \noindent is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} - occur twice. Then validity is preserved under - permutations in the sense that if @{text \} is valid then so is @{text "\ \ \"} for - all permutations @{text "\"}. This is again \emph{not} the case for arbitrary + occur twice. Then validity of typing contexts is preserved under + permutations in the sense that if @{text \} is valid then so is \mbox{@{text "\ \ \"}} for + all permutations @{text "\"}. Again, this is \emph{not} the case for arbitrary renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \}. Permutations also behave uniformly with respect to HOL's logic connectives. @@ -118,9 +117,9 @@ This uniform behaviour can also be extended to quantifiers and functions. Because of these good properties of permutations, we are able to automate reasoning to do with \emph{equivariance}. By equivariance we mean the property - that every permutation leaves an object unchanged, that is @{term "\ \ x = x"} + that every permutation leaves a function unchanged, that is @{term "\ \ f = f"} for all @{text "\"}. This will often simplify arguments involving support - and functions, since equivariant objects have empty support---or + of functions, since if they are equivariant then they have empty support---or `no free atoms'. There are a number of subtle differences between the nominal logic work by @@ -158,7 +157,7 @@ text {* The two most basic notions in the nominal logic work are a countably - infinite collection of sorted atoms and sort-respecting permutations. + infinite collection of sorted atoms and sort-respecting permutations of atoms. The existing nominal logic work usually leaves implicit the sorting information for atoms and as far as we know leaves out a description of how sorts are represented. In our formalisation, we @@ -182,8 +181,8 @@ for their variables.} The use of type \emph{string} for sorts is merely for convenience; any countably infinite type would work as well. The set of all atoms we shall write as @{term "UNIV::atom set"}. - We have two - auxiliary functions @{text sort} and @{const nat_of} that are defined as + We have two auxiliary functions for atoms, namely @{text sort} + and @{const nat_of} which are defined as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} @@ -236,7 +235,7 @@ consider what happens if a user states a swapping of atoms with different sorts. The following definition\footnote{To increase legibility, we omit here and in what follows the @{term Rep_perm} and @{term "Abs_perm"} - wrappers that are needed in our implementation since we defined permutation + wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation not to be the full function space, but only those functions of type @{typ perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.} @@ -317,8 +316,19 @@ nominal theory as smoothly as possible in Isabelle/HOL, we tolerate the non-standard notation in order to reuse the existing libraries. - In order to reason abstractly about permutations, we use Isabelle/HOL's - type classes~\cite{Wenzel04} and state the following two + + A permutation operation, written @{text "\ \ x"}, applies a permutation + @{text "\"} to an object @{text "x"}. This operation has the generic type + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "_ \ _ :: perm \ \ \ \"} + \end{isabelle} + + \noindent + and Isabelle/HOL will allow us to give a definition of this operation for + `base' types, such as booleans and atoms, and for type-constructors, such as + products and lists. In order to reason abstractly about this operation, + we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two \emph{permutation properties}: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -331,9 +341,10 @@ \noindent The use of type classes allows us to delegate much of the routine resoning involved in determining whether these properties are satisfied to Isabelle/HOL's type system: - we only have to establish that `base' types, such as @{text booleans} and - @{text atoms}, satisfy them and that type-constructors, such as products and lists, - preserve them. For this we define + 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 permutation properties. + For this we define the notion of a \emph{permutation type}: \begin{definition}[Permutation type] A type @{text "\"} is a \emph{permutation type} if the permutation @@ -368,7 +379,26 @@ \end{isabelle} \noindent - In order to lift the permutation operation to other types, we can define for: + We can also show that the following property holds for any permutation type. + + \begin{lemma}\label{permutecompose} + Given @{term x} is of permutation type, then + @{text "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}. + \end{lemma} + + \begin{proof} The proof is as follows: + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} + & @{text "\\<^isub>1 \ \\<^isub>2 \ x"}\\ + @{text "="} & @{text "\\<^isub>1 \ \\<^isub>2 \ (-\\<^isub>1) \ \\<^isub>1 \ x"} & by \eqref{cancel}\\ + @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2 - \\<^isub>1) \ (\\<^isub>1 \ x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ + @{text "\"} & @{text "(\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}\\ + \end{tabular}\hfill\qed + \end{isabelle} + \end{proof} + + \noindent + Next we define the permutation operation for some types: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} @@ -385,7 +415,7 @@ \end{isabelle} \noindent - and then establish: + and establish: \begin{theorem} If @{text \}, @{text "\\<^isub>1"} and @{text "\\<^isub>2"} are permutation types, @@ -420,47 +450,29 @@ \noindent which is a simple consequence of the definition and the cancellation property in \eqref{cancel}. - We can also show that the following property holds for any permutation type. - - \begin{lemma}\label{permutecompose} - Given @{term x} is of permutation type, then - @{text "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}. - \end{lemma} - - \begin{proof} The proof is as follows: - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} - & @{text "\\<^isub>1 \ \\<^isub>2 \ x"}\\ - @{text "="} & @{text "\\<^isub>1 \ \\<^isub>2 \ (-\\<^isub>1) \ (\\<^isub>1 \ x)"} & by \eqref{cancel}\\ - @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2 - \\<^isub>1) \ (\\<^isub>1 \ x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ - @{text "\"} & @{text "(\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"}\\ - \end{tabular}\hfill\qed - \end{isabelle} - \end{proof} - *} section {* Equivariance *} text {* An important notion in the nominal logic work is \emph{equivariance}. - An equivariant function is one that is invariant under - permutations of atoms. This notion can be defined - uniformly as follows: + An equivariant function is one that is invariant under the + permutation operation. This notion can be defined + uniformly for all constants in HOL as follows: \begin{definition}[Equivariance]\label{equivariance} - A function @{text f} is \emph{equivariant} if @{term "\\. \ \ f = f"}. + A constant @{text c} is \emph{equivariant} if @{term "\\. \ \ c = c"}. \end{definition} \noindent There are a number of equivalent formulations for the equivariance property. - For example, assuming @{text f} is of type @{text "\ \ \"}, then equivariance + For example, assuming @{text c} is of type @{text "\ \ \"}, then equivariance can also be stated as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} - @{text "\\ x. \ \ (f x) = f (\ \ x)"} + @{text "\\ x. \ \ (c x) = c (\ \ x)"} \end{tabular}\hfill\numbered{altequivariance} \end{isabelle} @@ -484,8 +496,10 @@ \noindent using the permutation operation on booleans and property \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the permutation operation is - equivariant. It is also easy to see that the boolean operators, like - @{text "\"}, @{text "\"}, @{text "\"} and @{text "\"} are all equivariant. Furthermore + equivariant. The permutation operation for lists and products, shown in \eqref{permdefs}, + state that the constructors for products, @{text "Nil"} and @{text Cons} are equivariant. Also + the booleans @{const True} and @{const False} are equivariant by the permutation + operation. Furthermore a simple calculation will show that our swapping functions are equivariant, that is \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -495,13 +509,61 @@ \end{isabelle} \noindent - for all @{text a}, @{text b} and @{text \}. + for all @{text a}, @{text b} and @{text \}. + It is also easy to see that the boolean operators, like + @{text "\"}, @{text "\"}, @{text "\"} and @{text "\"} are all equivariant. + + In contrast, the equation in Definition~\ref{equivariance} together with the permutation + operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel} + leads to a simple rewrite system that pushes permutations inside a term until they reach + either function constants or variables. The permutations in front of + equivariant constants disappear. This helps us to establish equivariance + for any notion in HOL that is defined in terms of more primitive notions. To + see this let us define \emph{HOL-terms}. They are given by the grammar + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \x. t"} + \hfill\numbered{holterms} + \end{isabelle} + + \noindent + whereby @{text c} stands for constants. 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. + With these definitions in place we can define the notion of an \emph{equivariant} + HOL-term - In contrast, Definition~\ref{equivariance} together with the permutation - operation for functions and \eqref{permutefunapp} lead to a simple - rewrite system that pushes permutations inside a term until they reach - either function constants or variables. The permutations in front of - equivariant functions disappear. Such a rewrite system is often very helpful + \begin{definition}[Equivariant HOL-term] + A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, + abstractions and equivariant constants only. + \end{definition} + + \noindent + For equivariant terms we have + + \begin{lemma} + For an equivariant HOL-term @{text "t"}, @{term "\ \ t = t"} for all permutations @{term "\"}. + \end{lemma} + + \begin{proof} + By induction on the grammar of HOL-terms. The case for variables cannot arise since + equivariant HOL-terms are closed. The case for constants is clear by Definition + \ref{equivariance}. The case for applications is also straightforward since by + \eqref{permutefunapp} we have @{term "\ \ (t\<^isub>1 t\<^isub>2) = (\ \ t\<^isub>1) (\ \ t\<^isub>2)"}. + For the case of abstractions we can reason as follows + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} + & @{text "\ \ (\x. t)"}\\ + @{text "\"} & @{text "\y. \ \ ((\x. t) ((-\) \ y))"} & by \eqref{permdefs}\\ + + \end{tabular}\hfill\qed + \end{isabelle} + \end{proof} + + database of equivariant functions + + Such a rewrite system is often very helpful in determining whether @{text "\ \ t = t"} holds for a compound term @{text t}. ??? *} diff -r 7085ab735de7 -r 56b8d977d1c0 Pearl-jv/document/root.bib --- a/Pearl-jv/document/root.bib Mon Mar 14 16:35:59 2011 +0100 +++ b/Pearl-jv/document/root.bib Tue Mar 15 00:40:39 2011 +0100 @@ -33,7 +33,7 @@ @InProceedings{AydemirBohannonWeirich07, author = {B.~Aydemir and A.~Bohannon and S.~Weihrich}, title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)}, - booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages: + booktitle = {Proc.~of the 2st International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)}, pages = {69--77}, year = {2007}, diff -r 7085ab735de7 -r 56b8d977d1c0 Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Mon Mar 14 16:35:59 2011 +0100 +++ b/Pearl-jv/document/root.tex Tue Mar 15 00:40:39 2011 +0100 @@ -38,9 +38,9 @@ binding based on the notions of atoms, permutations and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case Isabelle/HOL. For this we have to formulate the -theory so that it is compatible with HOL, which the original formulation by -Pitts is not. We achieve this by not requiring that every object in our -discourse has finite support. We present a formalisation that is based on a +theory so that it is compatible with Higher-Order Logic, which the original formulation by +Pitts is not. We achieve this by not requiring that every construction has +to have finite support. We present a formalisation that is based on a unified atom type and that represents permutations by bijective functions from atoms to atoms. Interestingly, we allow swappings, which are permutations build from two atoms, to be ill-sorted. We also describe a formalisation of