1283   raw datatype. We also define permutation operations by 

  1283   ``raw'' datatype. We also define permutation operations by 

  1720   corresponding binding cluase specifies a binder with two bodies.

  1720   corresponding binding clause specifies a binder with two bodies.

  1744   The function package of Isabelle/HOL \cite{Krauss09} allows us to prove the

  1744   The function package of Isabelle/HOL allows us to prove the first part by

  1745   first part is by mutual induction over the definitions of the functions.\footnote{We

  1745   mutual induction over the definitions of the functions.\footnote{We have

  1746   know that they are terminating functions. From this an induction principle

  1746   that they are terminating functions. From this an induction principle is

  1747   is derived by the function package.} The second is by a straightforward 

  1747   derived by the function package \cite{Krauss09}.} The second is by a

  1748   induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using 

  1748   straightforward induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and

  1749   the first part.

  1749   @{text "\<approx>bn"}$_{1..m}$ using the first part.

  1859   are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$.

  1859   are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$ (similarly for the

  1860   other binding modes).

  1876   "bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.

  1877   "bn\<AL>"}$_{1..m}$ and size functions @{text "size_ty\<AL>"}$_{1..n}$.

  1877   The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$

  1878   The latter are defined automatically for the ``raw'' types @{text "ty"}$_{1..n}$

  1882   lemmas allow the user to deduce a property @{text "P"} by exhaustively 

  1883   lemmas allow the user to deduce a property @{text "P"} by exhaustively

  1883   analysing all cases how an element in a type @{text "ty\<AL>"}$_i$ can

  1884   analysing how an element in a type, say @{text "ty\<AL>"}$_i$, can be

  1884   be constructed (that means one case for each of term-constructors

  1885   constructed (that means one case for each of the term-constructors in @{text

  1885   of type @{text "ty\<AL>"}$_i\,$). The lifted cases

  1886   "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text

  1886   lemma for the type @{text "ty\<AL>"}$_i\,$ looks as

  1887   "ty\<AL>"}$_i\,$ looks as follows

  1887   follows

  1888 

  1888 

  1889   \begin{equation}\label{cases}

  1889   \[

  1896   \]\smallskip

  1896   \end{equation}\smallskip

  1904    \[

  1904    \begin{equation}\label{induct}

  1911   \]\smallskip

  1911   \end{equation}\smallskip

  1912 

  1912 

  1913   \noindent

  1913   \noindent

  1914   whereby the @{text P}$_{1..n}$ are the properties established by induction 

  1914   whereby the @{text P}$_{1..n}$ are the properties established by the induction

  1915   and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. 

  1915   and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$. Note that 

  1916   This induction principle has for the term constructors @{text "C"}$^\alpha_1$ 

  1916   the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a

  1917   a premise of the form

  1917   premise of the form

  1918   

  1918 

  1919   \begin{equation}\label{weakprem}

  1919   \[

  1921   \end{equation}\smallskip

  1921   \]\smallskip

  1924   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are 

  1924   in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are the

  1925   the recursive arguments of this term constructor (similarly for the other

  1925   recursive arguments of this term constructor (similarly for the other

  1926   term-constructors). In case of the lambda-calculus (with constructors

  1926   term-constructors). 

  1927    @{text "Var\<^sup>\<alpha>"},  @{text "App\<^sup>\<alpha>"} and  @{text "Lam\<^sup>\<alpha>"}),

  1927 

  1928   the cases lemmas and the induction principle boil down to the following

  1928   Recall the lambda-calculus with @{text "Let"}-patterns shown in

  1929   two inference rules:

  1929   \eqref{letpat}. The cases lemmas and the induction principle shown in

  1930 

  1930   \eqref{cases} and \eqref{induct} boil down to the following three inference

  1931   \[\mbox{

  1931   rules (the cases lemmas are on the left-hand side; the induction principle

  1932   on the right):

  1933 

  1934   \begin{equation}\label{inductex}\mbox{

  1933   \infer{@{text "P"}}

  1936   \begin{tabular}{@ {}c@ {}}

  1937   \infer{@{text "P\<^bsub>trm\<^esub>"}}

  1935    @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P"}\\

  1939    @{text "\<forall>x. y = Var\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>trm\<^esub>"}\\

  1936    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}\\

  1940    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\

  1937    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P"}

  1941    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}\\

  1938    \end{array}} &

  1942    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"}

  1939 

  1943    \end{array}}\medskip\\

  1940   \infer{@{text "P y"}}

  1944 

  1945   \infer{@{text "P\<^bsub>pat\<^esub>"}}

  1942    @{text "\<forall>x. P (Var\<^sup>\<alpha> x)"}\\

  1947    @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\

  1943    @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>1 \<and> P x\<^isub>2 \<Rightarrow> P (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  1948    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\

  1944    @{text "\<forall>x\<^isub>1 x\<^isub>2. P x\<^isub>2 \<Rightarrow> P (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}

  1949    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}

  1945    \end{array}}

  1950   \end{array}}

  1946   \end{tabular}}

  1951   \end{tabular} 

  1947   \]\smallskip

  1952   &

  1948 

  1953   

  1949   \noindent

  1954   \begin{tabular}{@ {}c@ {}}

  1950   We will show in the next section that these inference rules are not very 

  1955   \infer{@{text "P\<^bsub>trm\<^esub> y\<^isub>1 \<and> P\<^bsub>pat\<^esub> y\<^isub>2"}}

  1951   convenient for the user to establish properties about lambda-terms, but

  1956   {\begin{array}{l}

  1952   they are crucial for completing our reasoning infrastructure for the 

  1957    @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\

  1953   types @{text "ty\<AL>"}$_{1..n}$.

  1958    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  1959    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  1960    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  1961    @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\

  1962    @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\

  1963    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}

  1964   \end{array}}

  1965   \end{tabular}

  1966   \end{tabular}}

  1967   \end{equation}\smallskip

  1956   can first show that the free-atom functions and binding functions are

  1970   can first show using \eqref{calphaeqvt} that the support of each term

  1957   equivariant, namely

  1971   constructor is included in the support of its arguments, 

  1972   namely

  1973 

  1974   \[

  1975   @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}

  1976   \]\smallskip

  1977 

  1978   \noindent

  1979   This allows us to prove using the induction principle for  @{text "ty\<AL>"}$_{1..n}$ 

  1980   that every element of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported 

  1981   (using Prop.~\ref{supportsprop}{\it (i)}). 

  1982   Similarly, we can establish by induction that the free-atom functions and binding 

  1983   functions are equivariant, namely

  1969   These properties can be established using the induction principle for the

  1995   Lastly, we can show that the support of elements in @{text

  1970   types @{text "ty\<AL>"}$_{1..n}$.  Having these

  1996   "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.  This fact

  1971   equivariant properties at our disposal, we can show that the support of

  1997   is important in the nominal setting where the general theory is formulated

  1972   term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its

  1998   in terms of support and freshness, but also provides evidence that our

  1973   arguments, that means

  1999   notions of free-atoms and alpha-equivalence ``match up''.

  1974 

  1975   \[

  1976   @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}

  1977   \]\smallskip

  1978  

  1979   \noindent

  1980   holds. This allows us to prove by induction that every @{text x} of type

  1981   @{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by

  1982   the induction principle for  @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the

  1983   support of elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text

  1984   "fa_ty\<AL>"}$_{1..n}$.  This fact is important in the nominal setting

  1985   where the general theory is formulated in terms of @{text "supp"} and @{text "#"}, but

  1986   also provides evidence that our notions of free-atoms and alpha-equivalence

  1987   are sensible.

  1998   proof. For the abstraction cases we use the facts derived in Theorem~\ref{suppabs}.

  2010   proof. For the abstraction cases we use then the facts derived in Theorem~\ref{suppabs},

  2011   for which we have to know that every body of an abstraction is finitely supported.

  2012   This we have proved earlier.

  2002   To sum up this section, we can establish automatically a reasoning infrastructure

  2016   To sum up this section, we can establish a reasoning infrastructure for the

  2003   for the types @{text "ty\<AL>"}$_{1..n}$ 

  2017   types @{text "ty\<AL>"}$_{1..n}$ by first lifting definitions from the

  2004   by first lifting definitions from the ``raw'' level to the quotient level and

  2018   ``raw'' level to the quotient level and then by proving facts about

  2005   then by establishing facts about these lifted definitions. All necessary proofs

  2019   these lifted definitions. All necessary proofs are generated automatically

  2006   are generated automatically by custom ML-code. 

  2020   by custom ML-code.

  2007 

  2014   In the previous section we derived induction principles for alpha-equated terms. 

  2027   In the previous section we derived induction principles for alpha-equated

  2015   We call such induction principles \emph{weak}, because for a 

  2028   terms (see \eqref{induct} and \eqref{inductex}). This was done by lifting

  2016   term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}

  2029   the corresponding inductions principles for ``raw'' terms.  We already

  2017   the induction hypothesis requires us to establish the implications \eqref{weakprem}.

  2030   employed these induction principles in order to derive several facts for

  2018   The problem with these implications is that in general they are difficult to establish.

  2031   alpha-equated terms, including the property that the free-variable functions

  2019   The reason is that we cannot make any assumption about the bound atoms that might be in @{text "C\<^sup>\<alpha>"}. 

  2032   and the notion of support coincide. Still, we call these induction

  2020   (for example we cannot assume the variable convention for them).

  2033   principles \emph{weak}, because for a term-constructor, say \mbox{@{text

  2021 

  2034   "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}, the induction hypothesis requires us to

  2022   In \cite{UrbanTasson05} we introduced a method for automatically

  2035   establish (under some assumptions) a property @{text "P (C\<^sup>\<alpha>

  2023   strengthening weak induction principles for terms containing single

  2036   x\<^isub>1\<dots>x\<^isub>r)"} for \emph{all} @{text "x"}$_{1..r}$. The problem is that in the

  2024   binders. These stronger induction principles allow the user to make additional

  2037   presence of binders we cannot make any assumptions about the atoms that are

  2025   assumptions about bound atoms. 

  2038   bound, and we have to potentially rename them. This renaming has to be

  2026   These additional assumptions amount to a formal

  2039   done manually and is often very cumbersome (especially in the case for 

  2027   version of the informal variable convention for binders. 

  2040   multiple bound atoms).

  2028   To sketch how this strengthening extends to the case of multiple binders, we use as

  2041 

  2029   running example the term-constructors @{text "Lam"} and @{text "Let"}

  2042   For the older versions of Nominal Isabelle we introduced in

  2030   from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},

  2043   \cite{UrbanTasson05} a method for automatically strengthening weak induction

  2031   the stronger induction principle for \eqref{letpat} establishes properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}

  2044   principles in case of single binders. These stronger induction principles

  2032   where the additional parameter @{text c} controls

  2045   allow the user to make additional assumptions about bound atoms. The main

  2033   which freshness assumptions the binders should satisfy. For the two term constructors 

  2046   point is that these additional assumptions amount to a formal version of the

  2034   this means that the user has to establish in inductions the implications

  2047   informal variable convention for binders and nearly always make manual

  2035   

  2048   renaming of binders unnecessary.

  2036   \begin{center}

  2049 

  2037   \begin{tabular}{l}

  2050   To explain how the strengthening works in the presence of multiple binders,

  2038   @{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)"}\\

  2051   we use as running example the lambda-calculus with @{text "Let"}-patterns

  2039   @{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)"}\\%[-0mm]

  2052   shown in \eqref{letpat}. Its weak induction principle is given in \eqref{inductex}.

  2040   \end{tabular}

  2053   The stronger induction principle is as follows

  2041   \end{center}

  2054 

  2042 

  2055   \begin{equation}\label{stronginduct}

  2043   In \cite{UrbanTasson05} we showed how the weaker induction principles imply

  2056   \mbox{

  2044   the stronger ones. This was done by some quite complicated, nevertheless automated,

  2057   \begin{tabular}{@ {}c@ {}}

  2045   induction proof. In this paper we simplify this work by leveraging the automated proof

  2058   \infer{@{text "P\<^bsub>trm\<^esub> c y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"}}

  2046   methods from the function package of Isabelle/HOL. 

  2059   {\begin{array}{l}

  2047   The reasoning principle these methods employ is well-founded induction. 

  2060    @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\

  2048   To use them in our setting, we have to discharge

  2061    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  2049   two proof obligations: one is that we have

  2062    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. {atom x\<^isub>1} #\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  2050   well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in 

  2063    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (set (bn x\<^isub>1)) #\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\

  2051   every induction step and the other is that we have covered all cases. 

  2064    @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\

  2052   As measures we use the size functions 

  2065    @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\

  2053   @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are 

  2066    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}

  2054   all well-founded. It is straightforward to establish that these measures decrease 

  2067   \end{array}}

  2055   in every induction step.

  2068   \end{tabular}}

  2056   

  2069   \end{equation}\smallskip

  2057   What is left to show is that we covered all cases. To do so, we use 

  2070 

  2058   a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} 

  2071 

  2072   \noindent

  2073   Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub> y\<^isub>1 \<and>

  2074   P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the stronger

  2075   induction principle establishes the properties @{text " P\<^bsub>trm\<^esub> c

  2076   y\<^isub>1 \<and> P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional

  2077   parameter @{text c} is assumed to be of finite support. The purpose of

  2078   @{text "c"} is to ``control'' which freshness assumptions the binders should

  2079   satisfy in the @{text "Lam\<^sup>\<alpha>"} and @{text "Let\<^sup>\<alpha>"} cases (these are the cases 

  2080   where the user specified some binding clauses).

  2081 

  2082   In what follows we will show that the induction principle in

  2083   \eqref{inductex} implies \eqref{stronginduct}. This fact was established in

  2084   \cite{UrbanTasson05} by some quite involved, nevertheless automated,

  2085   induction proof. In this paper we simplify the proof by leveraging the

  2086   automated proof methods from the function package of Isabelle/HOL

  2087   \cite{Krauss09}. The reasoning principle behind these methods is

  2088   well-founded induction. To use them in our setting, we have to discharge two

  2089   proof obligations: one is that we have well-founded measures (one for each type

  2090   @{text "ty"}$^\alpha_{1..n}$) that decrease in every induction step and the

  2091   other is that we have covered all cases. 

  2092 

  2093   As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$,

  2094   which we lifted in the previous section and which are all well-founded. It

  2095   is straightforward to establish that these measures decrease in every

  2096   induction step. What is left to show is that we covered all cases. 

  2097   To do so, we use a \emph{cases lemma} derived for each type. For the terms in \eqref{letpat} 

  2355   term-constructor and function is repectful w.r.t.~alpha-equivalence.

  2394   term-constructor and function is respectful w.r.t.~alpha-equivalence.