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 relations |
1283 %%% TODO Fix 'Andrew Pitts' in bibliography |
1284 are equivalence relations. |
1284 |
|
1285 To define the quotient types we first need to show that the defined |
|
1286 relations are equivalence relations. |
1285 |
1287 |
1286 \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} |
1288 \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 and are equivariant. |
1289 defined as above are equivalence relations and are equivariant. |
1288 \end{lemma} |
1290 \end{lemma} |
1289 \begin{proof} Reflexivity by induction on the raw datatype. Symmetry, |
1291 \begin{proof} Reflexivity by induction on the raw datatype. Symmetry, |
1321 lift the theorems that talk about the raw constants to theorems on the quotient |
1323 lift the theorems that talk about the raw constants to theorems on the quotient |
1322 level. The following lifted properties are proved: |
1324 level. The following lifted properties are proved: |
1323 |
1325 |
1324 \begin{center} |
1326 \begin{center} |
1325 \begin{tabular}{cp{7cm}} |
1327 \begin{tabular}{cp{7cm}} |
|
1328 %skipped permute_zero and permute_add, since we do not have a permutation |
|
1329 %definition |
1326 $\bullet$ & permutation defining equations \\ |
1330 $\bullet$ & permutation defining equations \\ |
1327 $\bullet$ & @{term "bn"} defining equations \\ |
1331 $\bullet$ & @{term "bn"} defining equations \\ |
1328 $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\ |
1332 $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\ |
1329 $\bullet$ & induction (weak induction, just on the term structure) \\ |
1333 $\bullet$ & induction. The induction principle that we obtain by lifting |
1330 $\bullet$ & quasi-injectivity, the equations that specify when two |
1334 is the weak induction principle, just on the term structure \\ |
1331 constructors are equal\\ |
1335 $\bullet$ & quasi-injectivity. This means the equations that specify |
|
1336 when two constructors are equal and comes from lifting the alpha |
|
1337 equivalence defining relations\\ |
1332 $\bullet$ & distinctness\\ |
1338 $\bullet$ & distinctness\\ |
|
1339 %may be skipped |
1333 $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\ |
1340 $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\ |
1334 \end{tabular} |
1341 \end{tabular} |
1335 \end{center} |
1342 \end{center} |
|
1343 |
|
1344 Notice that until now we have not said anything about the support of the |
|
1345 defined type. This is because we could not use the general definition of |
|
1346 support in lifted theorems, since it does not preserve the relation. |
|
1347 Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"}, |
|
1348 since the @{term "x"} is bound. On the raw level, before the binding is |
|
1349 introduced the term has the support equal to @{text "{x}"}. |
|
1350 |
|
1351 We will now show that the quotient types have a finite support. |
|
1352 |
|
1353 |
|
1354 |
1336 |
1355 |
1337 *} |
1356 *} |
1338 |
1357 |
1339 text {* |
1358 text {* |
1340 Restrictions |
1359 Restrictions |