388 A respectfulness condition for a constant can be expressed in |
388 A respectfulness condition for a constant can be expressed in |
389 terms of an aggregate relation between the constant and itself, |
389 terms of an aggregate relation between the constant and itself, |
390 for example the respectfullness for @{term "append"} |
390 for example the respectfullness for @{term "append"} |
391 can be stated as: |
391 can be stated as: |
392 |
392 |
393 @{thm [display] append_rsp[no_vars]} |
393 @{thm [display, indent=10] append_rsp[no_vars]} |
394 |
394 |
395 \noindent |
395 \noindent |
396 Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to: |
396 Which after unfolding the definition of @{term "op ===>"} is equivalent to: |
397 |
397 |
398 @{thm [display] append_rsp_unfolded[no_vars]} |
398 @{thm [display, indent=10] append_rsp_unfolded[no_vars]} |
399 |
399 |
400 An aggregate relation is defined in terms of relation composition, |
400 \noindent An aggregate relation is defined in terms of relation |
401 so we define it first: |
401 composition, so we define it first: |
402 |
402 |
403 \begin{definition}[Composition of Relations] |
403 \begin{definition}[Composition of Relations] |
404 @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate |
404 @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate |
405 composition @{thm pred_compI[no_vars]} |
405 composition @{thm pred_compI[no_vars]} |
406 \end{definition} |
406 \end{definition} |
418 |
418 |
419 Again, the last case is novel, so lets look at the example of |
419 Again, the last case is novel, so lets look at the example of |
420 respectfullness for @{term concat}. The statement according to |
420 respectfullness for @{term concat}. The statement according to |
421 the definition above is: |
421 the definition above is: |
422 |
422 |
423 @{thm [display] concat_rsp[no_vars]} |
423 @{thm [display, indent=10] concat_rsp[no_vars]} |
424 |
424 |
425 \noindent |
425 \noindent |
426 By unfolding the definition of relation composition and relation map |
426 By unfolding the definition of relation composition and relation map |
427 we can see the equivalent statement just using the primitive list |
427 we can see the equivalent statement just using the primitive list |
428 equivalence relation: |
428 equivalence relation: |
429 |
429 |
430 @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} |
430 @{thm [display, indent=10] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} |
431 |
431 |
432 The statement reads that, for any lists of lists @{term a} and @{term b} |
432 The statement reads that, for any lists of lists @{term a} and @{term b} |
433 if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} |
433 if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} |
434 such that each element of @{term a} is in the relation with an appropriate |
434 such that each element of @{term a} is in the relation with an appropriate |
435 element of @{term a'}, @{term a'} is in relation with @{term b'} and each |
435 element of @{term a'}, @{term a'} is in relation with @{term b'} and each |
439 *} |
439 *} |
440 |
440 |
441 subsection {* Preservation *} |
441 subsection {* Preservation *} |
442 |
442 |
443 text {* |
443 text {* |
444 To be able to lift theorems that talk about constants that are not |
444 Sometimes a non-lifted polymorphic constant is instantiated to a |
445 lifted but whose type changes when lifting is performed additionally |
445 type being lifted. For example take the @{term "op #"} which inserts |
446 preservation theorems are needed. |
446 an element in a list of pairs of natural numbers. When the theorem |
|
447 is lifted, the pairs of natural numbers are to become integers, but |
|
448 the head constant is still supposed to be the head constant, just |
|
449 with a different type. To be able to lift such theorems |
|
450 automatically, additional theorems provided by the user are |
|
451 necessary, we call these \emph{preservation} theorems following |
|
452 Homeier's naming. |
447 |
453 |
448 To lift theorems that talk about insertion in lists of lifted types |
454 To lift theorems that talk about insertion in lists of lifted types |
449 we need to know that for any quotient type with the abstraction and |
455 we need to know that for any quotient type with the abstraction and |
450 representation functions @{text "Abs"} and @{text Rep} we have: |
456 representation functions @{text "Abs"} and @{text Rep} we have: |
451 |
457 |
452 @{thm [display] (concl) cons_prs[no_vars]} |
458 @{thm [display, indent=10] (concl) cons_prs[no_vars]} |
453 |
459 |
454 This is not enough to lift theorems that talk about quotient compositions. |
460 This is not enough to lift theorems that talk about quotient compositions. |
455 For some constants (for example empty list) it is possible to show a |
461 For some constants (for example empty list) it is possible to show a |
456 general compositional theorem, but for @{term "op #"} it is necessary |
462 general compositional theorem, but for @{term "op #"} it is necessary |
457 to show that it respects the particular quotient type: |
463 to show that it respects the particular quotient type: |
458 |
464 |
459 @{thm [display] insert_preserve2[no_vars]} |
465 @{thm [display, indent=10] insert_preserve2[no_vars]} |
460 *} |
466 *} |
461 |
467 |
462 subsection {* Composition of Quotient theorems *} |
468 subsection {* Composition of Quotient theorems *} |
463 |
469 |
464 text {* |
470 text {* |