279 To be able to lift theorems that talk about constants that are not |
279 To be able to lift theorems that talk about constants that are not |
280 lifted but whose type changes when lifting is performed additionally |
280 lifted but whose type changes when lifting is performed additionally |
281 preservation theorems are needed. |
281 preservation theorems are needed. |
282 *} |
282 *} |
283 |
283 |
284 section {* Lifting Theorems *} |
284 subsection {* Composition of Quotient theorems *} |
285 |
285 |
286 text{* |
286 text {* |
|
287 Given two quotients, one of which quotients a container, and the |
|
288 other quotients the type in the container, we can write the |
|
289 composition of those quotients. This becomes especially interesting |
|
290 when we compose the quotient with itself, as there is no simple |
|
291 intermediate step. |
|
292 |
|
293 Lets take again the example of @{term concat}. To |
|
294 |
287 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
295 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
288 present in composition quotients. An example composition quotient |
296 present in composition quotients. An example composition quotient |
289 theorem that needs to be proved is the one needed to lift theorems |
297 theorem that needs to be proved is the one needed to lift theorems |
290 about concat: |
298 about concat: |
291 |
299 |
292 @{thm [display] quotient_compose_list[no_vars]} |
300 @{thm [display] quotient_compose_list[no_vars]} |
293 *} |
301 |
|
302 section {* Lifting Theorems *} |
294 |
303 |
295 text {* TBD *} |
304 text {* TBD *} |
296 |
305 |
297 text {* Why providing a statement to prove is necessary is some cases *} |
306 text {* Why providing a statement to prove is necessary is some cases *} |
298 |
307 |