--- a/Quotient-Paper/Paper.thy Fri Jun 11 17:52:06 2010 +0200
+++ b/Quotient-Paper/Paper.thy Fri Jun 11 21:58:25 2010 +0200
@@ -14,12 +14,12 @@
fun_map (infix "\<longrightarrow>" 51) and
fun_rel (infix "\<Longrightarrow>" 51) and
list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
- fempty ("\<emptyset>\<^isub>f") and
- funion ("_ \<union>\<^isub>f _") and
- finsert ("{_} \<union>\<^isub>f _") and
+ fempty ("\<emptyset>") and
+ funion ("_ \<union> _") and
+ finsert ("{_} \<union> _") and
Cons ("_::_") and
concat ("flat") and
- fconcat ("fset'_flat")
+ fconcat ("\<Union>")
@@ -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 many quotient
+ understood how to use both mechanisms for dealing with 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
@@ -74,7 +74,7 @@
"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
+ by quotienting the type @{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)"}
@@ -82,7 +82,7 @@
which states that two lists are equivalent if every element in one list is also
member in the other (@{text "\<in>"} stands here for membership in lists). The
empty finite set, written @{term "{||}"}, can then be defined as the
- empty list and the union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append.
+ empty list and the union of two finite sets, written @{text "\<union>"}, as list append.
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
@@ -96,8 +96,8 @@
\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
+ $\alpha$-equivalence, then the reasoning infrastructure provided,
+ for example, by Nominal Isabelle \cite{UrbanKaliszyk11} makes the formal
proof of the substitution lemma almost trivial.
The difficulty is that in order to be able to reason about integers, finite
@@ -106,16 +106,16 @@
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 \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
+ It is feasible to to this work manually, if one has only a few quotient
+ constructions at hand. 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
- 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:
+ 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{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}
@@ -143,15 +143,15 @@
\end{center}
\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, 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
+ The starting point is an existing type over which an equivalence relation
+ given by the user is defined. With this input the package introduces a new
+ type, which comes with two associated abstraction and representation
+ functions, written @{text Abs} and @{text Rep}. These functions relate
+ elements in the existing and new type, and can be uniquely identified by
+ their type (which however we often omit for better readability). They
+ represent 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)"}
@@ -168,11 +168,10 @@
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
+ that none of them can deal with slightly more complicated definitions involving
\emph{compositions} of quotients. Such compositions are needed for example
- 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
+ in case of finite sets. For example over lists one can define an operator
+ that flattens lists of lists as follows
@{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
@@ -183,20 +182,25 @@
@{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
\noindent
- The problem is that we want to quotient lists to obtain finite sets and
- @{term concat} is of type @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}. We expect
- that @{term "fconcat"} has type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. But
- what should its definition be? It is not possible to just take the representation
- of the argument and then take the abstraction of the result of flattening
- the resulting list. The problem is that a single @{text "Rep"} only gives
- us lists of finite sets, not lists of lists. It turns out that we need
- to be able to build aggregate representation and abstraction function, which in
+ The quotient package should provide us with a definition for @{text "\<Union>"} in
+ terms of @{text flat}, @{text Rep} and @{text Abs}. The problem is that it
+ is not enough to just take the representation of the argument and then
+ take the abstraction of the result, because in that case we obtain an operator
+ with type @{text "(\<alpha> list) fset \<Rightarrow> \<alpha> fset"}, not the expected
+ @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}. It turns out that we need
+ to build aggregate representation and abstraction functions, which in
case of @{term "fconcat"} produce the following definition
- @{text [display, indent=10] "fset_flat S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
+ @{text [display, indent=10] "\<Union> S \<equiv> Abs (concat ((map Rep \<circ> Rep) S))"}
\noindent
- where @{term map} is the usual mapping function for lists.
+ where @{term map} is the usual mapping function for lists. In this paper we
+ will present a formal definition for our aggregate abstraction and
+ representation functions (this definition was omitted in \cite{Homeier05}).
+ They generate definitions like the one above for @{text add} and @{text "\<Union>"}
+ according to the type of the ``raw'' constant and the type
+ of the quotient constant.
+
*}