1039 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or |
1039 in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or |
1040 the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. |
1040 the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. |
1041 Larry Paulson shows a construction of quotients that does not require the |
1041 Larry Paulson shows a construction of quotients that does not require the |
1042 Hilbert Choice operator, again only first order~\cite{Paulson06}. |
1042 Hilbert Choice operator, again only first order~\cite{Paulson06}. |
1043 |
1043 |
1044 The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}... |
1044 The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, |
|
1045 which is the first one to support lifting of higher order theorems. In |
|
1046 comparison with this package we explore the notion of composition of quotients, |
|
1047 which allows lifting constants like @{term "concat"} and theorems about it. |
|
1048 The HOL4 package requires a big lists of constants, theorems to lift, |
|
1049 respectfullness conditions as input. Our package is modularized, so that |
|
1050 single definitions, single theorems or single respectfullness conditions etc |
|
1051 can be added, which allows a natural use of the quotient package together |
|
1052 with type-classes and locales. |
1045 |
1053 |
1046 The code of the quotient package described here is already included in the |
1054 The code of the quotient package described here is already included in the |
1047 standard distribution of Isabelle.\footnote{Available from |
1055 standard distribution of Isabelle.\footnote{Available from |
1048 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1056 \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is |
1049 heavily used in Nominal Isabelle, which provides a convenient reasoning |
1057 heavily used in Nominal Isabelle, which provides a convenient reasoning |