284 subsection {* Composition of Quotient 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 |
287 Given two quotients, one of which quotients a container, and the |
288 other quotients the type in the container, we can write the |
288 other quotients the type in the container, we can write the |
289 composition of those quotients. This becomes especially interesting |
289 composition of those quotients. To compose two quotient theorems |
|
290 we compose the relations with relation composition |
|
291 and the abstraction and relation functions with function composition. |
|
292 The @{term "Rep"} and @{term "Abs"} functions that we obtain are |
|
293 the same as the ones created by in the aggregate functions and the |
|
294 relation is the same as the one given by aggregate relations. |
|
295 This becomes especially interesting |
290 when we compose the quotient with itself, as there is no simple |
296 when we compose the quotient with itself, as there is no simple |
291 intermediate step. |
297 intermediate step. |
292 |
298 |
293 Lets take again the example of @{term concat}. To |
299 Lets take again the example of @{term concat}. To be able to lift |
294 |
300 theorems that talk about it we will first prove the composition |
295 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
301 quotient theorems, which then lets us perform the lifting procedure |
296 present in composition quotients. An example composition quotient |
302 in an unchanged way: |
297 theorem that needs to be proved is the one needed to lift theorems |
|
298 about concat: |
|
299 |
303 |
300 @{thm [display] quotient_compose_list[no_vars]} |
304 @{thm [display] quotient_compose_list[no_vars]} |
301 *} |
305 *} |
302 |
306 |
303 |
307 |
304 section {* Lifting Theorems *} |
308 section {* Lifting Theorems *} |
|
309 |
|
310 |
305 |
311 |
306 text {* TBD *} |
312 text {* TBD *} |
307 |
313 |
308 text {* Why providing a statement to prove is necessary is some cases *} |
314 text {* Why providing a statement to prove is necessary is some cases *} |
309 |
315 |