# HG changeset patch # User Christian Urban # Date 1277335657 -3600 # Node ID a0fecce8b24492f288093040d7fdb7cbf06d45f7 # Parent 9a560e489c648e7231d746d3dbb04b6a7ec0ee9c even further polishing of the qpaper diff -r 9a560e489c64 -r a0fecce8b244 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Wed Jun 23 22:41:16 2010 +0100 +++ b/Quotient-Paper/Paper.thy Thu Jun 24 00:27:37 2010 +0100 @@ -13,6 +13,8 @@ * - what do all preservation theorems look like, in particular preservation for quotient compositions + - explain how Quotient R Abs Rep is proved (j-version) + - give an example where precise specification helps (core Haskell in nominal?) *) notation (latex output) @@ -309,7 +311,7 @@ procedures showing that one theorem implies another by decomposing the term underlying the first theorem. - Like Homeier, our work relies on map-functions defined for every type + Like Homeier's, our work relies on map-functions defined for every type constructor taking some arguments, for example @{text map} for lists. Homeier describes in \cite{Homeier05} map-functions for products, sums, options and also the following map for function types @@ -390,7 +392,7 @@ always discharge a proof obligation involving @{text "Quotient"}. Our quotient package makes heavy use of this part of Homeier's work including an extension - to deal with compositions of equivalence relations defined as follows: + for dealing with compositions of equivalence relations defined as follows: \begin{definition}[Composition of Relations] @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\\"} is the predicate @@ -745,17 +747,17 @@ \noindent which is straightforward given the definition shown in \eqref{listequiv}. - The second restriction we have to impose arises from - non-lifted polymorphic constants, which are instantiated to a - type being quotient. For example, take the @{term "cons"}-constructor to - add a pair of natural numbers to a list, whereby the pair of natural numbers - turns into an integer in the quotient construction. The point is that we - still want to use @{text cons} for - adding integers to lists---just with a different type. - To be able to lift such theorems, we need a \emph{preservation property} - for @{text cons}. Assuming we have a polymorphic raw constant - @{text "c\<^isub>r :: \"} and a corresponding quotient constant @{text "c\<^isub>q :: \"}, - then a preservation property is as follows + The second restriction we have to impose arises from non-lifted polymorphic + constants, which are instantiated to a type being quotient. For example, + take the @{term "cons"}-constructor to add a pair of natural numbers to a + list, whereby we assume the pair of natural numbers turns into an integer in + the quotient construction. The point is that we still want to use @{text + cons} for adding integers to lists---just with a different type. To be able + to lift such theorems, we need a \emph{preservation property} for @{text + cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \"} + and a corresponding quotient constant @{text "c\<^isub>q :: \"}, then a + preservation property is as follows + @{text [display, indent=10] "Quotient R\<^bsub>\s\<^esub> Abs\<^bsub>\s\<^esub> Rep\<^bsub>\s\<^esub> implies ABS (\, \) c\<^isub>r = c\<^isub>r"} @@ -889,7 +891,7 @@ \noindent In the above definition we omitted the cases for existential quantifiers and unique existential quantifiers, as they are very similar to the cases - for the universal quantifier. For the third and fourt clause, note that + for the universal quantifier. For the third and fourth clause, note that @{text "\x. P"} is defined as @{text "\ (\x. P)"}. Next we define the function @{text INJ} which takes as argument @@ -1068,7 +1070,7 @@ \end{isabelle} \noindent - This property needs to beproved by the user. It + This property needs to be proved by the user. It can be discharged automatically by Isabelle when hinting to unfold the definition of @{text "\"}. After this, the user can prove the lifted lemma as follows: @@ -1078,7 +1080,7 @@ \end{isabelle} \noindent - or by using the completely automated stating just: + or by using the completely automated mode stating just: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ % \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"} @@ -1090,57 +1092,58 @@ @{text [display, indent=10] "0 + x = x"} \noindent + where @{text x} is of type integer. Although seemingly simple, arriving at this result without the help of a quotient - package requires a substantial reasoning effort. + package requires a substantial reasoning effort (see \cite{Paulson06}). *} section {* Conclusion and Related Work\label{sec:conc}*} text {* - 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 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}. + 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 of 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. + 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. - 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 resoning infrastructure - for alpha-equated terms. + + 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 %%