857 section {* Alpha-Equivalence and Free Variables *}

   857 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}

  1272 section {* The Lifting of Definitions and Properties *} 

  1272 section {* The Lifting of Definitions and Properties *}

  1273 

  1274 text {*

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

  1276   in an equivalence relation.

  1277 

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

  1279   defined as above are equivalence relations.

  1280   \end{lemma}

  1281   \begin{proof}

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

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

  1284   conditions follow by simple calculations.

  1285   \end{proof}

  1286 

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

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

  1289   relation. We follow the definition of respectfullness given by

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

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

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

  1293   taken into account, equvalence is replaced by equality.

  1294 

  1295 % Could be written as a \{lemma}

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

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

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

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

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

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

  1302   by induction from type definitions.

  1303 

  1304 

  1305 *}