1283   To define quotient types of the raw types we first show that the defined relation

  1283   To define quotient types of the raw types we first show that the defined relations

  1284   in an equivalence relation.

  1284   are equivalence relations.

  1285 

  1285 

  1286   \begin{lemma} The relations $\approx_1,\ldots,\approx_n,\approx_{bn1},\ldots,\approx_{bnm}$

  1286   \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}

  1287   defined as above are equivalence relations.

  1287   defined as above are equivalence relations and are equivariant.

  1289   \begin{proof}

  1289   \begin{proof} Reflexivity by induction on the raw datatype. Symmetry,

  1290   Reflexivity by induction on the raw datatype, symmetry and transitivity by

  1290   transitivity and equivariance by induction on the alpha equivalence

  1291   induction on the alpha equivalence relation. Using lemma \ref{alphaeq}, the

  1291   relation. Using lemma \ref{alphaeq}, the conditions follow by simple

  1292   conditions follow by simple calculations.

  1292   calculations.  \end{proof}

  1293   \end{proof}

  1293 

  1294 

  1294   \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift

  1295   \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift the raw

  1295   the raw definitions to the quotient type, we need to prove that they

  1296   definitions to the quotient type, we need to prove that they \emph{respect} the

  1296   \emph{respect} the relation. We follow the definition of respectfullness given

  1297   relation. We follow the definition of respectfullness given by

  1297   by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition

  1298   Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition is that

  1298   is that when a function (or constructor) is given arguments that are

  1299   when a function (or constructor) is given arguments that are alpha-equivalent the

  1299   alpha-equivalent the results are also alpha equivalent. For arguments that are

  1300   results are also alpha equivalent. For arguments that are not of any of the relations

  1300   not of any of the relations taken into account, equivalence is replaced by

  1301   taken into account, equvalence is replaced by equality.

  1301   equality. In particular the respectfullness condition for a @{text "bn"}

  1302 

  1302   function means that for alpha equivalent raw terms it returns the same bound

  1303 % Could be written as a \{lemma}

  1303   names. Thanks to the restrictions on the binding functions introduced in

  1304   In particular the respectfullness condition for a @{text "bn"} function means that for

  1304   Section~\ref{sec:alpha} we can show that are respectful.

  1305   alpha equivalent raw terms it returns the same bound names. Thanks to the

  1305 

  1306   restrictions on the binding functions introduced in Section~\ref{sec:alpha}, we can

  1306   \begin{lemma} The functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \<dots> fv_ty\<^isub>n"},

  1307   show that are respectful. With this we can show the respectfullness of @{text "fv_ty"}

  1307   the raw constructors, the raw permutations and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are

  1308   functions by induction. Respectfullness of permutations is a direct consequence

  1308   respectful w.r.t. the relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>n"}.

  1309   of equivariance. Respectfullness of type constructors and of @{text "alpha_bn"} follows

  1309   \end{lemma}

  1310   by induction from type definitions.

  1310   \begin{proof} Respectfullness of permutations is a direct consequence of

  1311 

  1311   equivariance.  All other properties by induction on the alpha-equivalence

  1312   relation.  For @{text "bn"} the thesis follows by simple calculations thanks

  1313   to the restrictions on the binding functions. For @{text "fv"} functions it

  1314   follows using respectfullness of @{text "bn"}. For type constructors it is a

  1315   simple calculation thanks to the way alpha-equivalence was defined. For @{text

  1316   "alpha_bn"} after a second induction on the second relation by simple

  1317   calculations.  \end{proof}

  1318 

  1319   With these respectfullness properties we can use the quotient package

  1320   to define the above constants on the quotient level. We can then automatically

  1321   lift the theorems that talk about the raw constants to theorems on the quotient

  1322   level. The following lifted properties are proved:

  1323 

  1324   \begin{center}

  1325   \begin{tabular}{cp{7cm}}

  1326   $\bullet$ & permutation defining equations \\

  1327   $\bullet$ & @{term "bn"} defining equations \\

  1328   $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\

  1329   $\bullet$ & induction (weak induction, just on the term structure) \\

  1330   $\bullet$ & quasi-injectivity, the equations that specify when two

  1331      constructors are equal\\

  1332   $\bullet$ & distinctness\\

  1333   $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\

  1334   \end{tabular}

  1335   \end{center}