57 

    57 

    58 

    58 

    59 section {* Introduction *}

    59 section {* Introduction *}

    60 

    60 

    61 text {*

    61 text {*

    67   Nominal Isabelle derives automatically a reasoning infrastructure that has

    71   Nominal Isabelle derives automatically a reasoning infrastructure that has

    68   been used successfully in formalisations of an equivalence checking

    72   been used successfully in formalisations of an equivalence checking

    69   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

    73   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

    70   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

    74   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency

    71   \cite{BengtsonParow09} and a strong normalisation result for cut-elimination

    75   \cite{BengtsonParow09} and a strong normalisation result for cut-elimination

    72   in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for

    76   in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for

    73   formalisations in the locally-nameless approach to binding

    77   formalisations in the locally-nameless approach to binding

    74   \cite{SatoPollack10}.

    78   \cite{SatoPollack10}.

    75 

    79 

    78   respectively, of the form

    82   respectively, of the form

    80   \begin{equation}\label{tysch}

    84   \begin{equation}\label{tysch}

    81   \begin{array}{l}

    85   \begin{array}{l}

    83   @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}

    87   @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}

    84   \end{array}

    88   \end{array}

    87   \noindent

    91   \noindent

    88   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of

    92   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of

    89   type-variables.  While it is possible to implement this kind of more general

    93   type-variables.  While it is possible to implement this kind of more general

    90   binders by iterating single binders, this leads to a rather clumsy

    94   binders by iterating single binders, this leads to a rather clumsy

    99 

   100 

   100   Binding multiple variables has interesting properties that cannot be captured

   101   Binding multiple variables has interesting properties that cannot be captured

   101   easily by iterating single binders. For example in the case of type-schemes we do not

   102   easily by iterating single binders. For example in the case of type-schemes we do not

   102   want to make a distinction about the order of the bound variables. Therefore

   103   want to make a distinction about the order of the bound variables. Therefore

   104   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,

   105   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,

   107   \begin{equation}\label{ex1}

   108   \begin{equation}\label{ex1}

   108   @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}

   109   @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}

   109   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}

   110   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"}

   114   only on \emph{vacuous} binders, such as

   115   only on \emph{vacuous} binders, such as

   116   \begin{equation}\label{ex3}

   117   \begin{equation}\label{ex3}

   117   @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, z}. x \<rightarrow> y"}

   118   @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, z}. x \<rightarrow> y"}

   120   \noindent

   121   \noindent

   121   where @{text z} does not occur freely in the type.  In this paper we will

   122   where @{text z} does not occur freely in the type.  In this paper we will

   123   that can be used to faithfully represent this kind of binding in Nominal

   124   that can be used to faithfully represent this kind of binding in Nominal

   126   can be appreciated in this case by considering that the definition given by

   126   can be appreciated in this case by considering that the definition given by

   130   binders is not always wanted. For example in terms like

   130   binders is not always wanted. For example in terms like

   132   \begin{equation}\label{one}

   132   \begin{equation}\label{one}

   133   @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}

   133   @{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}

   135 

   135 

   136   \noindent

   136   \noindent

   137   we might not care in which order the assignments @{text "x = 3"} and

   137   we might not care in which order the assignments @{text "x = 3"} and

   142   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}

   142   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}

   145   \noindent

   145   \noindent

   146   Therefore we will also provide a separate binding mechanism for cases in

   146   Therefore we will also provide a separate binding mechanism for cases in

   147   which the order of binders does not matter, but the ``cardinality'' of the

   147   which the order of binders does not matter, but the ``cardinality'' of the

   148   binders has to agree.

   148   binders has to agree.

   149 

   149 

   150   However, we found that this is still not sufficient for dealing with

   150   However, we found that this is still not sufficient for dealing with

   151   language constructs frequently occurring in programming language

   151   language constructs frequently occurring in programming language

   152   research. For example in @{text "\<LET>"}s containing patterns like

   152   research. For example in @{text "\<LET>"}s containing patterns like

   154   \begin{equation}\label{two}

   154   \begin{equation}\label{two}

   155   @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}

   155   @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}

   158   \noindent

   158   \noindent

   159   we want to bind all variables from the pattern inside the body of the

   159   we want to bind all variables from the pattern inside the body of the

   160   $\mathtt{let}$, but we also care about the order of these variables, since

   160   $\mathtt{let}$, but we also care about the order of these variables, since

   164   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}

   164   @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}

   167   \noindent

   167   \noindent

   168   As a result, we provide three general binding mechanisms each of which binds

   168   As a result, we provide three general binding mechanisms each of which binds

   169   multiple variables at once, and let the user chose which one is intended

   169   multiple variables at once, and let the user chose which one is intended

   172 

   171 

   173   By providing these general binding mechanisms, however, we have to work

   172   By providing these general binding mechanisms, however, we have to work

   174   around a problem that has been pointed out by Pottier \cite{Pottier06} and

   173   around a problem that has been pointed out by Pottier \cite{Pottier06} and

   175   Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form

   174   Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form

   178   @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}

   177   @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}

   184   "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if

   182   "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if

   185   we represent the @{text "\<LET>"}-constructor by something like

   183   we represent the @{text "\<LET>"}-constructor by something like

   188   @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}

   186   @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}

   191   \noindent

   189   \noindent

   192   where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text

   190   where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text

   193   "x\<^isub>i"} becomes bound in @{text s}. In this representation the term

   191   "x\<^isub>i"} becomes bound in @{text s}. In this representation the term

   211   \noindent

   209   \noindent

   212   where @{text assn} is an auxiliary type representing a list of assignments

   210   where @{text assn} is an auxiliary type representing a list of assignments

   213   and @{text bn} an auxiliary function identifying the variables to be bound

   211   and @{text bn} an auxiliary function identifying the variables to be bound

   214   by the @{text "\<LET>"}. This function can be defined by recursion over @{text

   212   by the @{text "\<LET>"}. This function can be defined by recursion over @{text

   215   assn} as follows

   213   assn} as follows

   219   @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 

   217   @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 

   222   \noindent

   220   \noindent

   223   The scope of the binding is indicated by labels given to the types, for

   221   The scope of the binding is indicated by labels given to the types, for

   224   example @{text "s::trm"}, and a binding clause, in this case

   222   example @{text "s::trm"}, and a binding clause, in this case

   225   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding

   223   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding

   234 

   232 

   235   However, we will not be able to cope with all specifications that are

   233   However, we will not be able to cope with all specifications that are

   252   @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 

   247   @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 

   258   terms (offending specifications, which for example bind a variable according

   253   terms (offending specifications, which for example bind a variable according

   259   to a variable bound somewhere else, are not excluded by Ott, but we have

   254   to a variable bound somewhere else, are not excluded by Ott, but we have

   260   to).  

   255   to).  

   261 

   256 

   263   wealth of experience we gained with the older version of Nominal Isabelle:

   258   wealth of experience we gained with the older version of Nominal Isabelle:

   265   easier than reasoning with raw terms. The fundamental reason for this is

   260   easier than reasoning with raw terms. The fundamental reason for this is

   266   that the HOL-logic underlying Nominal Isabelle allows us to replace

   261   that the HOL-logic underlying Nominal Isabelle allows us to replace

   267   ``equals-by-equals''. In contrast, replacing

   262   ``equals-by-equals''. In contrast, replacing

   269   requires a lot of extra reasoning work.

   264   requires a lot of extra reasoning work.

   270 

   265 

   272   terms is nearly always taken for granted, establishing it automatically in

   267   terms is nearly always taken for granted, establishing it automatically in

   273   Isabelle/HOL is a rather non-trivial task. For every

   268   Isabelle/HOL is a rather non-trivial task. For every

   274   specification we will need to construct type(s) containing as elements the

   269   specification we will need to construct type(s) containing as elements the

   276   a new type by identifying a non-empty subset of an existing type.  The

   271   a new type by identifying a non-empty subset of an existing type.  The

   277   construction we perform in Isabelle/HOL can be illustrated by the following picture:

   272   construction we perform in Isabelle/HOL can be illustrated by the following picture:

   281   %\draw[step=2mm] (-4,-1) grid (4,1);

   276   %\draw[step=2mm] (-4,-1) grid (4,1);

   282   

   277   

   283   \draw[very thick] (0.7,0.4) circle (4.25mm);

   278   \draw[very thick] (0.7,0.4) circle (4.25mm);

   284   \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);

   279   \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);

   285   \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);

   280   \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);

   288   \draw (-2.0,-0.045)  -- (0.7,-0.045);

   283   \draw (-2.0,-0.045)  -- (0.7,-0.045);

   289 

   284 

   290   \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};

   285   \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};

   291   \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};

   286   \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};

   292   \draw (1.8, 0.48) node[right=-0.1mm]

   287   \draw (1.8, 0.48) node[right=-0.1mm]

   294   \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};

   289   \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};

   296   

   291   

   297   \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);

   292   \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);

   298   \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};

   293   \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};

   299 

   294 

   303   \noindent

   298   \noindent

   304   We take as the starting point a definition of raw terms (defined as a

   299   We take as the starting point a definition of raw terms (defined as a

   311 

   306 

   312   The fact that we obtain an isomorphism between the new type and the

   307   The fact that we obtain an isomorphism between the new type and the

   313   non-empty subset shows that the new type is a faithful representation of

   308   non-empty subset shows that the new type is a faithful representation of

   315   locally nameless representation of binders \cite{McKinnaPollack99}: in this

   310   locally nameless representation of binders \cite{McKinnaPollack99}: in this

   316   representation there are ``junk'' terms that need to be excluded by

   311   representation there are ``junk'' terms that need to be excluded by

   317   reasoning about a well-formedness predicate.

   312   reasoning about a well-formedness predicate.

   318 

   313 

   319   The problem with introducing a new type in Isabelle/HOL is that in order to

   314   The problem with introducing a new type in Isabelle/HOL is that in order to

   320   be useful, a reasoning infrastructure needs to be ``lifted'' from the

   315   be useful, a reasoning infrastructure needs to be ``lifted'' from the

   321   underlying subset to the new type. This is usually a tricky and arduous

   316   underlying subset to the new type. This is usually a tricky and arduous

   322   task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package

   317   task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package

   323   described by Homeier \cite{Homeier05} for the HOL4 system. This package

   318   described by Homeier \cite{Homeier05} for the HOL4 system. This package

   324   allows us to lift definitions and theorems involving raw terms to

   319   allows us to lift definitions and theorems involving raw terms to

   326   define the free-variable function over raw lambda-terms

   321   define the free-variable function over raw lambda-terms

   327 

   322 

   328   \begin{center}

   323   \begin{center}

   332   \end{center}

   327   \end{center}

   333   

   328   

   334   \noindent

   329   \noindent

   335   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}

   330   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}

   337   lifted function is characterised by the equations

   332   lifted function is characterised by the equations

   338 

   333 

   339   \begin{center}

   334   \begin{center}

   340   @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}

   335   @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}

   341   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}

   336   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}

   343   \end{center}

   338   \end{center}

   344 

   339 

   345   \noindent

   340   \noindent

   346   (Note that this means also the term-constructors for variables, applications

   341   (Note that this means also the term-constructors for variables, applications

   347   and lambda are lifted to the quotient level.)  This construction, of course,

   342   and lambda are lifted to the quotient level.)  This construction, of course,

   350   For example, we will not be able to lift a bound-variable function. Although

   345   For example, we will not be able to lift a bound-variable function. Although

   351   this function can be defined for raw terms, it does not respect

   346   this function can be defined for raw terms, it does not respect

   353   To sum up, every lifting

   348   To sum up, every lifting

   354   of theorems to the quotient level needs proofs of some respectfulness

   349   of theorems to the quotient level needs proofs of some respectfulness

   355   properties (see \cite{Homeier05}). In the paper we show that we are able to

   350   properties (see \cite{Homeier05}). In the paper we show that we are able to

   356   automate these proofs and as a result can automatically establish a reasoning 

   351   automate these proofs and as a result can automatically establish a reasoning 

   358 

   353 

   359   The examples we have in mind where our reasoning infrastructure will be

   354   The examples we have in mind where our reasoning infrastructure will be

   360   helpful includes the term language of Core-Haskell. This term language

   355   helpful includes the term language of Core-Haskell. This term language

   361   involves patterns that have lists of type-, coercion- and term-variables,

   356   involves patterns that have lists of type-, coercion- and term-variables,

   362   all of which are bound in @{text "\<CASE>"}-expressions. In these

   357   all of which are bound in @{text "\<CASE>"}-expressions. In these

   364   be bound. Another example is the specification of SML, which includes

   359   be bound. Another example is the specification of SML, which includes

   365   includes bindings as in type-schemes.\medskip

   360   includes bindings as in type-schemes.\medskip

   366 

   361 

   367   \noindent

   362   \noindent

   368   {\bf Contributions:}  We provide three new definitions for when terms

   363   {\bf Contributions:}  We provide three new definitions for when terms

   370   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic

   365   inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic

   372   terms, including properties about support, freshness and equality

   367   terms, including properties about support, freshness and equality

   374   induction principles that have the variable convention already built in.

   369   induction principles that have the variable convention already built in.

   375   The method behind our specification of general binders is taken 

   370   The method behind our specification of general binders is taken 

   376   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 

   371   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 

   378   The main improvement over Ott is that we introduce three binding modes

   373   The main improvement over Ott is that we introduce three binding modes

   380   for free variables of our terms, and also derive a reasoning infrastructure

   375   for free variables of our terms, and also derive a reasoning infrastructure

   381   for our specifications from ``first principles''.

   376   for our specifications from ``first principles''.

   382 

   377 

   383 

   378 

   384   %\begin{figure}

   379   %\begin{figure}

   497   \end{center}

   492   \end{center}

   498 

   493 

   499   The most original aspect of the nominal logic work of Pitts is a general

   494   The most original aspect of the nominal logic work of Pitts is a general

   500   definition for the notion of the ``set of free variables of an object @{text

   495   definition for the notion of the ``set of free variables of an object @{text

   501   "x"}''.  This notion, written @{term "supp x"}, is general in the sense that

   496   "x"}''.  This notion, written @{term "supp x"}, is general in the sense that

   503   products, sets and even functions. The definition depends only on the

   498   products, sets and even functions. The definition depends only on the

   504   permutation operation and on the notion of equality defined for the type of

   499   permutation operation and on the notion of equality defined for the type of

   505   @{text x}, namely:

   500   @{text x}, namely:

   506   %

   501   %

   507   \begin{equation}\label{suppdef}

   502   \begin{equation}\label{suppdef}

   518   without knowing anything about the structure of @{term x} that

   513   without knowing anything about the structure of @{term x} that

   519   swapping two fresh atoms, say @{text a} and @{text b}, leaves 

   514   swapping two fresh atoms, say @{text a} and @{text b}, leaves 

   520   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}

   515   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}

   521   then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   516   then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   522   

   517   

   524   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}

   519   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}

   526   

   521   

   527   While often the support of an object can be relatively easily 

   522   While often the support of an object can be relatively easily 

   528   described, for example for atoms, products, lists, function applications, 

   523   described, for example for atoms, products, lists, function applications, 

   529   booleans and permutations as follows

   524   booleans and permutations as follows

   530   

   525   

   551   

   546   

   552   Reasoning about

   547   Reasoning about

   553   such approximations can be simplified with the notion \emph{supports}, defined 

   548   such approximations can be simplified with the notion \emph{supports}, defined 

   554   as follows:

   549   as follows:

   555   

   550   

   557   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}

   552   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}

   558   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   553   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.

   560   

   555   

   561   \noindent

   556   \noindent

   562   The main point of @{text supports} is that we can establish the following 

   557   The main point of @{text supports} is that we can establish the following 

   563   two properties.

   558   two properties.

   564   

   559   

   566   Given a set @{text "as"} of atoms.

   561   Given a set @{text "as"} of atoms.

   567   {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}

   562   {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}

   568   {\it (ii)} @{thm supp_supports[no_vars]}.

   563   {\it (ii)} @{thm supp_supports[no_vars]}.

   570   

   565   

   571   Another important notion in the nominal logic work is \emph{equivariance}.

   566   Another important notion in the nominal logic work is \emph{equivariance}.

   572   For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 

   567   For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 

   573   it is required that every permutation leaves @{text f} unchanged, that is

   568   it is required that every permutation leaves @{text f} unchanged, that is

   574   

   569   

   603   Property~\ref{swapfreshfresh}

   598   Property~\ref{swapfreshfresh}

   604   this property to rename single binders, it this property 

   599   this property to rename single binders, it this property 

   605   proved too unwieldy for dealing with multiple binders. For such binders the 

   600   proved too unwieldy for dealing with multiple binders. For such binders the 

   606   following generalisations turned out to be easier to use.

   601   following generalisations turned out to be easier to use.

   607 

   602 

   609   @{thm[mode=IfThen] supp_perm_eq[no_vars]}

   604   @{thm[mode=IfThen] supp_perm_eq[no_vars]}

   613   For a finite set @{text as} and a finitely supported @{text x} with

   608   For a finite set @{text as} and a finitely supported @{text x} with

   614   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there

   609   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there

   615   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and

   610   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and

   616   @{term "supp x \<sharp>* p"}.

   611   @{term "supp x \<sharp>* p"}.

   618 

   613 

   619   \noindent

   614   \noindent

   620   The idea behind the second property is that given a finite set @{text as}

   615   The idea behind the second property is that given a finite set @{text as}

   621   of binders (being bound, or fresh, in @{text x} is ensured by the

   616   of binders (being bound, or fresh, in @{text x} is ensured by the

   622   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that

   617   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that

   626   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 

   621   fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders 

   627   @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.

   622   @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.

   628 

   623 

   629   Most properties given in this section are described in detail in \cite{HuffmanUrban10}

   624   Most properties given in this section are described in detail in \cite{HuffmanUrban10}

   630   and all are formalised in Isabelle/HOL. In the next sections we will make 

   625   and all are formalised in Isabelle/HOL. In the next sections we will make 

   632   the presence of multiple binders.

   627   the presence of multiple binders.

   633 *}

   628 *}

   634 

   629 

   635 

   630 

   636 section {* General Bindings\label{sec:binders} *}

   631 section {* General Bindings\label{sec:binders} *}

   649   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs

   644   first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.  These pairs

   650   are intended to represent the abstraction, or binding, of the set of atoms @{text

   645   are intended to represent the abstraction, or binding, of the set of atoms @{text

   651   "as"} in the body @{text "x"}.

   646   "as"} in the body @{text "x"}.

   652 

   647 

   653   The first question we have to answer is when two pairs @{text "(as, x)"} and

   648   The first question we have to answer is when two pairs @{text "(as, x)"} and

   656   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}

   651   vacuous binders.) To answer this question, we identify four conditions: {\it (i)}

   657   given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

   652   given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

   658   set"}}, then @{text x} and @{text y} need to have the same set of free

   653   set"}}, then @{text x} and @{text y} need to have the same set of free

   659   atoms; moreover there must be a permutation @{text p} such that {\it

   654   atoms; moreover there must be a permutation @{text p} such that {\it

   660   (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but

   655   (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but

   673   \end{array}

   668   \end{array}

   674   \end{equation}

   669   \end{equation}

   675   %

   670   %

   676   \noindent

   671   \noindent

   677   Note that this relation depends on the permutation @{text

   672   Note that this relation depends on the permutation @{text

   679   existentially quantify over this @{text "p"}. Also note that the relation is

   674   existentially quantify over this @{text "p"}. Also note that the relation is

   680   dependent on a free-atom function @{text "fa"} and a relation @{text

   675   dependent on a free-atom function @{text "fa"} and a relation @{text

   681   "R"}. The reason for this extra generality is that we will use

   676   "R"}. The reason for this extra generality is that we will use

   683   the latter case, @{text R} will be replaced by equality @{text "="} and we

   678   the latter case, @{text R} will be replaced by equality @{text "="} and we

   684   will prove that @{text "fa"} is equal to @{text "supp"}.

   679   will prove that @{text "fa"} is equal to @{text "supp"}.

   685 

   680 

   686   The definition in \eqref{alphaset} does not make any distinction between the

   681   The definition in \eqref{alphaset} does not make any distinction between the

   688   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 

   683   for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"} 

   689   as follows

   684   as follows

   690   %

   685   %

   691   \begin{equation}\label{alphalist}

   686   \begin{equation}\label{alphalist}

   692   \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}

   687   \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}

   715              \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\

   710              \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\

   716   \end{array}

   711   \end{array}

   717   \end{equation}

   712   \end{equation}

   718 

   713 

   719   It might be useful to consider first some examples how these definitions

   714   It might be useful to consider first some examples how these definitions

   721   abstracting a set of atoms over types (as in type-schemes). We set

   716   abstracting a set of atoms over types (as in type-schemes). We set

   722   @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we

   717   @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we

   723   define

   718   define

   724   %

   719   %

   725   \begin{center}

   720   \begin{center}

   727   \end{center}

   722   \end{center}

   728 

   723 

   729   \noindent

   724   \noindent

   730   Now recall the examples shown in \eqref{ex1} and

   725   Now recall the examples shown in \eqref{ex1} and

   731   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and

   726   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and

   733   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to

   728   $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to

   734   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text

   729   be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text

   735   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}

   730   "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}

   736   since there is no permutation that makes the lists @{text "[x, y]"} and

   731   since there is no permutation that makes the lists @{text "[x, y]"} and

   737   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}

   732   @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}

   739   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity

   734   @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity

   740   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}

   735   permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}

   741   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no

   736   $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no

   742   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal

   737   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal

   743   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be

   738   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be

   745   abstract a single atom.

   740   abstract a single atom.

   746 

   741 

   747   In the rest of this section we are going to introduce three abstraction 

   742   In the rest of this section we are going to introduce three abstraction 

   748   types. For this we define 

   743   types. For this we define 

   749   %

   744   %

   754   \noindent

   749   \noindent

   755   (similarly for $\approx_{\,\textit{abs\_set+}}$ 

   750   (similarly for $\approx_{\,\textit{abs\_set+}}$ 

   756   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 

   751   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 

   757   relations. %% and equivariant.

   752   relations. %% and equivariant.

   758 

   753 

   760   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$

   755   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$

   761   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 

   756   and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if 

   762   %@{term "abs_set (as, x) (bs, y)"} then also 

   757   %@{term "abs_set (as, x) (bs, y)"} then also 

   763   %@{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).

   765 

   760 

   766   \begin{proof}

   761   \begin{proof}

   767   Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have

   762   Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have

   768   a permutation @{text p} and for the proof obligation take @{term "-p"}. In case 

   763   a permutation @{text p} and for the proof obligation take @{term "-p"}. In case 

   769   of transitivity, we have two permutations @{text p} and @{text q}, and for the

   764   of transitivity, we have two permutations @{text p} and @{text q}, and for the

   772   \end{proof}

   767   \end{proof}

   773 

   768 

   774   \noindent

   769   \noindent

   775   This lemma allows us to use our quotient package for introducing 

   770   This lemma allows us to use our quotient package for introducing 

   776   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}

   771   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}

   778   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}

   773   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}

   779   (in the third case). 

   774   (in the third case). 

   780   The elements in these types will be, respectively, written as

   775   The elements in these types will be, respectively, written as

   781   

   776   

   782   \begin{center}

   777   \begin{center}

   789   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will

   784   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will

   790   call the types \emph{abstraction types} and their elements

   785   call the types \emph{abstraction types} and their elements

   791   \emph{abstractions}. The important property we need to derive is the support of 

   786   \emph{abstractions}. The important property we need to derive is the support of 

   792   abstractions, namely:

   787   abstractions, namely:

   793 

   788 

   795   Assuming @{text x} has finite support, then

   790   Assuming @{text x} has finite support, then

   796 

   791 

   797   \begin{center}

   792   \begin{center}

   798   \begin{tabular}{l}

   793   \begin{tabular}{l}

   799   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$

   794   @{thm (lhs) supp_Abs(1)[no_vars]} $\;\;=\;\;$

   800   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\

   795   @{thm (lhs) supp_Abs(2)[no_vars]} $\;\;=\;\;$ @{thm (rhs) supp_Abs(2)[no_vars]}, and\\

   801   @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$

   796   @{thm (lhs) supp_Abs(3)[where bs="bs", no_vars]} $\;\;=\;\;$

   802   @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}

   797   @{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}

   803   \end{tabular}

   798   \end{tabular}

   804   \end{center}

   799   \end{center}

   806 

   801 

   807   \noindent

   802   \noindent

   808   This theorem states that the bound names do not appear in the support.

   803   This theorem states that the bound names do not appear in the support.

   809   For brevity we omit the proof and again refer the reader to

   804   For brevity we omit the proof and again refer the reader to

   810   our formalisation in Isabelle/HOL.

   805   our formalisation in Isabelle/HOL.

   826   @{thm permute_Abs[no_vars]}

   821   @{thm permute_Abs[no_vars]}

   827   \end{equation}

   822   \end{equation}

   828 

   823 

   829   \noindent

   824   \noindent

   830   The second fact derives from the definition of permutations acting on pairs 

   825   The second fact derives from the definition of permutations acting on pairs 

   832   (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 

   827   (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 

   833   the following lemma about swapping two atoms in an abstraction.

   828   the following lemma about swapping two atoms in an abstraction.

   834   

   829   

   836   @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}

   831   @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}

   838   

   833   

   839   \begin{proof}

   834   \begin{proof}

   840   This lemma is straightforward using \eqref{abseqiff} and observing that

   835   This lemma is straightforward using \eqref{abseqiff} and observing that

   841   the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.

   836   the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.

   842   Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).

   837   Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).

   884   form @{term "Abs_set as x"} etc is motivated by the fact that 

   879   form @{term "Abs_set as x"} etc is motivated by the fact that 

   885   we can conveniently establish  at the Isabelle/HOL level

   880   we can conveniently establish  at the Isabelle/HOL level

   886   properties about them.  It would be

   881   properties about them.  It would be

   887   laborious to write custom ML-code that derives automatically such properties 

   882   laborious to write custom ML-code that derives automatically such properties 

   888   for every term-constructor that binds some atoms. Also the generality of

   883   for every term-constructor that binds some atoms. Also the generality of

   890 *}

   885 *}

   891 

   886 

   892 section {* Specifying General Bindings\label{sec:spec} *}

   887 section {* Specifying General Bindings\label{sec:spec} *}

   893 

   888 

   894 text {*

   889 text {*

   903   

   898   

   904   \begin{equation}\label{scheme}

   899   \begin{equation}\label{scheme}

   905   \mbox{\begin{tabular}{@ {}p{2.5cm}l}

   900   \mbox{\begin{tabular}{@ {}p{2.5cm}l}

   906   type \mbox{declaration part} &

   901   type \mbox{declaration part} &

   907   $\begin{cases}

   902   $\begin{cases}

   909   \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\

   904   \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\

   910   \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\

   905   \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\

   911   \raisebox{2mm}{$\ldots$}\\[-2mm] 

   906   \raisebox{2mm}{$\ldots$}\\[-2mm] 

   912   \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 

   907   \isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\ 

   913   \end{tabular}}

   908   \end{tabular}}

   914   \end{cases}$\\

   909   \end{cases}$\\

   915   binding \mbox{function part} &

   910   binding \mbox{function part} &

   916   $\begin{cases}

   911   $\begin{cases}

   918   \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\

   913   \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\

   919   \isacommand{where}\\

   914   \isacommand{where}\\

   920   \raisebox{2mm}{$\ldots$}\\[-2mm]

   915   \raisebox{2mm}{$\ldots$}\\[-2mm]

   921   \end{tabular}}

   916   \end{tabular}}

   922   \end{cases}$\\

   917   \end{cases}$\\

   959   %

   954   %

   960   \noindent

   955   \noindent

   961   The first mode is for binding lists of atoms (the order of binders matters);

   956   The first mode is for binding lists of atoms (the order of binders matters);

   962   the second is for sets of binders (the order does not matter, but the

   957   the second is for sets of binders (the order does not matter, but the

   963   cardinality does) and the last is for sets of binders (with vacuous binders

   958   cardinality does) and the last is for sets of binders (with vacuous binders

   965   clause will be called \emph{bodies}; the

   960   clause will be called \emph{bodies}; the

   966   ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to

   961   ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to

   967   Ott, we allow multiple labels in binders and bodies. 

   962   Ott, we allow multiple labels in binders and bodies. 

   968 

   963 

   969   For example we allow

   964   For example we allow

   981 

   976 

   982   \noindent

   977   \noindent

   983   Similarly for the other binding modes. 

   978   Similarly for the other binding modes. 

   984   Interestingly, in case of \isacommand{bind (set)}

   979   Interestingly, in case of \isacommand{bind (set)}

   985   and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics

   980   and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics

   987   show this later with an example.

   982   show this later with an example.

   988   

   983   

   989   There are also some restrictions we need to impose on our binding clauses in comparison to

   984   There are also some restrictions we need to impose on our binding clauses in comparison to

   990   the ones of Ott. The

   985   the ones of Ott. The

   991   main idea behind these restrictions is that we obtain a sensible notion of

   986   main idea behind these restrictions is that we obtain a sensible notion of

   993   atom occurrence cannot be both bound and free at the same time.  The first

   988   atom occurrence cannot be both bound and free at the same time.  The first

   994   restriction is that a body can only occur in

   989   restriction is that a body can only occur in

   995   \emph{one} binding clause of a term constructor (this ensures that the bound

   990   \emph{one} binding clause of a term constructor (this ensures that the bound

   996   atoms of a body cannot be free at the same time by specifying an

   991   atoms of a body cannot be free at the same time by specifying an

   997   alternative binder for the same body). 

   992   alternative binder for the same body). 

  1004   the labels must refer to atom types or lists of atom types. Two examples for

   999   the labels must refer to atom types or lists of atom types. Two examples for

  1005   the use of shallow binders are the specification of lambda-terms, where a

  1000   the use of shallow binders are the specification of lambda-terms, where a

  1006   single name is bound, and type-schemes, where a finite set of names is

  1001   single name is bound, and type-schemes, where a finite set of names is

  1007   bound:

  1002   bound:

  1008 

  1003 

  1010   \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}

  1005   \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}

  1011   \begin{tabular}{@ {}l}

  1006   \begin{tabular}{@ {}l}

  1012   \isacommand{nominal\_datatype} @{text lam} $=$\\

  1007   \isacommand{nominal\_datatype} @{text lam} $=$\\

  1013   \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\

  1008   \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\

  1014   \hspace{2mm}$\mid$~@{text "App lam lam"}\\

  1009   \hspace{2mm}$\mid$~@{text "App lam lam"}\\

  1043   must be given in the binding function part of the scheme shown in

  1038   must be given in the binding function part of the scheme shown in

  1044   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

  1039   \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with

  1045   tuple patterns might be specified as:

  1040   tuple patterns might be specified as:

  1046   %

  1041   %

  1047   \begin{equation}\label{letpat}

  1042   \begin{equation}\label{letpat}

  1049   \begin{tabular}{l}

  1044   \begin{tabular}{l}

  1050   \isacommand{nominal\_datatype} @{text trm} $=$\\

  1045   \isacommand{nominal\_datatype} @{text trm} $=$\\

  1051   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\

  1046   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\

  1052   \hspace{5mm}$\mid$~@{term "App trm trm"}\\

  1047   \hspace{5mm}$\mid$~@{term "App trm trm"}\\

  1053   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 

  1048   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 

  1086   binders \emph{recursive}.  To see the purpose of such recursive binders,

  1081   binders \emph{recursive}.  To see the purpose of such recursive binders,

  1087   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following

  1082   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following

  1088   specification:

  1083   specification:

  1089   %

  1084   %

  1090   \begin{equation}\label{letrecs}

  1085   \begin{equation}\label{letrecs}

  1092   \begin{tabular}{@ {}l@ {}}

  1087   \begin{tabular}{@ {}l@ {}}

  1093   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\

  1088   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\

  1094   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 

  1089   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 

  1095      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\

  1090      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\

  1096   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}

  1091   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}

  1106   %

  1101   %

  1107   \noindent

  1102   \noindent

  1108   The difference is that with @{text Let} we only want to bind the atoms @{text

  1103   The difference is that with @{text Let} we only want to bind the atoms @{text

  1109   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms

  1104   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms

  1110   inside the assignment. This difference has consequences for the associated

  1105   inside the assignment. This difference has consequences for the associated

  1112   

  1107   

  1113   To make sure that atoms bound by deep binders cannot be free at the

  1108   To make sure that atoms bound by deep binders cannot be free at the

  1114   same time, we cannot have more than one binding function for a deep binder. 

  1109   same time, we cannot have more than one binding function for a deep binder. 

  1115   Consequently we exclude specifications such as

  1110   Consequently we exclude specifications such as

  1116   %

  1111   %

  1118   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  1113   \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  1119   @{text "Baz\<^isub>1 p::pat t::trm"} & 

  1114   @{text "Baz\<^isub>1 p::pat t::trm"} & 

  1120      \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\

  1115      \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\

  1121   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 

  1116   @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & 

  1122      \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},

  1117      \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},

  1126 

  1121 

  1127   \noindent

  1122   \noindent

  1128   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 

  1123   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 

  1129   out different atoms to become bound, respectively be free, in @{text "p"}.

  1124   out different atoms to become bound, respectively be free, in @{text "p"}.

  1130   (Since the Ott-tool does not derive a reasoning infrastructure for 

  1125   (Since the Ott-tool does not derive a reasoning infrastructure for 

  1132   

  1127   

  1133   We also need to restrict the form of the binding functions in order 

  1128   We also need to restrict the form of the binding functions in order 

  1135   terms. The main restriction is that we cannot return an atom in a binding function that is also

  1130   terms. The main restriction is that we cannot return an atom in a binding function that is also

  1136   bound in the corresponding term-constructor. That means in \eqref{letpat} 

  1131   bound in the corresponding term-constructor. That means in \eqref{letpat} 

  1137   that the term-constructors @{text PVar} and @{text PTup} may

  1132   that the term-constructors @{text PVar} and @{text PTup} may

  1138   not have a binding clause (all arguments are used to define @{text "bn"}).

  1133   not have a binding clause (all arguments are used to define @{text "bn"}).

  1139   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}

  1134   In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}

  1140   may have a binding clause involving the argument @{text trm} (the only one that

  1135   may have a binding clause involving the argument @{text trm} (the only one that

  1141   is \emph{not} used in the definition of the binding function). This restriction

  1136   is \emph{not} used in the definition of the binding function). This restriction

  1143 

  1138 

  1144   In the version of

  1139   In the version of

  1145   Nominal Isabelle described here, we also adopted the restriction from the

  1140   Nominal Isabelle described here, we also adopted the restriction from the

  1146   Ott-tool that binding functions can only return: the empty set or empty list

  1141   Ott-tool that binding functions can only return: the empty set or empty list

  1147   (as in case @{text PNil}), a singleton set or singleton list containing an

  1142   (as in case @{text PNil}), a singleton set or singleton list containing an

  1148   atom (case @{text PVar}), or unions of atom sets or appended atom lists

  1143   atom (case @{text PVar}), or unions of atom sets or appended atom lists

  1149   (case @{text PTup}). This restriction will simplify some automatic definitions and proofs

  1144   (case @{text PTup}). This restriction will simplify some automatic definitions and proofs

  1150   later on.

  1145   later on.

  1151   

  1146   

  1153   we shall assume specifications 

  1148   we shall assume specifications 

  1154   of term-calculi are implicitly \emph{completed}. By this we mean that  

  1149   of term-calculi are implicitly \emph{completed}. By this we mean that  

  1155   for every argument of a term-constructor that is \emph{not} 

  1150   for every argument of a term-constructor that is \emph{not} 

  1156   already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding

  1151   already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding

  1157   clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case

  1152   clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case

  1158   of the lambda-terms, the completion produces

  1153   of the lambda-terms, the completion produces

  1159 

  1154 

  1161   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}

  1156   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}

  1162   \isacommand{nominal\_datatype} @{text lam} =\\

  1157   \isacommand{nominal\_datatype} @{text lam} =\\

  1163   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}

  1158   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}

  1164     \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\

  1159     \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\

  1165   \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}

  1160   \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}

  1184   re-arranging the arguments of

  1179   re-arranging the arguments of

  1185   term-constructors so that binders and their bodies are next to each other will 

  1180   term-constructors so that binders and their bodies are next to each other will 

  1186   result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. 

  1181   result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. 

  1187   Therefore we will first

  1182   Therefore we will first

  1188   extract ``raw'' datatype definitions from the specification and then define 

  1183   extract ``raw'' datatype definitions from the specification and then define 

  1191 

  1186 

  1192   The ``raw'' datatype definition can be obtained by stripping off the 

  1187   The ``raw'' datatype definition can be obtained by stripping off the 

  1193   binding clauses and the labels from the types. We also have to invent

  1188   binding clauses and the labels from the types. We also have to invent

  1194   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}

  1189   new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}

  1195   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.

  1190   given by the user. In our implementation we just use the affix ``@{text "_raw"}''.

  1196   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 

  1191   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 

  1198   for the corresponding notion given on the ``raw'' level. So for example 

  1193   for the corresponding notion given on the ``raw'' level. So for example 

  1199   we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}

  1194   we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}

  1200   where @{term ty} is the type used in the quotient construction for 

  1195   where @{term ty} is the type used in the quotient construction for 

  1201   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 

  1196   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 

  1202 

  1197 

  1360   "ANil"} and @{text "ACons"}. Since there is a binding function defined for

  1355   "ANil"} and @{text "ACons"}. Since there is a binding function defined for

  1361   assignments, we have three free-atom functions, namely @{text

  1356   assignments, we have three free-atom functions, namely @{text

  1362   "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text

  1357   "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text

  1363   "fa\<^bsub>bn\<^esub>"} as follows:

  1358   "fa\<^bsub>bn\<^esub>"} as follows:

  1364   %

  1359   %

  1366   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

  1361   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

  1367   @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\

  1362   @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\

  1368   @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]

  1363   @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]

  1369 

  1364 

  1370   @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\

  1365   @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\

  1399   example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any

  1394   example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any

  1400   atoms, even if the binding function is specified over assignments. 

  1395   atoms, even if the binding function is specified over assignments. 

  1401   Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will

  1396   Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will

  1402   some atoms actually become bound.  This is a phenomenon that has also been pointed

  1397   some atoms actually become bound.  This is a phenomenon that has also been pointed

  1403   out in \cite{ott-jfp}. For us this observation is crucial, because we would 

  1398   out in \cite{ott-jfp}. For us this observation is crucial, because we would 

  1405   atoms that are bound. In that case, these functions would \emph{not} respect

  1400   atoms that are bound. In that case, these functions would \emph{not} respect

  1409   "ty"}$_{1..n}$ from the specification. We write them as

  1404   "ty"}$_{1..n}$ from the specification. We write them as

  1410   

  1405   

  1411   \begin{center}

  1406   \begin{center}

  1412   @{text "\<approx>ty"}$_{1..n}$.

  1407   @{text "\<approx>ty"}$_{1..n}$.

  1413   \end{center}

  1408   \end{center}

  1414   

  1409   

  1415   \noindent

  1410   \noindent

  1416   Like with the free-atom functions, we also need to

  1411   Like with the free-atom functions, we also need to

  1418   

  1413   

  1419   \begin{center}

  1414   \begin{center}

  1420   @{text "\<approx>bn\<^isub>"}$_{1..m}$

  1415   @{text "\<approx>bn\<^isub>"}$_{1..m}$

  1421   \end{center}

  1416   \end{center}

  1422   

  1417   

  1432   @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\

  1427   @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\

  1433   \end{tabular}

  1428   \end{tabular}

  1434   \end{center}

  1429   \end{center}

  1435 

  1430 

  1436 

  1431 

  1438   having a single clause for each term-constructor. Assuming a

  1433   having a single clause for each term-constructor. Assuming a

  1439   term-constructor @{text C} is of type @{text ty} and has the binding clauses

  1434   term-constructor @{text C} is of type @{text ty} and has the binding clauses

  1441   

  1436   

  1442   \begin{center}

  1437   \begin{center}

  1443   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}

  1438   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n  \<approx>ty  C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}

  1444   {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} 

  1439   {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}} 

  1445   \end{center}

  1440   \end{center}

  1452   \begin{center}

  1447   \begin{center}

  1453   \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}

  1448   \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}

  1454   \end{center}

  1449   \end{center}

  1455 

  1450 

  1456   \noindent

  1451   \noindent

  1458   we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}  

  1453   we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}  

  1459   whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and

  1454   whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and

  1460   respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate

  1455   respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate

  1462   

  1457   

  1463   \begin{equation}\label{rempty}

  1458   \begin{equation}\label{rempty}

  1464   \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}

  1459   \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}

  1465   \end{equation}

  1460   \end{equation}

  1466 

  1461 

  1487 

  1482 

  1488   \noindent

  1483   \noindent

  1489   In this case we define a premise @{text P} using the relation

  1484   In this case we define a premise @{text P} using the relation

  1490   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly

  1485   $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly

  1491   $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other

  1486   $\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other

  1493   involving multiple binders. As above, we first build the tuples @{text "D"} and

  1488   involving multiple binders. As above, we first build the tuples @{text "D"} and

  1494   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding

  1489   @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding

  1496   For $\approx_{\,\textit{set}}$  we also need

  1491   For $\approx_{\,\textit{set}}$  we also need

  1497   a compound free-atom function for the bodies defined as

  1492   a compound free-atom function for the bodies defined as

  1498   

  1493   

  1499   \begin{center}

  1494   \begin{center}

  1500   \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}

  1495   \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}

  1516   \begin{center}

  1511   \begin{center}

  1517   \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.

  1512   \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.

  1518   \end{center}

  1513   \end{center}

  1519 

  1514 

  1520   \noindent

  1515   \noindent

  1522   clause. 

  1517   clause. 

  1523   However, in case the binders have non-recursive deep binders, this premise

  1518   However, in case the binders have non-recursive deep binders, this premise

  1524   is not enough:

  1519   is not enough:

  1526   these binders. An example is @{text "Let"} where we have to make sure the

  1521   these binders. An example is @{text "Let"} where we have to make sure the

  1528   relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).

  1523   relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).

  1529   Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are

  1524   Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are

  1530   

  1525   

  1531   \begin{center}

  1526   \begin{center}

  1532   @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.

  1527   @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.

  1540   \begin{center}

  1535   \begin{center}

  1541   @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}

  1536   @{text "prems(bc\<^isub>i) \<equiv> P  \<and>   L R' L'"}

  1542   \end{center} 

  1537   \end{center} 

  1543 

  1538 

  1544   \noindent 

  1539   \noindent 

  1546   in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form

  1541   in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form

  1547   

  1542   

  1548   \begin{center}

  1543   \begin{center}

  1549   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}

  1544   @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}

  1550   \end{center}

  1545   \end{center}

  1551   

  1546   

  1552   \noindent

  1547   \noindent

  1553   where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,

  1548   where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,

  1555   

  1550   

  1556   \begin{center}

  1551   \begin{center}

  1557   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}

  1552   \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}

  1558   {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}

  1553   {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}

  1559   \end{center}

  1554   \end{center}

  1573   recursive call.

  1568   recursive call.

  1574   \end{tabular}

  1569   \end{tabular}

  1575   \end{center}

  1570   \end{center}

  1576 

  1571 

  1577   \noindent

  1572   \noindent

  1579   that the premises of empty binding clauses are a special case of the clauses for 

  1574   that the premises of empty binding clauses are a special case of the clauses for 

  1580   non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}

  1575   non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}

  1581   for the existentially quantified permutation).

  1576   for the existentially quantified permutation).

  1582 

  1577 

  1583   Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}

  1578   Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}

  1584   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and

  1579   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and

  1585   $\approx_{\textit{bn}}$ with the following clauses:

  1580   $\approx_{\textit{bn}}$ with the following clauses:

  1586 

  1581 

  1588   \begin{tabular}{@ {}c @ {}}

  1583   \begin{tabular}{@ {}c @ {}}

  1589   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}

  1584   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}

  1590   {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\

  1585   {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\

  1591   \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}

  1586   \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}

  1592   {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}

  1587   {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}

  1593   \end{tabular}

  1588   \end{tabular}

  1594   \end{center}

  1589   \end{center}

  1595 

  1590 

  1597   \begin{tabular}{@ {}c @ {}}

  1592   \begin{tabular}{@ {}c @ {}}

  1598   \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}

  1593   \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}

  1599   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}

  1594   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}

  1600   {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}

  1595   {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}

  1601   \end{tabular}

  1596   \end{tabular}

  1602   \end{center}

  1597   \end{center}

  1603 

  1598 

  1605   \begin{tabular}{@ {}c @ {}}

  1600   \begin{tabular}{@ {}c @ {}}

  1606   \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}

  1601   \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}

  1607   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}

  1602   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}

  1608   {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}

  1603   {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}

  1609   \end{tabular}

  1604   \end{tabular}

  1610   \end{center}

  1605   \end{center}

  1611 

  1606 

  1612   \noindent

  1607   \noindent

  1613   Note the difference between  $\approx_{\textit{assn}}$ and

  1608   Note the difference between  $\approx_{\textit{assn}}$ and

  1615   the components in an assignment that are \emph{not} bound. This is needed in the 

  1610   the components in an assignment that are \emph{not} bound. This is needed in the 

  1616   clause for @{text "Let"} (which has

  1611   clause for @{text "Let"} (which has

  1617   a non-recursive binder). 

  1612   a non-recursive binder). 

  1618   The underlying reason is that the terms inside an assignment are not meant 

  1613   The underlying reason is that the terms inside an assignment are not meant 

  1619   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 

  1614   to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, 

  1622 

  1617 

  1623 section {* Establishing the Reasoning Infrastructure *}

  1618 section {* Establishing the Reasoning Infrastructure *}

  1624 

  1619 

  1625 text {*

  1620 text {*

  1626   Having made all necessary definitions for raw terms, we can start

  1621   Having made all necessary definitions for raw terms, we can start

  1628   @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch

  1623   @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch

  1629   in this section the proofs we need for establishing this infrastructure. One

  1624   in this section the proofs we need for establishing this infrastructure. One

  1630   main point of our work is that we have completely automated these proofs in Isabelle/HOL.

  1625   main point of our work is that we have completely automated these proofs in Isabelle/HOL.

  1631 

  1626 

  1632   First we establish that the

  1627   First we establish that the

  1634   equivalence relations.

  1629   equivalence relations.

  1635 

  1630 

  1637   Given the raw types @{text "ty"}$_{1..n}$ and binding functions

  1632   Given the raw types @{text "ty"}$_{1..n}$ and binding functions

  1638   @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 

  1633   @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 

  1639   @{text "\<approx>bn"}$_{1..m}$ are equivalence relations. and equivariant.

  1634   @{text "\<approx>bn"}$_{1..m}$ are equivalence relations. and equivariant.

  1641 

  1636 

  1642   \begin{proof} 

  1637   \begin{proof} 

  1643   The proof is by mutual induction over the definitions. The non-trivial

  1638   The proof is by mutual induction over the definitions. The non-trivial

  1644   cases involve premises built up by $\approx_{\textit{set}}$, 

  1639   cases involve premises built up by $\approx_{\textit{set}}$, 

  1645   $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 

  1640   $\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They 

  1646   can be dealt with as in Lemma~\ref{alphaeq}.

  1641   can be dealt with as in Lemma~\ref{alphaeq}.

  1647   \end{proof}

  1642   \end{proof}

  1648 

  1643 

  1649   \noindent 

  1644   \noindent 

  1650   We can feed this lemma into our quotient package and obtain new types @{text

  1645   We can feed this lemma into our quotient package and obtain new types @{text

  1652   We also obtain definitions for the term-constructors @{text

  1647   We also obtain definitions for the term-constructors @{text

  1653   "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text

  1648   "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text

  1654   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text

  1649   "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text

  1655   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text

  1650   "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text

  1656   "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the 

  1651   "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the 

  1667   @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 

  1662   @{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}} 

  1668   \end{equation}

  1663   \end{equation}

  1669   

  1664   

  1670   \noindent

  1665   \noindent

  1671   whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.

  1666   whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.

  1673   and establish that

  1668   and establish that

  1674   

  1669   

  1675   \begin{equation}\label{distinctraw}

  1670   \begin{equation}\label{distinctraw}

  1676   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}

  1671   \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}

  1677   \end{equation}

  1672   \end{equation}

  1678 

  1673 

  1679   \noindent

  1674   \noindent

  1680   holds for the corresponding raw term-constructors.

  1675   holds for the corresponding raw term-constructors.

  1681   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient

  1676   In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient

  1682   package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 

  1677   package needs to know that the raw term-constructors @{text "C"} and @{text "D"} 

  1684   Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types

  1679   Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types

  1685   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that

  1680   @{text "ty"}$_{1..r}$, respectfulness amounts to showing that

  1686   

  1681   

  1687   \begin{center}

  1682   \begin{center}

  1688   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1683   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1691   \noindent

  1686   \noindent

  1692   holds under the assumptions that we have \mbox{@{text

  1687   holds under the assumptions that we have \mbox{@{text

  1693   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}

  1688   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}

  1694   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and

  1689   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and

  1695   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this

  1690   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this

  1697   definition and by establishing the following auxiliary implications %facts 

  1692   definition and by establishing the following auxiliary implications %facts 

  1698   %

  1693   %

  1699   \begin{equation}\label{fnresp}

  1694   \begin{equation}\label{fnresp}

  1700   \mbox{%

  1695   \mbox{%

  1701   \begin{tabular}{ll@ {\hspace{7mm}}ll}

  1696   \begin{tabular}{ll@ {\hspace{7mm}}ll}

  1713   third \emph{only} holds because of our restriction

  1708   third \emph{only} holds because of our restriction

  1714   imposed on the form of the binding functions---namely \emph{not} returning 

  1709   imposed on the form of the binding functions---namely \emph{not} returning 

  1715   any bound atoms. In Ott, in contrast, the user may 

  1710   any bound atoms. In Ott, in contrast, the user may 

  1716   define @{text "bn"}$_{1..m}$ so that they return bound

  1711   define @{text "bn"}$_{1..m}$ so that they return bound

  1717   atoms and in this case the third implication is \emph{not} true. A 

  1712   atoms and in this case the third implication is \emph{not} true. A 

  1719   terms is impossible.

  1714   terms is impossible.

  1720 

  1715 

  1721   Having established respectfulness for the raw term-constructors, the 

  1716   Having established respectfulness for the raw term-constructors, the 

  1722   quotient package is able to automatically deduce \eqref{distinctalpha} from 

  1717   quotient package is able to automatically deduce \eqref{distinctalpha} from 

  1723   \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 

  1718   \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can 

  1726   \begin{center}

  1721   \begin{center}

  1727   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1722   @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}

  1728   \end{center}

  1723   \end{center}

  1729 

  1724 

  1730   \noindent

  1725   \noindent

  1733   

  1728   

  1734   \begin{center}

  1729   \begin{center}

  1735   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.

  1730   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.

  1736   \end{center}

  1731   \end{center}

  1737   

  1732   

  1738   \noindent

  1733   \noindent

  1739   We call these conditions as \emph{quasi-injectivity}. They correspond to

  1734   We call these conditions as \emph{quasi-injectivity}. They correspond to

  1741 

  1736 

  1742   Next we can lift the permutation 

  1737   Next we can lift the permutation 

  1743   operations defined in \eqref{ceqvt}. In order to make this 

  1738   operations defined in \eqref{ceqvt}. In order to make this 

  1744   lifting to go through, we have to show that the permutation operations are respectful. 

  1739   lifting to go through, we have to show that the permutation operations are respectful. 

  1745   This amounts to showing that the 

  1740   This amounts to showing that the 

  1747   , which we already established 

  1742   , which we already established 

  1748   in Lemma~\ref{equiv}. 

  1743   in Lemma~\ref{equiv}. 

  1749   As a result we can add the equations

  1744   As a result we can add the equations

  1750   

  1745   

  1751   \begin{equation}\label{calphaeqvt}

  1746   \begin{equation}\label{calphaeqvt}

  1780 

  1775 

  1781   \noindent 

  1776   \noindent 

  1782   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 

  1777   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are 

  1783   the recursive arguments of @{text "C\<AL>"}. 

  1778   the recursive arguments of @{text "C\<AL>"}. 

  1784 

  1779 

  1786   can first show that the free-atom functions and binding functions are

  1781   can first show that the free-atom functions and binding functions are

  1787   equivariant, namely

  1782   equivariant, namely

  1788   

  1783   

  1789   \begin{center}

  1784   \begin{center}

  1790   \begin{tabular}{rcl@ {\hspace{10mm}}rcl}

  1785   \begin{tabular}{rcl@ {\hspace{10mm}}rcl}

  1811   This can be again shown by induction 

  1806   This can be again shown by induction 

  1812   over @{text "ty\<AL>"}$_{1..n}$. 

  1807   over @{text "ty\<AL>"}$_{1..n}$. 

  1813   Lastly, we can show that the support of 

  1808   Lastly, we can show that the support of 

  1814   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.

  1809   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.

  1815   This fact is important in a nominal setting, but also provides evidence 

  1810   This fact is important in a nominal setting, but also provides evidence 

  1819   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have

  1814   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have

  1820   @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.

  1815   @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.

  1822 

  1817 

  1823   \begin{proof}

  1818   \begin{proof}

  1824   The proof is by induction. In each case

  1819   The proof is by induction. In each case

  1825   we unfold the definition of @{text "supp"}, move the swapping inside the 

  1820   we unfold the definition of @{text "supp"}, move the swapping inside the 

  1826   term-constructors and then use the quasi-injectivity lemmas in order to complete the

  1821   term-constructors and then use the quasi-injectivity lemmas in order to complete the

  1909 

  1904 

  1910 

  1905 

  1911 section {* Strong Induction Principles *}

  1906 section {* Strong Induction Principles *}

  1912 

  1907 

  1913 text {*

  1908 text {*

  1915   We call such induction principles \emph{weak}, because for a 

  1910   We call such induction principles \emph{weak}, because for a 

  1916   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}

  1911   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}

  1917   the induction hypothesis requires us to establish the implications \eqref{weakprem}.

  1912   the induction hypothesis requires us to establish the implications \eqref{weakprem}.

  1918   The problem with these implications is that in general they are difficult to establish.

  1913   The problem with these implications is that in general they are difficult to establish.

  1919   The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 

  1914   The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 

  2064   \end{tabular}

  2059   \end{tabular}

  2065   \end{center}

  2060   \end{center}

  2066   

  2061   

  2067   \noindent

  2062   \noindent

  2068   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 

  2063   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 

  2072   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}

  2067   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}

  2073   {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}

  2068   {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}

  2074     @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.

  2069     @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.

  2076 

  2071 

  2077   \begin{proof} 

  2072   \begin{proof} 

  2078   By induction on @{text x}. The equations follow by simple unfolding 

  2073   By induction on @{text x}. The equations follow by simple unfolding 

  2079   of the definitions. 

  2074   of the definitions. 

  2080   \end{proof}

  2075   \end{proof}

  2239   front-end for creating \LaTeX{} documents from specifications of

  2234   front-end for creating \LaTeX{} documents from specifications of

  2240   term-calculi involving general binders. For a subset of the specifications

  2235   term-calculi involving general binders. For a subset of the specifications

  2241   Ott can also generate theorem prover code using a raw representation of

  2236   Ott can also generate theorem prover code using a raw representation of

  2242   terms, and in Coq also a locally nameless representation. The developers of

  2237   terms, and in Coq also a locally nameless representation. The developers of

  2243   this tool have also put forward (on paper) a definition for

  2238   this tool have also put forward (on paper) a definition for

  2245   rather different from ours, not using any nominal techniques.  To our

  2240   rather different from ours, not using any nominal techniques.  To our

  2246   knowledge there is no concrete mathematical result concerning this

  2241   knowledge there is no concrete mathematical result concerning this

  2248   notion of free variables

  2243   notion of free variables

  2249   is work in progress.

  2244   is work in progress.

  2250 

  2245 

  2251   Although we were heavily inspired by the syntax of Ott,

  2246   Although we were heavily inspired by the syntax of Ott,

  2253   Nominal Isabelle. First, it is far too complicated to be a basis for

  2248   Nominal Isabelle. First, it is far too complicated to be a basis for

  2254   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  2249   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  2255   covers cases of binders depending on other binders, which just do not make

  2250   covers cases of binders depending on other binders, which just do not make

  2257   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2252   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2258   binding clauses. In Ott you specify binding clauses with a single body; we 

  2253   binding clauses. In Ott you specify binding clauses with a single body; we 

  2259   allow more than one. We have to do this, because this makes a difference 

  2254   allow more than one. We have to do this, because this makes a difference 

  2261   \isacommand{bind (set+)}. 

  2256   \isacommand{bind (set+)}. 

  2262   

  2257   

  2263   Consider the examples

  2258   Consider the examples

  2264   

  2259   

  2265   \begin{center}

  2260   \begin{center}

  2303   can be specified using special markers, written @{text "inner"} and 

  2298   can be specified using special markers, written @{text "inner"} and 

  2304   @{text "outer"}. It seems our and his specifications can be

  2299   @{text "outer"}. It seems our and his specifications can be

  2305   inter-translated as long as ours use the binding mode 

  2300   inter-translated as long as ours use the binding mode 

  2306   \isacommand{bind} only.

  2301   \isacommand{bind} only.

  2307   However, we have not proved this. Pottier gives a definition for 

  2302   However, we have not proved this. Pottier gives a definition for 

  2309   Still, this definition is rather different from ours and he only proves that

  2304   Still, this definition is rather different from ours and he only proves that

  2310   it defines an equivalence relation. A complete

  2305   it defines an equivalence relation. A complete

  2311   reasoning infrastructure is well beyond the purposes of his language. 

  2306   reasoning infrastructure is well beyond the purposes of his language. 

  2312   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.

  2307   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.

  2313   

  2308   

  2314   In a slightly different domain (programming with dependent types), the 

  2309   In a slightly different domain (programming with dependent types), the 

  2315   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2310   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2317   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it

  2312   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it

  2318   has a more operational flavour and calculates a partial (renaming) map. 

  2313   has a more operational flavour and calculates a partial (renaming) map. 

  2319   In this way, the definition can deal with vacuous binders. However, to our

  2314   In this way, the definition can deal with vacuous binders. However, to our

  2320   best knowledge, no concrete mathematical result concerning this

  2315   best knowledge, no concrete mathematical result concerning this

  2322 *}

  2317 *}

  2323 

  2318 

  2324 section {* Conclusion *}

  2319 section {* Conclusion *}

  2325 

  2320 

  2326 text {*

  2321 text {*

  2327   We have presented an extension of Nominal Isabelle for dealing with

  2325   We have presented an extension of Nominal Isabelle for dealing with

  2328   general binders, that is term-constructors having multiple bound 

  2326   general binders, that is term-constructors having multiple bound 

  2329   variables. For this extension we introduced new definitions of 

  2327   variables. For this extension we introduced new definitions of 

  2331   To specify general binders we used the specifications from Ott, but extended them 

  2329   To specify general binders we used the specifications from Ott, but extended them 

  2332   in some places and restricted

  2330   in some places and restricted

  2334   We also introduced two binding modes (set and set+) that do not 

  2332   We also introduced two binding modes (set and set+) that do not 

  2335   exist in Ott. 

  2333   exist in Ott. 

  2336   We have tried out the extension with calculi such as Core-Haskell, type-schemes 

  2334   We have tried out the extension with calculi such as Core-Haskell, type-schemes 

  2337   and approximately a  dozen of other typical examples from programming 

  2335   and approximately a  dozen of other typical examples from programming 

  2338   language research~\cite{SewellBestiary}. 

  2336   language research~\cite{SewellBestiary}. 

  2341   it can be downloaded from the Mercurial repository linked at

  2339   it can be downloaded from the Mercurial repository linked at

  2342   \href{http://isabelle.in.tum.de/nominal/download}

  2340   \href{http://isabelle.in.tum.de/nominal/download}

  2343   {http://isabelle.in.tum.de/nominal/download}.}

  2341   {http://isabelle.in.tum.de/nominal/download}.}

  2344 

  2342 

  2345   We have left out a discussion about how functions can be defined over

  2343   We have left out a discussion about how functions can be defined over

  2347   Isabelle this turned out to be a thorny issue.  We

  2345   Isabelle this turned out to be a thorny issue.  We

  2348   hope to do better this time by using the function package that has recently

  2346   hope to do better this time by using the function package that has recently

  2349   been implemented in Isabelle/HOL and also by restricting function

  2347   been implemented in Isabelle/HOL and also by restricting function

  2350   definitions to equivariant functions (for them we can

  2348   definitions to equivariant functions (for them we can

  2351   provide more automation).

  2349   provide more automation).

  2369   

  2367   

  2370   \noindent

  2368   \noindent

  2371   allow us to support more interesting binding functions. 

  2369   allow us to support more interesting binding functions. 

  2372   

  2370   

  2373   We have also not yet played with other binding modes. For example we can

  2371   We have also not yet played with other binding modes. For example we can

  2388 *}

  2384 *}

  2389 

  2385 

  2390 

  2386 

  2391 (*<*)