--- a/Quotient-Paper/Paper.thy Fri Jun 11 16:36:02 2010 +0200
+++ b/Quotient-Paper/Paper.thy Fri Jun 11 17:52:06 2010 +0200
@@ -58,7 +58,7 @@
very restricted mechanisms for extending the logic: one is the definition of
new constants in terms of existing ones; the other is the introduction of
new types by identifying non-empty subsets in existing types. It is well
- understood how to use both mechanisms for dealing with quotient
+ understood how to use both mechanisms for dealing with many quotient
constructions in HOL (see \cite{Homeier05,Paulson06}). For example the
integers in Isabelle/HOL are constructed by a quotient construction over the
type @{typ "nat \<times> nat"} and the equivalence relation
@@ -71,10 +71,10 @@
natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations
such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in
terms of operations on pairs of natural numbers (namely @{text
- "add\<^bsub>nat\<times>nat\<^esub> (x\<^isub>1, y\<^isub>1) (x\<^isub>2,
- y\<^isub>2) \<equiv> (x\<^isub>1 + x\<^isub>2, y\<^isub>1 + y\<^isub>2)"}).
- Similarly one can construct the type of finite sets by quotienting lists
- according to the equivalence relation
+ "add\<^bsub>nat\<times>nat\<^esub> (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+ m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
+ Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"},
+ by quotienting @{text "\<alpha> list"} according to the equivalence relation
@{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
@@ -90,28 +90,32 @@
@{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
\noindent
- The problem with this definition arises when one, for example, attempts to
- prove formally the substitution lemma \cite{Barendregt81} by induction
- ove the structure of terms. This can be fiendishly complicated (see
+ The problem with this definition arises when one attempts to
+ prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
+ over the structure of terms. This can be fiendishly complicated (see
\cite[Pages 94--104]{CurryFeys58} for some ``rough'' sketches of a proof
about ``raw'' lambda-terms). In contrast, if we reason about
$\alpha$-equated lambda-terms, that means terms quotient according to
$\alpha$-equivalence, then the reasoning infrastructure provided by,
for example, Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
- proof of the substitution lemma almost trivial.
+ proof of the substitution lemma almost trivial.
The difficulty is that in order to be able to reason about integers, finite
sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
infrastructure by transferring, or \emph{lifting}, definitions and theorems
from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}
(similarly for finite sets and $\alpha$-equated lambda-terms). This lifting
- usually requires a \emph{lot} of tedious reasoning effort.
+ usually requires a \emph{lot} of tedious reasoning effort \cite{Paulson06}.
+ It is feasible to to this work manually if one has only a few quotient
+ constructions, but if they have to be done over and over again as in
+ Nominal Isabelle, then manual reasoning is not an option.
The purpose of a \emph{quotient package} is to ease the lifting and automate
the reasoning as much as possible. In the context of HOL, there have been
- several quotient packages (...). The most notable is the one by Homeier
- (...) implemented in HOL4. The fundamental construction the quotient
- package performs can be illustrated by the following picture:
+ a few quotient packages already \cite{harrison-thesis,Slotosch97}. The
+ most notable is the one by Homeier \cite{Homeier05} implemented in HOL4.
+ The fundamental construction these quotient packages perform can be
+ illustrated by the following picture:
\begin{center}
\mbox{}\hspace{20mm}\begin{tikzpicture}
@@ -141,13 +145,12 @@
\noindent
The starting point is an existing type over which a user-given equivalence
relation is defined. With this input, the package introduces a new type,
- which comes with two associated abstraction and representation functions,
- @{text Abs} and @{text Rep}, that relate elements in the existing and new
- type. These two function represent an isomorphism between the non-empty
- subset and the new type.
-
- The abstractions and representation functions are important for defining
- concepts involving the new type. For example @{text "0"} and @{text "1"}
+ which comes with two associated abstraction and representation functions, written
+ @{text Abs} and @{text Rep}. They relate elements in the existing and new
+ type and can be uniquely identified by their type (which however we omit for
+ better readability). These two function represent an isomorphism between
+ the non-empty subset and the new type. They are necessary making definitions
+ over the new type. For example @{text "0"} and @{text "1"}
of type @{typ int} can be defined as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -155,21 +158,21 @@
\end{isabelle}
\noindent
- Slightly more complicated is the definition of @{text "add"} with type
- @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition looks as follows
+ Slightly more complicated is the definition of @{text "add"} which has type
+ @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
- @{text [display, indent=10] "add x y \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep x) (Rep y))"}
+ @{text [display, indent=10] "add n m \<equiv> Abs (add\<^bsub>nat\<times>nat\<^esub> (Rep n) (Rep m))"}
\noindent
- where we have to take first the representation of @{text x} and @{text y},
+ where we have to take first the representation of @{text n} and @{text m},
add them according to @{text "add\<^bsub>nat\<times>nat\<^esub>"} and then take the
abstraction of the result. This is all straightforward and the existing
quotient packages can deal with such definitions. But what is surprising
that none of them can deal with more complicated definitions involving
\emph{compositions} of quotients. Such compositions are needed for example
- when quotienting finite lists (@{text "\<alpha> list"}) to yield finite sets
- (@{text "\<alpha> fset"}). There one would like to have a corresponding definition
- for the operator @{term "concat"}, which flattens lists of lists as follows
+ in case of finite sets. There one would like to have a corresponding definition
+ for finite sets for the operator @{term "concat"} defined over lists. This
+ operator flattens lists of lists as follows
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
@@ -228,7 +231,7 @@
\end{itemize}
*}
-section {* Quotient Type*}
+section {* General Quotient *}