diff -r e4699a240d2c -r 4ae32dd02d14 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Tue Jun 15 08:56:13 2010 +0200 +++ b/Quotient-Paper/Paper.thy Tue Jun 15 09:44:16 2010 +0200 @@ -357,6 +357,10 @@ and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]} \end{proposition} + \begin{definition}[Respects] + An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}. + \end{definition} + \noindent As a result, Homeier was able to build an automatic prover that can nearly always discharge a proof obligation involving @{text "Quotient"}. Our quotient @@ -372,10 +376,12 @@ \end{definition} \noindent - Unfortunately, restrictions in HOL's type-system prevent us from stating - and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions - of relations. However, we can prove all instances where @{text R\<^isub>1} and - @{text "R\<^isub>2"} are built up by constituent equivalence relations. + Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for + the composition of any two quotients in not true (it is not even typable in + the HOL type system). However, we can prove useful instances for compatible + containers. We will show such example in Section \ref{sec:resp}. + + *} section {* Quotient Types and Quotient Definitions\label{sec:type} *} @@ -739,9 +745,12 @@ Lets take again the example of @{term flat}. To be able to lift theorems that talk about it we provide the composition quotient - theorem: + theorem which allows quotienting inside the container: - @{thm [display, indent=10] quotient_compose_list[no_vars]} + If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} + then + + @{text [display, indent=10] "Quotient (list_rel R \\\ \\<^bsub>list\<^esub>) (abs_fset \ map Abs) (map Rep o rep_fset)"} \noindent this theorem will then instantiate the quotients needed in the @@ -792,10 +801,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 (\, \) : \"}\\ @@ -1036,27 +1045,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 @@ -1067,38 +1057,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