499 *) |
499 *) |
500 |
500 |
501 subsection {* Injection *} |
501 subsection {* Injection *} |
502 |
502 |
503 text {* |
503 text {* |
504 |
504 The injection proof starts with an equality between the regularized theorem |
505 The 2 key lemmas are: |
505 and the injected version. The proof again follows by the structure of the |
|
506 two term, and is defined for a goal being a relation between the two terms. |
|
507 |
|
508 \begin{itemize} |
|
509 \item For two constants, an appropriate constant respectfullness assumption is used. |
|
510 \item For two variables, the regularization assumptions state that they are related. |
|
511 \item For two abstractions, they are eta-expanded and beta-reduced. |
|
512 \end{itemize} |
|
513 |
|
514 Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
|
515 in the injected theorem we can use the theorem: |
|
516 |
|
517 @{thm [display] rep_abs_rsp[no_vars]} |
|
518 |
|
519 and continue the proof. |
|
520 |
|
521 Otherwise we introduce an appropriate relation between the subterms and continue with |
|
522 two subgoals using the lemma: |
506 |
523 |
507 @{thm [display] apply_rsp[no_vars]} |
524 @{thm [display] apply_rsp[no_vars]} |
508 @{thm [display] rep_abs_rsp[no_vars]} |
525 |
509 |
526 *} |
510 |
|
511 |
|
512 *} |
|
513 |
|
514 |
|
515 |
|
516 |
527 |
517 subsection {* Cleaning *} |
528 subsection {* Cleaning *} |
518 |
529 |
519 text {* Preservation of quantifiers, abstractions, relations, quotient-constants |
530 text {* Preservation of quantifiers, abstractions, relations, quotient-constants |
520 (definitions) and user given constant preservation lemmas *} |
531 (definitions) and user given constant preservation lemmas *} |