820 first two phases into the form the user has specified. Abstractly, our |
820 first two phases into the form the user has specified. Abstractly, our |
821 package establishes the following three proof steps: |
821 package establishes the following three proof steps: |
822 |
822 |
823 \begin{center} |
823 \begin{center} |
824 \begin{tabular}{l@ {\hspace{4mm}}l} |
824 \begin{tabular}{l@ {\hspace{4mm}}l} |
825 1.) Regularisation & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
825 1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\ |
826 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
826 2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\ |
827 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
827 3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\ |
828 \end{tabular} |
828 \end{tabular} |
829 \end{center} |
829 \end{center} |
830 |
830 |
831 \noindent |
831 \noindent |
832 which means the raw theorem implies the quotient theorem. |
832 which means, stringed together, the raw theorem implies the quotient theorem. |
833 In contrast to other quotient packages, our package requires |
833 In contrast to other quotient packages, our package requires that the user specifies |
834 the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we |
834 both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we |
835 also provide a fully automated mode, where the @{text "quot_thm"} is guessed |
835 also provide a fully automated mode, where the @{text "quot_thm"} is guessed |
836 from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some |
836 from the form of @{text "raw_thm"}.} As a result, the user has fine control |
837 occurrences of a raw type, but not others. |
837 over which parts of a raw theorem should be lifted. |
838 |
838 |
839 The second and third proof step will always succeed if the appropriate |
839 The second and third proof step performed in package will always succeed if the appropriate |
840 respectfulness and preservation theorems are given. In contrast, the first |
840 respectfulness and preservation theorems are given. In contrast, the first |
841 proof step can fail: a theorem given by the user does not always |
841 proof step can fail: a theorem given by the user does not always |
842 imply a regularized version and a stronger one needs to be proved. An example |
842 imply a regularized version and a stronger one needs to be proved. An example |
843 for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}. |
843 for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}. |
844 One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"}, |
844 One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"}, |
845 but this raw theorem only shows that particular element in the |
845 but this raw theorem only shows that two particular elements in the |
846 equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a |
846 equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a |
847 more general statement stipulating that the equivalence classes are not |
847 more general statement stipulating that the equivalence classes are not |
848 equal is necessary. This kind of failure is beyond the scope where the |
848 equal is necessary. This kind of failure is beyond the scope where the |
849 quotient package can help: the user has to provide a raw theorem that |
849 quotient package can help: the user has to provide a raw theorem that |
850 can be regularized automatically, or has to provide an explicit proof |
850 can be regularized automatically, or has to provide an explicit proof |
854 regularized theorem based on @{text "raw_thm"} and |
854 regularized theorem based on @{text "raw_thm"} and |
855 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
855 @{text "quot_thm"}. Then we define the statement of the injected theorem, based |
856 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
856 on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps, |
857 which can all be performed independently from each other. |
857 which can all be performed independently from each other. |
858 |
858 |
859 We first define the function @{text REG}. The intuition |
859 We first define the function @{text REG}, which takes terms of the |
|
860 @{text "raw_thm"} and @{text "quot_thm"} as input and returns |
|
861 @{text "reg_thm"}. The intuition |
860 behind this function is that it replaces quantifiers and |
862 behind this function is that it replaces quantifiers and |
861 abstractions involving raw types by bounded ones, and equalities |
863 abstractions involving raw types by bounded ones, and equalities |
862 involving raw types are replaced by appropriate aggregate |
864 involving raw types are replaced by appropriate aggregate |
863 equivalence relations. It is defined as follows: |
865 equivalence relations. It is defined by simultaneously recursing on |
|
866 the structure of @{text "raw_thm"} and @{text "quot_thm"} as follows: |
864 |
867 |
865 \begin{center} |
868 \begin{center} |
866 \begin{longtable}{rcl} |
869 \begin{tabular}{rcl} |
867 \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\ |
870 \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\ |
868 @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & |
871 @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & |
869 $\begin{cases} |
872 $\begin{cases} |
870 @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\ |
873 @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\ |
871 @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"} |
874 @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"} |
881 %% REL of two equal types is the equality so we do not need a separate case |
884 %% REL of two equal types is the equality so we do not need a separate case |
882 @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\ |
885 @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\ |
883 \multicolumn{3}{@ {}l}{applications, variables and constants:}\\ |
886 \multicolumn{3}{@ {}l}{applications, variables and constants:}\\ |
884 @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\ |
887 @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\ |
885 @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\ |
888 @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\ |
886 @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm] |
889 @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\ |
887 \end{longtable} |
890 \end{tabular} |
888 \end{center} |
891 \end{center} |
889 % |
892 % |
890 \noindent |
893 \noindent |
891 In the above definition we omitted the cases for existential quantifiers |
894 In the above definition we omitted the cases for existential quantifiers |
892 and unique existential quantifiers, as they are very similar to the cases |
895 and unique existential quantifiers, as they are very similar to the cases |