653 relation is the same as the one given by aggregate relations. |
653 relation is the same as the one given by aggregate relations. |
654 This becomes especially interesting |
654 This becomes especially interesting |
655 when we compose the quotient with itself, as there is no simple |
655 when we compose the quotient with itself, as there is no simple |
656 intermediate step. |
656 intermediate step. |
657 |
657 |
658 Lets take again the example of @{term concat}. To be able to lift |
658 Lets take again the example of @{term flat}. To be able to lift |
659 theorems that talk about it we provide the composition quotient |
659 theorems that talk about it we provide the composition quotient |
660 theorems, which then lets us perform the lifting procedure in an |
660 theorems, which then lets us perform the lifting procedure in an |
661 unchanged way: |
661 unchanged way: |
662 |
662 |
663 @{thm [display] quotient_compose_list[no_vars]} |
663 @{thm [display] quotient_compose_list[no_vars]} |
744 |
744 |
745 *} |
745 *} |
746 |
746 |
747 subsection {* Proof procedure *} |
747 subsection {* Proof procedure *} |
748 |
748 |
749 (* In the below the type-guiding 'QuotTrue' assumption is removed; since we |
749 (* In the below the type-guiding 'QuotTrue' assumption is removed. We need it |
750 present in a paper a version with typed-variables it is not necessary *) |
750 only for bound variables without types, while in the paper presentation |
|
751 variables are typed *) |
751 |
752 |
752 text {* |
753 text {* |
753 |
754 |
754 With the above definitions of @{text "REG"} and @{text "INJ"} we can show |
755 With the above definitions of @{text "REG"} and @{text "INJ"} we can show |
755 how the proof is performed. The first step is always the application of |
756 how the proof is performed. The first step is always the application of |
769 |
770 |
770 The injection and cleaning subgoals are always solved if the appropriate |
771 The injection and cleaning subgoals are always solved if the appropriate |
771 respectfulness and preservation theorems are given. It is not the case |
772 respectfulness and preservation theorems are given. It is not the case |
772 with regularization; sometimes a theorem given by the user does not |
773 with regularization; sometimes a theorem given by the user does not |
773 imply a regularized version and a stronger one needs to be proved. This |
774 imply a regularized version and a stronger one needs to be proved. This |
774 is outside of the scope of the quotient package, so the user is then left |
775 is outside of the scope of the quotient package, so such obligations are |
775 with such obligations. As an example lets see the simplest possible |
776 left to the user. Take a simple statement for integers @{term "0 \<noteq> 1"}. |
776 non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"} |
777 It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because |
777 on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It |
778 of regularization. The raw theorem only shows that particular items in the |
778 only shows that particular items in the equivalence classes are not equal, |
779 equivalence classes are not equal. A more general statement saying that |
779 a more general statement saying that the classes are not equal is necessary. |
780 the classes are not equal is necessary. |
780 *} |
781 *} |
781 |
782 |
782 subsection {* Proving Regularization *} |
783 subsection {* Proving Regularization *} |
783 |
784 |
784 text {* |
785 text {* |
785 |
786 |
786 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
787 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
787 of similar statements into simpler implication subgoals. These are enhanced |
788 of similar statements into simpler implication subgoals. These are enhanced |
788 with special quotient theorem in the regularization goal. Below we only show |
789 with special quotient theorem in the regularization goal. Below we only show |
789 the versions for the universal quantifier. For the existential quantifier |
790 the versions for the universal quantifier. For the existential quantifier |
790 and abstraction they are analogous with some symmetry. |
791 and abstraction they are analogous. |
791 |
792 |
792 First, bounded universal quantifiers can be removed on the right: |
793 First, bounded universal quantifiers can be removed on the right: |
793 |
794 |
794 @{thm [display, indent=10] ball_reg_right[no_vars]} |
795 @{thm [display, indent=10] ball_reg_right[no_vars]} |
795 |
796 |
799 |
800 |
800 And finally it can be removed anywhere if @{term R2} is an equivalence relation, then: |
801 And finally it can be removed anywhere if @{term R2} is an equivalence relation, then: |
801 |
802 |
802 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
803 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
803 |
804 |
804 The last theorem is new in comparison with Homeier's package, there the |
805 The last theorem is new in comparison with Homeier's package. There the |
805 injection procedure would be used to prove goals with such shape, and there |
806 injection procedure would be used to prove goals with such shape, and there |
806 the equivalence assumption would be useful. We use it directly also for |
807 the equivalence assumption would be used. We use the above theorem directly |
807 composed relations where the range type is a type for which we know an |
808 also for composed relations where the range type is a type for which we know an |
808 equivalence theorem. This allows separating regularization from injection. |
809 equivalence theorem. This allows separating regularization from injection. |
809 |
810 |
810 *} |
811 *} |
811 |
812 |
812 (* |
813 (* |
821 subsection {* Injection *} |
822 subsection {* Injection *} |
822 |
823 |
823 text {* |
824 text {* |
824 The injection proof starts with an equality between the regularized theorem |
825 The injection proof starts with an equality between the regularized theorem |
825 and the injected version. The proof again follows by the structure of the |
826 and the injected version. The proof again follows by the structure of the |
826 two term, and is defined for a goal being a relation between the two terms. |
827 two terms, and is defined for a goal being a relation between these two terms. |
827 |
828 |
828 \begin{itemize} |
829 \begin{itemize} |
829 \item For two constants, an appropriate constant respectfullness assumption is used. |
830 \item For two constants, an appropriate constant respectfullness assumption is used. |
830 \item For two variables, the regularization assumptions state that they are related. |
831 \item For two variables, we use the assumptions proved in regularization. |
831 \item For two abstractions, they are eta-expanded and beta-reduced. |
832 \item For two abstractions, they are eta-expanded and beta-reduced. |
832 \end{itemize} |
833 \end{itemize} |
833 |
834 |
834 Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
835 Otherwise the two terms are applications. There are two cases: If there is a REP/ABS |
835 in the injected theorem we can use the theorem: |
836 in the injected theorem we can use the theorem: |