# HG changeset patch # User Cezary Kaliszyk # Date 1288329950 -32400 # Node ID ea0cdb7c645548aca16ada5b731b254a22fa5a9e # Parent bf4b28ebb4125125c61168f2aabedb4cdc5e4467 Qpaper / Move examples to commented out appendix diff -r bf4b28ebb412 -r ea0cdb7c6455 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Thu Oct 28 15:16:43 2010 +0900 +++ b/Quotient-Paper/Paper.thy Fri Oct 29 14:25:50 2010 +0900 @@ -315,8 +315,8 @@ sketch this part of our work in Section 5 and we defer the reader to a longer version for the details. However, we will give in Section 3 and 4 all definitions that specify the input and output data of our three-step - lifting procedure. Section 6 gives an example how our quotient package - works in practise. + lifting procedure. + %Appendix A gives an example how our quotient package works in practise. *} section {* Preliminaries and General\\ Quotients\label{sec:prelims} *} @@ -1179,8 +1179,76 @@ %in two equal terms that can be solved by reflexivity. *} +section {* Conclusion and Related Work\label{sec:conc}*} -section {* Examples \label{sec:examples} *} +text {* + + \noindent + 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/}.} + The package is + heavily used in the new version of Nominal Isabelle, which provides a + convenient reasoning infrastructure for programming language calculi + involving general binders. To achieve this, it builds types representing + @{text \}-equivalent terms. Earlier versions of Nominal Isabelle have been + used successfully in formalisations of an equivalence checking algorithm for + LF \cite{UrbanCheneyBerghofer08}, Typed + Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency + \cite{BengtsonParow09} and a strong normalisation result for cut-elimination + in classical logic \cite{UrbanZhu08}. + + + There is a wide range of existing literature for dealing with quotients + in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that + automatically defines quotient types for Isabelle/HOL. But he did not + include theorem lifting. Harrison's quotient package~\cite{harrison-thesis} + is the first one that is able to automatically lift theorems, however only + first-order theorems (that is theorems where abstractions, quantifiers and + variables do not involve functions that include the quotient type). There is + also some work on quotient types in non-HOL based systems and logical + frameworks, including theory interpretations in + PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and + setoids in Coq \cite{ChicliPS02}. Paulson showed a construction of + quotients that does not require the Hilbert Choice operator, but also only + first-order theorems can be lifted~\cite{Paulson06}. The most related work + to our package is the package for HOL4 by Homeier~\cite{Homeier05}. He + introduced most of the abstract notions about quotients and also deals with + lifting of higher-order theorems. However, he cannot deal with quotient + compositions (needed for lifting theorems about @{text flat}). Also, a + number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc + only exist in \cite{Homeier05} as ML-code, not included in the paper. + Like Homeier's, our quotient package can deal with partial equivalence + relations, but for lack of space we do not describe the mechanisms + needed for this kind of quotient constructions. + +%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS, +%%% and some comparison. I don't think we have the space for any additions... + + One feature of our quotient package is that when lifting theorems, the user + can precisely specify what the lifted theorem should look like. This feature + is necessary, for example, when lifting an induction principle for two + lists. Assuming this principle has as the conclusion a predicate of the + form @{text "P xs ys"}, then we can precisely specify whether we want to + quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very + useful in the new version of Nominal Isabelle, where such a choice is + required to generate a reasoning infrastructure for alpha-equated terms. +%% +%% give an example for this +%% + \medskip + + \noindent + {\bf Acknowledgements:} We would like to thank Peter Homeier for the many + discussions about his HOL4 quotient package and explaining to us + some of its finer points in the implementation. Without his patient + help, this work would have been impossible. + +% \appendix + +*} + +(* section {* Examples \label{sec:examples} *} text {* @@ -1189,7 +1257,7 @@ %%% it due to lack of space... \noindent - In this section we will show a sequence of declarations for defining the + In this appendix we will show a sequence of declarations for defining the type of integers by quotienting pairs of natural numbers, and lifting one theorem. @@ -1271,74 +1339,7 @@ Although seemingly simple, arriving at this result without the help of a quotient package requires a substantial reasoning effort (see \cite{Paulson06}). *} - -section {* Conclusion and Related Work\label{sec:conc}*} - -text {* - - \noindent - 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/}.} - The package is - heavily used in the new version of Nominal Isabelle, which provides a - convenient reasoning infrastructure for programming language calculi - involving general binders. To achieve this, it builds types representing - @{text \}-equivalent terms. Earlier versions of Nominal Isabelle have been - used successfully in formalisations of an equivalence checking algorithm for - LF \cite{UrbanCheneyBerghofer08}, Typed - Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency - \cite{BengtsonParow09} and a strong normalisation result for cut-elimination - in classical logic \cite{UrbanZhu08}. - - - There is a wide range of existing literature for dealing with quotients - in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that - automatically defines quotient types for Isabelle/HOL. But he did not - include theorem lifting. Harrison's quotient package~\cite{harrison-thesis} - is the first one that is able to automatically lift theorems, however only - first-order theorems (that is theorems where abstractions, quantifiers and - variables do not involve functions that include the quotient type). There is - also some work on quotient types in non-HOL based systems and logical - frameworks, including theory interpretations in - PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and - setoids in Coq \cite{ChicliPS02}. Paulson showed a construction of - quotients that does not require the Hilbert Choice operator, but also only - first-order theorems can be lifted~\cite{Paulson06}. The most related work - to our package is the package for HOL4 by Homeier~\cite{Homeier05}. He - introduced most of the abstract notions about quotients and also deals with - lifting of higher-order theorems. However, he cannot deal with quotient - compositions (needed for lifting theorems about @{text flat}). Also, a - number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc - only exist in \cite{Homeier05} as ML-code, not included in the paper. - Like Homeier's, our quotient package can deal with partial equivalence - relations, but for lack of space we do not describe the mechanisms - needed for this kind of quotient constructions. - -%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS, -%%% and some comparison. I don't think we have the space for any additions... - - One feature of our quotient package is that when lifting theorems, the user - can precisely specify what the lifted theorem should look like. This feature - is necessary, for example, when lifting an induction principle for two - lists. Assuming this principle has as the conclusion a predicate of the - form @{text "P xs ys"}, then we can precisely specify whether we want to - quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very - useful in the new version of Nominal Isabelle, where such a choice is - required to generate a reasoning infrastructure for alpha-equated terms. -%% -%% give an example for this -%% - \medskip - - \noindent - {\bf Acknowledgements:} We would like to thank Peter Homeier for the many - discussions about his HOL4 quotient package and explaining to us - some of its finer points in the implementation. Without his patient - help, this work would have been impossible. - -*} - +*) (*<*)