--- 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 \<times> nat"} and the equivalence relation
- @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> 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 "\<alpha> fset"},
by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
- @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> 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 \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
@@ -225,27 +230,27 @@
They generate definitions, like the one above for @{text "\<Union>"},
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 \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
+ \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
+ \end{tabular}
+ \end{isabelle}
+
+ \noindent
+ which introduce the type of integers and of finite sets using the
+ equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
+ "\<approx>\<^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 "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>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 "\<sigma>"} must be included in the type variables @{text "\<alpha>s"} declared for
- @{text "\<kappa>\<^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 "\<sigma>"} must be included in the type variables @{text
+ "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will provide us with
+ abstraction and representation functions having the type
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
@@ -341,39 +365,54 @@
\noindent
on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
- definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the quotient type
- and the raw type directly, as can be seen from their type, namely @{text "\<sigma>
- \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"}, respectively. Given that
- @{text "R"} is an equivalence relation, the following property
+ definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
+ quotient type and the raw type directly, as can be seen from their type,
+ namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+ respectively. Given that @{text "R"} is an equivalence relation, the
+ following property
+
@{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^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 :: \<tau>"}~\isacommand{is}~@{text "c' :: \<sigma>"}
+ \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
\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 \<sigma>} can always be inferred)
+ and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
+ given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} 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 "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> 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 "\<tau>"} and the raw type @{text "\<sigma>"}.
+ They allow us to define aggregate abstraction and representation functions
+ using the functions @{text "ABS (\<sigma>, \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} 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 (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s')))"}\\
- @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}\\
+ @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>q"}
\end{longtable}
\end{center}
%
\noindent
- where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>q"} is a quotient of
- the raw type @{text "\<rho>s \<kappa>"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}).
- The quotient construction ensures that the type variables in @{text "\<rho>s"}
- must be amongst the @{text "\<alpha>s"}. Now the @{text "\<sigma>s'"} are given by the matchers
- for the @{text "\<alpha>s"}
- when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the
- same type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}.
- 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 "\<alpha>s
+ \<kappa>\<^isub>q"} is a quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
+ @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
+ list"}). The quotient construction ensures that the type variables in @{text
+ "\<rho>s"} must be amongst the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+ matchers for the @{text "\<alpha>s"} when matching @{text "\<sigma>s \<kappa>\<^isub>q"} against
+ @{text "\<alpha>s \<kappa>\<^isub>q"}; similarly the @{text "\<tau>s'"} are given by the same
+ type-variables when matching @{text "\<tau>s \<kappa>"} against @{text "\<rho>s \<kappa>"}. The
+ function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
+ type as follows:
+ %
\begin{center}
- \begin{tabular}{rcl}
- @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a"}\\
+ \begin{longtable}{rcl}
+ @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
@{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
@{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
- \end{tabular}
+ \end{longtable}
\end{center}
-
+ %
\noindent
In this definition we abuse the fact that we can interpret type-variables @{text \<alpha>} 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 "(\<alpha>, \<beta>) foo"},
+ This aggregate map-function is necessary if we build quotients, say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"},
out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
generates the aggregate map-function:
@@ -429,11 +469,11 @@
@{text [display, indent=10] "(map (map id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map id"}
\noindent
- where we already performed some @{text "\<beta>"}-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 \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
-
+ where we already performed some @{text "\<beta>"}-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
+ \<circ> id = id \<circ> f = f"}. This gives us the simplified abstraction function
+
@{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
\noindent
@@ -441,25 +481,18 @@
@{text [display, indent=10] "\<Union> \<equiv> ((map Rep_fset \<circ> Rep_fset) \<singlearr> 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 "\<singlearr>"} we do not have to
+ distinguish between arguments and results: teh representation and abstraction
+ functions are just inverses which we can combine using @{text "\<singlearr>"}.
+ 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 \<equiv> ABS (\<sigma>, \<tau>) 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 \<sigma>} is the type of @{text "t"} and @{text "\<tau>"} 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 (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
@@ -468,8 +501,13 @@
@{text "\<tau> \<Rightarrow> \<sigma>"}.
\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}.
+
*}