# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1275919023 -7200
# Node ID b307de538d2013a9a537c9a34a89889da2dd1de8
# Parent  02e03d4287ec66ccc4423a7f0b3f0cb973c7be40
more work on intro and abstract (done for today)

diff -r 02e03d4287ec -r b307de538d20 Quotient-Paper/Paper.thy
--- 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
diff -r 02e03d4287ec -r b307de538d20 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Mon Jun 07 15:13:39 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 07 15:57:03 2010 +0200
@@ -24,7 +24,7 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL), used in several theorem provers, is based on a small
+Higher-order logic (HOL), used in a number of theorem provers, is based on a small
 logic kernel, whose only mechanism for extension is the introduction of safe
 definitions and non-empty types. Both extensions are often performed by
 quotient constructions; for example finite sets are constructed by quotienting