684 |
684 |
685 |
685 |
686 section {* Lifting of Theorems *} |
686 section {* Lifting of Theorems *} |
687 |
687 |
688 text {* |
688 text {* |
689 The core of the quotient package takes an original theorem that |
689 The core of our quotient package takes an original theorem that |
690 talks about the raw types, and the statement of the theorem that |
690 talks about the raw types and the statement of the theorem that |
691 it is supposed to produce. This is different from other existing |
691 it is supposed to produce. This is different from existing |
692 quotient packages, where only the raw theorems were necessary. |
692 quotient packages, where only the raw theorems are necessary. |
693 We notice that in some cases only some occurrences of the raw |
693 To simplify the use of the quotient package we additionally provide |
694 types need to be lifted. This is for example the case in the |
694 an automated statement translation mechanism which can optionally |
695 new Nominal package, where a raw datatype that talks about |
695 take a list of quotient types. It is possible that a user wants |
696 pairs of natural numbers or strings (being lists of characters) |
696 to lift only some occurrences of a quotiented type. In this case |
697 should not be changed to a quotient datatype with constructors |
697 the user specifies the complete lifted goal instead of using the |
698 taking integers or finite sets of characters. To simplify the |
698 automated mechanism. |
699 use of the quotient package we additionally provide an automated |
|
700 statement translation mechanism that replaces occurrences of |
|
701 types that match given quotients by appropriate lifted types. |
|
702 |
699 |
703 Lifting the theorems is performed in three steps. In the following |
700 Lifting the theorems is performed in three steps. In the following |
704 we call these steps \emph{regularization}, \emph{injection} and |
701 we call these steps \emph{regularization}, \emph{injection} and |
705 \emph{cleaning} following the names used in Homeier's HOL |
702 \emph{cleaning} following the names used in Homeier's HOL4 |
706 implementation. |
703 implementation. |
707 |
704 |
708 We first define the statement of the regularized theorem based |
705 We first define the statement of the regularized theorem based |
709 on the original theorem and the goal theorem. Then we define |
706 on the original theorem and the goal theorem. Then we define |
710 the statement of the injected theorem, based on the regularized |
707 the statement of the injected theorem, based on the regularized |
715 |
712 |
716 subsection {* Regularization and Injection statements *} |
713 subsection {* Regularization and Injection statements *} |
717 |
714 |
718 text {* |
715 text {* |
719 |
716 |
720 We first define the function @{text REG}, which takes the statements |
717 We define the function @{text REG}, which takes the statements |
721 of the raw theorem and the lifted theorem (both as terms) and |
718 of the raw theorem and the lifted theorem (both as terms) and |
722 returns the statement of the regularized version. The intuition |
719 returns the statement of the regularized version. The intuition |
723 behind this function is that it replaces quantifiers and |
720 behind this function is that it replaces quantifiers and |
724 abstractions involving raw types by bounded ones, and equalities |
721 abstractions involving raw types by bounded ones, and equalities |
725 involving raw types are replaced by appropriate aggregate |
722 involving raw types are replaced by appropriate aggregate |
726 relations. It is defined as follows: |
723 equivalence relations. It is defined as follows: |
727 |
724 |
728 \begin{center} |
725 \begin{center} |
729 \begin{tabular}{rcl} |
726 \begin{tabular}{rcl} |
730 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
727 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
731 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
728 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |