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

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

  1276   in an equivalence relation.

  1276   are equivalence relations.

  1277 

  1277 

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

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

  1279   defined as above are equivalence relations.

  1279   defined as above are equivalence relations and are equivariant.

  1281   \begin{proof}

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

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

  1282   transitivity and equivariance by induction on the alpha equivalence

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

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

  1284   conditions follow by simple calculations.

  1284   calculations.  \end{proof}

  1285   \end{proof}

  1285 

  1286 

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

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

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

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

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

  1289   relation. We follow the definition of respectfullness given by

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

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

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

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

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

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

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

  1293   taken into account, equvalence is replaced by equality.

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

  1294 

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

  1295 % Could be written as a \{lemma}

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

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

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

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

  1297 

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

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

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

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

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

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

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

  1301   \end{lemma}

  1302   by induction from type definitions.

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

  1303 

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

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

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

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

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

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

  1309   calculations.  \end{proof}

  1310 

  1311   With these respectfullness properties we can use the quotient package

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

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

  1314   level. The following lifted properties are proved:

  1315 

  1316   \begin{center}

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

  1318   $\bullet$ & permutation defining equations \\

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

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

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

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

  1323      constructors are equal\\

  1324   $\bullet$ & distinctness\\

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

  1326   \end{tabular}

  1327   \end{center}