# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276534945 -7200
# Node ID f5f21feaa168a5809e68f12d7ccaf22e9b39bb9e
# Parent  ba068c04a8d9769122c15d9eaa179527d8c6e166
some slight tuning of the preliminary section

diff -r ba068c04a8d9 -r f5f21feaa168 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 16:45:29 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 19:02:25 2010 +0200
@@ -97,8 +97,8 @@
   \end{isabelle}
 
   \noindent
-  The problem with this definition arises when one attempts to
-  prove formally, for example, the substitution lemma \cite{Barendregt81} by induction
+  The problem with this definition arises, for instance, when one attempts to
+  prove formally 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
@@ -159,7 +159,7 @@
   the functions @{text Abs} and @{text Rep} need to be derived from them. We
   will show the details later. } These functions relate elements in the
   existing type to elements in the new type and vice versa; they can be uniquely
-  identified by their type. For example for the integer quotient construction
+  identified by their quotient type. For example for the integer quotient construction
   the types of @{text Abs} and @{text Rep} are
 
 
@@ -206,7 +206,7 @@
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
   \noindent
-  The quotient package should provide us with a definition for @{text "\<Union>"} in
+  The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
   terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is 
   that the method  used in the existing quotient
   packages of just taking the representation of the arguments and then taking
@@ -242,8 +242,8 @@
   quotient package is the first one that is modular so that it allows to lift
   single theorems separately. This has the advantage for the user of being able to develop a
   formal theory interactively as a natural progression. A pleasing side-result of
-  the modularity is that we are able to clearly specify what needs to be
-  done in the lifting process (this was only hinted at in \cite{Homeier05} and
+  the modularity is that we are able to clearly specify what is involved
+  in the lifting process (this was only hinted at in \cite{Homeier05} and
   implemented as a ``rough recipe'' in ML-code).
 
 
@@ -251,15 +251,39 @@
   some necessary preliminaries; Section \ref{sec:type} describes the definitions 
   of quotient types and shows how definitions of constants can be made over 
   quotient types. Section \ref{sec:resp} introduces the notions of respectfullness
-  and preservation.\ldots
+  and preservation; Section \ref{sec:lift} describes the lifting of theorems, 
+  and Section \ref{sec:conc} concludes and compares our results to existing 
+  work.
 *}
 
 
 section {* Preliminaries and General Quotient\label{sec:prelims} *}
 
 text {*
-  In this section we present the definitions of a quotient that follow
-  closely those given by Homeier.
+  We describe here briefly some of the most basic concepts of HOL 
+  we rely on and some of the important definitions given by Homeier 
+  \cite{Homeier05}. 
+  
+  HOL is based on a simply-typed term-language, where types are 
+  annotated in Church-style (that is we can obtain immediately
+  infer the type of term and its subterms). 
+
+  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{tabular}{@ {}rl@ {\hspace{3mm}}l@ {}}
+  @{text "\<sigma>, \<tau> ::="} & @{text "\<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & (type variables and type constructors)\\
+  @{text "t, s ::="} & @{text "x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"} & 
+  (variables, constants, applications and abstractions)\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
+  @{text "\<sigma>s"} to stand for list of type variables and types, respectively.
+  The type of a term is often made explicit by writing @{text "t :: \<sigma>"} HOL
+  contains a type @{typ bool} for booleans and the function type, written
+  @{text "\<sigma> \<Rightarrow> \<tau>"}.
+
+
 
   \begin{definition}[Quotient]
   A relation $R$ with an abstraction function $Abs$
@@ -288,20 +312,7 @@
   Higher Order Logic 
 
 
-  Types:
-  \begin{eqnarray}\nonumber
-  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
-      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
-  \end{eqnarray}
-
-  Terms:
-  \begin{eqnarray}\nonumber
-  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
-      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
-      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
-      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
-  \end{eqnarray}
-
+  
   {\it Say more about containers / maping functions }
 
   Such maps for most common types (list, pair, sum,
@@ -689,7 +700,7 @@
 *}
 
 
-section {* Lifting of Theorems *}
+section {* Lifting of Theorems\label{sec:lift} *}
 
 text {*
   The core of our quotient package takes an original theorem that
@@ -976,10 +987,11 @@
   obtaining the same result.
 *}
 
-section {* Related Work *}
+section {* Conclusion and Related Work\label{sec:conc}*}
 
 text {*
-  \begin{itemize}
+  
+\begin{itemize}
 
   \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
 
@@ -1002,11 +1014,6 @@
   \item Setoids in Coq and \cite{ChicliPS02}
 
   \end{itemize}
-*}
-
-section {* Conclusion *}
-
-text {*
 
 
   The code of the quotient package described here is already included in the