685 |
685 |
686 |
686 |
687 section {* Lifting of Theorems *} |
687 section {* Lifting of Theorems *} |
688 |
688 |
689 text {* |
689 text {* |
690 The core of the quotient package takes an original theorem that |
690 The core of our quotient package takes an original theorem that |
691 talks about the raw types, and the statement of the theorem that |
691 talks about the raw types and the statement of the theorem that |
692 it is supposed to produce. This is different from other existing |
692 it is supposed to produce. This is different from existing |
693 quotient packages, where only the raw theorems were necessary. |
693 quotient packages, where only the raw theorems are necessary. |
694 We notice that in some cases only some occurrences of the raw |
694 To simplify the use of the quotient package we additionally provide |
695 types need to be lifted. This is for example the case in the |
695 an automated statement translation mechanism which can optionally |
696 new Nominal package, where a raw datatype that talks about |
696 take a list of quotient types. It is possible that a user wants |
697 pairs of natural numbers or strings (being lists of characters) |
697 to lift only some occurrences of a quotiented type. In this case |
698 should not be changed to a quotient datatype with constructors |
698 the user specifies the complete lifted goal instead of using the |
699 taking integers or finite sets of characters. To simplify the |
699 automated mechanism. |
700 use of the quotient package we additionally provide an automated |
|
701 statement translation mechanism that replaces occurrences of |
|
702 types that match given quotients by appropriate lifted types. |
|
703 |
700 |
704 Lifting the theorems is performed in three steps. In the following |
701 Lifting the theorems is performed in three steps. In the following |
705 we call these steps \emph{regularization}, \emph{injection} and |
702 we call these steps \emph{regularization}, \emph{injection} and |
706 \emph{cleaning} following the names used in Homeier's HOL |
703 \emph{cleaning} following the names used in Homeier's HOL4 |
707 implementation. |
704 implementation. |
708 |
705 |
709 We first define the statement of the regularized theorem based |
706 We first define the statement of the regularized theorem based |
710 on the original theorem and the goal theorem. Then we define |
707 on the original theorem and the goal theorem. Then we define |
711 the statement of the injected theorem, based on the regularized |
708 the statement of the injected theorem, based on the regularized |
716 |
713 |
717 subsection {* Regularization and Injection statements *} |
714 subsection {* Regularization and Injection statements *} |
718 |
715 |
719 text {* |
716 text {* |
720 |
717 |
721 We first define the function @{text REG}, which takes the statements |
718 We define the function @{text REG}, which takes the statements |
722 of the raw theorem and the lifted theorem (both as terms) and |
719 of the raw theorem and the lifted theorem (both as terms) and |
723 returns the statement of the regularized version. The intuition |
720 returns the statement of the regularized version. The intuition |
724 behind this function is that it replaces quantifiers and |
721 behind this function is that it replaces quantifiers and |
725 abstractions involving raw types by bounded ones, and equalities |
722 abstractions involving raw types by bounded ones, and equalities |
726 involving raw types are replaced by appropriate aggregate |
723 involving raw types are replaced by appropriate aggregate |
727 relations. It is defined as follows: |
724 equivalence relations. It is defined as follows: |
728 |
725 |
729 \begin{center} |
726 \begin{center} |
730 \begin{tabular}{rcl} |
727 \begin{tabular}{rcl} |
731 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
728 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
732 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
729 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
815 |
812 |
816 text {* |
813 text {* |
817 |
814 |
818 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
815 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
819 of similar statements into simpler implication subgoals. These are enhanced |
816 of similar statements into simpler implication subgoals. These are enhanced |
820 with special quotient theorem in the regularization goal. Below we only show |
817 with special quotient theorem in the regularization proof. Below we only show |
821 the versions for the universal quantifier. For the existential quantifier |
818 the versions for the universal quantifier. For the existential quantifier |
822 and abstraction they are analogous. |
819 and abstraction they are analogous. |
823 |
820 |
824 First, bounded universal quantifiers can be removed on the right: |
821 First, bounded universal quantifiers can be removed on the right: |
825 |
822 |
826 @{thm [display, indent=10] ball_reg_right[no_vars]} |
823 @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]} |
827 |
824 |
828 They can be removed anywhere if the relation is an equivalence relation: |
825 They can be removed anywhere if the relation is an equivalence relation: |
829 |
826 |
830 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
827 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
831 |
828 |