Paper/Paper.thy
changeset 2514 69780ae147f5
parent 2513 ae860c95bf9f
child 2515 06a8f782b2c1
equal deleted inserted replaced
2513:ae860c95bf9f 2514:69780ae147f5
   122   %
   122   %
   123   \noindent
   123   \noindent
   124   where @{text z} does not occur freely in the type.  In this paper we will
   124   where @{text z} does not occur freely in the type.  In this paper we will
   125   give a general binding mechanism and associated notion of $\alpha$-equivalence
   125   give a general binding mechanism and associated notion of $\alpha$-equivalence
   126   that can be used to faithfully represent this kind of binding in Nominal
   126   that can be used to faithfully represent this kind of binding in Nominal
   127   Isabelle.  The difficulty of finding the right notion for $\alpha$-equivalence
   127   Isabelle.  
   128   can be appreciated in this case by considering that the definition given by
   128   %The difficulty of finding the right notion for $\alpha$-equivalence
   129   Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
   129   %can be appreciated in this case by considering that the definition given by
       
   130   %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). 
   130 
   131 
   131   However, the notion of $\alpha$-equivalence that is preserved by vacuous
   132   However, the notion of $\alpha$-equivalence that is preserved by vacuous
   132   binders is not always wanted. For example in terms like
   133   binders is not always wanted. For example in terms like
   133   %
   134   %
   134   \begin{equation}\label{one}
   135   \begin{equation}\label{one}
   238   allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
   239   allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
   239   types like @{text "t ::= t t | \<lambda>x. t"}
   240   types like @{text "t ::= t t | \<lambda>x. t"}
   240   where no clause for variables is given. Arguably, such specifications make
   241   where no clause for variables is given. Arguably, such specifications make
   241   some sense in the context of Coq's type theory (which Ott supports), but not
   242   some sense in the context of Coq's type theory (which Ott supports), but not
   242   at all in a HOL-based environment where every datatype must have a non-empty
   243   at all in a HOL-based environment where every datatype must have a non-empty
   243   set-theoretic model \cite{Berghofer99}.
   244   set-theoretic model. % \cite{Berghofer99}.
   244 
   245 
   245   Another reason is that we establish the reasoning infrastructure
   246   Another reason is that we establish the reasoning infrastructure
   246   for $\alpha$-\emph{equated} terms. In contrast, Ott produces  a reasoning 
   247   for $\alpha$-\emph{equated} terms. In contrast, Ott produces  a reasoning 
   247   infrastructure in Isabelle/HOL for
   248   infrastructure in Isabelle/HOL for
   248   \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms
   249   \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms
   259   only support specifications that make sense on the level of $\alpha$-equated
   260   only support specifications that make sense on the level of $\alpha$-equated
   260   terms (offending specifications, which for example bind a variable according
   261   terms (offending specifications, which for example bind a variable according
   261   to a variable bound somewhere else, are not excluded by Ott, but we have
   262   to a variable bound somewhere else, are not excluded by Ott, but we have
   262   to).  
   263   to).  
   263 
   264 
   264   Our insistence on reasoning with $\alpha$-equated terms comes from the
   265   %Our insistence on reasoning with $\alpha$-equated terms comes from the
   265   wealth of experience we gained with the older version of Nominal Isabelle:
   266   %wealth of experience we gained with the older version of Nominal Isabelle:
   266   for non-trivial properties, reasoning with $\alpha$-equated terms is much
   267   %for non-trivial properties, reasoning with $\alpha$-equated terms is much
   267   easier than reasoning with raw terms. The fundamental reason for this is
   268   %easier than reasoning with raw terms. The fundamental reason for this is
   268   that the HOL-logic underlying Nominal Isabelle allows us to replace
   269   %that the HOL-logic underlying Nominal Isabelle allows us to replace
   269   ``equals-by-equals''. In contrast, replacing
   270   %``equals-by-equals''. In contrast, replacing
   270   ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
   271   %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
   271   requires a lot of extra reasoning work.
   272   %requires a lot of extra reasoning work.
   272 
   273 
   273   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   274   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   274   terms is nearly always taken for granted, establishing it automatically in
   275   terms is nearly always taken for granted, establishing it automatically in
   275   the Isabelle/HOL is a rather non-trivial task. For every
   276   the Isabelle/HOL is a rather non-trivial task. For every
   276   specification we will need to construct a type containing as elements the
   277   specification we will need to construct a type containing as elements the
   347   \noindent
   348   \noindent
   348   (Note that this means also the term-constructors for variables, applications
   349   (Note that this means also the term-constructors for variables, applications
   349   and lambda are lifted to the quotient level.)  This construction, of course,
   350   and lambda are lifted to the quotient level.)  This construction, of course,
   350   only works if $\alpha$-equivalence is indeed an equivalence relation, and the
   351   only works if $\alpha$-equivalence is indeed an equivalence relation, and the
   351   ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
   352   ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
   352   For example, we will not be able to lift a bound-variable function. Although
   353   %For example, we will not be able to lift a bound-variable function. Although
   353   this function can be defined for raw terms, it does not respect
   354   %this function can be defined for raw terms, it does not respect
   354   $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
   355   %$\alpha$-equivalence and therefore cannot be lifted. 
       
   356   To sum up, every lifting
   355   of theorems to the quotient level needs proofs of some respectfulness
   357   of theorems to the quotient level needs proofs of some respectfulness
   356   properties (see \cite{Homeier05}). In the paper we show that we are able to
   358   properties (see \cite{Homeier05}). In the paper we show that we are able to
   357   automate these proofs and as a result can automatically establish a reasoning 
   359   automate these proofs and as a result can automatically establish a reasoning 
   358   infrastructure for $\alpha$-equated terms.\smallskip
   360   infrastructure for $\alpha$-equated terms.\smallskip
   359 
   361 
   377   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
   379   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
   378   that our specifications make sense for reasoning about $\alpha$-equated terms.  
   380   that our specifications make sense for reasoning about $\alpha$-equated terms.  
   379   The main improvement over Ott is that we introduce three binding modes
   381   The main improvement over Ott is that we introduce three binding modes
   380   (only one is present in Ott), provide definitions for $\alpha$-equivalence and 
   382   (only one is present in Ott), provide definitions for $\alpha$-equivalence and 
   381   for free variables of our terms, and also derive a reasoning infrastructure
   383   for free variables of our terms, and also derive a reasoning infrastructure
   382   about our specifications inside Isabelle/HOL.
   384   for our specifications inside Isabelle/HOL.
   383 
   385 
   384 
   386 
   385   %\begin{figure}
   387   %\begin{figure}
   386   %\begin{boxedminipage}{\linewidth}
   388   %\begin{boxedminipage}{\linewidth}
   387   %%\begin{center}
   389   %%\begin{center}
   446 
   448 
   447   Permutations are bijective functions from atoms to atoms that are 
   449   Permutations are bijective functions from atoms to atoms that are 
   448   the identity everywhere except on a finite number of atoms. There is a 
   450   the identity everywhere except on a finite number of atoms. There is a 
   449   two-place permutation operation written
   451   two-place permutation operation written
   450   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   452   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
   451   where the generic type @{text "\<beta>"} stands for the type of the object 
   453   where the generic type @{text "\<beta>"} is the type of the object 
   452   over which the permutation 
   454   over which the permutation 
   453   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   455   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   454   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   456   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   455   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   457   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   456   operation is defined over the type-hierarchy \cite{HuffmanUrban10};
   458   operation is defined over the type-hierarchy \cite{HuffmanUrban10};
   502   A striking consequence of these definitions is that we can prove
   504   A striking consequence of these definitions is that we can prove
   503   without knowing anything about the structure of @{term x} that
   505   without knowing anything about the structure of @{term x} that
   504   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
   506   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
   505   @{text x} unchanged:
   507   @{text x} unchanged:
   506 
   508 
   507   \begin{property}\label{swapfreshfresh}
   509   \begin{myproperty}\label{swapfreshfresh}
   508   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
   510   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
   509   \end{property}
   511   \end{myproperty}
   510 
   512 
   511   %While often the support of an object can be relatively easily 
   513   %While often the support of an object can be relatively easily 
   512   %described, for example for atoms, products, lists, function applications, 
   514   %described, for example for atoms, products, lists, function applications, 
   513   %booleans and permutations as follows
   515   %booleans and permutations as follows
   514   %%
   516   %%
   544   %
   546   %
   545   %\noindent
   547   %\noindent
   546   %The main point of @{text supports} is that we can establish the following 
   548   %The main point of @{text supports} is that we can establish the following 
   547   %two properties.
   549   %two properties.
   548   %
   550   %
   549   %\begin{property}\label{supportsprop}
   551   %\begin{myproperty}\label{supportsprop}
   550   %Given a set @{text "as"} of atoms.
   552   %Given a set @{text "as"} of atoms.
   551   %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
   553   %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
   552   %{\it (ii)} @{thm supp_supports[no_vars]}.
   554   %{\it (ii)} @{thm supp_supports[no_vars]}.
   553   %\end{property}
   555   %\end{myproperty}
   554   %
   556   %
   555   %Another important notion in the nominal logic work is \emph{equivariance}.
   557   %Another important notion in the nominal logic work is \emph{equivariance}.
   556   %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
   558   %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
   557   %it is required that every permutation leaves @{text f} unchanged, that is
   559   %it is required that every permutation leaves @{text f} unchanged, that is
   558   %%
   560   %%
   587   %Property~\ref{swapfreshfresh}
   589   %Property~\ref{swapfreshfresh}
   588   this property to rename single binders, it %%this property 
   590   this property to rename single binders, it %%this property 
   589   proved too unwieldy for dealing with multiple binders. For such binders the 
   591   proved too unwieldy for dealing with multiple binders. For such binders the 
   590   following generalisations turned out to be easier to use.
   592   following generalisations turned out to be easier to use.
   591 
   593 
   592   \begin{property}\label{supppermeq}
   594   \begin{myproperty}\label{supppermeq}
   593   @{thm[mode=IfThen] supp_perm_eq[no_vars]}
   595   @{thm[mode=IfThen] supp_perm_eq[no_vars]}
   594   \end{property}
   596   \end{myproperty}
   595 
   597 
   596   \begin{property}\label{avoiding}
   598   \begin{myproperty}\label{avoiding}
   597   For a finite set @{text as} and a finitely supported @{text x} with
   599   For a finite set @{text as} and a finitely supported @{text x} with
   598   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
   600   @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
   599   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
   601   exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
   600   @{term "supp x \<sharp>* p"}.
   602   @{term "supp x \<sharp>* p"}.
   601   \end{property}
   603   \end{myproperty}
   602 
   604 
   603   \noindent
   605   \noindent
   604   The idea behind the second property is that given a finite set @{text as}
   606   The idea behind the second property is that given a finite set @{text as}
   605   of binders (being bound, or fresh, in @{text x} is ensured by the
   607   of binders (being bound, or fresh, in @{text x} is ensured by the
   606   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
   608   assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that
   758   This lemma allows us to use our quotient package for introducing 
   760   This lemma allows us to use our quotient package for introducing 
   759   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   761   new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
   760   representing $\alpha$-equivalence classes of pairs of type 
   762   representing $\alpha$-equivalence classes of pairs of type 
   761   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
   763   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
   762   (in the third case). 
   764   (in the third case). 
   763   The elements in these types will be, respectively, written as:
   765   The elements in these types will be, respectively, written as
   764 
   766   %
   765   \begin{center}
   767   %\begin{center}
   766   @{term "Abs_set as x"} \hspace{5mm} 
   768   @{term "Abs_set as x"}, %\hspace{5mm} 
   767   @{term "Abs_res as x"} \hspace{5mm}
   769   @{term "Abs_res as x"} and %\hspace{5mm}
   768   @{term "Abs_lst as x"} 
   770   @{term "Abs_lst as x"}, 
   769   \end{center}
   771   %\end{center}
   770 
   772   %
   771   \noindent
   773   %\noindent
   772   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
   774   indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
   773   call the types \emph{abstraction types} and their elements
   775   call the types \emph{abstraction types} and their elements
   774   \emph{abstractions}. The important property we need to derive is the support of 
   776   \emph{abstractions}. The important property we need to derive is the support of 
   775   abstractions, namely:
   777   abstractions, namely:
   776 
   778 
   873 
   875 
   874 section {* Specifying General Bindings\label{sec:spec} *}
   876 section {* Specifying General Bindings\label{sec:spec} *}
   875 
   877 
   876 text {*
   878 text {*
   877   Our choice of syntax for specifications is influenced by the existing
   879   Our choice of syntax for specifications is influenced by the existing
   878   datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
   880   datatype package of Isabelle/HOL %\cite{Berghofer99} 
       
   881   and by the syntax of the
   879   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
   882   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
   880   collection of (possibly mutual recursive) type declarations, say @{text
   883   collection of (possibly mutual recursive) type declarations, say @{text
   881   "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
   884   "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
   882   binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
   885   binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
   883   syntax in Nominal Isabelle for such specifications is roughly as follows:
   886   syntax in Nominal Isabelle for such specifications is roughly as follows:
   973   $\alpha$-equivalence where it is ensured that within a given scope an 
   976   $\alpha$-equivalence where it is ensured that within a given scope an 
   974   atom occurrence cannot be both bound and free at the same time.  The first
   977   atom occurrence cannot be both bound and free at the same time.  The first
   975   restriction is that a body can only occur in
   978   restriction is that a body can only occur in
   976   \emph{one} binding clause of a term constructor (this ensures that the bound
   979   \emph{one} binding clause of a term constructor (this ensures that the bound
   977   atoms of a body cannot be free at the same time by specifying an
   980   atoms of a body cannot be free at the same time by specifying an
   978   alternative binder for the same body). For binders we distinguish between
   981   alternative binder for the same body). 
       
   982 
       
   983   For binders we distinguish between
   979   \emph{shallow} and \emph{deep} binders.  Shallow binders are just
   984   \emph{shallow} and \emph{deep} binders.  Shallow binders are just
   980   labels. The restriction we need to impose on them is that in case of
   985   labels. The restriction we need to impose on them is that in case of
   981   \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
   986   \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
   982   refer to atom types or to sets of atom types; in case of \isacommand{bind}
   987   refer to atom types or to sets of atom types; in case of \isacommand{bind}
   983   the labels must refer to atom types or lists of atom types. Two examples for
   988   the labels must refer to atom types or lists of atom types. Two examples for
  1106 
  1111 
  1107   \noindent
  1112   \noindent
  1108   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
  1113   Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"}  pick 
  1109   out different atoms to become bound, respectively be free, in @{text "p"}.
  1114   out different atoms to become bound, respectively be free, in @{text "p"}.
  1110   (Since the Ott-tool does not derive a reasoning infrastructure for 
  1115   (Since the Ott-tool does not derive a reasoning infrastructure for 
  1111   $\alpha$-equated terms, it can permit such specifications.)
  1116   $\alpha$-equated terms with deep binders, it can permit such specifications.)
  1112   
  1117   
  1113   We also need to restrict the form of the binding functions in order 
  1118   We also need to restrict the form of the binding functions in order 
  1114   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
  1119   to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated 
  1115   terms. The main restriction is that we cannot return an atom in a binding function that is also
  1120   terms. The main restriction is that we cannot return an atom in a binding function that is also
  1116   bound in the corresponding term-constructor. That means in \eqref{letpat} 
  1121   bound in the corresponding term-constructor. That means in \eqref{letpat} 
  1179   for the corresponding notion given on the ``raw'' level. So for example 
  1184   for the corresponding notion given on the ``raw'' level. So for example 
  1180   we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
  1185   we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
  1181   where @{term ty} is the type used in the quotient construction for 
  1186   where @{term ty} is the type used in the quotient construction for 
  1182   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
  1187   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
  1183 
  1188 
  1184   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
  1189   %The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
  1185   non-empty and the types in the constructors only occur in positive 
  1190   %non-empty and the types in the constructors only occur in positive 
  1186   position (see \cite{Berghofer99} for an in-depth description of the datatype package
  1191   %position (see \cite{Berghofer99} for an in-depth description of the datatype package
  1187   in Isabelle/HOL). We subsequently define each of the user-specified binding 
  1192   %in Isabelle/HOL). 
       
  1193   We subsequently define each of the user-specified binding 
  1188   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
  1194   functions @{term "bn"}$_{1..m}$ by recursion over the corresponding 
  1189   raw datatype. We can also easily define permutation operations by 
  1195   raw datatype. We can also easily define permutation operations by 
  1190   recursion so that for each term constructor @{text "C"} we have that
  1196   recursion so that for each term constructor @{text "C"} we have that
  1191   %
  1197   %
  1192   \begin{equation}\label{ceqvt}
  1198   \begin{equation}\label{ceqvt}
  1672   holds under the assumptions that we have \mbox{@{text
  1678   holds under the assumptions that we have \mbox{@{text
  1673   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
  1679   "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
  1674   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
  1680   and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
  1675   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
  1681   @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
  1676   implication by applying the corresponding rule in our $\alpha$-equivalence
  1682   implication by applying the corresponding rule in our $\alpha$-equivalence
  1677   definition and by establishing the following auxiliary facts 
  1683   definition and by establishing the following auxiliary implications %facts 
  1678   %
  1684   %
  1679   \begin{equation}\label{fnresp}
  1685   \begin{equation}\label{fnresp}
  1680   \mbox{%
  1686   \mbox{%
  1681   \begin{tabular}{l}
  1687   \begin{tabular}{ll@ {\hspace{7mm}}ll}
  1682   @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\
  1688   \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
  1683   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\
  1689   \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
  1684   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
  1690 
  1685   @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
  1691   \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
       
  1692   \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
  1686   \end{tabular}}
  1693   \end{tabular}}
  1687   \end{equation}
  1694   \end{equation}
  1688 
  1695 
  1689   \noindent
  1696   \noindent
  1690   They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
  1697   They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first,
  1708 
  1715 
  1709   \noindent
  1716   \noindent
  1710   are $\alpha$-equivalent. This gives us conditions when the corresponding
  1717   are $\alpha$-equivalent. This gives us conditions when the corresponding
  1711   $\alpha$-equated terms are \emph{equal}, namely
  1718   $\alpha$-equated terms are \emph{equal}, namely
  1712   %
  1719   %
  1713   \begin{center}
  1720   %\begin{center}
  1714   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
  1721   @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
  1715   \end{center}
  1722   %\end{center}
  1716 
  1723   %
  1717   \noindent
  1724   %\noindent
  1718   We call these conditions as \emph{quasi-injectivity}. They correspond to
  1725   We call these conditions as \emph{quasi-injectivity}. They correspond to
  1719   the premises in our $\alpha$-equivalence relations.
  1726   the premises in our $\alpha$-equivalence relations.
  1720 
  1727 
  1721   Next we can lift the permutation 
  1728   Next we can lift the permutation 
  1722   operations defined in \eqref{ceqvt}. In order to make this 
  1729   operations defined in \eqref{ceqvt}. In order to make this 
  1742   Finally we can add to our infrastructure a cases lemma (explained in the next section)
  1749   Finally we can add to our infrastructure a cases lemma (explained in the next section)
  1743   and a structural induction principle 
  1750   and a structural induction principle 
  1744   for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
  1751   for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
  1745   of the form
  1752   of the form
  1746   %
  1753   %
  1747   \begin{equation}\label{weakinduct}
  1754   %\begin{equation}\label{weakinduct}
  1748   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
  1755   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
  1749   \end{equation} 
  1756   %\end{equation} 
  1750 
  1757   %
  1751   \noindent
  1758   %\noindent
  1752   whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
  1759   whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ 
  1753   have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
  1760   have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
  1754   term constructor @{text "C"}$^\alpha$ a premise of the form
  1761   term constructor @{text "C"}$^\alpha$ a premise of the form
  1755   %
  1762   %
  1756   \begin{equation}\label{weakprem}
  1763   \begin{equation}\label{weakprem}
  1764   By working now completely on the $\alpha$-equated level, we
  1771   By working now completely on the $\alpha$-equated level, we
  1765   can first show that the free-atom functions and binding functions are
  1772   can first show that the free-atom functions and binding functions are
  1766   equivariant, namely
  1773   equivariant, namely
  1767   %
  1774   %
  1768   \begin{center}
  1775   \begin{center}
  1769   \begin{tabular}{rcl}
  1776   \begin{tabular}{rcl@ {\hspace{10mm}}rcl}
  1770   @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\
  1777   @{text "p \<bullet> (fa_ty\<AL>\<^isub>i  x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &
       
  1778   @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\
  1771   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
  1779   @{text "p \<bullet> (fa_bn\<AL>\<^isub>j  x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
  1772   @{text "p \<bullet> (bn\<AL>\<^isub>j  x)"}    & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}
       
  1773   \end{tabular}
  1780   \end{tabular}
  1774   \end{center}
  1781   \end{center}
  1775 
  1782   %
  1776   \noindent
  1783   \noindent
  1777   These properties can be established using the induction principle
  1784   These properties can be established using the induction principle.
  1778   in \eqref{weakinduct}.
  1785   %%in \eqref{weakinduct}.
  1779   Having these equivariant properties established, we can
  1786   Having these equivariant properties established, we can
  1780   show for every term-constructor @{text "C\<^sup>\<alpha>"} that 
  1787   show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
  1781 
  1788   the support of its arguments, that means 
  1782   \begin{center}
  1789 
  1783   @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
  1790   \begin{center}
       
  1791   @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
  1784   \end{center}
  1792   \end{center}
  1785  
  1793  
  1786   \noindent
  1794   \noindent
  1787   holds. This together with Property~\ref{supportsprop} allows us to prove
  1795   holds. This allows us to prove by induction that
  1788   that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, 
  1796   every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported. 
  1789   namely @{text "finite (supp x)"}. This can be again shown by induction 
  1797   %This can be again shown by induction 
  1790   over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of 
  1798   %over @{text "ty\<AL>"}$_{1..n}$. 
       
  1799   Lastly, we can show that the support of 
  1791   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
  1800   elements in  @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
  1792   This fact is important in a nominal setting, but also provides evidence 
  1801   This fact is important in a nominal setting, but also provides evidence 
  1793   that our notions of free-atoms and $\alpha$-equivalence are correct.
  1802   that our notions of free-atoms and $\alpha$-equivalence are correct.
  1794 
  1803 
  1795   \begin{lemma} 
  1804   \begin{theorem} 
  1796   For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
  1805   For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
  1797   @{text "supp x = fa_ty\<AL>\<^isub>i x"}.
  1806   @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
  1798   \end{lemma}
  1807   \end{theorem}
  1799 
  1808 
  1800   \begin{proof}
  1809   \begin{proof}
  1801   The proof is by induction. In each case
  1810   The proof is by induction. In each case
  1802   we unfold the definition of @{text "supp"}, move the swapping inside the 
  1811   we unfold the definition of @{text "supp"}, move the swapping inside the 
  1803   term-constructors and then use the quasi-injectivity lemmas in order to complete the
  1812   term-constructors and then use the quasi-injectivity lemmas in order to complete the
  1886 
  1895 
  1887 
  1896 
  1888 section {* Strong Induction Principles *}
  1897 section {* Strong Induction Principles *}
  1889 
  1898 
  1890 text {*
  1899 text {*
  1891   In the previous section we were able to provide induction principles that 
  1900   In the previous section we derived induction principles for $\alpha$-equated terms. 
  1892   allow us to perform structural inductions over $\alpha$-equated terms. 
  1901   We call such induction principles \emph{weak}, because for a 
  1893   We call such induction principles \emph{weak}, because in case of the 
  1902   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
  1894   term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
       
  1895   the induction hypothesis requires us to establish the implications \eqref{weakprem}.
  1903   the induction hypothesis requires us to establish the implications \eqref{weakprem}.
  1896   The problem with these implications is that in general they are difficult to establish.
  1904   The problem with these implications is that in general they are difficult to establish.
  1897   The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} 
  1905   The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}. 
  1898   (for example we cannot assume the variable convention for them).
  1906   %%(for example we cannot assume the variable convention for them).
  1899 
  1907 
  1900   In \cite{UrbanTasson05} we introduced a method for automatically
  1908   In \cite{UrbanTasson05} we introduced a method for automatically
  1901   strengthening weak induction principles for terms containing single
  1909   strengthening weak induction principles for terms containing single
  1902   binders. These stronger induction principles allow the user to make additional
  1910   binders. These stronger induction principles allow the user to make additional
  1903   assumptions about binders. 
  1911   assumptions about binders. 
  1904   These additional assumptions amount to a formal
  1912   %These additional assumptions amount to a formal
  1905   version of the informal variable convention for binders. A natural question is
  1913   %version of the informal variable convention for binders. 
  1906   whether we can also strengthen the weak induction principles involving
  1914   To sketch how this strengthening extends to the case of multiple binders, we use as
  1907   the general binders presented here. We will indeed be able to so, but for this we need an 
  1915   running example the term-constructors @{text "Lam"} and @{text "Let"}
  1908   additional notion for permuting deep binders. 
  1916   from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
  1909 
  1917   the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
  1910   Given a binding function @{text "bn"} we define an auxiliary permutation 
  1918   where the additional parameter @{text c} controls
  1911   operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
  1919   which freshness assumptions the binders should satisfy. For the two term constructors 
  1912   Assuming a clause of @{text bn} is given as 
  1920   this means that the user has to establish in inductions the implications
  1913   %
  1921   %
  1914   \begin{center}
  1922   \begin{center}
  1915   @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
  1923   \begin{tabular}{l}
  1916   \end{center}
  1924   @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
  1917 
  1925   @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
  1918   \noindent 
  1926   \end{tabular}
  1919   then we define 
  1927   \end{center}
       
  1928 
       
  1929   In \cite{UrbanTasson05} we showed how the weaker induction principles imply
       
  1930   the stronger ones. This was done by some quite complicated, nevertheless automated,
       
  1931   induction proofs. In this paper we simplify this work by leveraging the automated proof
       
  1932   methods from the function package of Isabelle/HOL generates. 
       
  1933 
       
  1934   The reasoning principle we employ here is well-founded induction. For this we have to discharge
       
  1935   two proof obligations: one is that we have
       
  1936   well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 
       
  1937   every induction step and the other is that we have covered all cases. 
       
  1938   As measures we use are the size functions 
       
  1939   @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 
       
  1940   all well-founded. It is straightforward to establish that these measures decrease 
       
  1941   in every induction step.
       
  1942   
       
  1943   What is left to show is that we covered all cases. To do so, we use 
       
  1944   a cases lemma derived for each type, which for the terms in \eqref{letpat} 
       
  1945   is of the form
       
  1946   %
       
  1947   \begin{equation}\label{weakcases}
       
  1948   \infer{@{text "P\<^bsub>trm\<^esub>"}}
       
  1949   {\begin{array}{l@ {\hspace{9mm}}l}
       
  1950   @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
       
  1951   @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
       
  1952   \end{array}}
       
  1953   \end{equation}
       
  1954   %
       
  1955   These cases lemmas have a premise for auch term-constructor.
       
  1956   The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
       
  1957   provided we can show that this property holds if we substitute for @{text "t"} all 
       
  1958   possible term-constructors. 
       
  1959   
       
  1960   The only remaining difficulty is that in order to derive the stronger induction
       
  1961   principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
       
  1962   in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and 
       
  1963   \emph{all} @{text Let}-terms. 
       
  1964   What we need instead is a cases rule where we only have to consider terms that have 
       
  1965   binders being fresh w.r.t.~a context @{text "c"}, namely
       
  1966   %
       
  1967   \begin{center}
       
  1968   \begin{tabular}{l}
       
  1969   @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
       
  1970   @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}
       
  1971   \end{tabular}
       
  1972   \end{center}
       
  1973   %
       
  1974   However, this can be relatively easily be derived from the implications in \eqref{weakcases} 
       
  1975   by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
       
  1976   that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with 
       
  1977   a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and 
       
  1978   @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
       
  1979   By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
       
  1980   and we are done with this case.
       
  1981 
       
  1982   The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
       
  1983   The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
       
  1984   because @{text p} might contain names that are bound (by @{text bn}) and that are 
       
  1985   free. To solve this problem we have to introduce a permutation functions that only
       
  1986   permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
       
  1987   by lifting. Assuming a
       
  1988   clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define 
  1920   %
  1989   %
  1921   \begin{center}
  1990   \begin{center}
  1922   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
  1991   @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
  1923   \end{center}
  1992   \end{center}
  1924   
  1993   %
  1925   \noindent
  1994   \noindent
  1926   with @{text "y\<^isub>i"} determined as follows:
  1995   with @{text "y\<^isub>i"} determined as follows:
  1927   %
  1996   %
  1928   \begin{center}
  1997   \begin{center}
  1929   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
  1998   \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
  1930   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
  1999   $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
  1931   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
  2000   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
  1932   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
  2001   $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
  1933   \end{tabular}
  2002   \end{tabular}
  1934   \end{center}
  2003   \end{center}
       
  2004   %
       
  2005   Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
       
  2006   @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
       
  2007   is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
       
  2008   these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
       
  2009   completes the interesting cases in \eqref{letpat} for stregthening the induction
       
  2010   principles.
  1935   
  2011   
  1936   \noindent
  2012 
  1937   Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
  2013 
  1938   $\alpha$-equated terms. We can then prove the following two facts
  2014   %A natural question is
  1939 
  2015   %whether we can also strengthen the weak induction principles involving
  1940   \begin{lemma}\label{permutebn} 
  2016   %the general binders presented here. We will indeed be able to so, but for this we need an 
  1941   Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
  2017   %additional notion for permuting deep binders. 
  1942   {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
  2018 
  1943     @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
  2019   %Given a binding function @{text "bn"} we define an auxiliary permutation 
  1944   \end{lemma}
  2020   %operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
  1945 
  2021   %Assuming a clause of @{text bn} is given as 
  1946   \begin{proof} 
  2022   %
  1947   By induction on @{text x}. The equations follow by simple unfolding 
  2023   %\begin{center}
  1948   of the definitions. 
  2024   %@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, 
  1949   \end{proof}
  2025   %\end{center}
  1950 
  2026 
  1951   \noindent
  2027   %\noindent 
  1952   The first property states that a permutation applied to a binding function is
  2028   %then we define 
  1953   equivalent to first permuting the binders and then calculating the bound
  2029   %
  1954   atoms. The second amounts to the fact that permuting the binders has no 
  2030   %\begin{center}
  1955   effect on the free-atom function. The main point of this permutation
  2031   %@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} 
  1956   function, however, is that if we have a permutation that is fresh 
  2032   %\end{center}
  1957   for the support of an object @{text x}, then we can use this permutation 
  2033   
  1958   to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
  2034   %\noindent
  1959   @{text "Let"} term-constructor from the example shown 
  2035   %with @{text "y\<^isub>i"} determined as follows:
  1960   in \eqref{letpat} this means for a permutation @{text "r"}
  2036   %
  1961   %
  2037   %\begin{center}
  1962   \begin{equation}\label{renaming}
  2038   %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
  1963   \begin{array}{l}
  2039   %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
  1964   \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
  2040   %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
  1965   \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
  2041   %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
  1966   \end{array}
  2042   %\end{tabular}
  1967   \end{equation}
  2043   %\end{center}
  1968 
  2044   
  1969   \noindent
  2045   %\noindent
  1970   This fact will be crucial when establishing the strong induction principles below.
  2046   %Using again the quotient package  we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to 
       
  2047   %$\alpha$-equated terms. We can then prove the following two facts
       
  2048 
       
  2049   %\begin{lemma}\label{permutebn} 
       
  2050   %Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
       
  2051   %{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
       
  2052   %  @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
       
  2053   %\end{lemma}
       
  2054 
       
  2055   %\begin{proof} 
       
  2056   %By induction on @{text x}. The equations follow by simple unfolding 
       
  2057   %of the definitions. 
       
  2058   %\end{proof}
       
  2059 
       
  2060   %\noindent
       
  2061   %The first property states that a permutation applied to a binding function is
       
  2062   %equivalent to first permuting the binders and then calculating the bound
       
  2063   %atoms. The second amounts to the fact that permuting the binders has no 
       
  2064   %effect on the free-atom function. The main point of this permutation
       
  2065   %function, however, is that if we have a permutation that is fresh 
       
  2066   %for the support of an object @{text x}, then we can use this permutation 
       
  2067   %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the 
       
  2068   %@{text "Let"} term-constructor from the example shown 
       
  2069   %in \eqref{letpat} this means for a permutation @{text "r"}
       
  2070   %%
       
  2071   %\begin{equation}\label{renaming}
       
  2072   %\begin{array}{l}
       
  2073   %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2)  \<sharp>* r"}}\\ 
       
  2074   %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
       
  2075   %\end{array}
       
  2076   %\end{equation}
       
  2077 
       
  2078   %\noindent
       
  2079   %This fact will be crucial when establishing the strong induction principles below.
  1971 
  2080 
  1972  
  2081  
  1973   In our running example about @{text "Let"}, the strong induction
  2082   %In our running example about @{text "Let"}, the strong induction
  1974   principle means that instead 
  2083   %principle means that instead 
  1975   of establishing the implication 
  2084   %of establishing the implication 
  1976   %
  2085   %
  1977   \begin{center}
  2086   %\begin{center}
  1978   @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
  2087   %@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
  1979   \end{center}
  2088   %\end{center}
  1980 
  2089   %
  1981   \noindent
  2090   %\noindent
  1982   it is sufficient to establish the following implication
  2091   %it is sufficient to establish the following implication
  1983   %
  2092   %
  1984   \begin{equation}\label{strong}
  2093   %\begin{equation}\label{strong}
  1985   \mbox{\begin{tabular}{l}
  2094   %\mbox{\begin{tabular}{l}
  1986   @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
  2095   %@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
  1987   \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
  2096   %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
  1988   \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
  2097   %\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
  1989   \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
  2098   %\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
  1990   \end{tabular}}
  2099   %\end{tabular}}
  1991   \end{equation}
  2100   %\end{equation}
  1992 
  2101   %
  1993   \noindent 
  2102   %\noindent 
  1994   While this implication contains an additional argument, namely @{text c}, and 
  2103   %While this implication contains an additional argument, namely @{text c}, and 
  1995   also additional universal quantifications, it is usually easier to establish.
  2104   %also additional universal quantifications, it is usually easier to establish.
  1996   The reason is that we have the freshness 
  2105   %The reason is that we have the freshness 
  1997   assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
  2106   %assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily 
  1998   chosen by the user as long as it has finite support.
  2107   %chosen by the user as long as it has finite support.
  1999 
  2108   %
  2000   Let us now show how we derive the strong induction principles from the
  2109   %Let us now show how we derive the strong induction principles from the
  2001   weak ones. In case of the @{text "Let"}-example we derive by the weak 
  2110   %weak ones. In case of the @{text "Let"}-example we derive by the weak 
  2002   induction the following two properties
  2111   %induction the following two properties
  2003   %
  2112   %
  2004   \begin{equation}\label{hyps}
  2113   %\begin{equation}\label{hyps}
  2005   @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
  2114   %@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} 
  2006   @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
  2115   %@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
  2007   \end{equation} 
  2116   %\end{equation} 
  2008 
  2117   %
  2009   \noindent
  2118   %\noindent
  2010   For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
  2119   %For the @{text Let} term-constructor  we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} 
  2011   assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
  2120   %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). 
  2012   By Property~\ref{avoiding} we
  2121   %By Property~\ref{avoiding} we
  2013   obtain a permutation @{text "r"} such that 
  2122   %obtain a permutation @{text "r"} such that 
  2014   %
  2123   %
  2015   \begin{equation}\label{rprops}
  2124   %\begin{equation}\label{rprops}
  2016   @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
  2125   %@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
  2017   @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
  2126   %@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
  2018   \end{equation}
  2127   %\end{equation}
  2019 
  2128   %
  2020   \noindent
  2129   %\noindent
  2021   hold. The latter fact and \eqref{renaming} give us
  2130   %hold. The latter fact and \eqref{renaming} give us
  2022   %
  2131   %%
  2023   \begin{center}
  2132   %\begin{center}
  2024   \begin{tabular}{l}
  2133   %\begin{tabular}{l}
  2025   @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
  2134   %@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
  2026   \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
  2135   %\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
  2027   \end{tabular}
  2136   %\end{tabular}
  2028   \end{center}
  2137   %\end{center}
  2029 
  2138   %
  2030   \noindent
  2139   %\noindent
  2031   So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
  2140   %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
  2032   establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
  2141   %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
  2033   To do so, we will use the implication \eqref{strong} of the strong induction
  2142   %To do so, we will use the implication \eqref{strong} of the strong induction
  2034   principle, which requires us to discharge
  2143   %principle, which requires us to discharge
  2035   the following four proof obligations:
  2144   %the following four proof obligations:
  2036   %
  2145   %%
  2037   \begin{center}
  2146   %\begin{center}
  2038   \begin{tabular}{rl}
  2147   %\begin{tabular}{rl}
  2039   {\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
  2148   %{\it (i)} &   @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
  2040   {\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
  2149   %{\it (ii)} &  @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
  2041   {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
  2150   %{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
  2042   {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
  2151   %{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
  2043   \end{tabular}
  2152   %\end{tabular}
  2044   \end{center}
  2153   %\end{center}
  2045 
  2154   %
  2046   \noindent
  2155   %\noindent
  2047   The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
  2156   %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the 
  2048   others from the induction hypotheses in \eqref{hyps} (in the fourth case
  2157   %others from the induction hypotheses in \eqref{hyps} (in the fourth case
  2049   we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
  2158   %we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
  2050 
  2159   %
  2051   Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
  2160   %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
  2052   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
  2161   %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
  2053   This completes the proof showing that the weak induction principles imply 
  2162   %This completes the proof showing that the weak induction principles imply 
  2054   the strong induction principles. 
  2163   %the strong induction principles. 
  2055 *}
  2164 *}
  2056 
  2165 
  2057 
  2166 
  2058 section {* Related Work *}
  2167 section {* Related Work *}
  2059 
  2168 
  2071   representations of bindings comes for free in theorem provers like Isabelle/HOL or
  2180   representations of bindings comes for free in theorem provers like Isabelle/HOL or
  2072   Coq, since the corresponding term-calculi can be implemented as ``normal''
  2181   Coq, since the corresponding term-calculi can be implemented as ``normal''
  2073   datatypes.  However, in both approaches it seems difficult to achieve our
  2182   datatypes.  However, in both approaches it seems difficult to achieve our
  2074   fine-grained control over the ``semantics'' of bindings (i.e.~whether the
  2183   fine-grained control over the ``semantics'' of bindings (i.e.~whether the
  2075   order of binders should matter, or vacuous binders should be taken into
  2184   order of binders should matter, or vacuous binders should be taken into
  2076   account). To do so, one would require additional predicates that filter out
  2185   account). %To do so, one would require additional predicates that filter out
  2077   unwanted terms. Our guess is that such predicates result in rather
  2186   %unwanted terms. Our guess is that such predicates result in rather
  2078   intricate formal reasoning.
  2187   %intricate formal reasoning.
  2079 
  2188 
  2080   Another representation technique for binding is higher-order abstract syntax
  2189   Another representation technique for binding is higher-order abstract syntax
  2081   (HOAS), which for example is implemented in the Twelf system. This representation
  2190   (HOAS), which for example is implemented in the Twelf system. This representation
  2082   technique supports very elegantly many aspects of \emph{single} binding, and
  2191   technique supports very elegantly many aspects of \emph{single} binding, and
  2083   impressive work has been done that uses HOAS for mechanising the metatheory
  2192   impressive work has been done that uses HOAS for mechanising the metatheory
  2156   %
  2265   %
  2157   %\noindent
  2266   %\noindent
  2158   %and therefore need the extra generality to be able to distinguish between 
  2267   %and therefore need the extra generality to be able to distinguish between 
  2159   %both specifications.
  2268   %both specifications.
  2160   Because of how we set up our definitions, we also had to impose some restrictions
  2269   Because of how we set up our definitions, we also had to impose some restrictions
  2161   (like a single binding function for a deep binder) that are not present in Ott. Our
  2270   (like a single binding function for a deep binder) that are not present in Ott. 
  2162   expectation is that we can still cover many interesting term-calculi from
  2271   %Our
  2163   programming language research, for example Core-Haskell. 
  2272   %expectation is that we can still cover many interesting term-calculi from
       
  2273   %programming language research, for example Core-Haskell. 
  2164 
  2274 
  2165   Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
  2275   Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
  2166   representing terms with general binders inside OCaml. This language is
  2276   representing terms with general binders inside OCaml. This language is
  2167   implemented as a front-end that can be translated to OCaml with the help of
  2277   implemented as a front-end that can be translated to OCaml with the help of
  2168   a library. He presents a type-system in which the scope of general binders
  2278   a library. He presents a type-system in which the scope of general binders
  2173   However, we have not proved this. Pottier gives a definition for 
  2283   However, we have not proved this. Pottier gives a definition for 
  2174   $\alpha$-equivalence, which also uses a permutation operation (like ours).
  2284   $\alpha$-equivalence, which also uses a permutation operation (like ours).
  2175   Still, this definition is rather different from ours and he only proves that
  2285   Still, this definition is rather different from ours and he only proves that
  2176   it defines an equivalence relation. A complete
  2286   it defines an equivalence relation. A complete
  2177   reasoning infrastructure is well beyond the purposes of his language. 
  2287   reasoning infrastructure is well beyond the purposes of his language. 
       
  2288   Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.
  2178   
  2289   
  2179   In a slightly different domain (programming with dependent types), the 
  2290   In a slightly different domain (programming with dependent types), the 
  2180   paper \cite{Altenkirch10} presents a calculus with a notion of 
  2291   paper \cite{Altenkirch10} presents a calculus with a notion of 
  2181   $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
  2292   $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
  2182   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
  2293   The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it