--- a/Quotient-Paper/Paper.thy Mon Jun 07 15:13:39 2010 +0200
+++ b/Quotient-Paper/Paper.thy Mon Jun 07 15:57:03 2010 +0200
@@ -58,35 +58,45 @@
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 to use both mechanisms for dealing with quotient constructions in
- HOL (see for example \cite{Homeier05,Paulson06}). For example the integers
+ 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
@{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
\noindent
- This produces the type @{typ int} and definitions for @{text "0::int"} and
- @{text "1::int"} in terms of pairs of natural numbers can be given (namely
- @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as @{text "add::int
- \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on pairs of natural
- numbers. Similarly one can construct the type of finite sets by quotienting
- lists according to the equivalence relation
+ This constructions yields the type @{typ int} and definitions for @{text
+ "0::int"} and @{text "1::int"} in terms of pairs of natural numbers can be
+ given (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
@{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
\noindent
- which means two lists are equivalent if every element in one list is also
+ 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 problem is that in order to start reasoning about, for example integers,
- definitions and theorems need to be transferred, or \emph{lifted},
- from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}.
- This lifting usually requires a lot of tedious reasoning effort.
- The purpose of a \emph{quotient package} is to ease the lifting and automate
- the reasoning involved as much as possible. Such a package is a central
- component of the new version of Nominal Isabelle where representations
- of alpha-equated terms are constructed according to specifications given by
- the user.
+ The problem is that in order to be able to reason about integers and
+ finite sets, 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
+ @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}). This lifting usually
+ requires a \emph{lot} of tedious reasoning effort. The purpose of a \emph{quotient
+ package} is to ease the lifting and automate the reasoning as much as
+ possible. While for integers and finite sets teh tedious reasoning needs
+ to be done only once, Nominal Isabelle providing a reasoning infrastructure
+ for binders and @{text "\<alpha>"}-equated terms it needs to be done over and over
+ again.
+
+ Such a package is a central component of the new version of
+ Nominal Isabelle where representations of alpha-equated terms are
+ constructed according to specifications given by the user.
+
In the context of HOL, there have been several quotient packages (...). The
most notable is the one by Homeier (...) implemented in HOL4. However, what is