# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282896019 -28800
# Node ID 5606de1e5034749cbf460e00354b0d0411df4dd7
# Parent  1f9360daf6e1554cc1c428b71d8916cfcc887a41
first pass on section 1

diff -r 1f9360daf6e1 -r 5606de1e5034 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Aug 27 13:57:00 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Fri Aug 27 16:00:19 2010 +0800
@@ -66,26 +66,24 @@
 section {* Introduction *}
 
 text {* 
-   \begin{flushright}
-  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
-    collect all the theorems we shall ever want into one giant list;''}\\
-    Larry Paulson \cite{Paulson06}
-  \end{flushright}
+  \noindent
+  One might think they have been studied to death, but in the context of
+  theorem provers many questions concerning quotients are far from settled. In
+  this paper we address the question how a convenient reasoning infrastructure
+  for quotient constructions can be established in Isabelle/HOL, a popular
+  generic theorem prover. Higher-Order Logic (HOL) 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
 
-  \noindent
-  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
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + m\<^isub>2 = m\<^isub>1 + n\<^isub>2"}\hfill\numbered{natpairequiv}
   \end{isabelle}
 
@@ -100,7 +98,7 @@
   Similarly one can construct the type of finite sets, written @{term "\<alpha> fset"}, 
   by quotienting the type @{text "\<alpha> list"} according to the equivalence relation
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
   \end{isabelle}
 
@@ -115,7 +113,7 @@
   is the lambda-calculus, whose raw terms are defined as
 
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "t ::= x | t t | \<lambda>x.t"}\hfill\numbered{lambda}
   \end{isabelle}
 
@@ -136,7 +134,7 @@
   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 do this work manually, if one has only a few quotient
+  In principle it is feasible to do 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.
 
@@ -194,7 +192,7 @@
   the types of @{text Abs} and @{text Rep} are
 
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
   \end{isabelle}
 
@@ -208,7 +206,7 @@
   "0"} and @{text "1"} of type @{typ int} can be defined as
 
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
   \end{isabelle}
 
@@ -216,7 +214,7 @@
   Slightly more complicated is the definition of @{text "add"} having type 
   @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
 
-   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
   \hfill\numbered{adddef}
   \end{isabelle}
@@ -231,13 +229,19 @@
   in case of quotienting lists to yield finite sets and the operator that 
   flattens lists of lists, defined as follows
 
-  @{thm [display, indent=10] concat.simps(1) concat.simps(2)[no_vars]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} 
+  @{thm concat.simps(2)[THEN eq_reflection, no_vars]}
+  \end{isabelle}
 
   \noindent
   We expect that the corresponding operator on finite sets, written @{term "fconcat"},
   builds finite unions of finite sets:
 
-  @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm} 
+  @{thm fconcat_insert[THEN eq_reflection, no_vars]}
+  \end{isabelle}
 
   \noindent
   The quotient package should automatically provide us with a definition for @{text "\<Union>"} in
@@ -247,7 +251,9 @@
   the abstraction of the result is \emph{not} enough. The reason is that in case
   of @{text "\<Union>"} we obtain the incorrect definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<Union> S \<equiv> Abs_fset (flat (Rep_fset S))"}
+  \end{isabelle}
 
   \noindent
   where the right-hand side is not even typable! This problem can be remedied in the
@@ -258,7 +264,9 @@
   representation and abstraction functions, which in case of @{text "\<Union>"}
   generate the following definition
 
-  @{text [display, indent=10] "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<Union> S \<equiv> Abs_fset (flat ((map_list Rep_fset \<circ> Rep_fset) S))"}
+  \end{isabelle}
 
   \noindent
   where @{term map_list} is the usual mapping function for lists. In this paper we
@@ -281,36 +289,38 @@
   implemented as a ``rough recipe'' in ML-code).
 
 
-  The paper is organised as follows: Section \ref{sec:prelims} presents briefly
-  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 respectfulness
-  and preservation; Section \ref{sec:lift} describes the lifting of theorems;
-  Section \ref{sec:examples} presents some examples
-  and Section \ref{sec:conc} concludes and compares our results to existing 
-  work.
+  %The paper is organised as follows: Section \ref{sec:prelims} presents briefly
+  %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 respectfulness
+  %and preservation; Section \ref{sec:lift} describes the lifting of theorems;
+  %Section \ref{sec:examples} presents some examples
+  %and Section \ref{sec:conc} concludes and compares our results to existing 
+  %work.
 *}
 
-section {* Preliminaries and General Quotients\label{sec:prelims} *}
+section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
 
 text {*
+  \noindent
   We give in this section a crude overview of HOL and describe the main
   definitions given by Homeier for quotients \cite{Homeier05}.
 
   At its core, HOL is based on a simply-typed term language, where types are 
   recorded in Church-style fashion (that means, we can always infer the type of 
   a term and its subterms without any additional information). The grammars
-  for types and terms are as follows
+  for types and terms are
 
-  \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)\\
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  @{text "\<sigma>, \<tau> ::= \<alpha> | (\<sigma>,\<dots>, \<sigma>) \<kappa>"} & 
+  @{text "t, s ::= x\<^isup>\<sigma> | c\<^isup>\<sigma> | t t | \<lambda>x\<^isup>\<sigma>. t"}\\
   \end{tabular}
   \end{isabelle}
 
   \noindent
+  with types being either type variables or type constructors and terms
+  being variables, constants, applications or abstractions.
   We often write just @{text \<kappa>} for @{text "() \<kappa>"}, and use @{text "\<alpha>s"} and
   @{text "\<sigma>s"} to stand for collections of type variables and types,
   respectively.  The type of a term is often made explicit by writing @{text
@@ -331,13 +341,17 @@
   describes in \cite{Homeier05} map-functions for products, sums, options and
   also the following map for function types
 
-  @{thm [display, indent=10] fun_map_def[no_vars, THEN eq_reflection]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm fun_map_def[no_vars, THEN eq_reflection]}
+  \end{isabelle}
 
   \noindent
   Using this map-function, we can give the following, equivalent, but more 
   uniform definition for @{text add} shown in \eqref{adddef}:
 
-  @{text [display, indent=10] "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "add \<equiv> (Rep_int \<singlearr> Rep_int \<singlearr> Abs_int) add_pair"}
+  \end{isabelle}
 
   \noindent
   Using extensionality and unfolding the definition of @{text "\<singlearr>"}, 
@@ -354,14 +368,16 @@
   relations. For example given two equivalence relations @{text "R\<^isub>1"}
   and @{text "R\<^isub>2"}, we can define an equivalence relations over 
   products as follows
-  %
-  @{text [display, indent=10] "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(R\<^isub>1 \<tripple> R\<^isub>2) (x\<^isub>1, x\<^isub>2) (y\<^isub>1, y\<^isub>2) \<equiv> R\<^isub>1 x\<^isub>1 y\<^isub>1 \<and> R\<^isub>2 x\<^isub>2 y\<^isub>2"}
+  \end{isabelle}
 
   \noindent
   Homeier gives also the following operator for defining equivalence 
   relations over function types
   %
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
   \hfill\numbered{relfun}
   \end{isabelle}
@@ -433,9 +449,9 @@
   composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 
   with @{text R} being an equivalence relation, then
 
-  @{text [display, indent=2] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
-
-  \vspace{-.5mm}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text  "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+  \end{isabelle}
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -447,7 +463,7 @@
   relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
   the quotient type declaration is therefore
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
   \end{isabelle}
 
@@ -456,7 +472,7 @@
   examples are
 
   
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   \isacommand{quotient\_type}~~@{text "int = nat \<times> nat / \<approx>\<^bsub>nat \<times> nat\<^esub>"}\\
   \isacommand{quotient\_type}~~@{text "\<alpha> fset = \<alpha> list / \<approx>\<^bsub>list\<^esub>"}
@@ -471,7 +487,7 @@
   relations is omitted).  Given this data, we define for declarations shown in
   \eqref{typedecl} the quotient types internally as
   
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
   \end{isabelle}
 
@@ -482,7 +498,7 @@
   "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
   abstraction and representation functions 
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "abs_\<kappa>\<^isub>q :: \<sigma> set \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"}\hspace{10mm}@{text "rep_\<kappa>\<^isub>q :: \<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma> set"}
   \end{isabelle}
 
@@ -491,7 +507,7 @@
   type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
   to work with the following derived abstraction and representation functions
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "Abs_\<kappa>\<^isub>q x \<equiv> abs_\<kappa>\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\<kappa>\<^isub>q x \<equiv> \<epsilon> (rep_\<kappa>\<^isub>q x)"}
   \end{isabelle}
   
@@ -513,7 +529,7 @@
   of the raw type (remember this is the only way how to extend HOL
   with new definitions). For the user the visible part of such definitions is the declaration
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
   \end{isabelle}
 
@@ -523,7 +539,7 @@
   given explicitly (the point is that @{text "\<tau>"} and @{text "\<sigma>"} can only differ 
   in places where a quotient and raw type is involved). Two concrete examples are
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
   \isacommand{quotient\_definition}~~@{text "\<Union> :: (\<alpha> fset) fset \<Rightarrow> \<alpha> fset"}~~%
@@ -609,8 +625,10 @@
 %%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
 %%% $\kappa$.' means, but also think that it is too vague.
 
-  @{text [display, indent=10] "\<lambda>a b. map_prod (map_list a) b"}
-  
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<lambda>a b. map_prod (map_list a) b"}
+  \end{isabelle}
+
   \noindent
   which is essential in order to define the corresponding aggregate 
   abstraction and representation functions.
@@ -621,7 +639,9 @@
   fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
   the abstraction function
 
-  @{text [display, indent=10] "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+  \end{isabelle}
 
   \noindent
   In our implementation we further
@@ -629,12 +649,16 @@
   "map"}s and @{text "id"}, for example @{term "map_list id = id"} and @{text "f \<circ> id =
   id \<circ> f = f"}. This gives us the simpler abstraction function
 
-  @{text [display, indent=10] "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset"}
+  \end{isabelle}
 
   \noindent
   which we can use for defining @{term "fconcat"} as follows
 
-  @{text [display, indent=10] "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<Union> \<equiv> ((map_list Rep_fset \<circ> Rep_fset) \<singlearr> Abs_fset) flat"}
+  \end{isabelle}
 
   \noindent
   Note that by using the operator @{text "\<singlearr>"} and special clauses
@@ -643,7 +667,9 @@
   Consequently, all definitions in the quotient package 
   are of the general form
 
-  @{text [display, indent=10] "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "c \<equiv> ABS (\<sigma>, \<tau>) t"}
+  \end{isabelle}
 
   \noindent
   where @{text \<sigma>} is the type of the definiens @{text "t"} and @{text "\<tau>"} the
@@ -691,7 +717,7 @@
   notable is the bound variable function, that is the constant @{text bn}, defined 
   for raw lambda-terms as follows
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
   @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
   @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
@@ -741,7 +767,9 @@
   constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation 
   we generate the following proof obligation
 
-  @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
+  \end{isabelle}
 
   \noindent
   Homeier calls these proof obligations \emph{respectfulness
@@ -756,25 +784,31 @@
   respectfulness proof obligations. In case of @{text bn}
   this obligation is as follows
 
-  @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text  "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
+  \end{isabelle}
 
   \noindent
   and the point is that the user cannot discharge it: because it is not true. To see this,
   we can just unfold the definition of @{text "\<doublearr>"} \eqref{relfun} 
   using extensionality to obtain the false statement
 
-  @{text [display, indent=10] "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
- 
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<forall>t\<^isub>1 t\<^isub>2. if t\<^isub>1 \<approx>\<^isub>\<alpha> t\<^isub>2 then bn(t\<^isub>1) = bn(t\<^isub>2)"}
+  \end{isabelle}
+
   \noindent
   In contrast, if we lift a theorem about @{text "append"} to a theorem describing 
   the union of finite sets, then we need to discharge the proof obligation
 
-  @{text [display, indent=10] "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(\<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub> \<doublearr> \<approx>\<^bsub>list\<^esub>) append append"}
+  \end{isabelle}
 
   \noindent
   To do so, we have to establish
   
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+  \begin{isabelle}\ \ \ \ \ %%%
   if @{text "xs \<approx>\<^bsub>list\<^esub> ys"} and  @{text "us \<approx>\<^bsub>list\<^esub> vs"}
   then @{text "xs @ us \<approx>\<^bsub>list\<^esub> ys @ vs"}
   \end{isabelle}
@@ -801,13 +835,17 @@
 %%% Cezary: I think this would be a nice thing to do but we have not
 %%% done it, the theorems need to be 'guessed' from the remaining obligations
 
-  @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
+  \end{isabelle}
 
   \noindent
   where the @{text "\<alpha>s"} stand for the type variables in the type of @{text "c\<^isub>r"}.
   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 
 
-  @{text [display, indent=10] "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+  \end{isabelle}
 
   \noindent
   under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
@@ -1000,7 +1038,9 @@
   for instance, a quantifier by a bounded quantifier. In this case we have 
   rules of the form
 
-  @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
+  \end{isabelle}
 
   \noindent
   They decompose a bounded quantifier on the right-hand side. We can decompose a
@@ -1008,7 +1048,9 @@
   if it is a relation over function types with the range being an equivalence
   relation. If @{text R} is an equivalence relation we can prove that
 
-  @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
+  \end{isabelle}
 
   \noindent
   If @{term R\<^isub>2} is an equivalence relation, we can prove that for any predicate @{term P}
@@ -1016,7 +1058,9 @@
 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
 %%% should include a proof sketch?
 
-  @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+  \end{isabelle}
 
   \noindent
   The last theorem is new in comparison with Homeier's package. There the
@@ -1038,12 +1082,16 @@
     @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
     can apply the theorem:
 
-    @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
+  \begin{isabelle}\ \ \ \ \ %%%
+    @{term "R x y \<longrightarrow> R x (Rep (Abs y))"}
+  \end{isabelle}
 
     Otherwise we introduce an appropriate relation between the subterms
     and continue with two subgoals using the lemma:
 
-    @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
+  \begin{isabelle}\ \ \ \ \ %%%
+    @{text "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
+  \end{isabelle}
   \end{itemize}
 
   We defined the theorem @{text "inj_thm"} in such a way that
@@ -1058,14 +1106,18 @@
   the lambda preservation theorem. Given
   @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 
-  @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+  \end{isabelle}
 
   \noindent
   Next, relations over lifted types can be rewritten to equalities
   over lifted type. Rewriting is performed with the following theorem,
   which has been shown by Homeier~\cite{Homeier05}:
 
-  @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) Quotient_rel_rep[no_vars]}
+  \end{isabelle}
 
   \noindent
   Finally, we rewrite with the preservation theorems. This will result
@@ -1089,7 +1141,7 @@
   the raw type with which the quotienting will be performed. We give
   the same integer relation as the one presented in \eqref{natpairequiv}:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
   \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\
   \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"}
@@ -1101,7 +1153,7 @@
   relation is an equivalence relation, which is solved automatically using the
   definition of equivalence and extensionality:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
   \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}\\
   \hspace{5mm}@{text "by (auto simp add: equivp_def expand_fun_eq)"}
@@ -1111,10 +1163,11 @@
   \noindent
   The user can then specify the constants on the quotient type:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
-  \isacommand{fun}~~@{text "add_pair"}~~\isacommand{where}~~%
+  \isacommand{fun}~~@{text "add_pair"}\\
+  \isacommand{where}~~%
   @{text "add_pair (m, n) (p, q) \<equiv> (m + p :: nat, n + q :: nat)"}\\
   \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
   \isacommand{is}~~@{text "add_pair"}\\
@@ -1124,7 +1177,7 @@
   \noindent
   The following theorem about addition on the raw level can be proved.
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
   \end{isabelle}
 
@@ -1133,7 +1186,7 @@
   automatically leaving the respectfulness proof for the constant @{text "add_pair"}
   as the only remaining proof obligation. This property needs to be proved by the user:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \begin{tabular}{@ {}l}
   \isacommand{lemma}~~@{text "[quot_respect]:"}\\ 
   @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
@@ -1145,23 +1198,19 @@
   of @{text "\<doublearr>"}.
   After this, the user can prove the lifted lemma as follows:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
   \end{isabelle}
 
   \noindent
   or by using the completely automated mode stating just:
 
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
+  \begin{isabelle}\ \ \ \ \ %
   \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
   \end{isabelle}
 
   \noindent
-  Both methods give the same result, namely
-
-  @{text [display, indent=10] "0 + x = x"}
-
-  \noindent
+  Both methods give the same result, namely @{text "0 + x = x"}
   where @{text x} is of type integer.
   Although seemingly simple, arriving at this result without the help of a quotient
   package requires a substantial reasoning effort (see \cite{Paulson06}).
diff -r 1f9360daf6e1 -r 5606de1e5034 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Fri Aug 27 13:57:00 2010 +0800
+++ b/Quotient-Paper/document/root.tex	Fri Aug 27 16:00:19 2010 +0800
@@ -17,8 +17,8 @@
 \newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
-\isabellestyle{it}
-\renewcommand{\isastyleminor}{\it}%
+\isabellestyle{rm}
+\renewcommand{\isastyleminor}{\rm}%
 \renewcommand{\isastyle}{\normalsize\rm}%
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
@@ -26,9 +26,9 @@
 \verbdef\doublearr|===>|
 \verbdef\tripple|###|
 
-\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymequiv}{$\triangleq$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
-\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
 
 \newcommand{\isasymsinglearr}{\singlearr}
@@ -63,19 +63,18 @@
 mechanism for extension is the introduction of safe definitions and of
 non-empty types. Both extensions are often performed in quotient
 constructions. To ease the work involved with such quotient constructions, we
-re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
-extended his work in order to deal with compositions of quotients. Like his
-package, we designed our quotient package so that every step in a quotient construction
-can be performed separately and as a result we are able to specify completely
-the procedure of lifting theorems from the raw level to the quotient level.
-The importance for programming language research is that many properties of
-programming language calculi are easier to verify over $\alpha$-equated, or
-$\alpha$-quotient, terms, than over raw terms.
+re-implemented in the popular Isabelle/HOL theorem prover the quotient 
+package by Homeier. In doing so we extended his work in order to deal with 
+compositions of quotients and we are also able to specify completely the procedure 
+of lifting theorems from the raw level to the quotient level.
+The importance for theorem proving is that many formal
+verifications, in order to be feasible, require a convenient resoning infrastructure 
+for quotient constructions.
 \end{abstract}
 
-\category{D.??}{TODO}{TODO}
+%\category{D.??}{TODO}{TODO}
 
-\keywords{quotients, isabelle, higher order logic}
+\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}
 
 % generated text of all theories
 \input{session}