--- a/Quotient-Paper/Paper.thy Sun Jun 13 20:54:50 2010 +0200
+++ b/Quotient-Paper/Paper.thy Mon Jun 14 04:38:25 2010 +0200
@@ -92,7 +92,9 @@
An area where quotients are ubiquitous is reasoning about programming language
calculi. A simple example is the lambda-calculus, whose raw terms are defined as
- @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
+ \end{isabelle}
\noindent
The problem with this definition arises when one attempts to
@@ -116,7 +118,7 @@
Nominal Isabelle, then manual reasoning is not an option.
The purpose of a \emph{quotient package} is to ease the lifting of theorems
- and automate the definitions and reasoning as much as possible. In the
+ and automate the reasoning as much as possible. In the
context of HOL, there have been a few quotient packages already
\cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
\cite{Homeier05} implemented in HOL4. The fundamental construction these
@@ -148,40 +150,42 @@
\end{center}
\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 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
+ The starting point is an existing type, to which we often refer 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 slightly more basic functions are given;
+ the functions @{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"}
\end{isabelle}
\noindent
- However we often leave this typing information implicit for better
- readability, but sometimes write @{text Abs_int} and @{text Rep_int} if the
- typing information is important. Every abstraction and representation
- function stands for an isomorphism between the non-empty subset and elements
- in the new type. They are necessary for making definitions involving the new
- type. For example @{text "0"} and @{text "1"} of type @{typ int} can be
- defined as
+ We therefore often write @{text Abs_int} and @{text Rep_int} if the
+ typing information is important.
+
+ Every abstraction and representation function stands for an isomorphism
+ between the non-empty subset and elements in the new type. They are
+ necessary for making definitions involving the new type. For example @{text
+ "0"} and @{text "1"} of type @{typ int} can be defined as
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "0 \<equiv> Abs (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs (1, 0)"}
+ @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
\end{isabelle}
\noindent
Slightly more complicated is the definition of @{text "add"} having type
@{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
- @{text [display, indent=10] "add n m \<equiv> Abs (add_pair (Rep n) (Rep m))"}
+ @{text [display, indent=10] "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
\noindent
where we take the representation of the arguments @{text n} and @{text m},
@@ -203,9 +207,8 @@
\noindent
The quotient package should provide us with a definition for @{text "\<Union>"} in
- terms of @{text flat}, @{text Rep} and @{text Abs} (the latter two having
- the type @{text "\<alpha> fset \<Rightarrow> \<alpha> list"} and @{text "\<alpha> list \<Rightarrow> \<alpha> fset"},
- respectively). The problem is that the method used in the existing quotient
+ terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is
+ that the method used in the existing quotient
packages of just taking the representation of the arguments and then take
the abstraction of the result is \emph{not} enough. The reason is that case in case
of @{text "\<Union>"} we obtain the incorrect definition
@@ -305,16 +308,18 @@
option, \ldots) are described in Homeier, and we assume that @{text "map"}
is the function that returns a map for a given type.
+ {\it say something about our use of @{text "\<sigma>s"}}
+
*}
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
- type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation defined over a
- raw type, say @{text "\<sigma>"}. The equivalence relation for the quotient
- construction, lets say @{text "R"}, must then be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
- bool"}. The user-visible part of the declaration is therefore
+ type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
+ defined over a raw type, say @{text "\<sigma>"}. The type of this equivalence
+ relation must be of type @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+ the declaration is therefore
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}
@@ -355,7 +360,7 @@
\end{isabelle}
\noindent
- and relating the new quotient type and equivalence classes of the raw
+ They relate the new quotient type and equivalence classes of the raw
type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
to work with the following derived abstraction and representation functions
@@ -377,10 +382,10 @@
\noindent
holds (for the proof see \cite{Homeier05}).
- 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
+ The next step in a quotient construction 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 to extend HOL
+ with new definitions). For the user visible is the declaration
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
@@ -390,7 +395,7 @@
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
+ in places where a quotient and raw type are involved). Two concrete examples are
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -402,22 +407,24 @@
\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.
+ 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 types @{text \<sigma>} and @{text \<tau>}, 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. All clauses
+ are as follows:
\begin{center}
- \begin{longtable}{rcl}
+ \begin{tabular}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
- @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
- @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
+ @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+ @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
\multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\
@{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
@{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
@@ -425,54 +432,57 @@
@{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
@{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"}
- \end{longtable}
+ @{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"}
+ \end{tabular}
\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
+ \<kappa>\<^isub>q"} is the 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
+ matchers for the @{text "\<alpha>s"} when matching @{text "\<rho>s \<kappa>"} against
+ @{text "\<sigma>s \<kappa>"}. The
function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
type as follows:
%
\begin{center}
- \begin{longtable}{rcl}
+ \begin{tabular}{rcl}
@{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
- @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id"}\\
+ @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
@{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
@{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
- \end{longtable}
+ \end{tabular}
\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>) \<kappa>\<^isub>q"},
- out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}. In this case @{text MAP}
- generates the aggregate map-function:
+ term variables @{text a}. In the last clause we build an abstraction over all
+ term-variables inside the aggregate map-function generated by the auxiliary function
+ @{text "MAP'"}.
+ The need of aggregate map-functions can be appreciated if we build quotients,
+ say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types of the form @{text "(\<alpha> list) \<times> \<beta>"}.
+ In this case @{text MAP} generates the aggregate map-function:
@{text [display, indent=10] "\<lambda>a b. map_prod (map a) b"}
\noindent
- Returning to our example about @{term "concat"} and @{term "fconcat"} which have the
- types @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. Feeding this
- into @{text ABS} gives us the abstraction function:
+ which we need to define the aggregate abstraction and representation functions.
+
+ To se how these definitions pan out in practise, let us return to our
+ example about @{term "concat"} and @{term "fconcat"}, where we have types
+ @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+ fset"}. Feeding them into @{text ABS} gives us the abstraction function
@{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 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
+ after some @{text "\<beta>"}-simplifications. In our implementation we further
+ simplify this abstraction function employing 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 abstraction function
@{text [display, indent=10] "(map Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
@@ -483,16 +493,18 @@
\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
+ distinguish between arguments and results: the representation and abstraction
+ functions are just inverses of each other, which we can combine using
+ @{text "\<singlearr>"} to deal uniformly with arguments of functions and
+ their result. As a result, all definitions in the quotient package
+ are of the general form
@{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
\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:
+ where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
+ type of the 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"}
@@ -502,19 +514,47 @@
\end{lemma}
\begin{proof}
- By induction of the definitions of @{text "ABS"}, @{text "REP"} and @{text "MAP"}.
+ By induction and analysing the definitions of @{text "ABS"}, @{text "REP"}
+ and @{text "MAP"}. The cases of equal and function types are straightforward
+ (the latter follows from @{text "\<singlearr>"} having the type
+ @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). The case of equal
+ type constructors follows by observing that a map-function after applying
+ the functions @{text "ABS (\<sigma>s, \<tau>s)"} produce a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.
+ The interesting case is the one with unequal type constructors. Since we know the
+ quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have that @{text "Abs_\<kappa>\<^isub>q"}
+ is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}, that can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"}
+ where the type variables @{text "\<alpha>s"} are instantiated with @{text "\<tau>s"}. The
+ complete type can be calculated by observing that @{text "MAP (\<rho>s \<kappa>)"} after applying
+ the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it, returns a term of type
+ @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}
+ as desired.\qed
\end{proof}
\noindent
- This lemma fails for the abstraction and representation functions used in,
- for example, Homeier's quotient package.
+ The reader should note that this lemma fails for the abstraction and representation
+ functions used, for example, in Homeier's quotient package.
*}
-subsection {* Respectfulness *}
+section {* Respectfulness and Preservation *}
text {*
+ Before we can lift theorems involving the raw types to theorems over
+ quotient types, we have to impose some restrictions. The reason is that not
+ all theorems can be lifted. Homeier formulates these restrictions in terms
+ of \emph{respectfullness} and \emph{preservation} of constants occuring in
+ theorems.
- A respectfulness lemma for a constant states that the equivalence
+ The respectfulness property for a constant states that it essentially
+ respects the equivalence relation involved in the quotient. An example
+ is the function returning bound variables of a lambda-term (see \eqref{lambda})
+ and @{text "\<alpha>"}-equivalence. It will turn out that this function is not
+ respectful.
+
+ To state the respectfulness property we have to define \emph{aggregate equivalence
+ relations}.
+
+ @{text [display] "GIVE DEFINITION HERE"}
+
class returned by this constant depends only on the equivalence
classes of the arguments applied to the constant. To automatically
lift a theorem that talks about a raw constant, to a theorem about
@@ -522,10 +562,10 @@
A respectfulness condition for a constant can be expressed in
terms of an aggregate relation between the constant and itself,
- for example the respectfullness for @{term "append"}
+ for example the respectfullness for @{text "append"}
can be stated as:
- @{thm [display, indent=10] append_rsp[no_vars]}
+ @{text [display, indent=10] "(R \<doublearr> R \<doublearr> R) append append"}
\noindent
Which after unfolding the definition of @{term "op ===>"} is equivalent to:
@@ -573,7 +613,6 @@
*}
-subsection {* Preservation *}
text {*
Sometimes a non-lifted polymorphic constant is instantiated to a