783 |
783 |
784 \begin{center} |
784 \begin{center} |
785 \begin{tabular}{rcl} |
785 \begin{tabular}{rcl} |
786 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
786 \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ |
787 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
787 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\ |
788 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
788 @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
789 \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ |
789 \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ |
790 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\ |
790 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\ |
791 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
791 @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\ |
792 \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\ |
792 \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\ |
793 @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\ |
793 @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\ |
794 @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\ |
794 @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\ |
795 \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\ |
795 \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\ |
796 @{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)"}\\ |
796 @{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)"}\\ |
1027 |
1027 |
1028 section {* Conclusion and Related Work\label{sec:conc}*} |
1028 section {* Conclusion and Related Work\label{sec:conc}*} |
1029 |
1029 |
1030 text {* |
1030 text {* |
1031 |
1031 |
|
1032 The code of the quotient package and the examples described here are |
|
1033 already included in the |
|
1034 standard distribution of Isabelle.\footnote{Available from |
|
1035 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
|
1036 heavily used in Nominal Isabelle, which provides a convenient reasoning |
|
1037 infrastructure for programming language calculi involving binders. Earlier |
|
1038 versions of Nominal Isabelle have been used successfully in formalisations |
|
1039 of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, |
|
1040 Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for |
|
1041 concurrency \cite{BengtsonParow09} and a strong normalisation result for |
|
1042 cut-elimination in classical logic \cite{UrbanZhu08}. |
|
1043 |
1032 Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically |
1044 Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically |
1033 defines quotient types for Isabelle/HOL. It did not include theorem lifting. |
1045 defines quotient types for Isabelle/HOL. It did not include theorem lifting. |
1034 John Harrison's quotient package~\cite{harrison-thesis} is the first one to |
1046 John Harrison's quotient package~\cite{harrison-thesis} is the first one to |
1035 lift theorems, however only first order. There is work on quotient types in |
1047 lift theorems, however only first order. There is work on quotient types in |
1036 non-HOL based systems and logical frameworks, namely theory interpretations |
1048 non-HOL based systems and logical frameworks, namely theory interpretations |
1037 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or |
1049 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or |
1038 the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. |
1050 the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. |
1039 Larry Paulson shows a construction of quotients that does not require the |
1051 Larry Paulson shows a construction of quotients that does not require the |
1040 Hilbert Choice operator, again only first order~\cite{Paulson06}. |
1052 Hilbert Choice operator, again only first order~\cite{Paulson06}. |
1041 |
|
1042 The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, |
1053 The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, |
1043 which is the first one to support lifting of higher order theorems. In |
1054 which is the first one to support lifting of higher order theorems. |
1044 comparison with this package we explore the notion of composition of quotients, |
1055 |
1045 which allows lifting constants like @{term "concat"} and theorems about it. |
1056 |
1046 The HOL4 package requires a big lists of constants, theorems to lift, |
1057 Our quotient package for the first time explore the notion of |
1047 respectfullness conditions as input. Our package is modularized, so that |
1058 composition of quotients, which allows lifting constants like @{term |
1048 single definitions, single theorems or single respectfullness conditions etc |
1059 "concat"} and theorems about it. We defined the composition of |
1049 can be added, which allows a natural use of the quotient package together |
1060 relations and showed examples of compositions of quotients which |
1050 with type-classes and locales. |
1061 allows lifting polymorphic types with subtypes quotiented as well. |
1051 |
1062 We extended the notions of respectfullness and preservation; |
1052 The code of the quotient package described here is already included in the |
1063 with quotient compositions there is more than one condition needed |
1053 standard distribution of Isabelle.\footnote{Available from |
1064 for a constant. |
1054 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1065 |
1055 heavily used in Nominal Isabelle, which provides a convenient reasoning |
1066 Our package is modularized, so that single definitions, single |
1056 infrastructure for programming language calculi involving binders. Earlier |
1067 theorems or single respectfullness conditions etc can be added, |
1057 versions of Nominal Isabelle have been used successfully in formalisations |
1068 which allows the use of the quotient package together with |
1058 of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, |
1069 type-classes and locales. This has the advantage over packages |
1059 Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for |
1070 requiring big lists as input for the user of being able to develop |
1060 concurrency \cite{BengtsonParow09} and a strong normalisation result for |
1071 a theory progressively. |
1061 cut-elimination in classical logic \cite{UrbanZhu08}. |
1072 |
1062 |
1073 We allow lifting only some occurrences of quotiented types, which |
1063 *} |
1074 is useful in Nominal. The package can be used automatically with |
1064 |
1075 an attribute, manually with separate tactics for parts of the lifting |
1065 |
1076 procedure, and programatically. Automated definitions of constants |
1066 subsection {* Contributions *} |
1077 and respectfulness proof obligations are used in Nominal. Finally |
1067 |
1078 we streamlined and showed the detailed lifting procedure, which |
1068 text {* |
1079 has not been presented before. |
1069 We present the detailed lifting procedure, which was not shown before. |
|
1070 |
|
1071 The quotient package presented in this paper has the following |
|
1072 advantages over existing packages: |
|
1073 \begin{itemize} |
|
1074 |
|
1075 \item We define quotient composition, function map composition and |
|
1076 relation map composition. This lets lifting polymorphic types with |
|
1077 subtypes quotiented as well. We extend the notions of |
|
1078 respectfulness and preservation to cope with quotient |
|
1079 composition. |
|
1080 |
|
1081 \item We allow lifting only some occurrences of quotiented |
|
1082 types. Rsp/Prs extended. (used in nominal) |
|
1083 |
|
1084 \item The quotient package is very modular. Definitions can be added |
|
1085 separately, rsp and prs can be proved separately, Quotients and maps |
|
1086 can be defined separately and theorems can |
|
1087 be lifted on a need basis. (useful with type-classes). |
|
1088 |
|
1089 \item Can be used both manually (attribute, separate tactics, |
|
1090 rsp/prs databases) and programatically (automated definition of |
|
1091 lifted constants, the rsp proof obligations and theorem statement |
|
1092 translation according to given quotients). |
|
1093 |
|
1094 \end{itemize} |
|
1095 |
1080 |
1096 \medskip |
1081 \medskip |
1097 \noindent |
1082 \noindent |
1098 {\bf Acknowledgements:} We would like to thank Peter Homeier for the |
1083 {\bf Acknowledgements:} We would like to thank Peter Homeier for the |
1099 discussions about the HOL4 quotient package and explaining us its |
1084 discussions about the HOL4 quotient package and explaining us its |