diff -r dff64b2e7ec3 -r 2c4c0d93daa6 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Jun 10 13:37:32 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Fri Jun 11 14:04:58 2010 +0200
@@ -7,8 +7,6 @@
         "../Nominal/FSet"
 begin
 
-print_syntax
-
 notation (latex output)
   rel_conj ("_ OOO _" [53, 53] 52) and
   "op -->" (infix "\<rightarrow>" 100) and
@@ -18,7 +16,9 @@
   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 
   Cons ("_::_") 
+ 
   
 
 ML {*
@@ -49,86 +49,101 @@
   \end{flushright}\smallskip
 
   \noindent
-  Isabelle is a generic theorem prover in which many logics can be
+  Isabelle is a popular generic theorem prover in which many logics can be
   implemented. The most widely used one, however, is Higher-Order Logic
   (HOL). This logic consists of a small number of axioms and inference rules
   over a simply-typed term-language. Safe reasoning in HOL is ensured by two
   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 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
+  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
 
   @{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 constructions yields the new type @{typ int} and definitions for @{text
-  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of 
-  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
+  "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of
+  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
 
   @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
 
   \noindent
   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 union of two finite sets, written @{text "\<union>\<^isub>f"}, as list append. 
+  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. 
+
+  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
+
+  @{text [display, indent=10] "t ::= x | t t | \<lambda>x.t"}
 
-  Another important area of quotients is reasoning about programming language
-  calculi. A simple example are lambda-terms defined as
+  \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
+  \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.
+
+  The difficulty is that in order to be able to reason about integers, finite
+  sets and $\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.  The purpose of a
+  \emph{quotient package} is to ease the lifting and automate the reasoning as
+  much as possible. 
 
   \begin{center}
-  @{text "t ::= x | t t | \<lambda>x.t"}
-  \end{center}
+  \mbox{}\hspace{20mm}\begin{tikzpicture}
+  %%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \draw[very thick] (0.7,0.3) circle (4.85mm);
+  \draw[rounded corners=1mm, very thick] ( 0.0,-0.9) rectangle ( 1.8, 0.9);
+  \draw[rounded corners=1mm, very thick] (-1.95,0.8) rectangle (-2.9,-0.195);
+  
+  \draw (-2.0, 0.8) --  (0.7,0.8);
+  \draw (-2.0,-0.195)  -- (0.7,-0.195);
 
-  \noindent
-  The difficulty with this definition of lambda-terms arises when, for 
-  example, proving formally the substitution lemma ...
-  On the other hand if we reason about alpha-equated lambda-terms, that means
-  terms quotient according to alpha-equivalence, then reasoning infrastructure
-  can be introduced that make the formal proof of the substitution lemma
-  almost trivial. 
+  \draw ( 0.7, 0.23) node {\begin{tabular}{@ {}c@ {}}equiv-\\[-1mm]clas.\end{tabular}};
+  \draw (-2.45, 0.35) node {\begin{tabular}{@ {}c@ {}}new\\[-1mm]type\end{tabular}};
+  \draw (1.8, 0.35) node[right=-0.1mm]
+    {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+  \draw (0.9, -0.55) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+  
+  \draw[->, very thick] (-1.8, 0.36) -- (-0.1,0.36);
+  \draw[<-, very thick] (-1.8, 0.16) -- (-0.1,0.16);
+  \draw (-0.95, 0.26) node[above=0.4mm] {Rep};
+  \draw (-0.95, 0.26) node[below=0.4mm] {Abs};
+
+  \end{tikzpicture}
+  \end{center}
 
 
-  The problem is that in order to be able to reason about integers, finite sets
-  and 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
-  @{text "\<alpha> list"} and finite sets of type @{text "\<alpha>"}, and also for raw lambda-terms
-  and alpha-equated lambda-terms). 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
   surprising, none of them can deal compositions of quotients, for example with 
   lifting theorems about @{text "concat"}:
 
-  @{thm [display] concat.simps(1)}
-  @{thm [display] concat.simps(2)[no_vars]}
+  @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
 
   \noindent
   One would like to lift this definition to the operation:
 
-  @{thm [display] fconcat_empty[no_vars]}
-  @{thm [display] fconcat_insert[no_vars]}
+  @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
   \noindent
   What is special about this operation is that we have as input