877 |
877 |
878 They can be removed anywhere if the relation is an equivalence relation: |
878 They can be removed anywhere if the relation is an equivalence relation: |
879 |
879 |
880 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
880 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
881 |
881 |
882 And finally it can be removed anywhere if @{term R2} is an equivalence relation, then: |
882 And finally it can be removed anywhere if @{term R2} is an equivalence relation: |
883 |
883 |
884 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
884 @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]} |
885 |
885 |
886 The last theorem is new in comparison with Homeier's package. There the |
886 The last theorem is new in comparison with Homeier's package. There the |
887 injection procedure would be used to prove goals with such shape, and there |
887 injection procedure would be used to prove goals with such shape, and there |
1028 *} |
1028 *} |
1029 |
1029 |
1030 section {* Conclusion and Related Work\label{sec:conc}*} |
1030 section {* Conclusion and Related Work\label{sec:conc}*} |
1031 |
1031 |
1032 text {* |
1032 text {* |
1033 |
1033 |
1034 \begin{itemize} |
1034 Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically |
1035 |
1035 defines quotient types for Isabelle/HOL. It did not include theorem lifting. |
1036 \item Peter Homeier's package~\cite{Homeier05} (and related work from there) |
1036 John Harrison's quotient package~\cite{harrison-thesis} is the first one to |
1037 |
1037 lift theorems, however only first order. There is work on quotient types in |
1038 \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems |
1038 non-HOL based systems and logical frameworks, namely theory interpretations |
1039 but only first order. |
1039 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or |
1040 |
1040 the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. |
1041 \item PVS~\cite{PVS:Interpretations} |
1041 Larry Paulson shows a construction of quotients that does not require the |
1042 \item MetaPRL~\cite{Nogin02} |
1042 Hilbert Choice operator, again only first order~\cite{Paulson06}. |
1043 |
1043 |
1044 % \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, |
1044 The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}... |
1045 % Dixon's FSet, \ldots) |
|
1046 |
|
1047 \item Oscar Slotosch defines quotient-type automatically but no |
|
1048 lifting~\cite{Slotosch97}. |
|
1049 |
|
1050 \item PER. And how to avoid it. |
|
1051 |
|
1052 \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06} |
|
1053 |
|
1054 \item Setoids in Coq and \cite{ChicliPS02} |
|
1055 |
|
1056 \end{itemize} |
|
1057 |
|
1058 |
1045 |
1059 The code of the quotient package described here is already included in the |
1046 The code of the quotient package described here is already included in the |
1060 standard distribution of Isabelle.\footnote{Available from |
1047 standard distribution of Isabelle.\footnote{Available from |
1061 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1048 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1062 heavily used in Nominal Isabelle, which provides a convenient reasoning |
1049 heavily used in Nominal Isabelle, which provides a convenient reasoning |