19   fresh ("_ # _" [51, 51] 50) and

    19   fresh ("_ # _" [51, 51] 50) and

    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and

    20   fresh_star ("_ #\<^sup>* _" [51, 51] 50) and

    21   supp ("supp _" [78] 73) and

    21   supp ("supp _" [78] 73) and

    22   uminus ("-_" [78] 73) and

    22   uminus ("-_" [78] 73) and

    23   If  ("if _ then _ else _" 10) and

    23   If  ("if _ then _ else _" 10) and

    27   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and

    27   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and

    28   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and

    28   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and

    29   fv ("fv'(_')" [100] 100) and

    29   fv ("fv'(_')" [100] 100) and

    30   equal ("=") and

    30   equal ("=") and

    31   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 

    31   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 

    44 

    44 

    45 text {*

    45 text {*

    46 %%%  @{text "(1, (2, 3))"}

    46 %%%  @{text "(1, (2, 3))"}

    47 

    47 

    48   So far, Nominal Isabelle provides a mechanism for constructing

    48   So far, Nominal Isabelle provides a mechanism for constructing

    50 

    50 

    51   \begin{center}

    51   \begin{center}

    52   @{text "t ::= x | t t | \<lambda>x. t"}

    52   @{text "t ::= x | t t | \<lambda>x. t"}

    53   \end{center}

    53   \end{center}

    54 

    54 

    55   \noindent

    55   \noindent

    57   Nominal Isabelle derives automatically a reasoning infrastructure that has

    57   Nominal Isabelle derives automatically a reasoning infrastructure that has

    58   been used successfully in formalisations of an equivalence checking

    58   been used successfully in formalisations of an equivalence checking

    59   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

    59   algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed

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

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

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

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

    85   also there one would like to bind multiple variables at once.

    85   also there one would like to bind multiple variables at once.

    86 

    86 

    87   Binding multiple variables has interesting properties that cannot be captured

    87   Binding multiple variables has interesting properties that cannot be captured

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

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

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

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

    91   %

    91   %

    92   \begin{equation}\label{ex1}

    92   \begin{equation}\label{ex1}

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

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

    94   \end{equation}

    94   \end{equation}

    95 

    95 

    96   \noindent

    96   \noindent

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

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

    99   %

    99   %

   100   \begin{equation}\label{ex2}

   100   \begin{equation}\label{ex2}

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

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

   102   \end{equation}

   102   \end{equation}

   103 

   103 

   104   \noindent

   104   \noindent

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

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

   107   %

   107   %

   108   \begin{equation}\label{ex3}

   108   \begin{equation}\label{ex3}

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

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

   110   \end{equation}

   110   \end{equation}

   111 

   111 

   112   \noindent

   112   \noindent

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

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

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

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

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

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

   118   Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 

   118   Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 

   119 

   119 

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

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

   122   %

   122   %

   123   \begin{equation}\label{one}

   123   \begin{equation}\label{one}

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

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

   125   \end{equation}

   125   \end{equation}

   126 

   126 

   127   \noindent

   127   \noindent

   131   %

   131   %

   132   \begin{center}

   132   \begin{center}

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

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

   134   \end{center}

   134   \end{center}

   135 

   135 

   147   \end{equation}

   147   \end{equation}

   148 

   148 

   149   \noindent

   149   \noindent

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

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

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

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

   153   %

   153   %

   154   \begin{center}

   154   \begin{center}

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

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

   156   \end{center}

   156   \end{center}

   157   %

   157   %

   174   but we do care about the information that there are as many @{text

   174   but we do care about the information that there are as many @{text

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

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

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

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

   177   %

   177   %

   178   \begin{center}

   178   \begin{center}

   192   %

   191   %

   193   \begin{center}

   192   \begin{center}

   194   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}

   193   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}

   195   @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ 

   194   @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ 

   197                                  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]

   196                                  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]

   198   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\

   197   @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\

   200   \end{tabular}

   199   \end{tabular}

   201   \end{center}

   200   \end{center}

   202 

   201 

   203   \noindent

   202   \noindent

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

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

   232   some sense in the context of Coq's type theory (which Ott supports), but not

   231   some sense in the context of Coq's type theory (which Ott supports), but not

   233   at all in a HOL-based environment where every datatype must have a non-empty

   232   at all in a HOL-based environment where every datatype must have a non-empty

   234   set-theoretic model \cite{Berghofer99}.

   233   set-theoretic model \cite{Berghofer99}.

   235 

   234 

   236   Another reason is that we establish the reasoning infrastructure

   235   Another reason is that we establish the reasoning infrastructure

   238   infrastructure in Isabelle/HOL for

   237   infrastructure in Isabelle/HOL for

   240   and the raw terms produced by Ott use names for bound variables,

   239   and the raw terms produced by Ott use names for bound variables,

   242   that the two type-schemes

   241   that the two type-schemes

   243 

   242 

   244   \begin{center}

   243   \begin{center}

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

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

   246   \end{center}

   245   \end{center}

   247   

   246   

   248   \noindent

   247   \noindent

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

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

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

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

   253   to).  

   252   to).  

   254 

   253 

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

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

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

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

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

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

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

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

   262   requires a lot of extra reasoning work.

   261   requires a lot of extra reasoning work.

   263 

   262 

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

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

   266   the Isabelle/HOL theorem prover is a rather non-trivial task. For every

   265   the Isabelle/HOL theorem prover is a rather non-trivial task. For every

   267   specification we will need to construct a type containing as elements the

   266   specification we will need to construct a type containing as elements the

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

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

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

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

   271 

   270 

   272   \begin{center}

   271   \begin{center}

   273   \begin{tikzpicture}

   272   \begin{tikzpicture}

   293   \end{tikzpicture}

   292   \end{tikzpicture}

   294   \end{center}

   293   \end{center}

   295 

   294 

   296   \noindent

   295   \noindent

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

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

   301   (non-emptiness is satisfied whenever the raw terms are definable as datatype

   300   (non-emptiness is satisfied whenever the raw terms are definable as datatype

   303   indeed an equivalence relation).

   302   indeed an equivalence relation).

   304 

   303 

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

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

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

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

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

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

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

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

   310   reasoning about a well-formedness predicate.

   309   reasoning about a well-formedness predicate.

   311 

   310 

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

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

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

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

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

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

   315   task. To ease it, we re-implemented in Isabelle/HOL the quotient package

   314   task. To ease it, we re-implemented in Isabelle/HOL the quotient package

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

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

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

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

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

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

   320 

   319 

   321   \begin{center}

   320   \begin{center}

   322   @{text "fv(x) = {x}"}\hspace{10mm}

   321   @{text "fv(x) = {x}"}\hspace{10mm}

   323   @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]

   322   @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]

   324   @{text "fv(\<lambda>x.t) = fv(t) - {x}"}

   323   @{text "fv(\<lambda>x.t) = fv(t) - {x}"}

   325   \end{center}

   324   \end{center}

   326   

   325   

   327   \noindent

   326   \noindent

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

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

   330   lifted function is characterised by the equations

   329   lifted function is characterised by the equations

   331 

   330 

   332   \begin{center}

   331   \begin{center}

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

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

   334   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]

   333   @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]

   336   \end{center}

   335   \end{center}

   337 

   336 

   338   \noindent

   337   \noindent

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   350 

   349 

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

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

   352   helpful includes the term language of System @{text "F\<^isub>C"}, also

   351   helpful includes the term language of System @{text "F\<^isub>C"}, also

   353   known as Core-Haskell (see Figure~\ref{corehas}). This term language

   352   known as Core-Haskell (see Figure~\ref{corehas}). This term language

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

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

   357   be bound. Another is that each bound variable comes with a kind or type

   356   be bound. Another is that each bound variable comes with a kind or type

   358   annotation. Representing such binders with single binders and reasoning

   357   annotation. Representing such binders with single binders and reasoning

   359   about them in a theorem prover would be a major pain.  \medskip

   358   about them in a theorem prover would be a major pain.  \medskip

   360 

   359 

   361   \noindent

   360   \noindent

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

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

   366   terms, including properties about support, freshness and equality

   365   terms, including properties about support, freshness and equality

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

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

   369 

   372 

   370   \begin{figure}

   373   \begin{figure}

   371   \begin{boxedminipage}{\linewidth}

   374   \begin{boxedminipage}{\linewidth}

   372   \begin{center}

   375   \begin{center}

   373   \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}

   376   \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}

   470   \end{center}

   473   \end{center}

   471 

   474 

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

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

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

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

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

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

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

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

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

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

   478   @{text x}, namely:

   481   @{text x}, namely:

   479   %

   482   %

   480   \begin{equation}\label{suppdef}

   483   \begin{equation}\label{suppdef}

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

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

   503   \end{property}

   506   \end{property}

   504 

   507 

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

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

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

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

   508   %

   511   %

   509   \begin{eqnarray}

   512   \begin{eqnarray}

   510   @{term "supp a"} & = & @{term "{a}"}\\

   513   @{term "supp a"} & = & @{term "{a}"}\\

   511   @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\

   514   @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\

   512   @{term "supp []"} & = & @{term "{}"}\\

   515   @{term "supp []"} & = & @{term "{}"}\\

   515   @{term "supp b"} & = & @{term "{}"}\\

   518   @{term "supp b"} & = & @{term "{}"}\\

   516   @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}

   519   @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}

   517   \end{eqnarray}

   520   \end{eqnarray}

   518   

   521   

   519   \noindent 

   522   \noindent 

   521   only an approximation can be established (see \eqref{suppfun} above). Reasoning about

   524   only an approximation can be established (see \eqref{suppfun} above). Reasoning about

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

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

   523   as follows:

   526   as follows:

   524 

   527 

   525   \begin{defn}

   528   \begin{defn}

   530   \noindent

   533   \noindent

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

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

   532   two properties.

   535   two properties.

   533 

   536 

   534   \begin{property}\label{supportsprop}

   537   \begin{property}\label{supportsprop}

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

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

   537   \end{property}

   541   \end{property}

   538 

   542 

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

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

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

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

   544   @{term "\<forall>p. p \<bullet> f = f"}

   548   @{term "\<forall>p. p \<bullet> f = f"}

   545   \end{equation}

   549   \end{equation}

   546 

   550 

   547   \noindent or equivalently that a permutation applied to the application

   551   \noindent or equivalently that a permutation applied to the application

   548   @{text "f x"} can be moved to the argument @{text x}. That means for equivariant

   552   @{text "f x"} can be moved to the argument @{text x}. That means for equivariant

   550   %

   554   %

   551   \begin{equation}\label{equivariance}

   555   \begin{equation}\label{equivariance}

   552   @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;

   556   @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;

   553   @{text "p \<bullet> (f x) = f (p \<bullet> x)"}

   557   @{text "p \<bullet> (f x) = f (p \<bullet> x)"}

   554   \end{equation}

   558   \end{equation}

   558   can easily deduce that equivariant functions have empty support. There is

   562   can easily deduce that equivariant functions have empty support. There is

   559   also a similar notion for equivariant relations, say @{text R}, namely the property

   563   also a similar notion for equivariant relations, say @{text R}, namely the property

   560   that

   564   that

   561   %

   565   %

   562   \begin{center}

   566   \begin{center}

   564   \end{center}

   568   \end{center}

   565 

   569 

   566   Finally, the nominal logic work provides us with general means to rename 

   570   Finally, the nominal logic work provides us with general means to rename 

   567   binders. While in the older version of Nominal Isabelle, we used extensively 

   571   binders. While in the older version of Nominal Isabelle, we used extensively 

   568   Property~\ref{swapfreshfresh} for renaming single binders, this property 

   572   Property~\ref{swapfreshfresh} for renaming single binders, this property 

   570   following generalisations turned out to be easier to use.

   574   following generalisations turned out to be easier to use.

   571 

   575 

   572   \begin{property}\label{supppermeq}

   576   \begin{property}\label{supppermeq}

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

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

   574   \end{property}

   578   \end{property}

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

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

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

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

   592 

   596 

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

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

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

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

   596   the presence of multiple binders.

   600   the presence of multiple binders.

   597 *}

   601 *}

   598 

   602 

   599 

   603 

   600 section {* General Binders\label{sec:binders} *}

   604 section {* General Binders\label{sec:binders} *}

   605   from this specification (remember that Nominal Isabelle is a definitional

   609   from this specification (remember that Nominal Isabelle is a definitional

   606   extension of Isabelle/HOL, which does not introduce any new axioms).

   610   extension of Isabelle/HOL, which does not introduce any new axioms).

   607 

   611 

   608   In order to keep our work with deriving the reasoning infrastructure

   612   In order to keep our work with deriving the reasoning infrastructure

   609   manageable, we will wherever possible state definitions and perform proofs

   613   manageable, we will wherever possible state definitions and perform proofs

   611   generates them anew for each specification. To that end, we will consider

   615   generates them anew for each specification. To that end, we will consider

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

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

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

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

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

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

   615 

   619 

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

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

   620   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

   624   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom

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

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

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

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

   626   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The

   630   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The

   627   requirements {\it i)} to {\it iv)} can be stated formally as follows:

   631   requirements {\it i)} to {\it iv)} can be stated formally as follows:

   628   %

   632   %

   629   \begin{equation}\label{alphaset}

   633   \begin{equation}\label{alphaset}

   636   \end{array}

   640   \end{array}

   637   \end{equation}

   641   \end{equation}

   638 

   642 

   639   \noindent

   643   \noindent

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

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

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

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

   643   dependent on a free-variable function @{text "fv"} and a relation @{text

   647   dependent on a free-variable function @{text "fv"} and a relation @{text

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

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

   647   will prove that @{text "fv"} is equal to @{text "supp"}.

   651   will prove that @{text "fv"} is equal to @{text "supp"}.

   648 

   652 

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

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

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

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

   652   as follows

   656   as follows

   653   %

   657   %

   654   \begin{equation}\label{alphalist}

   658   \begin{equation}\label{alphalist}

   661   \end{array}

   665   \end{array}

   662   \end{equation}

   666   \end{equation}

   663   

   667   

   664   \noindent

   668   \noindent

   666   Now the last clause ensures that the order of the binders matters (since @{text as}

   670   Now the last clause ensures that the order of the binders matters (since @{text as}

   667   and @{text bs} are lists of atoms).

   671   and @{text bs} are lists of atoms).

   668 

   672 

   669   If we do not want to make any difference between the order of binders \emph{and}

   673   If we do not want to make any difference between the order of binders \emph{and}

   670   also allow vacuous binders, then we keep sets of binders, but drop the fourth 

   674   also allow vacuous binders, then we keep sets of binders, but drop the fourth 

   671   condition in \eqref{alphaset}:

   675   condition in \eqref{alphaset}:

   672   %

   676   %

   673   \begin{equation}\label{alphares}

   677   \begin{equation}\label{alphares}

   679   \end{array}

   683   \end{array}

   680   \end{equation}

   684   \end{equation}

   681 

   685 

   686 

   691 

   687   \begin{center}

   692   \begin{center}

   688   @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}

   693   @{text "fv(x) = {x}"}  \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}

   689   \end{center}

   694   \end{center}

   690 

   695 

   691   \noindent

   696   \noindent

   692   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and

   697   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   707   abstract a single atom.

   712   abstract a single atom.

   708 

   713 

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

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

   710   types. For this we define 

   715   types. For this we define 

   711   %

   716   %

   712   \begin{equation}

   717   \begin{equation}

   713   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}

   718   @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}

   714   \end{equation}

   719   \end{equation}

   715   

   720   

   716   \noindent

   721   \noindent

   719   relations and equivariant.

   724   relations and equivariant.

   720 

   725 

   721   \begin{lemma}\label{alphaeq} 

   726   \begin{lemma}\label{alphaeq} 

   724   "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>

   729   "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>

   725   bs, p \<bullet> y)"} (similarly for the other two relations).

   730   bs, p \<bullet> y)"} (similarly for the other two relations).

   726   \end{lemma}

   731   \end{lemma}

   727 

   732 

   728   \begin{proof}

   733   \begin{proof}

   734   \end{proof}

   739   \end{proof}

   735 

   740 

   736   \noindent

   741   \noindent

   737   This lemma allows us to use our quotient package and introduce 

   742   This lemma allows us to use our quotient package and introduce 

   738   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}

   743   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}

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

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

   741   (in the third case). 

   746   (in the third case). 

   742   The elements in these types will be, respectively, written as:

   747   The elements in these types will be, respectively, written as:

   743 

   748 

   744   \begin{center}

   749   \begin{center}

   781   @{thm permute_Abs[no_vars]}

   786   @{thm permute_Abs[no_vars]}

   782   \end{equation}

   787   \end{equation}

   783 

   788 

   784   \noindent

   789   \noindent

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

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

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

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

   789   

   794   

   790   \begin{lemma}

   795   \begin{lemma}

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

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

   792   \end{lemma}

   797   \end{lemma}

   793 

   798 

   843   form @{term "Abs as x"} etc is motivated by the fact that 

   848   form @{term "Abs as x"} etc is motivated by the fact that 

   844   we can conveniently establish  at the Isabelle/HOL level

   849   we can conveniently establish  at the Isabelle/HOL level

   845   properties about them.  It would be

   850   properties about them.  It would be

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

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

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

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

   849 *}

   854 *}

   850 

   855 

   851 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}

   856 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}

   852 

   857 

   853 text {*

   858 text {*

   881   \end{tabular}}

   886   \end{tabular}}

   882   \end{equation}

   887   \end{equation}

   883 

   888 

   884   \noindent

   889   \noindent

   885   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 

   890   Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of 

   887   types that stand for the types of the arguments of the term-constructor.

   892   types that stand for the types of the arguments of the term-constructor.

   888   For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with

   893   For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with

   889 

   894 

   890   \begin{center}

   895   \begin{center}

   891   @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 

   896   @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"} 

   916 

   921 

   917   \noindent

   922   \noindent

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

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

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

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

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

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

   922   clause will be called \emph{bodies} (there can be more than one); the

   927   clause will be called \emph{bodies} (there can be more than one); the

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

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

   924   Ott, we allow multiple labels in binders and bodies. For example we allow

   929   Ott, we allow multiple labels in binders and bodies. For example we allow

   925   binding clauses of the form:

   930   binding clauses of the form:

   926 

   931 

   927   \begin{center}

   932   \begin{center}

   928   \begin{tabular}{@ {}ll@ {}}

   933   \begin{tabular}{@ {}ll@ {}}

   930       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\

   935       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\

   932       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 

   937       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, 

   933       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\

   938       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\

   934   \end{tabular}

   939   \end{tabular}

   935   \end{center}

   940   \end{center}

   936 

   941 

   937   \noindent

   942   \noindent

   938   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}

   943   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}

   939   and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics

   944   and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics

   941   show this later with an example.

   946   show this later with an example.

   942   

   947   

   945   binders we distinguish between \emph{shallow} and \emph{deep} binders.

   954   binders we distinguish between \emph{shallow} and \emph{deep} binders.

   946   Shallow binders are just labels. The restriction we need to impose on them

   955   Shallow binders are just labels. The restriction we need to impose on them

   947   is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the

   956   is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the

   948   labels must either refer to atom types or to sets of atom types; in case of

   957   labels must either refer to atom types or to sets of atom types; in case of

   949   \isacommand{bind} the labels must refer to atom types or lists of atom

   958   \isacommand{bind} the labels must refer to atom types or lists of atom

   952   set of names is bound:

   961   set of names is bound:

   953 

   962 

   954   \begin{center}

   963   \begin{center}

   955   \begin{tabular}{@ {}cc@ {}}

   964   \begin{tabular}{@ {}cc@ {}}

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

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

   958   \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\

   967   \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\

   959   \hspace{5mm}$\mid$~@{text "App lam lam"}\\

   968   \hspace{5mm}$\mid$~@{text "App lam lam"}\\

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

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

   961   \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\

   970   \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\

   962   \end{tabular} &

   971   \end{tabular} &

   963   \begin{tabular}{@ {}l@ {}}

   972   \begin{tabular}{@ {}l@ {}}

   965   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\

   974   \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\

   966   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\

   975   \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\

   967   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\

   976   \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\

   968   \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\

   977   \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\

   969   \end{tabular}

   978   \end{tabular}

   970   \end{tabular}

   979   \end{tabular}

   971   \end{center}

   980   \end{center}

   972 

   981 

   973   \noindent

   982   \noindent

   974   Note that for @{text lam} it does not matter which binding mode we use. The

   985   Note that for @{text lam} it does not matter which binding mode we use. The

   975   reason is that we bind only a single @{text name}. However, having

   986   reason is that we bind only a single @{text name}. However, having

   976   \isacommand{bind\_set} or \isacommand{bind} in the second case makes a

   987   \isacommand{bind\_set} or \isacommand{bind} in the second case makes a

   980 

   989 

   981 

   990 

   982   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

   991   A \emph{deep} binder uses an auxiliary binding function that ``picks'' out

   983   the atoms in one argument of the term-constructor, which can be bound in

   992   the atoms in one argument of the term-constructor, which can be bound in

   984   other arguments and also in the same argument (we will call such binders

   993   other arguments and also in the same argument (we will call such binders

   986   expected to return either a set of atoms (for \isacommand{bind\_set} and

   995   expected to return either a set of atoms (for \isacommand{bind\_set} and

   987   \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can

   996   \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can

   988   be defined by primitive recursion over the corresponding type; the equations

   997   be defined by primitive recursion over the corresponding type; the equations

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

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

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

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

  1006   \hspace{5mm}$\mid$~@{text "PVar name"}\\

  1015   \hspace{5mm}$\mid$~@{text "PVar name"}\\

  1007   \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 

  1016   \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 

  1008   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\

  1017   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\

  1009   \isacommand{where}~@{text "bn(PNil) = []"}\\

  1018   \isacommand{where}~@{text "bn(PNil) = []"}\\

  1010   \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\

  1019   \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\

  1012   \end{tabular}}

  1021   \end{tabular}}

  1013   \end{equation}

  1022   \end{equation}

  1014   

  1023   

  1015   \noindent

  1024   \noindent

  1016   In this specification the function @{text "bn"} determines which atoms of

  1025   In this specification the function @{text "bn"} determines which atoms of

  1054 

  1063 

  1055   \noindent

  1064   \noindent

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

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

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

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

  1058   inside the assignment. This difference has consequences for the free-variable 

  1067   inside the assignment. This difference has consequences for the free-variable 

  1061   we cannot have more than one binding function for one binder. So we exclude:

  1072   we cannot have more than one binding function for one binder. So we exclude:

  1062 

  1073 

  1063   \begin{center}

  1074   \begin{center}

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

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

  1074   We also need to restrict the form of the binding functions. As will shortly

  1085   We also need to restrict the form of the binding functions. As will shortly

  1075   become clear, we cannot return an atom in a binding function that is also

  1086   become clear, we cannot return an atom in a binding function that is also

  1076   bound in the corresponding term-constructor. That means in the example

  1087   bound in the corresponding term-constructor. That means in the example

  1077   \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may

  1088   \eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may

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

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

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

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

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

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

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

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

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

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

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

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

  1087   later on.

  1100   later on.

  1088   

  1101   

  1089   In order to simplify our definitions, we shall assume specifications 

  1102   In order to simplify our definitions, we shall assume specifications 

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

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

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

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

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

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

  1094   of the lambda-calculus, the completion produces

  1107   of the lambda-calculus, the completion produces

  1095 

  1108 

  1115   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 

  1128   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 

  1116   re-arranging the arguments of

  1129   re-arranging the arguments of

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

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

  1118   result in inadequate representations. Therefore we will first

  1131   result in inadequate representations. Therefore we will first

  1119   extract datatype definitions from the specification and then define 

  1132   extract datatype definitions from the specification and then define 

  1121 

  1134 

  1122 

  1135 

  1123   The datatype definition can be obtained by stripping off the 

  1136   The datatype definition can be obtained by stripping off the 

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

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

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

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

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

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

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

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

  1129   for the corresponding notion defined on the ``raw'' level. So for example 

  1142   for the corresponding notion defined on the ``raw'' level. So for example 

  1130   we have

  1143   we have

  1131   

  1144   

  1132   \begin{center}

  1145   \begin{center}

  1133   @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}

  1146   @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}

  1148   %

  1161   %

  1149   \begin{equation}\label{ceqvt}

  1162   \begin{equation}\label{ceqvt}

  1150   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}

  1163   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}

  1151   \end{equation}

  1164   \end{equation}

  1152   

  1165   

  1155   free variable functions:

  1189   free variable functions:

  1156 

  1190 

  1157   \begin{center}

  1191   \begin{center}

  1158   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  1192   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  1159   @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\

  1193   @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\

  1165   \noindent 

  1199   \noindent 

  1166   Like the coercion function @{text atom}, @{text "atoms"} coerces 

  1200   Like the coercion function @{text atom}, @{text "atoms"} coerces 

  1167   the set of atoms to a set of the generic atom type.

  1201   the set of atoms to a set of the generic atom type.

  1168   It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.

  1202   It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.

  1169 

  1203 

  1190 

  1204 

  1191   While the idea behind these free-variable functions is clear (they just

  1205   While the idea behind these free-variable functions is clear (they just

  1192   collect all atoms that are not bound), because of our rather complicated

  1206   collect all atoms that are not bound), because of our rather complicated

  1193   binding mechanisms their definitions are somewhat involved.  Given a

  1207   binding mechanisms their definitions are somewhat involved.  Given a

  1194   term-constructor @{text "C"} of type @{text ty} and some associated binding

  1208   term-constructor @{text "C"} of type @{text ty} and some associated binding

  1245 

  1259 

  1246   \noindent

  1260   \noindent

  1247   The reason why we only have to treat the empty binding clauses specially in

  1261   The reason why we only have to treat the empty binding clauses specially in

  1248   the definition of @{text "fv_bn"} is that binding functions can only use arguments

  1262   the definition of @{text "fv_bn"} is that binding functions can only use arguments

  1249   that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot

  1263   that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot

  1251 

  1265 

  1252 

  1266 

  1253   To see how these definitions work in practice, let us reconsider the term-constructors 

  1267   To see how these definitions work in practice, let us reconsider the term-constructors 

  1254   @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 

  1268   @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 

  1255   For this specification we need to define three free-variable functions, namely

  1269   For this specification we need to define three free-variable functions, namely

  1286   context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.  

  1300   context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.  

  1287   This is a phenomenon 

  1301   This is a phenomenon 

  1288   that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because

  1302   that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because

  1289   we would not be able to lift a @{text "bn"}-function that is defined over 

  1303   we would not be able to lift a @{text "bn"}-function that is defined over 

  1290   arguments that are either binders or bodies. In that case @{text "bn"} would

  1304   arguments that are either binders or bodies. In that case @{text "bn"} would

  1292   %

  1306   %

  1293   \begin{equation}\label{bnprop}

  1307   \begin{equation}\label{bnprop}

  1294   @{text "fv_ty x  =  bn x \<union> fv_bn x"}.

  1308   @{text "fv_ty x  =  bn x \<union> fv_bn x"}.

  1295   \end{equation}

  1309   \end{equation}

  1296 

  1310 

  1297   \noindent

  1311   \noindent

  1298   holds for any @{text "bn"}-function defined for the type @{text "ty"}.

  1312   holds for any @{text "bn"}-function defined for the type @{text "ty"}.

  1299 

  1313 

  1301   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 

  1315   @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, 

  1303   Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.

  1317   Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.

  1304   To simplify our definitions we will use the following abbreviations for 

  1318   To simplify our definitions we will use the following abbreviations for 

  1305   relations and free-variable acting on products.

  1319   relations and free-variable acting on products.

  1306   %

  1320   %

  1307   \begin{center}

  1321   \begin{center}

  1310   @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\

  1324   @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\

  1311   \end{tabular}

  1325   \end{tabular}

  1312   \end{center}

  1326   \end{center}

  1313 

  1327 

  1314 

  1328 

  1316   conclusions of the form  

  1330   conclusions of the form  

  1317   %

  1331   %

  1318   \begin{center}

  1332   \begin{center}

  1319   @{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"} 

  1333   @{text "C x\<^isub>1 \<dots> x\<^isub>n  \<approx>ty  C y\<^isub>1 \<dots> y\<^isub>n"} 

  1320   \end{center}

  1334   \end{center}

  1373   of excluding overlapping deep binders, as these would need to be translated into separate

  1387   of excluding overlapping deep binders, as these would need to be translated into separate

  1374   abstractions.

  1388   abstractions.

  1375 

  1389 

  1376 

  1390 

  1377 

  1391 

  1379   are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}

  1393   are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}

  1380   and need to generate appropriate premises. We generate first premises according to the first three

  1394   and need to generate appropriate premises. We generate first premises according to the first three

  1381   rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 

  1395   rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated 

  1382   differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the 

  1396   differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the 

  1383   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:

  1397   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:

  1425   \end{tabular}

  1439   \end{tabular}

  1426   \end{center}

  1440   \end{center}

  1427 

  1441 

  1428   \noindent

  1442   \noindent

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

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

  1431   the components in an assignment that are \emph{not} bound. Therefore we have

  1445   the components in an assignment that are \emph{not} bound. Therefore we have

  1432   a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 

  1446   a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is 

  1433   a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 

  1447   a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant 

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

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

  1435   because there everything from the assignment is under the binder. 

  1449   because there everything from the assignment is under the binder. 

  1437 

  1451 

  1438 section {* Establishing the Reasoning Infrastructure *}

  1452 section {* Establishing the Reasoning Infrastructure *}

  1439 

  1453 

  1440 text {*

  1454 text {*

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

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

  1443   user originally specified. We sketch in this section the facts we need for establishing

  1457   user originally specified. We sketch in this section the facts we need for establishing

  1444   this reasoning infrastructure. First we have to show that the

  1458   this reasoning infrastructure. First we have to show that the

  1446   equivalence relations.

  1460   equivalence relations.

  1447 

  1461 

  1448   \begin{lemma}\label{equiv} 

  1462   \begin{lemma}\label{equiv} 

  1449   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions

  1463   Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions

  1450   @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and 

  1464   @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and 

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

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

  1459   \end{proof}

  1473   \end{proof}

  1460 

  1474 

  1461   \noindent 

  1475   \noindent 

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

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

  1464   definitions for the term-constructors @{text

  1478   definitions for the term-constructors @{text

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

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

  1466   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text

  1480   "C"}$_{1..m}$, and similar definitions for the free-variable functions @{text

  1467   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text

  1481   "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text

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

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

  1477   \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 

  1491   \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} 

  1478   @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} 

  1492   @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.} 

  1479   \end{equation}

  1493   \end{equation}

  1480   

  1494   

  1481   \noindent

  1495   \noindent

  1483   for the raw term-constructors

  1497   for the raw term-constructors

  1484   %

  1498   %

  1485   \begin{equation}\label{distinctraw}

  1499   \begin{equation}\label{distinctraw}

  1486   \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}

  1500   \mbox{@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;$\not\approx$@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}

  1487   \end{equation}

  1501   \end{equation}

  1488 

  1502 

  1489   \noindent

  1503   \noindent

  1490   In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient

  1504   In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient

  1491   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 

  1505   package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"} 

  1493   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types

  1507   Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types

  1494   @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that

  1508   @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that

  1495   

  1509   

  1496   \begin{center}

  1510   \begin{center}

  1497   @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}

  1511   @{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}

  1498   \end{center}  

  1512   \end{center}  

  1499 

  1513 

  1500   \noindent

  1514   \noindent

  1502   and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by 

  1516   and  @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by 

  1503   analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish 

  1517   analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish 

  1504   the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 

  1518   the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined 

  1505   for the type @{text ty\<^isub>i}, we have that

  1519   for the type @{text ty\<^isub>i}, we have that

  1506   %

  1520   %

  1511   \noindent

  1525   \noindent

  1512   This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. 

  1526   This can be established by induction on the definition of @{text "\<approx>ty\<^isub>i"}. 

  1513    

  1527    

  1514   Having established respectfulness for every raw term-constructor, the 

  1528   Having established respectfulness for every raw term-constructor, the 

  1515   quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.

  1529   quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.

  1517   as long as they contain raw term-constructors only. The 

  1531   as long as they contain raw term-constructors only. The 

  1518   induction principles derived by the datatype package in Isabelle/HOL for the types @{text

  1532   induction principles derived by the datatype package in Isabelle/HOL for the types @{text

  1519   "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure

  1533   "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure

  1520   induction principles that establish

  1534   induction principles that establish

  1521 

  1535 

  1538   Next we lift the permutation operations defined in \eqref{ceqvt} for

  1552   Next we lift the permutation operations defined in \eqref{ceqvt} for

  1539   the raw term-constructors @{text "C"}. These facts contain, in addition 

  1553   the raw term-constructors @{text "C"}. These facts contain, in addition 

  1540   to the term-constructors, also permutation operations. In order to make the 

  1554   to the term-constructors, also permutation operations. In order to make the 

  1541   lifting go through, 

  1555   lifting go through, 

  1542   we have to know that the permutation operations are respectful 

  1556   we have to know that the permutation operations are respectful 

  1545   in Lemma~\ref{equiv}. As a result we can establish the equations

  1559   in Lemma~\ref{equiv}. As a result we can establish the equations

  1546   

  1560   

  1547   \begin{equation}\label{calphaeqvt}

  1561   \begin{equation}\label{calphaeqvt}

  1548   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

  1562   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

  1549   \end{equation}

  1563   \end{equation}

  1578   \begin{center}

  1592   \begin{center}

  1579   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}

  1593   @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}

  1580   \end{center}

  1594   \end{center}

  1581 

  1595 

  1582   \noindent

  1596   \noindent

  1585 

  1599 

  1586   \begin{center}

  1600   \begin{center}

  1587   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}

  1601   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}

  1588   \end{center}

  1602   \end{center}

  1589 

  1603 

  1590   \noindent

  1604   \noindent

  1591   We call these conditions as \emph{quasi-injectivity}. Except for one function, which

  1605   We call these conditions as \emph{quasi-injectivity}. Except for one function, which

  1592   we have to lift in the next section, we completed

  1606   we have to lift in the next section, we completed

  1593   the lifting part of establishing the reasoning infrastructure. 

  1607   the lifting part of establishing the reasoning infrastructure. 

  1594 

  1608 

  1596   the free-variable functions and binding functions

  1610   the free-variable functions and binding functions

  1597   are equivariant, namely

  1611   are equivariant, namely

  1598 

  1612 

  1599   \begin{center}

  1613   \begin{center}

  1600   \begin{tabular}{rcl}

  1614   \begin{tabular}{rcl}

  1607   \noindent

  1621   \noindent

  1608   These properties can be established by structural induction over the @{text x}

  1622   These properties can be established by structural induction over the @{text x}

  1609   (using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).

  1623   (using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).

  1610 

  1624 

  1611   Until now we have not yet derived anything about the support of the 

  1625   Until now we have not yet derived anything about the support of the 

  1613   the strong induction principles in the next section.

  1627   the strong induction principles in the next section.

  1614   Using the equivariance properties in \eqref{ceqvt} we can

  1628   Using the equivariance properties in \eqref{ceqvt} we can

  1615   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 

  1629   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 

  1616 

  1630 

  1617   \begin{center}

  1631   \begin{center}

  1725 

  1739 

  1726 section {* Strong Induction Principles *}

  1740 section {* Strong Induction Principles *}

  1727 

  1741 

  1728 text {*

  1742 text {*

  1729   In the previous section we were able to provide induction principles that 

  1743   In the previous section we were able to provide induction principles that 

  1731   We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},

  1745   We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},

  1732   the induction hypothesis requires us to establish the implication

  1746   the induction hypothesis requires us to establish the implication

  1733   %

  1747   %

  1734   \begin{equation}\label{weakprem}

  1748   \begin{equation}\label{weakprem}

  1735   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 

  1749   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"} 

  1770   \end{tabular}

  1784   \end{tabular}

  1771   \end{center}

  1785   \end{center}

  1772   

  1786   

  1773   \noindent

  1787   \noindent

  1774   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 

  1788   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 

  1776 

  1790 

  1777   \begin{lemma}\label{permutebn} 

  1791   \begin{lemma}\label{permutebn} 

  1778   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}

  1792   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}

  1779   {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}

  1793   {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"} and {\it ii)}

  1780     @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.

  1794     @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^esub>\<^sup>\<alpha> x)"}.

  1949   front-end for creating \LaTeX{} documents from specifications of

  1963   front-end for creating \LaTeX{} documents from specifications of

  1950   term-calculi involving general binders. For a subset of the specifications,

  1964   term-calculi involving general binders. For a subset of the specifications,

  1951   Ott can also generate theorem prover code using a raw representation of

  1965   Ott can also generate theorem prover code using a raw representation of

  1952   terms, and in Coq also a locally nameless representation. The developers of

  1966   terms, and in Coq also a locally nameless representation. The developers of

  1953   this tool have also put forward (on paper) a definition for

  1967   this tool have also put forward (on paper) a definition for

  1955   rather different from ours, not using any nominal techniques.  To our

  1969   rather different from ours, not using any nominal techniques.  To our

  1956   knowledge there is also no concrete mathematical result concerning this

  1970   knowledge there is also no concrete mathematical result concerning this

  1958   in a term are work in progress in Ott.

  1972   in a term are work in progress in Ott.

  1959 

  1973 

  1960   Although we were heavily inspired by their syntax,

  1974   Although we were heavily inspired by their syntax,

  1962   Nominal Isabelle. First, it is far too complicated to be a basis for

  1976   Nominal Isabelle. First, it is far too complicated to be a basis for

  1963   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  1977   automated proofs implemented on the ML-level of Isabelle/HOL. Second, it

  1964   covers cases of binders depending on other binders, which just do not make

  1978   covers cases of binders depending on other binders, which just do not make

  1966   meaning in a HOL-based theorem prover. We also had to generalise slightly their 

  1980   meaning in a HOL-based theorem prover. We also had to generalise slightly their 

  1967   binding clauses. In Ott you specify binding clauses with a single body; we 

  1981   binding clauses. In Ott you specify binding clauses with a single body; we 

  1968   allow more than one. We have to do this, because this makes a difference 

  1982   allow more than one. We have to do this, because this makes a difference 

  1970   \isacommand{bind\_res}. This makes 

  1984   \isacommand{bind\_res}. This makes 

  1971 

  1985 

  1972   \begin{center}

  1986   \begin{center}

  1984 

  2012 

  1985   \begin{center}

  2013   \begin{center}

  1986   \begin{tabular}{c}

  2014   \begin{tabular}{c}

  1987   @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\

  2015   @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\

  1988   @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\

  2016   @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\

  2014   can be indicated with some special constructs, written @{text "inner"} and 

  2042   can be indicated with some special constructs, written @{text "inner"} and 

  2015   @{text "outer"}. With this, it seems, our and his specifications can be

  2043   @{text "outer"}. With this, it seems, our and his specifications can be

  2016   inter-translated, but we have not proved this. However, we believe the

  2044   inter-translated, but we have not proved this. However, we believe the

  2017   binding specifications in the style of Ott are a more natural way for 

  2045   binding specifications in the style of Ott are a more natural way for 

  2018   representing terms involving bindings. Pottier gives a definition for 

  2046   representing terms involving bindings. Pottier gives a definition for 

  2020   Although he uses also a permutation in case of abstractions, his

  2048   Although he uses also a permutation in case of abstractions, his

  2021   definition is rather different from ours. He proves that his notion

  2049   definition is rather different from ours. He proves that his notion

  2023   reasoning infrastructure is well beyond the purposes of his language. 

  2051   reasoning infrastructure is well beyond the purposes of his language. 

  2024   In a slightly different domain (programming with dependent types), the 

  2052   In a slightly different domain (programming with dependent types), the 

  2025   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2053   paper \cite{Altenkirch10} presents a calculus with a notion of 

  2027   This definition is similar to the one by Pottier, except that it

  2055   This definition is similar to the one by Pottier, except that it

  2028   has a more operational flavour and calculates a partial (renaming) map. 

  2056   has a more operational flavour and calculates a partial (renaming) map. 

  2029   In this way they can handle vacous binders. However, their notion of

  2057   In this way they can handle vacous binders. However, their notion of

  2030   equality between terms also includes rules for $\beta$ and to our

  2058   equality between terms also includes rules for $\beta$ and to our

  2031   knowledge no concrete mathematical result concerning their notion

  2059   knowledge no concrete mathematical result concerning their notion

  2047   it can be downloaded from the Mercurial repository linked at

  2075   it can be downloaded from the Mercurial repository linked at

  2048   \href{http://isabelle.in.tum.de/nominal/download}

  2076   \href{http://isabelle.in.tum.de/nominal/download}

  2049   {http://isabelle.in.tum.de/nominal/download}.

  2077   {http://isabelle.in.tum.de/nominal/download}.

  2050 

  2078 

  2051   We have left out a discussion about how functions can be defined over

  2079   We have left out a discussion about how functions can be defined over

  2053   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We

  2081   Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue.  We

  2054   hope to do better this time by using the function package that has recently

  2082   hope to do better this time by using the function package that has recently

  2055   been implemented in Isabelle/HOL and also by restricting function

  2083   been implemented in Isabelle/HOL and also by restricting function

  2056   definitions to equivariant functions (for such functions it is possible to

  2084   definitions to equivariant functions (for such functions it is possible to

  2057   provide more automation).

  2085   provide more automation).

  2090   many discussions about Nominal Isabelle. We thank Peter Sewell for 

  2118   many discussions about Nominal Isabelle. We thank Peter Sewell for 

  2091   making the informal notes \cite{SewellBestiary} available to us and 

  2119   making the informal notes \cite{SewellBestiary} available to us and 

  2092   also for patiently explaining some of the finer points of the work on the Ott-tool. We

  2120   also for patiently explaining some of the finer points of the work on the Ott-tool. We

  2093   also thank Stephanie Weirich for suggesting to separate the subgrammars

  2121   also thank Stephanie Weirich for suggesting to separate the subgrammars

  2094   of kinds and types in our Core-Haskell example.  

  2122   of kinds and types in our Core-Haskell example.  

  2095 *}

  2126 *}

  2096 

  2127 

  2097 (*<*)

  2128 (*<*)

  2098 end

  2129 end

  2099 (*>*)

  2130 (*>*)