1278 *} |
1278 *} |
1279 |
1279 |
1280 section {* The Lifting of Definitions and Properties *} |
1280 section {* The Lifting of Definitions and Properties *} |
1281 |
1281 |
1282 text {* |
1282 text {* |
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. |
1288 \end{lemma} |
1288 \end{lemma} |
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} |
1312 |
1336 |
1313 *} |
1337 *} |
1314 |
1338 |
1315 text {* |
1339 text {* |
1316 Restrictions |
1340 Restrictions |