Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LMCS-Paper/Paper.thy
changeset 3002 02d98590454d
parent 3001 8d7d85e915b5
child 3003 8e8aabf01f52
child 3004 c6af56de923d
equal deleted inserted replaced
3001:8d7d85e915b5 3002:02d98590454d 
    28   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 
    28   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 
    29   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
 
    29   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
 
    30   fv ("fa'(_')" [100] 100) and
 
    30   fv ("fa'(_')" [100] 100) and
 
    31   equal ("=") and
 
    31   equal ("=") and
 
    32   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
    32   alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
       
    33   alpha_abs_lst ("_ \<approx>\<^raw:{$\,_{\textit{abs\_list}}$}> _") and 
       
    34   alpha_abs_res ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and 
    33   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
 
    35   Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
 
    34   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
 
    36   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
 
    35   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
 
    37   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
 
    36   Abs_res ("[_]\<^bsub>set+\<^esub>._") and
 
    38   Abs_res ("[_]\<^bsub>set+\<^esub>._") and
 
    37   Abs_print ("_\<^bsub>set\<^esub>._") and
 
    39   Abs_print ("_\<^bsub>set\<^esub>._") and
 
    92   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 
    94   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
 
    93   type-variables.  While it is possible to implement this kind of more general
 
    95   type-variables.  While it is possible to implement this kind of more general
 
    94   binders by iterating single binders, this leads to a rather clumsy
 
    96   binders by iterating single binders, this leads to a rather clumsy
 
    95   formalisation of W. The need of iterating single binders is also one reason
 
    97   formalisation of W. The need of iterating single binders is also one reason
 
    96   why Nominal Isabelle and similar theorem provers that only provide
 
    98   why Nominal Isabelle and similar theorem provers that only provide
 
    97   mechanisms for binding single variables has not fared extremely well with
 
    99   mechanisms for binding single variables have not fared extremely well with
 
    98   the more advanced tasks in the POPLmark challenge \cite{challenge05},
 
   100   the more advanced tasks in the POPLmark challenge \cite{challenge05},
 
    99   because also there one would like to bind multiple variables at once.
 
   101   because also there one would like to bind multiple variables at once.
 
   100 
   102 
   101   Binding multiple variables has interesting properties that cannot be captured
 
   103   Binding multiple variables has interesting properties that cannot be captured
 
   102   easily by iterating single binders. For example in the case of type-schemes we do not
 
   104   easily by iterating single binders. For example in the case of type-schemes we do not
 
   121   \noindent
 
   123   \noindent
 
   122   where @{text z} does not occur freely in the type.  In this paper we will
 
   124   where @{text z} does not occur freely in the type.  In this paper we will
 
   123   give a general binding mechanism and associated notion of alpha-equivalence
 
   125   give a general binding mechanism and associated notion of alpha-equivalence
 
   124   that can be used to faithfully represent this kind of binding in Nominal
 
   126   that can be used to faithfully represent this kind of binding in Nominal
 
   125   Isabelle.  The difficulty of finding the right notion for alpha-equivalence
 
   127   Isabelle.  The difficulty of finding the right notion for alpha-equivalence
 
   126   can be appreciated in this case by considering that the definition given by
 
   128   can be appreciated in this case by considering that the definition given for
 
   127   Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
 
   129   type-schemes by Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
 
   128 
   130 
   129   However, the notion of alpha-equivalence that is preserved by vacuous
 
   131   However, the notion of alpha-equivalence that is preserved by vacuous
 
   130   binders is not always wanted. For example in terms like
 
   132   binders is not always wanted. For example in terms like
 
   131 
   133 
   132   \begin{equation}\label{one}
 
   134   \begin{equation}\label{one}
 
   359   The examples we have in mind where our reasoning infrastructure will be
 
   361   The examples we have in mind where our reasoning infrastructure will be
 
   360   helpful includes the term language of Core-Haskell (see
 
   362   helpful includes the term language of Core-Haskell (see
 
   361   Figure~\ref{corehas}). This term language involves patterns that have lists
 
   363   Figure~\ref{corehas}). This term language involves patterns that have lists
 
   362   of type-, coercion- and term-variables, all of which are bound in @{text
 
   364   of type-, coercion- and term-variables, all of which are bound in @{text
 
   363   "\<CASE>"}-expressions. In these patterns we do not know in advance how many
 
   365   "\<CASE>"}-expressions. In these patterns we do not know in advance how many
 
   364   variables need to be bound. Another example is the algorithm W
 
   366   variables need to be bound. Another example is the algorithm W,
 
   365   which includes multiple binders in type-schemes.\medskip
 
   367   which includes multiple binders in type-schemes.\medskip
 
   366 
   368 
   367   \noindent
 
   369   \noindent
 
   368   {\bf Contributions:}  We provide three new definitions for when terms
 
   370   {\bf Contributions:}  We provide three new definitions for when terms
 
   369   involving general binders are alpha-equivalent. These definitions are
 
   371   involving general binders are alpha-equivalent. These definitions are
 
   430   \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
 
   432   \cite{HuffmanUrban10} (including proofs). We shall briefly review this work
 
   431   to aid the description of what follows. 
   433   to aid the description of what follows. 
   432 
   434 
   433   Two central notions in the nominal logic work are sorted atoms and
 
   435   Two central notions in the nominal logic work are sorted atoms and
 
   434   sort-respecting permutations of atoms. We will use the letters @{text "a, b,
 
   436   sort-respecting permutations of atoms. We will use the letters @{text "a, b,
 
   435   c, \<dots>"} to stand for atoms and @{text "\<pi>, \<dots>"} to stand for permutations,
 
   437   c, \<dots>"} to stand for atoms and @{text "\<pi>, \<pi>\<^isub>1, \<dots>"} to stand for permutations,
 
   436   which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to
 
   438   which in Nominal Isabelle have type @{typ perm}. The purpose of atoms is to
 
   437   represent variables, be they bound or free. The sorts of atoms can be used
 
   439   represent variables, be they bound or free. The sorts of atoms can be used
 
   438   to represent different kinds of variables, such as the term-, coercion- and
 
   440   to represent different kinds of variables, such as the term-, coercion- and
 
   439   type-variables in Core-Haskell.  It is assumed that there is an infinite
 
   441   type-variables in Core-Haskell.  It is assumed that there is an infinite
 
   440   supply of atoms for each sort. In the interest of brevity, we shall restrict
 
   442   supply of atoms for each sort. In the interest of brevity, we shall restrict
 
   447   where the generic type @{text "\<beta>"} is the type of the object 
   449   where the generic type @{text "\<beta>"} is the type of the object 
   448   over which the permutation 
   450   over which the permutation 
   449   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 
   451   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
 
   450   the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}, 
   452   the composition of two permutations @{term "\<pi>\<^isub>1"} and @{term "\<pi>\<^isub>2"} as \mbox{@{term "\<pi>\<^isub>1 + \<pi>\<^isub>2"}}, 
   451   and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
 
   453   and the inverse permutation of @{term "\<pi>"} as @{text "- \<pi>"}. The permutation
 
   452   operation is defined over the type-hierarchy \cite{HuffmanUrban10};
 
   454   operation is defined over Isabelle/HOL's type-hierarchy \cite{HuffmanUrban10};
 
   453   for example permutations acting on products, lists, sets, functions and booleans are
 
   455   for example permutations acting on products, lists, sets, functions and booleans are
 
   454   given by:
 
   456   given by:
 
   455   
   457   
   456   \begin{equation}\label{permute}
 
   458   \begin{equation}\label{permute}
 
   457   \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 
   459   \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 
   608   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
 
   610   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text "\<pi>"} such that
 
   609   the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
 
   611   the renamed binders @{term "\<pi> \<bullet> as"} avoid @{text c} (which can be arbitrarily chosen
 
   610   as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
 
   612   as long as it is finitely supported) and also @{text "\<pi>"} does not affect anything
 
   611   in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 
   613   in the support of @{text x} (that is @{term "supp x \<sharp>* \<pi>"}). The last 
   612   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
   614   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 
   613   @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}.
 
   615   @{text as} in @{text x}, because @{term "\<pi> \<bullet> x = x"}. Note that @{term "supp x \<sharp>* \<pi>"}
 
       
   616   is equivalent with @{term "supp \<pi> \<sharp>* x"}, which means we could also use the other
 
       
   617   `direction' in Propositions \ref{supppermeq} and \ref{avoiding}.
 
   614 
   618 
   615   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 
   619   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
 
   616   and all are formalised in Isabelle/HOL. In the next sections we will make 
   620   and all are formalised in Isabelle/HOL. In the next sections we will make 
   617   use of these properties in order to define alpha-equivalence in 
   621   use of these properties in order to define alpha-equivalence in 
   618   the presence of multiple binders.
 
   622   the presence of multiple binders.
 
   730   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 
   734   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
 
   731   shown that all three notions of alpha-equivalence coincide, if we only
 
   735   shown that all three notions of alpha-equivalence coincide, if we only
 
   732   abstract a single atom.
 
   736   abstract a single atom.
 
   733 
   737 
   734   In the rest of this section we are going to introduce three abstraction 
   738   In the rest of this section we are going to introduce three abstraction 
   735   types. For this we define 
   739   types. For this we define the relations
 
   736 
   740 
   737   \begin{equation}
 
   741   \begin{equation}
 
   738   \begin{array}{l}
 
   742   \begin{array}{r}
 
   739   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, x)"}\\
 
   743   @{term "alpha_abs_set (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}\\
 
   740   @{term "abs_res (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, x)"}\\
 
   744   @{term "alpha_abs_res (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, y)"}\\
 
   741   @{term "abs_lst (as, x) (bs, x) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, x)"}\\
 
   745   @{term "alpha_abs_lst (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, y)"}\\
 
   742   \end{array}
 
   746   \end{array}
 
   743   \end{equation}
 
   747   \end{equation}\smallskip
 
   744   
   748   
   745   \noindent
 
   749   \noindent
 
   746   We can show that these relations are equivalence 
   750   We can show that these relations are equivalence 
   747   relations and equivariant.
 
   751   relations and equivariant.
 
   748 
   752 
   749   \begin{lem}\label{alphaeq} 
   753   \begin{lem}\label{alphaeq} 
   750   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
 
   754   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
 
   751   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 
   755   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. 
       
   756   %, and if 
   752   %@{term "abs_set (as, x) (bs, y)"} then also 
   757   %@{term "abs_set (as, x) (bs, y)"} then also 
   753   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
 
   758   %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
 
   754   \end{lem}
 
   759   \end{lem}
 
   755 
   760 
   756   \begin{proof}
 
   761   \begin{proof}
 
   757   Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
 
   762   Reflexivity is by taking @{text "\<pi>"} to be @{text "0"}. For symmetry we have
 
   758   a permutation @{text p} and for the proof obligation take @{term "- \<pi>"}. In case 
   763   a permutation @{text "\<pi>"} and for the proof obligation take @{term "- \<pi>"}. In case 
   759   of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
 
   764   of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
 
   760   proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. All conditions are then by simple
 
   765   proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
 
   761   calculations. 
   766   @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} holds provided 
       
   767   @{term "abs_set (as, x) (bs, y)"}.
 
       
   768 
   762   \end{proof}
 
   769   \end{proof}
 
   763 
   770 
   764   \noindent
 
   771   \noindent
 
   765   This lemma allows us to use our quotient package for introducing 
   772   This lemma allows us to use our quotient package for introducing 
   766   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
 
   773   new types @{text "\<beta> abs\<^bsub>set\<^esub>"}, @{text "\<beta> abs\<^bsub>set+\<^esub>"} and @{text "\<beta> abs\<^bsub>list\<^esub>"}
 
   767   representing alpha-equivalence classes of pairs of type 
   774   representing alpha-equivalence classes of pairs of type 
   768   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
 
   775   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
 
   769   (in the third case). 
   776   (in the third case). 
   770   The elements in these types will be, respectively, written as
 
   777   The elements in these types will be, respectively, written as
 
   771   
   778   
   772   \begin{center}
 
   779   \[
 
   773   @{term "Abs_set as x"}, \hspace{5mm} 
   780   @{term "Abs_set as x"} \hspace{10mm} 
   774   @{term "Abs_res as x"} and \hspace{5mm}
 
   781   @{term "Abs_res as x"} \hspace{10mm}
 
   775   @{term "Abs_lst as x"}, 
   782   @{term "Abs_lst as x"} 
   776   \end{center}
 
   783   \]\smallskip
 
   777   
   784   
   778   \noindent
 
   785   \noindent
 
   779   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
 
   786   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
 
   780   call the types \emph{abstraction types} and their elements
 
   787   call the types \emph{abstraction types} and their elements
 
   781   \emph{abstractions}. The important property we need to derive is the support of 
   788   \emph{abstractions}. The important property we need to derive is the support of 
   782   abstractions, namely:
 
   789   abstractions, namely:
 
   783 
   790 
   784   \begin{thm}[Support of Abstractions]\label{suppabs} 
   791   \begin{thm}[Support of Abstractions]\label{suppabs} 
   785   Assuming @{text x} has finite support, then
 
   792   Assuming @{text x} has finite support, then
 
   786 
   793 
   787   \begin{center}
 
   794   \[
 
   788   \begin{tabular}{l}
 
   795   \begin{array}{l@ {\;=\;}l}
 
   789   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$
 
   796   @{thm (lhs) supp_Abs(1)[no_vars]} & @{thm (rhs) supp_Abs(1)[no_vars]}\\
 
   790   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\
 
   797   @{thm (lhs) supp_Abs(2)[no_vars]} & @{thm (rhs) supp_Abs(2)[no_vars]}\\
 
   791   @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$
 
   798   @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} &
 
   792   @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}
 
   799   @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}\\
 
   793   \end{tabular}
 
   800   \end{array}
 
   794   \end{center}
 
   801   \]\smallskip
 
   795   \end{thm}
 
   802   \end{thm}
 
   796 
   803 
   797   \noindent
 
   804   \noindent
 
   798   This theorem states that the bound names do not appear in the support.
 
   805   This theorem states that the bound names do not appear in the support.
 
   799   For brevity we omit the proof and again refer the reader to
 
   806   Below we will show the first equation. The others follow by similar
 
   800   our formalisation in Isabelle/HOL.
 
   807   arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
 
   801 
   808 
   802   \noindent
 
       
   803   Below we will show the first equation. The others 
       
   804   follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
       
   805   we have 
       
   806   
   809   
   807   \begin{equation}\label{abseqiff}
 
   810   \begin{equation}\label{abseqiff}
 
   808   @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
   811   @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
   809   @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
 
   812   @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
 
   810   \end{equation}
 
   813   \end{equation}\smallskip
 
   811   
   814   
   812   \noindent
 
   815   \noindent
 
   813   and also
 
   816   and also
 
   814   
   817   
   815   \begin{equation}\label{absperm}
 
   818   \begin{equation}\label{absperm}
 
   816   @{thm permute_Abs[no_vars]}
 
   819   @{thm permute_Abs(1)[where p="\<pi>", no_vars]}
 
   817   \end{equation}
 
   820   \end{equation}\smallskip
 
   818 
   821 
   819   \noindent
 
   822   \noindent
 
   820   The second fact derives from the definition of permutations acting on pairs 
   823   The second fact derives from the definition of permutations acting on pairs 
   821   \eqref{permute} and alpha-equivalence being equivariant 
   824   \eqref{permute} and alpha-equivalence being equivariant 
   822   (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
   825   (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
nominal2