674 when we compose the quotient with itself, as there is no simple |
674 when we compose the quotient with itself, as there is no simple |
675 intermediate step. |
675 intermediate step. |
676 |
676 |
677 Lets take again the example of @{term flat}. To be able to lift |
677 Lets take again the example of @{term flat}. To be able to lift |
678 theorems that talk about it we provide the composition quotient |
678 theorems that talk about it we provide the composition quotient |
679 theorems, which then lets us perform the lifting procedure in an |
679 theorem: |
680 unchanged way: |
680 |
681 |
681 @{thm [display, indent=10] quotient_compose_list[no_vars]} |
682 @{thm [display] quotient_compose_list[no_vars]} |
682 |
|
683 \noindent |
|
684 this theorem will then instantiate the quotients needed in the |
|
685 injection and cleaning proofs allowing the lifting procedure to |
|
686 proceed in an unchanged way. |
|
687 |
683 *} |
688 *} |
684 |
689 |
685 |
690 |
686 section {* Lifting of Theorems *} |
691 section {* Lifting of Theorems *} |
687 |
692 |
694 an automated statement translation mechanism which can optionally |
699 an automated statement translation mechanism which can optionally |
695 take a list of quotient types. It is possible that a user wants |
700 take a list of quotient types. It is possible that a user wants |
696 to lift only some occurrences of a quotiented type. In this case |
701 to lift only some occurrences of a quotiented type. In this case |
697 the user specifies the complete lifted goal instead of using the |
702 the user specifies the complete lifted goal instead of using the |
698 automated mechanism. |
703 automated mechanism. |
699 |
|
700 Lifting the theorems is performed in three steps. In the following |
704 Lifting the theorems is performed in three steps. In the following |
701 we call these steps \emph{regularization}, \emph{injection} and |
705 we call these steps \emph{regularization}, \emph{injection} and |
702 \emph{cleaning} following the names used in Homeier's HOL4 |
706 \emph{cleaning} following the names used in Homeier's HOL4 |
703 implementation. |
707 implementation. |
704 |
708 |
741 \end{center} |
745 \end{center} |
742 |
746 |
743 In the above definition we omitted the cases for existential quantifiers |
747 In the above definition we omitted the cases for existential quantifiers |
744 and unique existential quantifiers, as they are very similar to the cases |
748 and unique existential quantifiers, as they are very similar to the cases |
745 for the universal quantifier. |
749 for the universal quantifier. |
746 |
|
747 Next we define the function @{text INJ} which takes the statement of |
750 Next we define the function @{text INJ} which takes the statement of |
748 the regularized theorems and the statement of the lifted theorem both as |
751 the regularized theorems and the statement of the lifted theorem both as |
749 terms and returns the statement of the injected theorem: |
752 terms and returns the statement of the injected theorem: |
750 |
753 |
751 \begin{center} |
754 \begin{center} |
777 only for bound variables without types, while in the paper presentation |
780 only for bound variables without types, while in the paper presentation |
778 variables are typed *) |
781 variables are typed *) |
779 |
782 |
780 text {* |
783 text {* |
781 |
784 |
782 With the above definitions of @{text "REG"} and @{text "INJ"} we can show |
785 When lifting a theorem we first apply the following rule |
783 how the proof is performed. The first step is always the application of |
|
784 of the following lemma: |
|
785 |
786 |
786 @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"} |
787 @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"} |
787 |
788 |
788 With @{text A} instantiated to the original raw theorem, |
789 \noindent |
|
790 with @{text A} instantiated to the original raw theorem, |
789 @{text B} instantiated to @{text "REG(A)"}, |
791 @{text B} instantiated to @{text "REG(A)"}, |
790 @{text C} instantiated to @{text "INJ(REG(A))"}, |
792 @{text C} instantiated to @{text "INJ(REG(A))"}, |
791 and @{text D} instantiated to the statement of the lifted theorem. |
793 and @{text D} instantiated to the statement of the lifted theorem. |
792 The first assumption can be immediately discharged using the original |
794 The first assumption can be immediately discharged using the original |
793 theorem and the three left subgoals are exactly the subgoals of regularization, |
795 theorem and the three left subgoals are exactly the subgoals of regularization, |
1005 |
1007 |
1006 text {* |
1008 text {* |
1007 |
1009 |
1008 |
1010 |
1009 The code of the quotient package described here is already included in the |
1011 The code of the quotient package described here is already included in the |
1010 standard distribution of Isabelle.\footnote{Avaiable from |
1012 standard distribution of Isabelle.\footnote{Available from |
1011 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1013 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1012 heavily used in Nominal Isabelle, which provides a convenient reasoning |
1014 heavily used in Nominal Isabelle, which provides a convenient reasoning |
1013 infrastructure for programming language calculi involving binders. Earlier |
1015 infrastructure for programming language calculi involving binders. Earlier |
1014 versions of Nominal Isabelle have been used successfully in formalisations |
1016 versions of Nominal Isabelle have been used successfully in formalisations |
1015 of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, |
1017 of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, |