nominal2: comparison Pearl-jv/Paper.thy

equal deleted inserted replaced

-:d97e04126a3d
+:61d30863e5d1
 (*<*)
 theory Paper
 imports "../Nominal/Nominal2_Base"
-"../Nominal/Nominal2_Eqvt"
 "../Nominal/Atoms"
 "../Nominal/Nominal2_Abs"
 "LaTeXsugar"
 begin
 abbreviation
 "sort_ty \<equiv> sort_of_ty"
 (*>*)
-(*
-TODO: write about supp of finite sets, abstraction over finite sets
-*)
 section {* Introduction *}
 text {*
 Nominal Isabelle provides a proving infratructure for convenient reasoning
-about programming language calculi involving binders such as lambda abstractions or
+about programming language calculi involving binders, such as lambda abstractions or
 quantifications in type schemes:
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 @{text "\<lambda>x. t       \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
 \hfill\numbered{atomperm}
 \end{isabelle}
 \noindent
 At its core Nominal Isabelle is based on the nominal logic work by Pitts at
-al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a
+al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a
 sort-respecting permutation operation defined over a countably infinite
-collection of sorted atoms. The atoms are used for representing variable names
+collection of sorted atoms. The nominal logic work has been starting
-that might be bound or free. Multiple sorts are necessary for being able to
+point for a number of formalisations, most notable Norrish \cite{norrish04}
-represent different kinds of variables. For example, in the language Mini-ML
+in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own
-there are bound term variables in lambda abstractions and bound type variables in
+work in Isabelle/HOL.
-type schemes. In order to be able to separate them, each kind of variables needs to be
-represented by a different sort 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 therefore have to make a
-design decision about how to implement sorted atoms and sort-respecting
-permutations. One possibility, which we described in \cite{Urban08}, is to
-have separate types for the different
-kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. With this
-design one can represent permutations as lists of pairs of atoms and the
-operation of applying a permutation to an object as the function
-@{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-\noindent
-where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
-of the objects on which the permutation acts. For atoms
-the permutation operation is defined over the length of lists as follows
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
-@{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
-$\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
-@{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
-@{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
-\end{tabular}\hfill\numbered{atomperm}
-\end{isabelle}
-\noindent
-where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
-@{text "b"}. For atoms with different type than the permutation, we
-define @{text "\<pi> \<bullet> c \<equiv> c"}.
-With the separate atom types and the list representation of permutations it
-is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
-permutation, since the type system excludes lists containing atoms of
-different type. However, a disadvantage is that whenever we need to
-generalise induction hypotheses by quantifying over permutations, we have to
-build quantifications like
-@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
-\noindent
-where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
-The reason is that the permutation operation behaves differently for
-every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
-single quantification to stand for all permutations. Similarly, the
-notion of support
-@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
-\noindent
-which we will define later, cannot be
-used to express the support of an object over \emph{all} atoms. The reason
-is that support can behave differently for each @{text
-"\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
-a statement that an object, say @{text "x"}, is finitely supported we end up
-with having to state premises of the form
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-@{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
-\end{tabular}\hfill\numbered{fssequence}
-\end{isabelle}
-\noindent
-Because of these disadvantages, we will use in this paper a single unified atom type to
-represent atoms of different sorts. Consequently, we have to deal with the
-case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
-the type systems to exclude them.
-We also will not represent permutations as lists of pairs of atoms (as done in
-\cite{Urban08}).  Although an
-advantage of this representation is that the basic operations on
-permutations are already defined in Isabelle's list library: composition of
-two permutations (written @{text "_ @ _"}) is just list append, and
-inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
-list reversal, and another advantage is that there is a well-understood
-induction principle for lists, a disadvantage is that permutations
-do not have unique representations as lists. We have to explicitly identify
-them according to the relation
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-@{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
-\end{tabular}\hfill\numbered{permequ}
-\end{isabelle}
-\noindent
-This is a problem when lifting the permutation operation to other types, for
-example sets, functions and so on. For this we need to ensure that every definition
-is well-behaved in the sense that it satisfies some
-\emph{permutation properties}. In the list representation we need
-to state these properties as follows:
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
-i) & @{text "[] \<bullet> x = x"}\\
-ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
-iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
-\end{tabular}\hfill\numbered{permprops}
-\end{isabelle}
-\noindent
-where the last clause explicitly states that the permutation operation has
-to produce the same result for related permutations.  Moreover,
-``permutations-as-lists'' do not satisfy the group properties. This means by
-using this representation we will not be able to reuse the extensive
-reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
-in this paper permutations as functions from atoms to atoms. This representation
-is unique and satisfies the laws of non-commutative groups.
 Using a single atom type to represent atoms of different sorts and
 representing permutations as functions are not new ideas; see
 \cite{GunterOsbornPopescu09} \footnote{function rep.}  The main contribution
 of this paper is to show an example of how to make better theorem proving
 tools by choosing the right level of abstraction for the underlying
 *}
 section {* Sorted Atoms and Sort-Respecting Permutations *}
 text {*
+The most basic notion in this work is a
+sort-respecting permutation operation defined over a countably infinite
+collection of sorted atoms. The atoms are used for representing variable names
+that might be bound or free. Multiple sorts are necessary for being able to
+represent different kinds of variables. For example, in the language Mini-ML
+there are bound term variables in lambda abstractions and bound type variables in
+type schemes. In order to be able to separate them, each kind of variables needs to be
+represented by a different sort 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 therefore have to make a
+design decision about how to implement sorted atoms and sort-respecting
+permutations. One possibility, which we described in \cite{Urban08}, is to
+have separate types for the different
+kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
 In the nominal logic work of Pitts, binders and bound variables are
 represented by \emph{atoms}.  As stated above, we need to have different
 \emph{sorts} of atoms to be able to bind different kinds of variables.  A
 basic requirement is that there must be a countably infinite number of atoms
 of each sort.  We implement these atoms as
 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
 @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
 @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
-@{thm diff_def[where M="\<pi>\<^isub>1" and N="\<pi>\<^isub>2"]}
+@{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 and verify the simple properties
 together---it is no longer required to collect all atom declarations in one
 place.
 *}
-section {* Multi-Sorted Concrete Atoms *}
-(*<*)
-datatype ty = TVar string | Fun ty ty ("_ \<rightarrow> _")
-(*>*)
-text {*
-The formalisation presented so far allows us to streamline proofs and reduce
-the amount of custom ML-code in the existing implementation of Nominal
-Isabelle. In this section we describe a mechanism that extends the
-capabilities of Nominal Isabelle. This mechanism is about variables with
-additional information, for example typing constraints.
-While we leave a detailed treatment of binders and binding of variables for a
-later paper, we will have a look here at how such variables can be
-represented by concrete atoms.
-In the previous section we considered concrete atoms that can be used in
-simple binders like \emph{@{text "\<lambda>x. x"}}.  Such concrete atoms do
-not carry any information beyond their identities---comparing for equality
-is really the only way to analyse ordinary concrete atoms.
-However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms
-underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a
-more complicated structure. For example in the ``Church-style'' lambda-term
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-@{text "\<lambda>x\<^isub>\<alpha>. x\<^isub>\<alpha> x\<^isub>\<beta>"}
-\end{tabular}\hfill\numbered{church}
-\end{isabelle}
-\noindent
-both variables and binders include typing information indicated by @{text \<alpha>}
-and @{text \<beta>}. In this setting, we treat @{text "x\<^isub>\<alpha>"} and @{text
-"x\<^isub>\<beta>"} as distinct variables (assuming @{term "\<alpha>\<noteq>\<beta>"}) so that the
-variable @{text "x\<^isub>\<alpha>"} is bound by the lambda-abstraction, but not
-@{text "x\<^isub>\<beta>"}.
-To illustrate how we can deal with this phenomenon, let us represent object
-types like @{text \<alpha>} and @{text \<beta>} by the datatype
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-\isacommand{datatype}~~@{text "ty = TVar string | ty \<rightarrow> ty"}
-\end{tabular}
-\end{isabelle}
-\noindent
-If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the
-problem that a swapping, say @{term "(x \<leftrightarrow> y)"}, applied to the pair @{text "((x, \<alpha>), (x, \<beta>))"}
-will always permute \emph{both} occurrences of @{text x}, even if the types
-@{text "\<alpha>"} and @{text "\<beta>"} are different. This is unwanted, because it will
-eventually mean that both occurrences of @{text x} will become bound by a
-corresponding binder.
-Another attempt might be to define variables as an instance of the concrete
-atom type class, where a @{text ty} is somehow encoded within each variable.
-Remember we defined atoms as the datatype:
-*}
-datatype  atom\<iota>\<iota> = Atom\<iota>\<iota> string nat
-text {*
-\noindent
-Considering our method of defining concrete atom types, the usage of a string
-for the sort of atoms seems a natural choice.  However, none of the results so
-far depend on this choice and we are free to change it.
-One possibility is to encode types or any other information by making the sort
-argument parametric as follows:
-*}
-datatype  'a \<iota>atom\<iota>\<iota>\<iota> = \<iota>Atom\<iota>\<iota> 'a nat
-text {*
-\noindent
-The problem with this possibility is that we are then back in the old
-situation where our permutation operation is parametric in two types and
-this would require to work around Isabelle/HOL's restriction on type
-classes. Fortunately, encoding the types in a separate parameter is not
-necessary for what we want to achieve, as we only have to know when two
-types are equal or not. The solution is to use a different sort for each
-object type.  Then we can use the fact that permutations respect \emph{sorts} to
-ensure that permutations also respect \emph{object types}.  In order to do
-this, we must define an injective function @{text "sort_ty"} mapping from
-object types to sorts.  For defining functions like @{text "sort_ty"}, it is
-more convenient to use a tree datatype for sorts. Therefore we define
-*}
-datatype  sort = Sort string "(sort list)"
-datatype  atom\<iota>\<iota>\<iota>\<iota> = Atom\<iota>\<iota>\<iota>\<iota> sort nat
-text {*
-\noindent
-With this definition,
-the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}.
-The point, however, is that we can now define the function @{text sort_ty} simply as
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
-@{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\
-@{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2) = Sort ''Fun''  [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}
-\end{tabular}\hfill\numbered{sortty}
-\end{isabelle}
-\noindent
-which can easily be shown to be injective.
-Having settled on what the sorts should be for ``Church-like'' atoms, we have to
-give a subtype definition for concrete atoms. Previously we identified a subtype consisting
-of atoms of only one specified sort. This must be generalised to all sorts the
-function @{text "sort_ty"} might produce, i.e.~the
-range of @{text "sort_ty"}. Therefore we define
-\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-\isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"}
-\end{isabelle}
-\noindent
-This command gives us again injective representation and abstraction
-functions. We will write them also as \mbox{@{text "\<lfloor>_\<rfloor> :: var \<Rightarrow> atom"}} and
-@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> var"}, respectively.
-We can define the permutation operation for @{text var} as @{thm
-permute_var_def[where p="\<pi>", THEN eq_reflection, no_vars]} and the
-injective function to type @{typ atom} as @{thm atom_var_def[THEN
-eq_reflection, no_vars]}. Finally, we can define a constructor function that
-makes a @{text var} from a variable name and an object type:
-@{thm [display,indent=10] Var_def[where t="\<alpha>", THEN eq_reflection, no_vars]}
-\noindent
-With these definitions we can verify all the properties for concrete atom
-types except Property \ref{atomprops}@{text ".iii)"}, which requires every
-atom to have the same sort.  This last property is clearly not true for type
-@{text "var"}.
-This fact is slightly unfortunate since this
-property allowed us to use the type-checker in order to shield the user from
-all sort-constraints.  But this failure is expected here, because we cannot
-burden the type-system of Isabelle/HOL with the task of deciding when two
-object types are equal.  This means we sometimes need to explicitly state sort
-constraints or explicitly discharge them, but as we will see in the lemma
-below this seems a natural price to pay in these circumstances.
-To sum up this section, the encoding of type-information into atoms allows us
-to form the swapping @{term "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>)"} and to prove the following
-lemma
-*}
-lemma
-	    assumes asm: "\<alpha> \<noteq> \<beta>"
-	    shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
-	    using asm by simp
-text {*
-\noindent
-As we expect, the atom @{term "Var x \<beta>"} is left unchanged by the
-swapping. With this we can faithfully represent bindings in languages
-involving ``Church-style'' terms and bindings as shown in \eqref{church}. We
-expect that the creation of such atoms can be easily automated so that the
-user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
-where the argument, or arguments, are datatypes for which we can automatically
-define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
-Our hope is that with this approach Benzmueller and Paulson can make
-headway with formalising their results
-about simple type theory \cite{PaulsonBenzmueller}.
-Because of its limitations, they did not attempt this with the old version
-of Nominal Isabelle. We also hope we can make progress with formalisations of
-HOL-based languages.
-*}
 section {* Related Work *}
 text {*
 Add here comparison with old work.
 The main point is that the above reasoning blends smoothly with the reasoning
 infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single
 type class suffices.
+With this
+design one can represent permutations as lists of pairs of atoms and the
+operation of applying a permutation to an object as the function
+@{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+\noindent
+where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type
+of the objects on which the permutation acts. For atoms
+the permutation operation is defined over the length of lists as follows
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+@{text "[] \<bullet> c"} & @{text "="} & @{text c}\\
+@{text "(a b)::\<pi> \<bullet> c"} & @{text "="} &
+$\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\
+@{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\
+@{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$
+\end{tabular}\hfill\numbered{atomperm}
+\end{isabelle}
+\noindent
+where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and
+@{text "b"}. For atoms with different type than the permutation, we
+define @{text "\<pi> \<bullet> c \<equiv> c"}.
+With the separate atom types and the list representation of permutations it
+is impossible in systems like Isabelle/HOL to state an ``ill-sorted''
+permutation, since the type system excludes lists containing atoms of
+different type. However, a disadvantage is that whenever we need to
+generalise induction hypotheses by quantifying over permutations, we have to
+build quantifications like
+@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"}
+\noindent
+where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}.
+The reason is that the permutation operation behaves differently for
+every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a
+single quantification to stand for all permutations. Similarly, the
+notion of support
+@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"}
+\noindent
+which we will define later, cannot be
+used to express the support of an object over \emph{all} atoms. The reason
+is that support can behave differently for each @{text
+"\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in
+a statement that an object, say @{text "x"}, is finitely supported we end up
+with having to state premises of the form
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+@{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"}
+\end{tabular}\hfill\numbered{fssequence}
+\end{isabelle}
+\noindent
+Because of these disadvantages, we will use in this paper a single unified atom type to
+represent atoms of different sorts. Consequently, we have to deal with the
+case that a swapping of two atoms is ill-sorted: we cannot rely anymore on
+the type systems to exclude them.
+We also will not represent permutations as lists of pairs of atoms (as done in
+\cite{Urban08}).  Although an
+advantage of this representation is that the basic operations on
+permutations are already defined in Isabelle's list library: composition of
+two permutations (written @{text "_ @ _"}) is just list append, and
+inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just
+list reversal, and another advantage is that there is a well-understood
+induction principle for lists, a disadvantage is that permutations
+do not have unique representations as lists. We have to explicitly identify
+them according to the relation
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+@{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2  \<equiv>  \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"}
+\end{tabular}\hfill\numbered{permequ}
+\end{isabelle}
+\noindent
+This is a problem when lifting the permutation operation to other types, for
+example sets, functions and so on. For this we need to ensure that every definition
+is well-behaved in the sense that it satisfies some
+\emph{permutation properties}. In the list representation we need
+to state these properties as follows:
+\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
+i) & @{text "[] \<bullet> x = x"}\\
+ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\
+iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"}
+\end{tabular}\hfill\numbered{permprops}
+\end{isabelle}
+\noindent
+where the last clause explicitly states that the permutation operation has
+to produce the same result for related permutations.  Moreover,
+``permutations-as-lists'' do not satisfy the group properties. This means by
+using this representation we will not be able to reuse the extensive
+reasoning infrastructure in Isabelle about groups.  Because of this, we will represent
+in this paper permutations as functions from atoms to atoms. This representation
+is unique and satisfies the laws of non-commutative groups.
 *}
 section {* Conclusion *}

changeset 2736	61d30863e5d1
parent 2734	eee5deb35aa8
child 2740	a9e63abf3feb