--- a/Quotient-Paper/Paper.thy Sun Jun 13 14:39:55 2010 +0200
+++ b/Quotient-Paper/Paper.thy Sun Jun 13 17:01:15 2010 +0200
@@ -114,7 +114,7 @@
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
context of HOL, there have been a few quotient packages already
- \cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier
+ \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
\cite{Homeier05} implemented in HOL4. The fundamental construction these
quotient packages perform can be illustrated by the following picture:
@@ -144,19 +144,19 @@
\end{center}
\noindent
- The starting point is an existing type, often referred to as the
- \emph{raw level}, over which an equivalence relation given by the user is
+ 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 level}. This type comes with an
+ refer as the \emph{quotient type}. This type comes with an
\emph{abstraction} and a \emph{representation} function, written @{text Abs}
- and @{text Rep}. 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
-
+ 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
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "Abs::nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep::int \<Rightarrow> nat \<times> nat"}
+ @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
\end{isabelle}
\noindent
@@ -192,7 +192,7 @@
\noindent
We expect that the corresponding operator on finite sets, written @{term "fconcat"},
- behaves as follows:
+ builds the union of finite sets of finite sets:
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
@@ -205,7 +205,7 @@
the abstraction of the result is \emph{not} enough. The reason is that case in case
of @{text "\<Union>"} we obtain the incorrect definition
- @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat (Rep S))"}
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
\noindent
where the right-hand side is not even typable! This problem can be remedied in the
@@ -216,7 +216,7 @@
representation and abstraction functions, which in case of @{text "\<Union>"}
generate the following definition
- @{text [display, indent=10] "\<Union> S \<equiv> Abs (flat ((map Rep \<circ> Rep) S))"}
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map Rep_fset \<circ> Rep_fset) S))"}
\noindent
where @{term map} is the usual mapping function for lists. In this paper we
@@ -294,13 +294,52 @@
@{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
\end{eqnarray}
+ {\it Say more about containers / maping functions }
+
*}
section {* Quotient Types and Lifting of Definitions *}
-(* Say more about containers? *)
+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"}. Given this data, we can automatically declare the quotient type as
+
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+ \end{isabelle}
+
+ \noindent
+ being the 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
-text {*
+ \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"}
+ \end{isabelle}
+
+ \noindent
+ relating the new quotient type and raw type. However, as Homeier noted, it is easier
+ to work with the following derived definitions
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
+ \end{isabelle}
+
+ \noindent
+ on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"}. With these
+ definitions the abstraction and representation functions relate directly the
+ quotient and raw types (their type is @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+ respectively). We can show that the property
+
+ @{text [display, indent=10] "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+
+ \noindent
+ holds (for the proof see \cite{Homeier05}).
To define a constant on the lifted type, an aggregate abstraction
function is applied to the raw constant. Below we describe the operation
@@ -317,17 +356,9 @@
as follows:
{\it the first argument is the raw type and the second argument the quotient type}
-
-
+ %
\begin{center}
- \begin{tabular}{rcl}
-
- % type variable case says that variables must be equal...therefore subsumed by the equal case below
- %
- %\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\
- %@{text "ABS (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\\
- %@{text "REP (\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\
-
+ \begin{longtable}{rcl}
\multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\
@{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\\
@{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id"}\smallskip\\
@@ -338,19 +369,19 @@
@{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>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>2 \<circ> (MAP(\<rho>s \<kappa>\<^isub>1) (ABS (\<sigma>s', \<tau>s')))"}\\
- @{text "REP (\<sigma>s \<kappa>\<^isub>1, \<tau>s \<kappa>\<^isub>2)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>\<^isub>1) (REP (\<sigma>s', \<tau>s'))) \<circ> Rep_\<kappa>\<^isub>2"}\\
- \end{tabular}
+ @{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}
\end{center}
-
+ %
\noindent
- where in the last two clauses we have that the quotient type @{text "\<alpha>s \<kappa>\<^isub>2"} is a quotient of
- the raw type @{text "\<rho>s \<kappa>\<^isub>1"} (for example @{text "\<alpha> fset"} and @{text "\<alpha> list"}).
+ 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>2"} against @{text "\<alpha>s \<kappa>\<^isub>2"}; similarly the @{text "\<tau>s'"} are given by the
- same type-variables when matching @{text "\<tau>s \<kappa>\<^isub>1"} against @{text "\<rho>s \<kappa>\<^isub>1"}.
+ 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: