diff -r b8dda31890ff -r d1ab5d2d6926 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Sun Jun 13 17:41:07 2010 +0200 +++ b/Quotient-Paper/Paper.thy Sun Jun 13 20:54:50 2010 +0200 @@ -49,7 +49,7 @@ {\em ``Not using a [quotient] package has its advantages: we do not have to\\ collect all the theorems we shall ever want into one giant list;''}\\ Larry Paulson \cite{Paulson06} - \end{flushright}\smallskip + \end{flushright} \noindent Isabelle is a popular generic theorem prover in which many logics can be @@ -64,7 +64,9 @@ integers in Isabelle/HOL are constructed by a quotient construction over the type @{typ "nat \ nat"} and the equivalence relation - @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"} + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "(n\<^isub>1, n\<^isub>2) \ (m\<^isub>1, m\<^isub>2) \ n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv} + \end{isabelle} \noindent This constructions yields the new type @{typ int} and definitions for @{text @@ -77,7 +79,9 @@ Similarly one can construct the type of finite sets, written @{term "\ fset"}, by quotienting the type @{text "\ list"} according to the equivalence relation - @{text [display, indent=10] "xs \ ys \ (\x. memb x xs \ memb x ys)"} + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "xs \ ys \ (\x. memb x xs \ memb x ys)"}\hfill\numbered{listequiv} + \end{isabelle} \noindent which states that two lists are equivalent if every element in one list is @@ -145,15 +149,16 @@ \noindent The starting point is an existing type, often referred to as the \emph{raw - type}, over which an equivalence relation given by the user is - defined. With this input the package introduces a new type, to which we - refer as the \emph{quotient type}. This type comes with an - \emph{abstraction} and a \emph{representation} function, written @{text Abs} - and @{text Rep}.\footnote{Actually they need to be derived from slightly - more basic functions. We will show the details later. } These functions - relate elements in the existing type to ones in the new type and vice versa; - they can be uniquely identified by their type. For example for the integer - quotient construction the types of @{text Abs} and @{text Rep} are + type}, over which an equivalence relation given by the user is defined. With + this input the package introduces a new type, to which we refer as the + \emph{quotient type}. This type comes with an \emph{abstraction} and a + \emph{representation} function, written @{text Abs} and @{text + Rep}.\footnote{Actually slightly more basic functions are given; the @{text Abs} + and @{text Rep} need to be derived from them. We will show the details + later. } These functions relate elements in the existing type to ones in the + new type and vice versa; they can be uniquely identified by their type. For + example for the integer quotient construction the types of @{text Abs} and + @{text Rep} are \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "Abs :: nat \ nat \ int"}\hspace{10mm}@{text "Rep :: int \ nat \ nat"} @@ -225,27 +230,27 @@ They generate definitions, like the one above for @{text "\"}, according to the type of the raw constant and the type of the quotient constant. This means we also have to extend the notions - of \emph{aggregate relation}, \emph{respectfulness} and \emph{preservation} + of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} from Homeier \cite{Homeier05}. - We will also address the criticism by Paulson \cite{Paulson06} cited at the - beginning of this section about having to collect theorems that are lifted from the raw - level to the quotient level. Our quotient package is the first one that is modular so that it - allows to lift single theorems separately. This has the advantage for the - user to develop a formal theory interactively an a natural progression. A - pleasing result of the modularity is also that we are able to clearly - specify what needs to be done in the lifting process (this was only hinted at in - \cite{Homeier05} and implemented as a ``rough recipe'' in ML-code). - - The paper is organised as follows \ldots + We are also able to address the criticism by Paulson \cite{Paulson06} cited + at the beginning of this section about having to collect theorems that are + lifted from the raw level to the quotient level. Our quotient package is the + first one that is modular so that it allows to lift single theorems + separately. This has the advantage for the user to develop a formal theory + interactively an a natural progression. A pleasing result of the modularity + is also that we are able to clearly specify what needs to be done in the + lifting process (this was only hinted at in \cite{Homeier05} and implemented + as a ``rough recipe'' in ML-code). + + The paper is organised as follows: Section \ref{sec:prelims} presents briefly + some necessary preliminaries; Section \ref{sec:type} presents the definitions + of quotient types and shows how definitions can be made over quotient types. \ldots *} - section {* Preliminaries and General Quotient\label{sec:prelims} *} - - text {* In this section we present the definitions of a quotient that follow those by Homeier, the proofs can be found there. @@ -296,9 +301,13 @@ {\it Say more about containers / maping functions } + Such maps for most common types (list, pair, sum, + option, \ldots) are described in Homeier, and we assume that @{text "map"} + is the function that returns a map for a given type. + *} -section {* Quotient Types and Lifting of Definitions *} +section {* Quotient Types and Quotient Definitions\label{sec:type} *} text {* The first step in a quotient constructions is to take a name for the new @@ -312,19 +321,34 @@ \end{isabelle} \noindent - and a proof that @{text "R"} is indeed an equivalence relation. - Given this data, we can internally declare the quotient type as + and a proof that @{text "R"} is indeed an equivalence relation. Two concrete + examples are + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + \isacommand{quotient\_type}~~@{text "int = nat \ nat / \\<^bsub>nat \ nat\<^esub>"}\\ + \isacommand{quotient\_type}~~@{text "\ fset = \ list / \\<^bsub>list\<^esub>"} + \end{tabular} + \end{isabelle} + + \noindent + which introduce the type of integers and of finite sets using the + equivalence relations @{text "\\<^bsub>nat \ nat\<^esub>"} and @{text + "\\<^bsub>list\<^esub>"} defined earlier in \eqref{natpairequiv} and + \eqref{listequiv}, respectively. Given this data, we declare internally + the quotient types as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \isacommand{typedef}~~@{text "\s \\<^isub>q = {c. \x. c = R x}"} \end{isabelle} \noindent - being the (non-empty) set of equivalence classes of @{text "R"}. The - restriction in this declaration is that the type variables in the raw type - @{text "\"} must be included in the type variables @{text "\s"} declared for - @{text "\\<^isub>q"}. HOL will provide us with abstraction and - representation functions having the type + where the right hand side is the (non-empty) set of equivalence classes of + @{text "R"}. The restriction in this declaration is that the type variables + in the raw type @{text "\"} must be included in the type variables @{text + "\s"} declared for @{text "\\<^isub>q"}. HOL will provide us with + abstraction and representation functions having the type \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "abs_\\<^isub>q :: \ set \ \s \\<^isub>q"}\hspace{10mm}@{text "rep_\\<^isub>q :: \s \\<^isub>q \ \ set"} @@ -341,39 +365,54 @@ \noindent on the expense of having to use Hilbert's choice operator @{text "\"} in the - definition of @{text "Rep_\\<^isub>q"}. These derived notions relate the quotient type - and the raw type directly, as can be seen from their type, namely @{text "\ - \ \s \\<^isub>q"} and @{text "\s \\<^isub>q \ \"}, respectively. Given that - @{text "R"} is an equivalence relation, the following property + definition of @{text "Rep_\\<^isub>q"}. These derived notions relate the + quotient type and the raw type directly, as can be seen from their type, + namely @{text "\ \ \s \\<^isub>q"} and @{text "\s \\<^isub>q \ \"}, + respectively. Given that @{text "R"} is an equivalence relation, the + following property + @{text [display, indent=10] "Quotient R Abs_\\<^isub>q Rep_\\<^isub>q"} \noindent holds (for the proof see \cite{Homeier05}). - The next step is to lift definitions over the raw type to definitions over the - quotient type. For this we provide the declaration + The next step is to introduce new definitions involving the quotient type, + which need to be defined in terms of concepts of the raw type (remember this + is the only way how toe be able to extend HOL with new definitions). For the + user visible is the declaration \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \isacommand{quotient\_definition}~~@{text "c :: \"}~\isacommand{is}~@{text "c' :: \"} + \isacommand{quotient\_definition}~~@{text "c :: \"}~~\isacommand{is}~~@{text "t :: \"} \end{isabelle} - To define a constant on the lifted type, an aggregate abstraction - function is applied to the raw constant. Below we describe the operation - that generates - an aggregate @{term "Abs"} or @{term "Rep"} function given the - compound raw type and the compound quotient type. - This operation will also be used in translations of theorem statements - and in the lifting procedure. + \noindent + where @{text t} is the definiens (its type @{text \} can always be inferred) + and @{text "c"} is the name of definiendum, whose type @{text "\"} needs to be + given explicitly (the point is that @{text "\"} and @{text "\"} can only differ + in places where a quotient and raw type are involved). Two examples are - The operation is additionally able to descend into types for which - maps are known. Such maps for most common types (list, pair, sum, - option, \ldots) are described in Homeier, and we assume that @{text "map"} - is the function that returns a map for a given type. Then REP/ABS is defined - as follows: + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\ + \isacommand{quotient\_definition}~~@{text "\ :: (\ fset) fset \ \ fset"}~~% + \isacommand{is}~~@{text "flat"} + \end{tabular} + \end{isabelle} + + \noindent + The first one declares zero for integers and the second the operator for + building unions of finite sets. The problem for us is that from such + declarations we need to derive proper definitions using the @{text "Abs"} + and @{text "Rep"} functions for the quotient types involved. The data we + rely on is the given quotient type @{text "\"} and the raw type @{text "\"}. + They allow us to define aggregate abstraction and representation functions + using the functions @{text "ABS (\, \)"} and @{text "REP (\, \)"} whose + clauses are given below. The idea behind them is to recursively descend into + both types and generate the appropriate @{text "Abs"} and @{text "Rep"} + in places where the types differ. Therefore we returning just the identity + whenever the types are equal. - {\it the first argument is the raw type and the second argument the quotient type} - % \begin{center} \begin{longtable}{rcl} \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ @@ -387,35 +426,36 @@ @{text "REP (\s \, \s \)"} & $\dn$ & @{text "map_\ (REP (\s, \s))"}\smallskip\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ @{text "ABS (\s \, \s \\<^isub>q)"} & $\dn$ & @{text "Abs_\\<^isub>q \ (MAP(\s \) (ABS (\s', \s')))"}\\ - @{text "REP (\s \, \s \\<^isub>q)"} & $\dn$ & @{text "(MAP(\s \) (REP (\s', \s'))) \ Rep_\\<^isub>q"}\\ + @{text "REP (\s \, \s \\<^isub>q)"} & $\dn$ & @{text "(MAP(\s \) (REP (\s', \s'))) \ Rep_\\<^isub>q"} \end{longtable} \end{center} % \noindent - where in the last two clauses we have that the quotient type @{text "\s \\<^isub>q"} is a quotient of - the raw type @{text "\s \"} (for example @{text "\ fset"} and @{text "\ list"}). - The quotient construction ensures that the type variables in @{text "\s"} - must be amongst the @{text "\s"}. Now the @{text "\s'"} are given by the matchers - for the @{text "\s"} - when matching @{text "\s \\<^isub>q"} against @{text "\s \\<^isub>q"}; similarly the @{text "\s'"} are given by the - same type-variables when matching @{text "\s \"} against @{text "\s \"}. - The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type - as follows: - + where in the last two clauses we have that the quotient type @{text "\s + \\<^isub>q"} is a quotient of the raw type @{text "\s \"} (for example + @{text "int"} and @{text "nat \ nat"}, or @{text "\ fset"} and @{text "\ + list"}). The quotient construction ensures that the type variables in @{text + "\s"} must be amongst the @{text "\s"}. The @{text "\s'"} are given by the + matchers for the @{text "\s"} when matching @{text "\s \\<^isub>q"} against + @{text "\s \\<^isub>q"}; similarly the @{text "\s'"} are given by the same + type-variables when matching @{text "\s \"} against @{text "\s \"}. The + function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw + type as follows: + % \begin{center} - \begin{tabular}{rcl} - @{text "MAP' (\)"} & $\dn$ & @{text "a"}\\ + \begin{longtable}{rcl} + @{text "MAP' (\)"} & $\dn$ & @{text "a\<^sup>\"}\\ @{text "MAP' (\)"} & $\dn$ & @{text "id"}\\ @{text "MAP' (\s \)"} & $\dn$ & @{text "map_\ (MAP'(\s))"}\smallskip\\ @{text "MAP (\)"} & $\dn$ & @{text "\as. MAP'(\)"} - \end{tabular} + \end{longtable} \end{center} - + % \noindent In this definition we abuse the fact that we can interpret type-variables @{text \} as term variables @{text a}, and in the last clause build an abstraction over all term-variables inside the aggregate map-function generated by @{text "MAP'"}. - This aggregate map-function is necessary if we build quotients, say @{text "(\, \) foo"}, + This aggregate map-function is necessary if we build quotients, say @{text "(\, \) \\<^isub>q"}, out of compound raw types, say @{text "(\ list) \ \"}. In this case @{text MAP} generates the aggregate map-function: @@ -429,11 +469,11 @@ @{text [display, indent=10] "(map (map id \ Rep_fset) \ Rep_fset) \ Abs_fset \ map id"} \noindent - where we already performed some @{text "\"}-simplifications. In our implementation - we further simplified this by noticing the usual laws about @{text "map"}s and @{text "id"}, - namely @{term "map id = id"} and - @{text "f \ id = id \ f = f"}. This gives us the simplified abstraction function - + where we already performed some @{text "\"}-simplifications. In our + implementation we further simplify this by noticing the usual laws about + @{text "map"}s and @{text "id"}, namely @{term "map id = id"} and @{text "f + \ id = id \ f = f"}. This gives us the simplified abstraction function + @{text [display, indent=10] "(map Rep_fset \ Rep_fset) \ Abs_fset"} \noindent @@ -441,25 +481,18 @@ @{text [display, indent=10] "\ \ ((map Rep_fset \ Rep_fset) \ Abs_fset) flat"} - Apart from the last 2 points the definition is same as the one implemented in - in Homeier's HOL package. Adding composition in last two cases is necessary - for compositional quotients. We illustrate the different behaviour of the - definition by showing the derived definition of @{term fconcat}: - - @{thm fconcat_def[no_vars]} + \noindent + Note that by using the operator @{text "\"} we do not have to + distinguish between arguments and results: teh representation and abstraction + functions are just inverses which we can combine using @{text "\"}. + So all our definitions are of the general form - The aggregate @{term Abs} function takes a finite set of finite sets - and applies @{term "map rep_fset"} composed with @{term rep_fset} to - its input, obtaining a list of lists, passes the result to @{term concat} - obtaining a list and applies @{term abs_fset} obtaining the composed - finite set. + @{text [display, indent=10] "c \ ABS (\, \) t"} - For every type map function we require the property that @{term "map id = id"}. - With this we can compactify the term, removing the identity mappings, - obtaining a definition that is the same as the one provided by Homeier - in the cases where the internal type does not change. - - {\it we should be able to prove} + \noindent + where @{text \} is the type of @{text "t"} and @{text "\"} the type of the + newly defined quotient constant @{text "c"}. To ensure we obtained a correct + definition, we can prove: \begin{lemma} If @{text "ABS (\, \)"} returns some abstraction function @{text "Abs"} @@ -468,8 +501,13 @@ @{text "\ \ \"}. \end{lemma} - This lemma fails in the over-simplified abstraction and representation function used - in Homeier's quotient package. + \begin{proof} + By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}. + \end{proof} + + \noindent + This lemma fails for the abstraction and representation functions used in, + for example, Homeier's quotient package. *} subsection {* Respectfulness *} @@ -866,7 +904,19 @@ section {* Conclusion *} text {* - The package is part of the standard distribution of Isabelle. + + + The code of the quotient package described here is already included in the + standard distribution of Isabelle.\footnote{Avaiable from + \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is + heavily used in Nominal Isabelle, which provides a convenient reasoning + infrastructure for programming language calculi involving binders. 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}. + *}