# HG changeset patch # User Cezary Kaliszyk # Date 1276586558 -7200 # Node ID 3bcd715abd39ebb23d0b0536c18a7a645a608933 # Parent dcffc2f132c991d5e165e13a6459c77a09a3e605 conclusion diff -r dcffc2f132c9 -r 3bcd715abd39 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 15 09:12:54 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 15 09:22:38 2010 +0200 @@ -785,10 +785,10 @@ \begin{tabular}{rcl} \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\ @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \. REG (t, s)"}\\ - @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Res (REL (\, \)). REG (t, s)"}\\ + @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Respects (REL (\, \)). REG (t, s)"}\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\ @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \. REG (t, s)"}\\ - @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Res (REL (\, \)). REG (t, s)"}\\ + @{text "REG (\x : \. t, \x : \. s)"} & $\dn$ & @{text "\x : \ \ Respects (REL (\, \)). REG (t, s)"}\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\ @{text "REG ((op =) : \, (op =) : \)"} & $\dn$ & @{text "(op =) : \"}\\ @{text "REG ((op =) : \, (op =) : \)"} & $\dn$ & @{text "REL (\, \) : \"}\\ @@ -1029,27 +1029,8 @@ text {* - Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically - defines quotient types for Isabelle/HOL. It did not include theorem lifting. - John Harrison's quotient package~\cite{harrison-thesis} is the first one to - lift theorems, however only first order. There is work on quotient types in - non-HOL based systems and logical frameworks, namely theory interpretations - in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or - the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. - Larry Paulson shows a construction of quotients that does not require the - Hilbert Choice operator, again only first order~\cite{Paulson06}. - - The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, - which is the first one to support lifting of higher order theorems. In - comparison with this package we explore the notion of composition of quotients, - which allows lifting constants like @{term "concat"} and theorems about it. - The HOL4 package requires a big lists of constants, theorems to lift, - respectfullness conditions as input. Our package is modularized, so that - single definitions, single theorems or single respectfullness conditions etc - can be added, which allows a natural use of the quotient package together - with type-classes and locales. - - The code of the quotient package described here is already included in the + The code of the quotient package and the examples described here are + already included in the standard distribution of Isabelle.\footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is heavily used in Nominal Isabelle, which provides a convenient reasoning @@ -1060,38 +1041,42 @@ concurrency \cite{BengtsonParow09} and a strong normalisation result for cut-elimination in classical logic \cite{UrbanZhu08}. -*} + Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically + defines quotient types for Isabelle/HOL. It did not include theorem lifting. + John Harrison's quotient package~\cite{harrison-thesis} is the first one to + lift theorems, however only first order. There is work on quotient types in + non-HOL based systems and logical frameworks, namely theory interpretations + in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or + the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}. + Larry Paulson shows a construction of quotients that does not require the + Hilbert Choice operator, again only first order~\cite{Paulson06}. + The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05}, + which is the first one to support lifting of higher order theorems. -subsection {* Contributions *} - -text {* - We present the detailed lifting procedure, which was not shown before. - - The quotient package presented in this paper has the following - advantages over existing packages: - \begin{itemize} - - \item We define quotient composition, function map composition and - relation map composition. This lets lifting polymorphic types with - subtypes quotiented as well. We extend the notions of - respectfulness and preservation to cope with quotient - composition. + Our quotient package for the first time explore the notion of + composition of quotients, which allows lifting constants like @{term + "concat"} and theorems about it. We defined the composition of + relations and showed examples of compositions of quotients which + allows lifting polymorphic types with subtypes quotiented as well. + We extended the notions of respectfullness and preservation; + with quotient compositions there is more than one condition needed + for a constant. - \item We allow lifting only some occurrences of quotiented - types. Rsp/Prs extended. (used in nominal) + Our package is modularized, so that single definitions, single + theorems or single respectfullness conditions etc can be added, + which allows the use of the quotient package together with + type-classes and locales. This has the advantage over packages + requiring big lists as input for the user of being able to develop + a theory progressively. - \item The quotient package is very modular. Definitions can be added - separately, rsp and prs can be proved separately, Quotients and maps - can be defined separately and theorems can - be lifted on a need basis. (useful with type-classes). - - \item Can be used both manually (attribute, separate tactics, - rsp/prs databases) and programatically (automated definition of - lifted constants, the rsp proof obligations and theorem statement - translation according to given quotients). - - \end{itemize} + We allow lifting only some occurrences of quotiented types, which + is useful in Nominal. The package can be used automatically with + an attribute, manually with separate tactics for parts of the lifting + procedure, and programatically. Automated definitions of constants + and respectfulness proof obligations are used in Nominal. Finally + we streamlined and showed the detailed lifting procedure, which + has not been presented before. \medskip \noindent