1489   definitions for the term-constructors @{text

  1489   definitions for the term-constructors @{text

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

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

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

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

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

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

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

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

  1495   creating new types in Isabelle/HOL (recall the picture shown in the 

  1495   creating new types in Isabelle/HOL (recall the picture shown in the 

  1496   Introduction).

  1496   Introduction).

  1497 

  1497 

  1498   The first useful property to the user is the fact that term-constructors are 

  1498   The first useful property to the user is the fact that term-constructors are 

  1499   distinct, that is

  1499   distinct, that is

  1560 

  1560 

  1561   \noindent

  1561   \noindent

  1562   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 

  1562   where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. 

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

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

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

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

  1566   lifting to go through, 

  1566   lifting to go through, 

  1567   we have to know that the permutation operations are respectful 

  1567   we have to know that the permutation operations are respectful 

  1568   w.r.t.~alpha-equivalence. This amounts to showing that the 

  1568   w.r.t.~alpha-equivalence. This amounts to showing that the 

  1569   alpha-equivalence relations are equivariant, which we already established 

  1569   alpha-equivalence relations are equivariant, which we already established 

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

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

  1574   \end{equation}

  1574   \end{equation}

  1575 

  1575 

  1576   \noindent

  1576   \noindent

  1577   for our infrastructure. In a similar fashion we can lift the equations

  1577   for our infrastructure. In a similar fashion we can lift the equations

  1578   characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 

  1578   characterising the free-variable functions @{text "fn_ty\<AL>\<^isub>j"} and @{text "fv_bn\<AL>\<^isub>k"}, and the 

  1580   lifting are the properties:

  1580   lifting are the properties:

  1581   %

  1581   %

  1582   \begin{equation}\label{fnresp}

  1582   \begin{equation}\label{fnresp}

  1583   \mbox{%

  1583   \mbox{%

  1584   \begin{tabular}{l}

  1584   \begin{tabular}{l}