# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324371293 -32400
# Node ID a6b0220fb8aeed073675792d76a91f4aac3bb211
# Parent  660a4f5adee80fd1bdc165dde049e124c1af7c3f
Added an initial version of qpaper-jv and a TODO of things to write about.

diff -r 660a4f5adee8 -r a6b0220fb8ae .hgignore
--- a/.hgignore	Tue Dec 20 16:49:03 2011 +0900
+++ b/.hgignore	Tue Dec 20 17:54:53 2011 +0900
@@ -3,6 +3,10 @@
 *~
 .#*
 
+Quotient-Paper-jv/generated
+Quotient-Paper-jv/document.pdf
+qpaper-jv.pdf
+
 LMCS-Paper/generated
 LMCS-Paper/document.pdf
 lmcs-paper.pdf
diff -r 660a4f5adee8 -r a6b0220fb8ae IsaMakefile
--- a/IsaMakefile	Tue Dec 20 16:49:03 2011 +0900
+++ b/IsaMakefile	Tue Dec 20 17:54:53 2011 +0900
@@ -69,6 +69,15 @@
 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper/generated
 	@cp Quotient-Paper/document.pdf qpaper.pdf
 
+## Quotient Journal Paper
+
+qpaper-jv: $(LOG)/HOL-QPaper-jv.gz
+
+$(LOG)/HOL-QPaper-jv.gz: Quotient-Paper-jv/ROOT.ML Quotient-Paper-jv/document/root.* Quotient-Paper-jv/*.thy
+	@$(USEDIR) -D generated HOL Quotient-Paper-jv
+	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated
+	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf
+
 ## Nominal Functions paper
 
 fnpaper: $(LOG)/HOL-FnPaper.gz
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,1364 @@
+(*<*)
+theory Paper
+imports "Quotient"
+        "~~/src/HOL/Library/Quotient_Syntax"
+        "~~/src/HOL/Library/LaTeXsugar"
+        "~~/src/HOL/Quotient_Examples/FSet"
+begin
+
+(****
+
+** things to do for the next version
+*
+* - what are quot_thms?
+* - what do all preservation theorems look like,
+    in particular preservation for quotient
+    compositions
+  - explain how Quotient R Abs Rep is proved (j-version)
+  - give an example where precise specification helps (core Haskell in nominal?)
+
+  - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
+
+*)
+
+notation (latex output)
+  rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
+  pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
+  implies (infix "\<longrightarrow>" 100) and
+  "==>" (infix "\<Longrightarrow>" 100) and
+  map_fun ("_ \<singlearr> _" 51) and
+  fun_rel ("_ \<doublearr> _" 51) and
+  list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
+  empty_fset ("\<emptyset>") and
+  union_fset ("_ \<union> _") and
+  insert_fset ("{_} \<union> _") and
+  Cons ("_::_") and
+  concat ("flat") and
+  concat_fset ("\<Union>") and
+  Quotient ("Quot _ _ _")
+
+
+
+ML {*
+fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
+
+fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
+  let
+    val concl =
+      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
+  in
+    case concl of (_ $ l $ r) => proj (l, r)
+    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
+  end);
+*}
+
+setup {*
+  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
+  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
+  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
+*}
+
+lemma insert_preserve2:
+  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+         (id ---> rep_fset ---> abs_fset) op #"
+  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
+lemma list_all2_symp:
+  assumes a: "equivp R"
+  and b: "list_all2 R xs ys"
+  shows "list_all2 R ys xs"
+using list_all2_lengthD[OF b] b
+apply(induct xs ys rule: list_induct2)
+apply(auto intro: equivp_symp[OF a])
+done
+
+lemma concat_rsp_unfolded:
+  "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"
+proof -
+  fix a b ba bb
+  assume a: "list_all2 list_eq a ba"
+  assume b: "list_eq ba bb"
+  assume c: "list_all2 list_eq bb b"
+  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+    fix x
+    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+    next
+      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+      have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
+      have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+      have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
+      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+    qed
+  qed
+  then show "list_eq (concat a) (concat b)" by auto
+qed
+
+(*>*)
+
+
+section {* Introduction *}
+
+text {*
+  \noindent
+  One might think quotients have been studied to death, but in the context of
+  theorem provers many questions concerning them are far from settled. In
+  this paper we address the question of how to establish a convenient reasoning
+  infrastructure
+  for quotient constructions in the Isabelle/HOL
+  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. Previous work has shown 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}\ \ \ \ \ %%%
+  @{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}
+
+  \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_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2,
+  m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}).
+  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}\ \ \ \ \ %%%
+  @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv}
+  \end{isabelle}
+
+  \noindent
+  which states that two lists are equivalent if every element in one list is
+  also member in the other. The empty finite set, written @{term "{||}"}, can
+  then be defined as the empty list and the union of two finite sets, written
+  @{text "\<union>"}, as list append.
+
+  Quotients are important in a variety of areas, but they are really ubiquitous in
+  the area of reasoning about programming language calculi. A simple example
+  is the lambda-calculus, whose raw terms are defined as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "t ::= x | t t | \<lambda>x.t"}%\hfill\numbered{lambda}
+  \end{isabelle}
+
+  \noindent
+  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
+  $\alpha$-equated lambda-terms, that means terms quotient according to
+  $\alpha$-equivalence, then the reasoning infrastructure provided,
+  for example, by 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 or $\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 \cite{Paulson06}.
+  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.
+
+  The purpose of a \emph{quotient package} is to ease the lifting of theorems
+  and automate the reasoning as much as possible. In the
+  context of HOL, there have been a few quotient packages already
+  \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier
+  \cite{Homeier05} implemented in HOL4.  The fundamental construction these
+  quotient packages perform can be illustrated by the following picture:
+
+%%% FIXME: Referee 1 says:
+%%% Diagram is unclear.  Firstly, isn't an existing type a "set (not sets) of raw elements"?
+%%% Secondly, isn't the _set of_ equivalence classes mapped to and from the new type?
+%%% Thirdly, what do the words "non-empty subset" refer to ?
+
+%%% Cezary: I like the diagram, maybe 'new type' could be outside, but otherwise
+%%% I wouldn't change it.
+
+  \begin{center}
+  \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]
+  %%\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);
+
+  \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 elements)\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] {@{text Rep}};
+  \draw (-0.95, 0.26) node[below=0.4mm] {@{text Abs}};
+  \end{tikzpicture}
+  \end{center}
+
+  \noindent
+  The starting point is an existing type, to which we refer as the
+  \emph{raw type} and over which an equivalence relation is given by the user.
+  With this input the package introduces a new type, to which we
+  refer as the \emph{quotient type}. This type comes with an
+  \emph{abstraction} and a \emph{representation} function, written @{text Abs}
+  and @{text Rep}.\footnote{Actually slightly more basic functions are given;
+  the functions @{text Abs} and @{text Rep} need to be derived from them. We
+  will show the details later. } They relate elements in the
+  existing type to elements in the new type, % and vice versa,
+  and can be uniquely
+  identified by their quotient type. For example for the integer quotient construction
+  the types of @{text Abs} and @{text Rep} are
+
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "Abs :: nat \<times> nat \<Rightarrow> int"}\hspace{10mm}@{text "Rep :: int \<Rightarrow> nat \<times> nat"}
+  \end{isabelle}
+
+  \noindent
+  We therefore often write @{text Abs_int} and @{text Rep_int} if the
+  typing information is important.
+
+  Every abstraction and representation function stands for an isomorphism
+  between the non-empty subset and elements in the new type. They are
+  necessary for making definitions involving the new type. For example @{text
+  "0"} and @{text "1"} of type @{typ int} can be defined as
+
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "0 \<equiv> Abs_int (0, 0)"}\hspace{10mm}@{text "1 \<equiv> Abs_int (1, 0)"}
+  \end{isabelle}
+
+  \noindent
+  Slightly more complicated is the definition of @{text "add"} having type
+  @{typ "int \<Rightarrow> int \<Rightarrow> int"}. Its definition is as follows
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "add n m \<equiv> Abs_int (add_pair (Rep_int n) (Rep_int m))"}
+  \hfill\numbered{adddef}
+  \end{isabelle}
+
+  \noindent
+  where we take the representation of the arguments @{text n} and @{text m},
+  add them according to the function @{text "add_pair"} and then take the
+  abstraction of the result.  This is all straightforward and the existing
+  quotient packages can deal with such definitions. But what is surprising is
+  that none of them can deal with slightly more complicated definitions involving
+  \emph{compositions} of quotients. Such compositions are needed for example
+  in case of quotienting lists to yield finite sets and the operator that
+  flattens lists of lists, defined as follows
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm}
+  @{thm concat.simps(2)[THEN eq_reflection, no_vars]}
+  \end{isabelle}
+
+  \noindent
+  where @{text "@"} is the usual
+  list append. We expect that the corresponding
+  operator on finite sets, written @{term "fconcat"},
+  builds finite unions of finite sets:
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm}
+  @{thm concat_insert_fset[THEN eq_reflection, no_vars]}
+  \end{isabelle}
+
+  \noindent
+  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
+  the abstraction of the result is \emph{not} enough. The reason is that in case
+  of @{text "\<Union>"} we obtain the incorrect definition
+
+  \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
+  existing quotient packages by introducing an intermediate step and reasoning
+  about flattening of lists of finite sets. However, this remedy is rather
+  cumbersome and inelegant in light of our work, which can deal with such
+  definitions directly. The solution is that we need to build aggregate
+  representation and abstraction functions, which in case of @{text "\<Union>"}
+  generate the %%%following
+  definition
+
+  \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
+  will present a formal definition of our aggregate abstraction and
+  representation functions (this definition was omitted in \cite{Homeier05}).
+  They generate definitions, like the one above for @{text "\<Union>"},
+  according to the type of the raw constant and the type
+  of the quotient constant. This means we also have to extend the notions
+  of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
+  from Homeier \cite{Homeier05}.
+
+  In addition 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). A pleasing side-result
+  is that our procedure for lifting theorems is completely deterministic
+  following the structure of the theorem being lifted and the theorem
+  on the quotient level. Space constraints, unfortunately, allow us to only
+  sketch this part of our work in Section 5 and we defer the reader to a longer
+  version for the details. However, we will give in Section 3 and 4 all
+  definitions that specify the input and output data of our three-step
+  lifting procedure. Appendix A gives an example how our quotient
+  package works in practise.
+*}
+
+section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
+
+text {*
+  \noindent
+  We will 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
+
+  \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
+  "t :: \<sigma>"}. HOL includes a type @{typ bool} for booleans and the function
+  type, written @{text "\<sigma> \<Rightarrow> \<tau>"}. HOL also contains many primitive and defined
+  constants; for example, a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
+  bool"}, and the identity function with type @{text "id :: \<sigma> \<Rightarrow> \<sigma>"} is
+  defined as @{text "\<lambda>x\<^sup>\<sigma>. x\<^sup>\<sigma>"}.
+
+  An important point to note is that theorems in HOL can be seen as a subset
+  of terms that are constructed specially (namely through axioms and proof
+  rules). As a result we are able to define automatic proof
+  procedures showing that one theorem implies another by decomposing the term
+  underlying the first theorem.
+
+  Like Homeier's, our work relies on map-functions defined for every type
+  constructor taking some arguments, for example @{text map_list} for lists. Homeier
+  describes in \cite{Homeier05} map-functions for products, sums, options and
+  also the following map for function types
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm map_fun_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}:
+
+  \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>"},
+  we can get back to \eqref{adddef}.
+  In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function
+  of the type-constructor @{text \<kappa>}.
+  %% a general type for map all types is difficult to give (algebraic types are
+  %% easy, but for example the function type is not algebraic
+  %For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
+  %type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}.
+  %For example @{text "map_list"}
+  %has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
+  In our implementation we maintain
+  a database of these map-functions that can be dynamically extended.
+
+  It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"},
+  which define equivalence relations in terms of constituent equivalence
+  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
+
+  \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}\ \ \ \ \ %%%
+  @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+  \hfill\numbered{relfun}
+  \end{isabelle}
+
+  \noindent
+  In the context of quotients, the following two notions from \cite{Homeier05}
+  are needed later on.
+
+  \begin{definition}[Respects]\label{def:respects}
+  An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
+  \end{definition}
+
+  \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
+  @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
+  and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
+  \end{definition}
+
+  The central definition in Homeier's work \cite{Homeier05} relates equivalence
+  relations, abstraction and representation functions:
+
+  \begin{definition}[Quotient Types]
+  Given a relation $R$, an abstraction function $Abs$
+  and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
+  holds if and only if
+  \begin{isabelle}\ \ \ \ \ %%%%
+  \begin{tabular}{rl}
+  (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\
+  (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\
+  (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\
+  \end{tabular}
+  \end{isabelle}
+  \end{definition}
+
+  \noindent
+  The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can
+  often be proved in terms of the validity of @{term "Quot"} over the constituent
+  types of @{text "R"}, @{text Abs} and @{text Rep}.
+  For example Homeier proves the following property for higher-order quotient
+  types:
+
+  \begin{proposition}\label{funquot}
+  \begin{isa}
+  @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"
+      and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+  \end{isa}
+  \end{proposition}
+
+  \noindent
+  As a result, Homeier is able to build an automatic prover that can nearly
+  always discharge a proof obligation involving @{text "Quot"}. Our quotient
+  package makes heavy
+  use of this part of Homeier's work including an extension
+  for dealing with \emph{conjugations} of equivalence relations\footnote{That are
+  symmetric by definition.} defined as follows:
+
+%%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
+%%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
+
+  \begin{definition}%%[Composition of Relations]
+  @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
+  composition defined by
+  @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+  holds if and only if there exists a @{text y} such that @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
+  @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
+  \end{definition}
+
+  \noindent
+  Unfortunately a general quotient theorem for @{text "\<circ>\<circ>\<circ>"}, analogous to the one
+  for @{text "\<singlearr>"} given in Proposition \ref{funquot}, would not be true
+  in general. It cannot even be stated inside HOL, because of restrictions on types.
+  However, we can prove specific instances of a
+  quotient theorem for composing particular quotient relations.
+  For example, to lift theorems involving @{term flat} the quotient theorem for
+  composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"}
+  with @{text R} being an equivalence relation, then
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{r@ {\hspace{1mm}}l}
+  @{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
+                  & @{text "(Abs_fset \<circ> map_list Abs)"} @{text "(map_list Rep \<circ> Rep_fset)"}\\
+  \end{tabular}
+  \end{isabelle}
+*}
+
+section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
+
+text {*
+  \noindent
+  The first step in a quotient construction is to take a name for the new
+  type, say @{text "\<kappa>\<^isub>q"}, and an equivalence relation, say @{text R},
+  defined over a raw type, say @{text "\<sigma>"}. The type of the equivalence
+  relation must be @{text "\<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}. The user-visible part of
+  the quotient type declaration is therefore
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \isacommand{quotient\_type}~~@{text "\<alpha>s \<kappa>\<^isub>q = \<sigma> / R"}\hfill\numbered{typedecl}
+  \end{isabelle}
+
+  \noindent
+  and a proof that @{text "R"} is indeed an equivalence relation. The @{text "\<alpha>s"}
+  indicate the arity of the new type and the type-variables of @{text "\<sigma>"} can only
+  be contained in @{text "\<alpha>s"}. Two concrete
+  examples are
+
+
+  \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>"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  which introduce the type of integers and of finite sets using the
+  equivalence relations @{text "\<approx>\<^bsub>nat \<times> nat\<^esub>"} and @{text
+  "\<approx>\<^bsub>list\<^esub>"} defined in \eqref{natpairequiv} and
+  \eqref{listequiv}, respectively (the proofs about being equivalence
+  relations are omitted).  Given this data, we define for declarations shown in
+  \eqref{typedecl} the quotient types internally as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \isacommand{typedef}~~@{text "\<alpha>s \<kappa>\<^isub>q = {c. \<exists>x. c = R x}"}
+  \end{isabelle}
+
+  \noindent
+  where the right-hand side is the (non-empty) set of equivalence classes of
+  @{text "R"}. The constraint in this declaration is that the type variables
+  in the raw type @{text "\<sigma>"} must be included in the type variables @{text
+  "\<alpha>s"} declared for @{text "\<kappa>\<^isub>q"}. HOL will then provide us with the following
+  abstraction and representation functions
+
+  \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}
+
+  \noindent
+  As can be seen from the type, they relate the new quotient type and equivalence classes of the raw
+  type. However, as Homeier \cite{Homeier05} noted, it is much more convenient
+  to work with the following derived abstraction and representation functions
+
+  \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}
+
+  \noindent
+  on the expense of having to use Hilbert's choice operator @{text "\<epsilon>"} in the
+  definition of @{text "Rep_\<kappa>\<^isub>q"}. These derived notions relate the
+  quotient type and the raw type directly, as can be seen from their type,
+  namely @{text "\<sigma> \<Rightarrow> \<alpha>s \<kappa>\<^isub>q"} and @{text "\<alpha>s \<kappa>\<^isub>q \<Rightarrow> \<sigma>"},
+  respectively.  Given that @{text "R"} is an equivalence relation, the
+  following property holds  for every quotient type
+  (for the proof see \cite{Homeier05}).
+
+  \begin{proposition}
+  \begin{isa}@{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.\end{isa}
+  \end{proposition}
+
+  The next step in a quotient construction is to introduce definitions of new constants
+  involving the quotient type. These definitions need to be given in terms of concepts
+  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}\ \ \ \ \ %%%
+  \isacommand{quotient\_definition}~~@{text "c :: \<tau>"}~~\isacommand{is}~~@{text "t :: \<sigma>"}
+  \end{isabelle}
+
+  \noindent
+  where @{text t} is the definiens (its type @{text \<sigma>} can always be inferred)
+  and @{text "c"} is the name of definiendum, whose type @{text "\<tau>"} needs to be
+  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{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"}~~%
+  \isacommand{is}~~@{text "flat"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The first one declares zero for integers and the second the operator for
+  building unions of finite sets (@{text "flat"} having the type
+  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"}).
+
+  From such declarations given by the user, the quotient package needs to derive proper
+  definitions using @{text "Abs"} and @{text "Rep"}. The data we rely on is the given quotient type
+  @{text "\<tau>"} and the raw type @{text "\<sigma>"}.  They allow us to define \emph{aggregate
+  abstraction} and \emph{representation functions} using the functions @{text "ABS (\<sigma>,
+  \<tau>)"} and @{text "REP (\<sigma>, \<tau>)"} whose clauses we shall give below. The idea behind
+  these two functions is to simultaneously descend into the raw types @{text \<sigma>} and
+  quotient types @{text \<tau>}, and generate the appropriate
+  @{text "Abs"} and @{text "Rep"} in places where the types differ. Therefore
+  we generate just the identity whenever the types are equal. On the ``way'' down,
+  however we might have to use map-functions to let @{text Abs} and @{text Rep} act
+  over the appropriate types. In what follows we use the short-hand notation
+  @{text "ABS (\<sigma>s, \<tau>s)"} to mean @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1)\<dots>ABS (\<sigma>\<^isub>n, \<tau>\<^isub>n)"}; similarly
+  for @{text REP}.
+  %
+  \begin{center}
+  \hfill
+  \begin{tabular}{@ {\hspace{2mm}}l@ {}}
+  \multicolumn{1}{@ {}l}{equal types:}\\
+  @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\hspace{5mm}%\\
+  @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
+  \multicolumn{1}{@ {}l}{function types:}\\
+  @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+  @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+  \multicolumn{1}{@ {}l}{equal type constructors:}\\
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
+  \end{tabular}\hfill\numbered{ABSREP}
+  \end{center}
+  %
+  \noindent
+  In the last two clauses are subtle. We rely in them on the fact that the type @{text "\<alpha>s
+  \<kappa>\<^isub>q"} is the quotient of the raw type @{text "\<rho>s \<kappa>"} (for example
+  @{text "int"} and @{text "nat \<times> nat"}, or @{text "\<alpha> fset"} and @{text "\<alpha>
+  list"}). This data is given by declarations shown in \eqref{typedecl}.
+  The quotient construction ensures that the type variables in @{text
+  "\<rho>s \<kappa>"} must be among the @{text "\<alpha>s"}. The @{text "\<sigma>s'"} are given by the
+  substitutions for the @{text "\<alpha>s"} when matching  @{text "\<sigma>s \<kappa>"} against
+  @{text "\<rho>s \<kappa>"}. This calculation determines what are the types in place
+  of the type variables @{text "\<alpha>s"} in the instance of
+  quotient type @{text "\<alpha>s \<kappa>\<^isub>q"}---namely @{text "\<tau>s"}, and the corresponding
+  types in place of the @{text "\<alpha>s"} in the raw type @{text "\<rho>s \<kappa>"}---namely @{text "\<sigma>s'"}. The
+  function @{text "MAP"} calculates an \emph{aggregate map-function} for a raw
+  type as follows:
+  %
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
+  @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
+  @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
+  @{text "MAP (\<sigma>)"} & $\dn$ & @{text "\<lambda>as. MAP'(\<sigma>)"}
+  \end{tabular}
+  \end{center}
+  %
+  \noindent
+  In this definition we rely on the fact that in the first clause we can interpret type-variables @{text \<alpha>} as
+  term variables @{text a}. In the last clause we build an abstraction over all
+  term-variables of the map-function generated by the auxiliary function
+  @{text "MAP'"}.
+  The need for aggregate map-functions can be seen in cases where we build quotients,
+  say @{text "(\<alpha>, \<beta>) \<kappa>\<^isub>q"}, out of compound raw types, say @{text "(\<alpha> list) \<times> \<beta>"}.
+  In this case @{text MAP} generates  the
+  aggregate map-function:
+
+%%% FIXME: Reviewer 2 asks: last two lines defining ABS and REP for
+%%% unequal type constructors: How are the $\varrho$s defined? The
+%%% following paragraph mentions them, but this paragraph is unclear,
+%%% since it then mentions $\alpha$s, which do not seem to be defined
+%%% either. As a result, I do not understand the first two sentences
+%%% in this paragraph. I can imagine roughly what the following
+%%% sentence `The $\sigma$s' are given by the matchers for the
+%%% $\alpha$s$ when matching $\varrho$s $\kappa$ against $\sigma$s
+%%% $\kappa$.' means, but also think that it is too vague.
+
+  \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.
+
+  To see how these definitions pan out in practise, let us return to our
+  example about @{term "concat"} and @{term "fconcat"}, where we have the raw type
+  @{text "(\<alpha> list) list \<Rightarrow> \<alpha> list"} and the quotient type @{text "(\<alpha> fset) fset \<Rightarrow> \<alpha>
+  fset"}. Feeding these types into @{text ABS} gives us (after some @{text "\<beta>"}-simplifications)
+  the abstraction function
+
+  \begin{isabelle}\ \ \ %%%
+  \begin{tabular}{l}
+  @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
+  \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In our implementation we further
+  simplify this function by rewriting with the usual laws about @{text
+  "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
+
+  \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
+
+  \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
+  for function types in \eqref{ABSREP}, we do not have to
+  distinguish between arguments and results, but can deal with them uniformly.
+  Consequently, all definitions in the quotient package
+  are of the general form
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{@{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
+  type of the defined quotient constant @{text "c"}. This data can be easily
+  generated from the declaration given by the user.
+  To increase the confidence in this way of making definitions, we can prove
+  that the terms involved are all typable.
+
+  \begin{lemma}
+  If @{text "ABS (\<sigma>, \<tau>)"} returns some abstraction function @{text "Abs"}
+  and @{text "REP (\<sigma>, \<tau>)"} some representation function @{text "Rep"},
+  then @{text "Abs"} is of type @{text "\<sigma> \<Rightarrow> \<tau>"} and @{text "Rep"} of type
+  @{text "\<tau> \<Rightarrow> \<sigma>"}.
+  \end{lemma}
+
+  \begin{proof}
+  By mutual induction and analysing the definitions of @{text "ABS"} and @{text "REP"}.
+  The cases of equal types and function types are
+  straightforward (the latter follows from @{text "\<singlearr>"} having the
+  type @{text "(\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> (\<gamma> \<Rightarrow> \<delta>) \<Rightarrow> (\<beta> \<Rightarrow> \<gamma>) \<Rightarrow> (\<alpha> \<Rightarrow> \<delta>)"}). In case of equal type
+  constructors we can observe that a map-function after applying the functions
+  @{text "ABS (\<sigma>s, \<tau>s)"} produces a term of type @{text "\<sigma>s \<kappa> \<Rightarrow> \<tau>s \<kappa>"}.  The
+  interesting case is the one with unequal type constructors. Since we know
+  the quotient is between @{text "\<alpha>s \<kappa>\<^isub>q"} and @{text "\<rho>s \<kappa>"}, we have
+  that @{text "Abs_\<kappa>\<^isub>q"} is of type @{text "\<rho>s \<kappa> \<Rightarrow> \<alpha>s
+  \<kappa>\<^isub>q"}. This type can be more specialised to @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s
+  \<kappa>\<^isub>q"} where the type variables @{text "\<alpha>s"} are instantiated with the
+  @{text "\<tau>s"}. The complete type can be calculated by observing that @{text
+  "MAP (\<rho>s \<kappa>)"}, after applying the functions @{text "ABS (\<sigma>s', \<tau>s)"} to it,
+  returns a term of type @{text "\<rho>s[\<sigma>s'] \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}. This type is
+  equivalent to @{text "\<sigma>s \<kappa> \<Rightarrow> \<rho>s[\<tau>s] \<kappa>"}, which we just have to compose with
+  @{text "\<rho>s[\<tau>s] \<kappa> \<Rightarrow> \<tau>s \<kappa>\<^isub>q"} according to the type of @{text "\<circ>"}.\qed
+  \end{proof}
+*}
+
+section {* Respectfulness and\\ Preservation \label{sec:resp} *}
+
+text {*
+  \noindent
+  The main point of the quotient package is to automatically ``lift'' theorems
+  involving constants over the raw type to theorems involving constants over
+  the quotient type. Before we can describe this lifting process, we need to impose
+  two restrictions in form of proof obligations that arise during the
+  lifting. The reason is that even if definitions for all raw constants
+  can be given, \emph{not} all theorems can be lifted to the quotient type. Most
+  notable is the bound variable function, that is the constant @{text bn},
+  defined
+  for raw lambda-terms as follows
+
+  \begin{isabelle}
+  \begin{center}
+  @{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)"}\smallskip\\
+  @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+  \end{center}
+  \end{isabelle}
+
+  \noindent
+  We can generate a definition for this constant using @{text ABS} and @{text REP}.
+  But this constant does \emph{not} respect @{text "\<alpha>"}-equivalence and
+  consequently no theorem involving this constant can be lifted to @{text
+  "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of
+  the properties of \emph{respectfulness} and \emph{preservation}. We have
+  to slightly extend Homeier's definitions in order to deal with quotient
+  compositions.
+
+%%% FIXME: Reviewer 3 asks why are the definitions that follow enough to deal
+%%% with quotient composition.
+
+  To formally define what respectfulness is, we have to first define
+  the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}
+  The idea behind this function is to simultaneously descend into the raw types
+  @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate
+  quotient equivalence relations in places where the types differ and equalities
+  elsewhere.
+
+  \begin{center}
+  \hfill
+  \begin{tabular}{l}
+  \multicolumn{1}{@ {}l}{equal types:}
+  @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+   \multicolumn{1}{@ {}l}{equal type constructors:}\\
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+  \end{tabular}\hfill\numbered{REL}
+  \end{center}
+
+  \noindent
+  The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
+  again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type
+  @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching
+  @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
+
+  Let us return to the lifting procedure of theorems. Assume we have a theorem
+  that contains the raw constant @{text "c\<^isub>r :: \<sigma>"} and which we want to
+  lift to a theorem where @{text "c\<^isub>r"} is replaced by the corresponding
+  constant @{text "c\<^isub>q :: \<tau>"} defined over a quotient type. In this situation
+  we generate the following proof obligation
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}.
+  \end{isabelle}
+
+  \noindent
+  Homeier calls these proof obligations \emph{respectfulness
+  theorems}. However, unlike his quotient package, we might have several
+  respectfulness theorems for one constant---he has at most one.
+  The reason is that because of our quotient compositions, the types
+  @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}.
+  And for every instantiation of the types, a corresponding
+  respectfulness theorem is necessary.
+
+  Before lifting a theorem, we require the user to discharge
+  respectfulness proof obligations. In case of @{text bn}
+  this obligation is %%as follows
+
+  \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
+
+  \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, lifting a theorem about @{text "append"} to a theorem describing
+  the union of finite sets will mean to discharge the proof obligation
+
+  \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}\ \ \ \ \ %%%
+  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}
+
+  \noindent
+  which is straightforward given the definition shown in \eqref{listequiv}.
+
+  The second restriction we have to impose arises from non-lifted polymorphic
+  constants, which are instantiated to a type being quotient. For example,
+  take the @{term "cons"}-constructor to add a pair of natural numbers to a
+  list, whereby we assume the pair of natural numbers turns into an integer in
+  the quotient construction. The point is that we still want to use @{text
+  cons} for adding integers to lists---just with a different type. To be able
+  to lift such theorems, we need a \emph{preservation property} for @{text
+  cons}. Assuming we have a polymorphic raw constant @{text "c\<^isub>r :: \<sigma>"}
+  and a corresponding quotient constant @{text "c\<^isub>q :: \<tau>"}, then a
+  preservation property is as follows
+
+%%% FIXME: Reviewer 2 asks: You say what a preservation theorem is,
+%%% but not which preservation theorems you assume. Do you generate a
+%%% proof obligation for a preservation theorem for each raw constant
+%%% and its corresponding lifted constant?
+
+%%% 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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "Quot 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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}
+  \end{isabelle}
+
+  \noindent
+  under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have
+  an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated
+  with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
+  then we need to show this preservation property.
+
+  %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
+
+  %Given two quotients, one of which quotients a container, and the
+  %other quotients the type in the container, we can write the
+  %composition of those quotients. To compose two quotient theorems
+  %we compose the relations with relation composition as defined above
+  %and the abstraction and relation functions are the ones of the sub
+  %quotients composed with the usual function composition.
+  %The @ {term "Rep"} and @ {term "Abs"} functions that we obtain agree
+  %with the definition of aggregate Abs/Rep functions and the
+  %relation is the same as the one given by aggregate relations.
+  %This becomes especially interesting
+  %when we compose the quotient with itself, as there is no simple
+  %intermediate step.
+  %
+  %Lets take again the example of @ {term flat}. To be able to lift
+  %theorems that talk about it we provide the composition quotient
+  %theorem which allows quotienting inside the container:
+  %
+  %If @ {term R} is an equivalence relation and @ {term "Quotient R Abs Rep"}
+  %then
+  %
+  %@ {text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map_list Abs) (map_list Rep o rep_fset)"}
+  %%%
+  %%%\noindent
+  %%%this theorem will then instantiate the quotients needed in the
+  %%%injection and cleaning proofs allowing the lifting procedure to
+  %%%proceed in an unchanged way.
+*}
+
+section {* Lifting of Theorems\label{sec:lift} *}
+
+text {*
+
+%%% FIXME Reviewer 3 asks: Section 5 shows the technicalities of
+%%% lifting theorems. But there is no clarification about the
+%%% correctness. A reader would also be interested in seeing some
+%%% discussions about the generality and limitation of the approach
+%%% proposed there
+
+  \noindent
+  The main benefit of a quotient package is to lift automatically theorems over raw
+  types to theorems over quotient types. We will perform this lifting in
+  three phases, called \emph{regularization},
+  \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
+  Space restrictions, unfortunately, prevent us from giving anything but a sketch of these three
+  phases. However, we will precisely define the input and output data of these phases
+  (this was omitted in \cite{Homeier05}).
+
+  The purpose of regularization is to change the quantifiers and abstractions
+  in a ``raw'' theorem to quantifiers over variables that respect their respective relations
+  (Definition \ref{def:respects} states what respects means). The purpose of injection is to add @{term Rep}
+  and @{term Abs} of appropriate types in front of constants and variables
+  of the raw type so that they can be replaced by the corresponding constants from the
+  quotient type. The purpose of cleaning is to bring the theorem derived in the
+  first two phases into the form the user has specified. Abstractly, our
+  package establishes the following three proof steps:
+
+%%% FIXME: Reviewer 1 complains that the reader needs to guess the
+%%% meaning of reg_thm and inj_thm, as well as the arguments of REG
+%%% which are given above. I wouldn't change it.
+
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{4mm}}l}
+  1.) Regularization & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+  2.) Injection & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
+  3.) Cleaning & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  which means, stringed together, the raw theorem implies the quotient theorem.
+  In contrast to other quotient packages, our package requires that the user specifies
+  both, the @{text "raw_thm"} (as theorem) and the \emph{term} of the @{text "quot_thm"}.\footnote{Though we
+  also provide a fully automated mode, where the @{text "quot_thm"} is guessed
+  from the form of @{text "raw_thm"}.} As a result, the user has fine control
+  over which parts of a raw theorem should be lifted.
+
+  The second and third proof step performed in package will always succeed if the appropriate
+  respectfulness and preservation theorems are given. In contrast, the first
+  proof step can fail: a theorem given by the user does not always
+  imply a regularized version and a stronger one needs to be proved. An example
+  for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
+  One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},
+  but this raw theorem only shows that two particular elements in the
+  equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a
+  more general statement stipulating that the equivalence classes are not
+  equal is necessary.  This kind of failure is beyond the scope where the
+  quotient package can help: the user has to provide a raw theorem that
+  can be regularized automatically, or has to provide an explicit proof
+  for the first proof step. Homeier gives more details about this issue
+  in the long version of \cite{Homeier05}.
+
+  In the following we will first define the statement of the
+  regularized theorem based on @{text "raw_thm"} and
+  @{text "quot_thm"}. Then we define the statement of the injected theorem, based
+  on @{text "reg_thm"} and @{text "quot_thm"}. We then show the three proof steps,
+  which can all be performed independently from each other.
+
+  We first define the function @{text REG}, which takes the terms of the
+  @{text "raw_thm"} and @{text "quot_thm"} as input and returns
+  @{text "reg_thm"}. The idea
+  behind this function is that it replaces quantifiers and
+  abstractions involving raw types by bounded ones, and equalities
+  involving raw types by appropriate aggregate
+  equivalence relations. It is defined by simultaneous recursion on
+  the structure of  the terms of @{text "raw_thm"} and @{text "quot_thm"} as follows:
+  %
+  \begin{center}
+  \begin{tabular}{@ {}l@ {}}
+  \multicolumn{1}{@ {}l@ {}}{abstractions:}\\%%\smallskip\\
+  @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$
+  $\begin{cases}
+  @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \end{cases}$\\%%\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{universal quantifiers:}\\
+  @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
+  $\begin{cases}
+  @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \end{cases}$\\%%\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{equality:  \hspace{3mm}%%}\smallskip\\
+  %% REL of two equal types is the equality so we do not need a separate case
+  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}}\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{applications, variables and constants:}\\
+  @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
+  \end{tabular}
+  \end{center}
+  %
+  \noindent
+  In the above definition we omitted the cases for existential quantifiers
+  and unique existential quantifiers, as they are very similar to the cases
+  for the universal quantifier.
+
+  Next we define the function @{text INJ} which takes as argument
+  @{text "reg_thm"} and @{text "quot_thm"} (both as
+  terms) and returns @{text "inj_thm"}:
+
+  \begin{center}
+  \begin{tabular}{l}
+  \multicolumn{1}{@ {}l}{abstractions:}\\
+  @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
+  \hspace{18mm}$\begin{cases}
+  @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
+  \end{cases}$\smallskip\\
+  @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\
+  \hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+  @{text "INJ (\<forall> t, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s)"}\\
+  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+  \multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
+  @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} $\dn$ @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
+  $\begin{cases}
+  @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
+  \end{cases}$\\
+  @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$
+  $\begin{cases}
+  @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
+  \end{cases}$\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  In this definition we again omitted the cases for existential and unique existential
+  quantifiers.
+
+%%% FIXME: Reviewer2 citing following sentence: You mention earlier
+%%% that this implication may fail to be true. Does that meant that
+%%% the `first proof step' is a heuristic that proves the implication
+%%% raw_thm \implies reg_thm in some instances, but fails in others?
+%%% You should clarify under which circumstances the implication is
+%%% being proved here.
+%%% Cezary: It would be nice to cite Homeiers discussions in the
+%%% Quotient Package manual from HOL (the longer paper), do you agree?
+
+  In the first phase, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always
+  start with an implication. Isabelle provides \emph{mono} rules that can split up
+  the implications into simpler implicational subgoals. This succeeds for every
+  monotone connective, except in places where the function @{text REG} replaced,
+  for instance, a quantifier by a bounded quantifier. To decompose them, we have
+  to prove that the relations involved are aggregate equivalence relations.
+
+
+  %In this case we have
+  %rules of the form
+  %
+  % \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
+  %bounded quantifier anywhere if R is an equivalence relation or
+  %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
+
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %@{text "\<forall>x \<in> Resp 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}
+
+%%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we
+%%% should include a proof sketch?
+
+  %\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
+  %injection procedure would be used to prove such goals and
+  %the assumption about the equivalence relation would be used. We use the above theorem directly,
+  %because this allows us to completely separate the first and the second
+  %proof step into two independent ``units''.
+
+  The second phase, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality
+  between the terms of the regularized theorem and the injected theorem.
+  The proof again follows the structure of the
+  two underlying terms taking respectfulness theorems into account.
+
+  %\begin{itemize}
+  %\item For two constants an appropriate respectfulness theorem is applied.
+  %\item For two variables, we use the assumptions proved in the regularization step.
+  %\item For two abstractions, we @{text "\<eta>"}-expand and @{text "\<beta>"}-reduce them.
+  %\item For two applications, we check that the right-hand side is an application of
+  %  @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} holds. If yes then we
+  %  can apply the theorem:
+
+  %\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:
+
+  %\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
+  establishing in the third phase the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+  achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
+  definitions. This step also requires that the definitions of all lifted constants
+  are used to fold the @{term Rep} with the raw constants. We will give more details
+  about our lifting procedure in a longer version of this paper.
+
+  %Next for
+  %all abstractions and quantifiers the lambda and
+  %quantifier preservation theorems are used to replace the
+  %variables that include raw types with respects by quantifiers
+  %over variables that include quotient types. We show here only
+  %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:
+
+  %\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}:
+
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %@{thm (concl) Quotient_rel_rep[no_vars]}
+  %\end{isabelle}
+
+
+  %Finally, we rewrite with the preservation theorems. This will result
+  %in two equal terms that can be solved by reflexivity.
+*}
+
+section {* Conclusion and Related Work\label{sec:conc}*}
+
+text {*
+
+  \noindent
+  The code of the quotient package and the examples described here are already
+  included in the standard distribution of Isabelle.
+  \footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.}
+  The package is
+  heavily used in the new version of Nominal Isabelle, which provides a
+  convenient reasoning infrastructure for programming language calculi
+  involving general binders.  To achieve this, it builds types representing
+  @{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been
+  used successfully in formalisations of an equivalence checking algorithm for
+  LF \cite{UrbanCheneyBerghofer08}, Typed
+  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+  \cite{BengtsonParow09} and a strong normalisation result for cut-elimination
+  in classical logic \cite{UrbanZhu08}.
+
+
+  There is a wide range of existing literature for dealing with quotients
+  in theorem provers.  Slotosch~\cite{Slotosch97} implemented a mechanism that
+  automatically defines quotient types for Isabelle/HOL. But he did not
+  include theorem lifting.  Harrison's quotient package~\cite{harrison-thesis}
+  is the first one that is able to automatically lift theorems, however only
+  first-order theorems (that is theorems where abstractions, quantifiers and
+  variables do not involve functions that include the quotient type). There is
+  also some work on quotient types in non-HOL based systems and logical
+  frameworks, including theory interpretations in
+  PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, and
+  setoids in Coq \cite{ChicliPS02}.  Paulson showed a construction of
+  quotients that does not require the Hilbert Choice operator, but also only
+  first-order theorems can be lifted~\cite{Paulson06}.  The most related work
+  to our package is the package for HOL4 by Homeier~\cite{Homeier05}.  He
+  introduced most of the abstract notions about quotients and also deals with
+  lifting of higher-order theorems. However, he cannot deal with quotient
+  compositions (needed for lifting theorems about @{text flat}). Also, a
+  number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc
+  only exist in \cite{Homeier05} as ML-code, not included in the paper.
+  Like Homeier's, our quotient package can deal with partial equivalence
+  relations, but for lack of space we do not describe the mechanisms
+  needed for this kind of quotient constructions.
+
+%%% FIXME Reviewer 3 would like to know more about the lifting in Coq and PVS,
+%%% and some comparison. I don't think we have the space for any additions...
+
+  One feature of our quotient package is that when lifting theorems, the user
+  can precisely specify what the lifted theorem should look like. This feature
+  is necessary, for example, when lifting an induction principle for two
+  lists.  Assuming this principle has as the conclusion a predicate of the
+  form @{text "P xs ys"}, then we can precisely specify whether we want to
+  quotient @{text "xs"} or @{text "ys"}, or both. We found this feature very
+  useful in the new version of Nominal Isabelle, where such a choice is
+  required to generate a reasoning infrastructure for alpha-equated terms.
+%%
+%% give an example for this
+%%
+  \smallskip
+
+  \noindent
+  {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
+  discussions about his HOL4 quotient package and explaining to us
+  some of its finer points in the implementation. Without his patient
+  help, this work would have been impossible.
+*}
+
+text_raw {*
+  %%\bibliographystyle{abbrv}
+  \bibliography{root}
+
+  \appendix
+
+*}
+
+section {* Examples \label{sec:examples} *}
+
+text {*
+
+%%% FIXME Reviewer 1 would like an example of regularized and injected
+%%% statements. He asks for the examples twice, but I would still ignore
+%%% it due to lack of space...
+
+  \noindent
+  In this appendix we will show a sequence of declarations for defining the
+  type of integers by quotienting pairs of natural numbers, and
+  lifting one theorem.
+
+  A user of our quotient package first needs to define a relation on
+  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{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)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  Next the quotient type must be defined. This generates a proof obligation that the
+  relation is an equivalence relation, which is solved automatically using the
+  definition of equivalence and extensionality:
+
+  \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)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The user can then specify the constants on the quotient type:
+
+  \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}~~%
+  @{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"}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The following theorem about addition on the raw level can be proved.
+
+  \begin{isabelle}\ \ \ \ \ %
+  \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
+  \end{isabelle}
+
+  \noindent
+  If the user lifts this theorem, the quotient package performs all the lifting
+  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{tabular}{@ {}l}
+  \isacommand{lemma}~~@{text "[quot_respect]:"}\\
+  @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  It can be discharged automatically by Isabelle when hinting to unfold the definition
+  of @{text "\<doublearr>"}.
+  After this, the user can prove the lifted lemma as follows:
+
+  \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}\ \ \ \ \ %
+  \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
+  \end{isabelle}
+
+  \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}).
+*}
+
+
+
+(*<*)
+end
+(*>*)
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/ROOT.ML	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,5 @@
+quick_and_dirty := true;
+no_document use_thys ["Quotient", 
+                      "~~/src/HOL/Library/LaTeXsugar",
+                      "~~/src/HOL/Quotient_Examples/FSet" ];
+use_thys ["Paper"];
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/TODO
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/TODO	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,20 @@
+Things to describe not in the original quotient paper:
+
+* Type maps and Relation maps (show the case for functions)
+* Quotient extensions
+* Respectfulness and preservation
+  - Show special cases for quantifiers and lambda
+* Quotient-type locale
+  - Show the proof as much simpler than Homeier's one
+* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
+* Lifting vs Descending vs quot_lifted
+  - automatic theorem translation heuristic
+* Partial equivalence quotients
+  - Bounded abstraction
+  - Respects
+  - partial_descending
+* The heuristics for automatic regularization, injection and cleaning.
+* A complete example of a lifted theorem together with the regularized
+  injected and cleaned statement
+* Examples of quotients and properties that we used the package for.
+* co/contra-variance from Ondrej should be taken into account
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/mathpartir.sty	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,388 @@
+%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+%  Copyright (C) 2001, 2002, 2003 Didier Rémy
+%
+%  Author         : Didier Remy 
+%  Version        : 1.1.1
+%  Bug Reports    : to author
+%  Web Site       : http://pauillac.inria.fr/~remy/latex/
+% 
+%  WhizzyTeX is free software; you can redistribute it and/or modify
+%  it under the terms of the GNU General Public License as published by
+%  the Free Software Foundation; either version 2, or (at your option)
+%  any later version.
+%  
+%  Mathpartir is distributed in the hope that it will be useful,
+%  but WITHOUT ANY WARRANTY; without even the implied warranty of
+%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%  GNU General Public License for more details 
+%  (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%  File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+\newdimen \mpr@tmpdim
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing 
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineskip \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  } 
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
+  \vbox \bgroup \tabskip 0em \let \+ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \+\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \+#1\+#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\+#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+   \mpr@lista {\+}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \mpr@to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend  
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+%% Part III -- Type inference rules
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+   \def \+##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+             \else \unvbox \mpr@vlist \box \mpr@hlist
+             \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+%    \setbox \mpr@hlist
+%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+%    \setbox \mpr@vlist
+%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+%              \else \unvbox \mpr@vlist \box \mpr@hlist
+%              \fi}%
+% }
+
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be P or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+  \def \+##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{$\displaystyle {##1}$}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist 
+                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist
+                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
+           \fi
+         \else 
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist 
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by \mpr@sep
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@over #2}$}}
+\let \mpr@fraction \mpr@@fraction
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%       
+   \def \@test {#2}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+   \else 
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox 
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\RefTirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \+
+% Each \+ produces a break, attempting horizontal breaks if possible, 
+% and  vertical breaks if needed. 
+% 
+% An empty element obtained by \+\+ produces a vertical break in all cases. 
+%
+% The former rule is aligned on the fraction bar. 
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+% 
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%       
+%  width                set the width of the rule to val
+%  narrower             set the width of the rule to val\hsize
+%  before               execute val at the beginning/left
+%  lab                  put a label [Val] on top of the rule
+%  lskip                add negative skip on the right
+%  left                 put a left label [Val]
+%  Left                 put a left label [Val],  ignoring its width 
+%  right                put a right label [Val]
+%  Right                put a right label [Val], ignoring its width
+%  leftskip             skip negative space on the left-hand side
+%  rightskip            skip negative space on the right-hand side
+%  vdots                lift the rule by val and fill vertical space with dots
+%  after                execute val at the end/right
+%  
+%  Note that most options must come in this order to avoid strange
+%  typesetting (in particular  leftskip must preceed left and Left and
+%  rightskip must follow Right or right; vdots must come last 
+%  or be only followed by rightskip. 
+%  
+
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\def \mprset #1{\setkeys{mprset}{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newdimen \rule@dimen
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         $\setkeys{mpr}{#1}%
+          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$}
+  \setbox1 \hbox {\strut}
+  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
+  \raise \rule@dimen \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode 
+    \let \@do \mpr@inferstar@
+  \else 
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \tir@name #1{\hbox {\small \sc #1}}
+\let \TirName \tir@name
+\let \RefTirName \tir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/root.bib	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,203 @@
+@inproceedings{Nogin02,
+  author    = {Aleksey Nogin},
+  title     = {Quotient Types: A Modular Approach},
+  booktitle = {Proc.~of the 15th TPHOLs conference},
+  year      = {2002},
+  pages     = {263-280},
+  series    = {LNCS},
+  volume    = {2646}
+}
+
+@proceedings{DBLP:conf/tphol/2002,
+  editor    = {Victor Carre{\~n}o and
+               C{\'e}sar Mu{\~n}oz and
+               Sofi{\`e}ne Tahar},
+  title     = {Theorem Proving in Higher Order Logics, 15th International
+               Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23,
+               2002, Proceedings},
+  booktitle = {TPHOLs},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2410},
+  year      = {2002},
+  isbn      = {3-540-44039-9},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@techreport{PVS:Interpretations,
+        Author= {S. Owre and N. Shankar},
+        Title= {{T}heory {I}nterpretations in {PVS}},
+        Number= {SRI-CSL-01-01},
+        Institution= {Computer Science Laboratory, SRI International},
+        Address= {Menlo Park, CA},
+        Month= {April},
+        Year= {2001}}
+
+@inproceedings{ChicliPS02,
+  author    = {Laurent Chicli and
+               Loic Pottier and
+               Carlos Simpson},
+  title     = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
+  booktitle = {Proc of the TYPES workshop},
+  year      = {2002},
+  pages     = {95-107},
+  series    = {LNCS},
+  volume    = {2646}
+}
+
+@proceedings{DBLP:conf/types/2002,
+  editor    = {Herman Geuvers and
+               Freek Wiedijk},
+  title     = {Types for Proofs and Programs, Second International Workshop,
+               TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
+               Selected Papers},
+  booktitle = {TYPES},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2646},
+  year      = {2003},
+  isbn      = {3-540-14031-X},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@article{Paulson06,
+  author    = {Lawrence C. Paulson},
+  title     = {Defining functions on equivalence classes},
+  journal   = {ACM Trans. Comput. Log.},
+  volume    = {7},
+  number    = {4},
+  year      = {2006},
+  pages     = {658-675},
+  ee        = {http://doi.acm.org/10.1145/1183278.1183280},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{Slotosch97,
+  author    = {Oscar Slotosch},
+  title     = {Higher Order Quotients and their Implementation in Isabelle
+               HOL},
+  booktitle = {Proc.~of the 10th TPHOLs conference},
+  year      = {1997},
+  pages     = {291-306},
+  series    = {LNCS},
+  volume    = {1275}
+}
+
+@proceedings{DBLP:conf/tphol/1997,
+  editor    = {Elsa L. Gunter and
+               Amy P. Felty},
+  title     = {Theorem Proving in Higher Order Logics, 10th International
+               Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22,
+               1997, Proceedings},
+  booktitle = {TPHOLs},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1275},
+  year      = {1997},
+  isbn      = {3-540-63379-0},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{Homeier05,
+  author    = {Peter V. Homeier},
+  title     = {A Design Structure for Higher Order Quotients},
+  booktitle = {Proc of the 18th TPHOLs conference},
+  year      = {2005},
+  pages     = {130-146},
+  series    = {LNCS},
+  volume    = {3603}
+}
+
+@proceedings{DBLP:conf/tphol/2005,
+  editor    = {Joe Hurd and
+               Thomas F. Melham},
+  title     = {Theorem Proving in Higher Order Logics, 18th International
+               Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005,
+               Proceedings},
+  booktitle = {TPHOLs},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {3603},
+  year      = {2005},
+  isbn      = {3-540-28372-2},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@BOOK{harrison-thesis,
+        author          = "John Harrison",
+        title           = "Theorem Proving with the Real Numbers",
+        publisher       = "Springer-Verlag",
+        year            = 1998}
+
+@BOOK{Barendregt81,
+  AUTHOR = 	 "H.~Barendregt",
+  TITLE = 	 "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics",
+  PUBLISHER = 	 "North-Holland",
+  YEAR = 	 1981,
+  VOLUME = 	 103,
+  SERIES = 	 "Studies in Logic and the Foundations of Mathematics"
+}
+
+@BOOK{CurryFeys58,
+  AUTHOR = 	 "H.~B.~Curry and R.~Feys",
+  TITLE = 	 "{C}ombinatory {L}ogic",
+  PUBLISHER =    "North-Holland",
+  YEAR = 	 "1958",
+  VOLUME =       1,
+  SERIES =       "Studies in Logic and the Foundations of Mathematics"
+}
+
+@Unpublished{UrbanKaliszyk11,
+  author = 	 {C.~Urban and C.~Kaliszyk},
+  title = 	 {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
+  note = 	 {submitted for publication},
+  month =	 {July},
+  year =	 {2010},
+}
+
+@InProceedings{BengtsonParrow07,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
+  booktitle = {Proc.~of the 10th FOSSACS Conference},
+  year      = 2007,
+  pages     = {63--77},
+  series    = {LNCS},
+  volume    = {4423}
+}
+
+@inproceedings{BengtsonParow09,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {{P}si-{C}alculi in {I}sabelle},
+  booktitle = {Proc of the 22nd TPHOLs Conference},
+  year      = 2009,
+  pages     = {99--114},
+  series    = {LNCS},
+  volume    = {5674}
+}
+
+@inproceedings{TobinHochstadtFelleisen08,
+  author    = {S.~Tobin-Hochstadt and M.~Felleisen},
+  booktitle = {Proc.~of the 35rd POPL Symposium},
+  title     = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
+  publisher = {ACM},
+  year      = {2008},
+  pages     = {395--406}
+}
+
+@InProceedings{UrbanCheneyBerghofer08,
+  author = "C.~Urban and J.~Cheney and S.~Berghofer",
+  title = "{M}echanizing the {M}etatheory of {LF}",
+  pages = "45--56",
+  year = 2008,
+  booktitle = "Proc.~of the 23rd LICS Symposium"
+}
+
+@InProceedings{UrbanZhu08,
+  title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
+  author = "C.~Urban and B.~Zhu",
+  booktitle = "Proc.~of the 9th RTA Conference",
+  year = "2008",
+  pages = "409--424",
+  series = "LNCS",
+  volume = 5117
+}
\ No newline at end of file
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/root.tex	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,76 @@
+\documentclass{svjour3}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{pdfsetup}
+\usepackage{tikz}
+%\usepackage{pgf}
+\usepackage{stmaryrd}
+\usepackage{verbdef}
+%\usepackage{longtable}
+\usepackage{mathpartir}
+%\newtheorem{definition}{Definition}
+%\newtheorem{proposition}{Proposition}
+%\newtheorem{lemma}{Lemma}
+
+\urlstyle{rm}
+\isabellestyle{rm}
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastyle}{\normalsize\rm}%
+\renewcommand{\isastylescript}{\it}
+\def\dn{\,\triangleq\,}
+\verbdef\singlearr|---->|
+\verbdef\doublearr|===>|
+\verbdef\tripple|###|
+
+\renewcommand{\isasymequiv}{$\triangleq$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymUnion}{$\bigcup$}
+
+\newcommand{\isasymsinglearr}{$\mapsto$}
+\newcommand{\isasymdoublearr}{$\Mapsto$}
+\newcommand{\isasymtripple}{\tripple}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+
+\begin{document}
+
+\title{Quotients Revisited for Isabelle/HOL}
+\author{Cezary Kaliszyk \and Christian Urban}
+\institute{C.~Kaliszyk \at University of Tsukuba, Japan
+     \and C.~Urban \at Technical University of Munich, Germany}
+\date{Received: date / Accepted: date}
+
+\maketitle
+
+\begin{abstract}
+Higher-Order Logic (HOL) is based on a small logic kernel, whose only
+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 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 also specified 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 reasoning infrastructure
+for quotient constructions.
+\end{abstract}
+
+%\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}
+
+\bibliographystyle{abbrv}
+\input{session}
+
+
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/document/svglov3.clo
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/svglov3.clo	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,113 @@
+% SVJour3 DOCUMENT CLASS OPTION SVGLOV3 -- for standardised journals
+%
+% This is an enhancement for the LaTeX
+% SVJour3 document class for Springer journals
+%
+%%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+\ProvidesFile{svglov3.clo}
+              [2009/12/18 v3.2
+      style option for standardised journals]
+\typeout{SVJour Class option: svglov3.clo for standardised journals}
+\def\validfor{svjour3}
+\global\let\if@runhead\iftrue
+\ExecuteOptions{final,10pt}
+% No size changing allowed, hence a "copy" of size10.clo is included
+\DeclareFontShape{OT1}{cmr}{m}{n}{
+        <-6>    cmr5
+        <6-7>   cmr6
+        <7-8>   cmr7
+        <8-9>   cmr8
+        <9-10>  cmr9
+        <10-12> cmr10
+        <12-17> cmr12
+        <17->   cmr17
+      }{}
+%
+\renewcommand\normalsize{%
+\if@twocolumn
+   \@setfontsize\normalsize\@xpt{12.5pt}%
+\else
+   \if@smallext
+      \@setfontsize\normalsize\@xpt\@xiipt
+   \else
+      \@setfontsize\normalsize{9.5pt}{11.5pt}%
+   \fi
+\fi
+   \abovedisplayskip=3 mm plus6pt minus 4pt
+   \belowdisplayskip=3 mm plus6pt minus 4pt
+   \abovedisplayshortskip=0.0 mm plus6pt
+   \belowdisplayshortskip=2 mm plus4pt minus 4pt
+   \let\@listi\@listI}
+\normalsize
+\newcommand\small{%
+\if@twocolumn
+   \@setfontsize\small{8.5pt}\@xpt
+\else
+   \if@smallext
+      \@setfontsize\small\@viiipt{9.5pt}%
+   \else
+      \@setfontsize\small\@viiipt{9.25pt}%
+   \fi
+\fi
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 4\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+\let\footnotesize\small
+\newcommand\scriptsize{\@setfontsize\scriptsize\@viipt\@viiipt}
+\newcommand\tiny{\@setfontsize\tiny\@vpt\@vipt}
+\if@twocolumn
+   \newcommand\large{\@setfontsize\large\@xiipt\@xivpt}
+   \newcommand\LARGE{\@setfontsize\LARGE{16pt}{18pt}}
+\else
+   \newcommand\large{\@setfontsize\large\@xipt\@xiipt}
+   \newcommand\LARGE{\@setfontsize\LARGE{13pt}{15pt}}
+\fi
+\newcommand\Large{\@setfontsize\Large\@xivpt{16dd}}
+\newcommand\huge{\@setfontsize\huge\@xxpt{25}}
+\newcommand\Huge{\@setfontsize\Huge\@xxvpt{30}}
+%
+\def\runheadhook{\rlap{\smash{\lower6.5pt\hbox to\textwidth{\hrulefill}}}}
+\if@twocolumn
+\setlength{\textwidth}{17.4cm}
+\setlength{\textheight}{234mm}
+\AtEndOfClass{\setlength\columnsep{6mm}}
+\else
+   \if@smallext
+      \setlength{\textwidth}{11.9cm}
+      \setlength{\textheight}{19.4cm}
+   \else
+      \setlength{\textwidth}{12.2cm}
+      \setlength{\textheight}{19.8cm}
+   \fi
+\fi
+%
+\AtBeginDocument{%
+\@ifundefined{@journalname}
+ {\typeout{Unknown journal: specify \string\journalname\string{%
+<name of your journal>\string} in preambel^^J}}{}}
+%
+\endinput
+%%
+%% End of file `svglov3.clo'.
diff -r 660a4f5adee8 -r a6b0220fb8ae Quotient-Paper-jv/document/svjour3.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper-jv/document/svjour3.cls	Tue Dec 20 17:54:53 2011 +0900
@@ -0,0 +1,1431 @@
+% SVJour3 DOCUMENT CLASS -- version 3.2 for LaTeX2e
+%
+% LaTeX document class for Springer journals
+%
+%%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{svjour3}[2007/05/08 v3.2
+^^JLaTeX document class for Springer journals]
+\newcommand\@ptsize{}
+\newif\if@restonecol
+\newif\if@titlepage
+\@titlepagefalse
+\DeclareOption{a4paper}
+   {\setlength\paperheight {297mm}%
+    \setlength\paperwidth  {210mm}}
+\DeclareOption{10pt}{\renewcommand\@ptsize{0}}
+\DeclareOption{twoside}{\@twosidetrue  \@mparswitchtrue}
+\DeclareOption{draft}{\setlength\overfullrule{5pt}}
+\DeclareOption{final}{\setlength\overfullrule{0pt}}
+\DeclareOption{fleqn}{\input{fleqn.clo}\AtBeginDocument{\mathindent\z@}%
+\AtBeginDocument{\@ifpackageloaded{amsmath}{\@mathmargin\z@}{}}%
+\PassOptionsToPackage{fleqn}{amsmath}}
+%%%
+\DeclareOption{onecolumn}{}
+\DeclareOption{smallcondensed}{}
+\DeclareOption{twocolumn}{\@twocolumntrue\ExecuteOptions{fleqn}}
+\newif\if@smallext\@smallextfalse
+\DeclareOption{smallextended}{\@smallexttrue}
+\let\if@mathematic\iftrue
+\let\if@numbook\iffalse
+\DeclareOption{numbook}{\let\if@envcntsect\iftrue
+  \AtEndOfPackage{%
+   \renewcommand\thefigure{\thesection.\@arabic\c@figure}%
+   \renewcommand\thetable{\thesection.\@arabic\c@table}%
+   \renewcommand\theequation{\thesection.\@arabic\c@equation}%
+   \@addtoreset{figure}{section}%
+   \@addtoreset{table}{section}%
+   \@addtoreset{equation}{section}%
+  }%
+}
+\DeclareOption{openbib}{%
+  \AtEndOfPackage{%
+   \renewcommand\@openbib@code{%
+      \advance\leftmargin\bibindent
+      \itemindent -\bibindent
+      \listparindent \itemindent
+      \parsep \z@
+      }%
+   \renewcommand\newblock{\par}}%
+}
+\DeclareOption{natbib}{%
+\AtEndOfClass{\RequirePackage{natbib}%
+% Changing some parameters of NATBIB
+\setlength{\bibhang}{\parindent}%
+%\setlength{\bibsep}{0mm}%
+\let\bibfont=\small
+\def\@biblabel#1{#1.}%
+\newcommand{\etal}{et al.}%
+\bibpunct{(}{)}{;}{a}{}{,}}}
+%
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+\let\if@smartrunh\iffalse
+\DeclareOption{smartrunhead}{\let\if@smartrunh\iftrue}
+\DeclareOption{nosmartrunhead}{\let\if@smartrunh\iffalse}
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@referee\iffalse
+\DeclareOption{referee}{\let\if@referee\iftrue}
+\def\makereferee{\def\baselinestretch{2}}
+\let\if@instindent\iffalse
+\DeclareOption{instindent}{\let\if@instindent\iftrue}
+\let\if@smartand\iffalse
+\DeclareOption{smartand}{\let\if@smartand\iftrue}
+\let\if@spthms\iftrue
+\DeclareOption{nospthms}{\let\if@spthms\iffalse}
+%
+% language and babel dependencies
+\DeclareOption{deutsch}{\def\switcht@@therlang{\switcht@deutsch}%
+\gdef\svlanginfo{\typeout{Man spricht deutsch.}\global\let\svlanginfo\relax}}
+\DeclareOption{francais}{\def\switcht@@therlang{\switcht@francais}%
+\gdef\svlanginfo{\typeout{On parle francais.}\global\let\svlanginfo\relax}}
+\let\switcht@@therlang\relax
+\let\svlanginfo\relax
+%
+\AtBeginDocument{\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasUKenglish}{}{\addto\extrasUKenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+%
+\def\ClassInfoNoLine#1#2{%
+   \ClassInfo{#1}{#2\@gobble}%
+}
+\let\journalopt\@empty
+\DeclareOption*{%
+\InputIfFileExists{sv\CurrentOption.clo}{%
+\global\let\journalopt\CurrentOption}{%
+\ClassWarning{Springer-SVJour3}{Specified option or subpackage
+"\CurrentOption" not found -}\OptionNotUsed}}
+\ExecuteOptions{a4paper,twoside,10pt,instindent}
+\ProcessOptions
+%
+\ifx\journalopt\@empty\relax
+\ClassInfoNoLine{Springer-SVJour3}{extra/valid Springer sub-package (-> *.clo)
+\MessageBreak not found in option list of \string\documentclass
+\MessageBreak  - autoactivating "global" style}{}
+\input{svglov3.clo}
+\else
+\@ifundefined{validfor}{%
+\ClassError{Springer-SVJour3}{Possible option clash for sub-package
+\MessageBreak "sv\journalopt.clo" - option file not valid
+\MessageBreak for this class}{Perhaps you used an option of the old
+Springer class SVJour!}
+}{}
+\fi
+%
+\if@smartrunh\AtEndDocument{\islastpageeven\getlastpagenumber}\fi
+%
+\newcommand{\twocoltest}[2]{\if@twocolumn\def\@gtempa{#2}\else\def\@gtempa{#1}\fi
+\@gtempa\makeatother}
+\newcommand{\columncase}{\makeatletter\twocoltest}
+%
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+%
+\setlength\parindent{15\p@}
+\setlength\smallskipamount{3\p@ \@plus 1\p@ \@minus 1\p@}
+\setlength\medskipamount{6\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\bigskipamount{12\p@ \@plus 4\p@ \@minus 4\p@}
+\setlength\headheight{12\p@}
+\setlength\headsep   {14.50dd}
+\setlength\topskip   {10\p@}
+\setlength\footskip{30\p@}
+\setlength\maxdepth{.5\topskip}
+%
+\@settopoint\textwidth
+\setlength\marginparsep {10\p@}
+\setlength\marginparpush{5\p@}
+\setlength\topmargin{-10pt}
+\if@twocolumn
+   \setlength\oddsidemargin {-30\p@}
+   \setlength\evensidemargin{-30\p@}
+\else
+   \setlength\oddsidemargin {\z@}
+   \setlength\evensidemargin{\z@}
+\fi
+\setlength\marginparwidth  {48\p@}
+\setlength\footnotesep{8\p@}
+\setlength{\skip\footins}{9\p@ \@plus 4\p@ \@minus 2\p@}
+\setlength\floatsep    {12\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\textfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {20\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\dblfloatsep    {12\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\dbltextfloatsep{20\p@ \@plus 2\p@ \@minus 4\p@}
+\setlength\@fptop{0\p@}
+\setlength\@fpsep{12\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\@fpbot{0\p@ \@plus 1fil}
+\setlength\@dblfptop{0\p@}
+\setlength\@dblfpsep{12\p@ \@plus 2\p@ \@minus 2\p@}
+\setlength\@dblfpbot{0\p@ \@plus 1fil}
+\setlength\partopsep{2\p@ \@plus 1\p@ \@minus 1\p@}
+\def\@listi{\leftmargin\leftmargini
+            \parsep \z@
+            \topsep 6\p@ \@plus2\p@ \@minus4\p@
+            \itemsep\parsep}
+\let\@listI\@listi
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    \z@
+              \parsep    \topsep
+              \itemsep   \parsep}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    \z@
+              \parsep    \topsep
+              \itemsep   \parsep}
+\def\@listiv {\leftmargin\leftmarginiv
+              \labelwidth\leftmarginiv
+              \advance\labelwidth-\labelsep}
+\def\@listv  {\leftmargin\leftmarginv
+              \labelwidth\leftmarginv
+              \advance\labelwidth-\labelsep}
+\def\@listvi {\leftmargin\leftmarginvi
+              \labelwidth\leftmarginvi
+              \advance\labelwidth-\labelsep}
+%
+\setlength\lineskip{1\p@}
+\setlength\normallineskip{1\p@}
+\renewcommand\baselinestretch{}
+\setlength\parskip{0\p@ \@plus \p@}
+\@lowpenalty   51
+\@medpenalty  151
+\@highpenalty 301
+\setcounter{topnumber}{4}
+\renewcommand\topfraction{.9}
+\setcounter{bottomnumber}{2}
+\renewcommand\bottomfraction{.7}
+\setcounter{totalnumber}{6}
+\renewcommand\textfraction{.1}
+\renewcommand\floatpagefraction{.85}
+\setcounter{dbltopnumber}{3}
+\renewcommand\dbltopfraction{.85}
+\renewcommand\dblfloatpagefraction{.85}
+\def\ps@headings{%
+    \let\@oddfoot\@empty\let\@evenfoot\@empty
+    \def\@evenhead{\small\csname runheadhook\endcsname
+    \rlap{\thepage}\hfil\leftmark\unskip}%
+    \def\@oddhead{\small\csname runheadhook\endcsname
+    \ignorespaces\rightmark\hfil\llap{\thepage}}%
+    \let\@mkboth\@gobbletwo
+    \let\sectionmark\@gobble
+    \let\subsectionmark\@gobble
+    }
+% make indentations changeable
+\def\setitemindent#1{\settowidth{\labelwidth}{#1}%
+        \leftmargini\labelwidth
+        \advance\leftmargini\labelsep
+   \def\@listi{\leftmargin\leftmargini
+        \labelwidth\leftmargini\advance\labelwidth by -\labelsep
+        \parsep=\parskip
+        \topsep=\medskipamount
+        \itemsep=\parskip \advance\itemsep by -\parsep}}
+\def\setitemitemindent#1{\settowidth{\labelwidth}{#1}%
+        \leftmarginii\labelwidth
+        \advance\leftmarginii\labelsep
+\def\@listii{\leftmargin\leftmarginii
+        \labelwidth\leftmarginii\advance\labelwidth by -\labelsep
+        \parsep=\parskip
+        \topsep=\z@
+        \itemsep=\parskip \advance\itemsep by -\parsep}}
+% labels of description
+\def\descriptionlabel#1{\hspace\labelsep #1\hfil}
+% adjusted environment "description"
+% if an optional parameter (at the first two levels of lists)
+% is present, its width is considered to be the widest mark
+% throughout the current list.
+\def\description{\@ifnextchar[{\@describe}{\list{}{\labelwidth\z@
+          \itemindent-\leftmargin \let\makelabel\descriptionlabel}}}
+\let\enddescription\endlist
+%
+\def\describelabel#1{#1\hfil}
+\def\@describe[#1]{\relax\ifnum\@listdepth=0
+\setitemindent{#1}\else\ifnum\@listdepth=1
+\setitemitemindent{#1}\fi\fi
+\list{--}{\let\makelabel\describelabel}}
+%
+\newdimen\logodepth
+\logodepth=1.2cm
+\newdimen\headerboxheight
+\headerboxheight=163pt % 18 10.5dd-lines - 2\baselineskip
+\if@twocolumn\else\advance\headerboxheight by-14.5mm\fi
+\newdimen\betweenumberspace          % dimension for space between
+\betweenumberspace=3.33pt            % number and text of titles.
+\newdimen\aftertext                  % dimension for space after
+\aftertext=5pt                       % text of title.
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+\if@mathematic
+   \def\runinend{} % \enspace}
+   \def\floatcounterend{\enspace}
+   \def\sectcounterend{}
+\else
+   \def\runinend{.}
+   \def\floatcounterend{.\ }
+   \def\sectcounterend{.}
+\fi
+\def\email#1{\emailname: #1}
+\def\keywords#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
+\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
+}\noindent\keywordname\enspace\ignorespaces#1\par}}
+%
+\def\subclassname{{\bfseries Mathematics Subject Classification
+(2000)}\enspace}
+\def\subclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
+\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
+}\noindent\subclassname\ignorespaces#1\par}}
+%
+\def\PACSname{\textbf{PACS}\enspace}
+\def\PACS#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
+\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
+}\noindent\PACSname\ignorespaces#1\par}}
+%
+\def\CRclassname{{\bfseries CR Subject Classification}\enspace}
+\def\CRclass#1{\par\addvspace\medskipamount{\rightskip=0pt plus1cm
+\def\and{\ifhmode\unskip\nobreak\fi\ $\cdot$
+}\noindent\CRclassname\ignorespaces#1\par}}
+%
+\def\ESMname{\textbf{Electronic Supplementary Material}\enspace}
+\def\ESM#1{\par\addvspace\medskipamount
+\noindent\ESMname\ignorespaces#1\par}
+%
+\newcounter{inst}
+\newcounter{auth}
+\def\authdepth{2}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newbox\titrun
+\newtoks\titlerunning
+\def\authorfont{\bfseries}
+
+\def\combirunning#1{\gdef\@combi{#1}}
+\def\@combi{}
+\newbox\combirun
+%
+\def\ps@last{\def\@evenhead{\small\rlap{\thepage}\hfil
+\lastevenhead}}
+\newcounter{lastpage}
+\def\islastpageeven{\@ifundefined{lastpagenumber}
+{\setcounter{lastpage}{0}}{\setcounter{lastpage}{\lastpagenumber}}
+\ifnum\value{lastpage}>0
+   \ifodd\value{lastpage}%
+   \else
+      \if@smartrunh
+         \thispagestyle{last}%
+      \fi
+   \fi
+\fi}
+\def\getlastpagenumber{\clearpage
+\addtocounter{page}{-1}%
+   \immediate\write\@auxout{\string\gdef\string\lastpagenumber{\thepage}}%
+   \immediate\write\@auxout{\string\newlabel{LastPage}{{}{\thepage}}}%
+   \addtocounter{page}{1}}
+
+\def\journalname#1{\gdef\@journalname{#1}}
+
+\def\dedication#1{\gdef\@dedic{#1}}
+\def\@dedic{}
+
+\let\@date\undefined
+\def\notused{~}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\offprints#1{\begingroup
+\def\protect{\noexpand\protect\noexpand}\xdef\@thanks{\@thanks
+\protect\footnotetext[0]{\unskip\hskip-15pt{\itshape Send offprint requests
+to\/}: \ignorespaces#1}}\endgroup\ignorespaces}
+
+%\def\mail#1{\gdef\@mail{#1}}
+%\def\@mail{}
+
+\def\@thanks{}
+
+\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
+   \or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi\relax}
+%
+%\def\invthanks#1{\footnotetext[0]{\kern-\bibindent#1}}
+%
+\def\nothanksmarks{\def\thanks##1{\protected@xdef\@thanks{\@thanks
+        \protect\footnotetext[0]{\kern-\bibindent##1}}}}
+%
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\def\@subtitle{}
+
+\def\headnote#1{\gdef\@headnote{#1}}
+\def\@headnote{}
+
+\def\papertype#1{\gdef\paper@type{\MakeUppercase{#1}}}
+\def\paper@type{}
+
+\def\ch@ckobl#1#2{\@ifundefined{@#1}
+ {\typeout{SVJour3 warning: Missing
+\expandafter\string\csname#1\endcsname}%
+  \csname #1\endcsname{#2}}
+ {}}
+%
+\def\ProcessRunnHead{%
+    \def\\{\unskip\ \ignorespaces}%
+    \def\thanks##1{\unskip{}}%
+    \instindent=\textwidth
+    \advance\instindent by-\headlineindent
+    \if!\the\titlerunning!\else
+      \edef\@title{\the\titlerunning}%
+    \fi
+    \global\setbox\titrun=\hbox{\small\rmfamily\unboldmath\ignorespaces\@title
+                                \unskip}%
+    \ifdim\wd\titrun>\instindent
+       \typeout{^^JSVJour3 Warning: Title too long for running head.}%
+       \typeout{Please supply a shorter form with \string\titlerunning
+                \space prior to \string\maketitle}%
+       \global\setbox\titrun=\hbox{\small\rmfamily
+       Title Suppressed Due to Excessive Length}%
+    \fi
+    \xdef\@title{\copy\titrun}%
+%
+    \if!\the\authorrunning!
+    \else
+      \setcounter{auth}{1}%
+      \edef\@author{\the\authorrunning}%
+    \fi
+    \ifnum\value{inst}>\authdepth
+       \def\stripauthor##1\and##2\endauthor{%
+       \protected@xdef\@author{##1\unskip\unskip\if!##2!\else\ et al.\fi}}%
+       \expandafter\stripauthor\@author\and\endauthor
+    \else
+       \gdef\and{\unskip, \ignorespaces}%
+       {\def\and{\noexpand\protect\noexpand\and}%
+       \protected@xdef\@author{\@author}}
+    \fi
+    \global\setbox\authrun=\hbox{\small\rmfamily\unboldmath\ignorespaces
+                                 \@author\unskip}%
+    \ifdim\wd\authrun>\instindent
+    \typeout{^^JSVJour3 Warning: Author name(s) too long for running head.
+             ^^JPlease supply a shorter form with \string\authorrunning
+             \space prior to \string\maketitle}%
+    \global\setbox\authrun=\hbox{\small\rmfamily Please give a shorter version
+          with: {\tt\string\authorrunning\space and
+             \string\titlerunning\space prior to \string\maketitle}}%
+    \fi
+    \xdef\@author{\copy\authrun}%
+    \markboth{\@author}{\@title}%
+}
+%
+\let\orithanks=\thanks
+\def\thanks#1{\ClassWarning{SVJour3}{\string\thanks\space may only be
+used inside of \string\title, \string\author,\MessageBreak
+and \string\date\space prior to \string\maketitle}}
+%
+\def\maketitle{\par\let\thanks=\orithanks
+\ch@ckobl{journalname}{Noname}
+\ch@ckobl{date}{the date of receipt and acceptance should be inserted
+later}
+\ch@ckobl{title}{A title should be given}
+\ch@ckobl{author}{Name(s) and initial(s) of author(s) should be given}
+\ch@ckobl{institute}{Address(es) of author(s) should be given}
+\begingroup
+%
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \def\@makefnmark{$^{\@thefnmark}$}%
+    \renewcommand\@makefntext[1]{%
+    \noindent
+    \hb@xt@\bibindent{\hss\@makefnmark\enspace}##1\vrule height0pt
+    width0pt depth8pt}
+%
+ \def\lastand{\ifnum\value{inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip, \andname\
+              \fi}%
+ \def\and{\stepcounter{auth}\relax
+          \if@smartand
+             \ifnum\value{auth}=\value{inst}%
+                \lastand
+             \else
+                \unskip,
+             \fi
+          \else
+             \unskip,
+          \fi}%
+ \thispagestyle{empty}
+ \ifnum \col@number=\@ne
+   \@maketitle
+ \else
+   \twocolumn[\@maketitle]%
+ \fi
+%
+ \global\@topnum\z@
+ \if!\@thanks!\else
+    \@thanks
+\insert\footins{\vskip-3pt\hrule\@width\if@twocolumn\columnwidth
+\else 38mm\fi\vskip3pt}%
+ \fi
+ {\def\thanks##1{\unskip{}}%
+ \def\iand{\\[5pt]\let\and=\nand}%
+ \def\nand{\ifhmode\unskip\nobreak\fi\ $\cdot$ }%
+ \let\and=\nand
+ \def\at{\\\let\and=\iand}%
+ \footnotetext[0]{\kern-\bibindent
+ \ignorespaces\@institute}\vspace{5dd}}%
+%\if!\@mail!\else
+%   \footnotetext[0]{\kern-\bibindent\mailname\
+%   \ignorespaces\@mail}%
+%\fi
+%
+ \if@runhead
+    \ProcessRunnHead
+ \fi
+%
+ \endgroup
+ \setcounter{footnote}{0}
+ \global\let\thanks\relax
+ \global\let\maketitle\relax
+ \global\let\@maketitle\relax
+ \global\let\@thanks\@empty
+ \global\let\@author\@empty
+ \global\let\@date\@empty
+ \global\let\@title\@empty
+ \global\let\@subtitle\@empty
+ \global\let\title\relax
+ \global\let\author\relax
+ \global\let\date\relax
+ \global\let\and\relax}
+
+\def\makeheadbox{{%
+\hbox to0pt{\vbox{\baselineskip=10dd\hrule\hbox
+to\hsize{\vrule\kern3pt\vbox{\kern3pt
+\hbox{\bfseries\@journalname\ manuscript No.}
+\hbox{(will be inserted by the editor)}
+\kern3pt}\hfil\kern3pt\vrule}\hrule}%
+\hss}}}
+%
+\def\rubric{\setbox0=\hbox{\small\strut}\@tempdima=\ht0\advance
+\@tempdima\dp0\advance\@tempdima2\fboxsep\vrule\@height\@tempdima
+\@width\z@}
+\newdimen\rubricwidth
+%
+\def\@maketitle{\newpage
+\normalfont
+\vbox to0pt{\if@twocolumn\vskip-39pt\else\vskip-49pt\fi
+\nointerlineskip
+\makeheadbox\vss}\nointerlineskip
+\vbox to 0pt{\offinterlineskip\rubricwidth=\columnwidth
+%%%%\vskip-12.5pt          % -12.5pt
+\if@twocolumn\else % one column journal
+   \divide\rubricwidth by144\multiply\rubricwidth by89 % perform golden section
+   \vskip-\topskip
+\fi
+\hrule\@height0.35mm\noindent
+\advance\fboxsep by.25mm
+\global\advance\rubricwidth by0pt
+\rubric
+\vss}\vskip19.5pt    % war 9pt
+%
+\if@twocolumn\else
+ \gdef\footnoterule{%
+  \kern-3\p@
+  \hrule\@width38mm     % \columnwidth  \rubricwidth
+  \kern2.6\p@}
+\fi
+%
+ \setbox\authrun=\vbox\bgroup
+     \if@twocolumn
+        \hrule\@height10.5mm\@width0\p@
+     \else
+        \hrule\@height 2mm\@width0\p@
+     \fi
+     \pretolerance=10000
+     \rightskip=0pt plus 4cm
+    \nothanksmarks
+%   \if!\@headnote!\else
+%     \noindent
+%     {\LARGE\normalfont\itshape\ignorespaces\@headnote\par}\vskip 3.5mm
+%   \fi
+    {\LARGE\bfseries
+     \noindent\ignorespaces
+     \@title \par}\vskip 17pt\relax
+    \if!\@subtitle!\else
+      {\large\bfseries
+      \pretolerance=10000
+      \rightskip=0pt plus 3cm
+      \vskip-12pt
+%     \noindent\ignorespaces\@subtitle \par}\vskip 11.24pt\relax
+      \noindent\ignorespaces\@subtitle \par}\vskip 17pt\relax
+    \fi
+    {\authorfont
+    \setbox0=\vbox{\setcounter{auth}{1}\def\and{\stepcounter{auth} }%
+                   \hfuzz=2\textwidth\def\thanks##1{}\@author}%
+    \setcounter{footnote}{0}%
+    \global\value{inst}=\value{auth}%
+    \setcounter{auth}{1}%
+    \if@twocolumn
+       \rightskip43mm plus 4cm minus 3mm
+    \else % one column journal
+       \rightskip=\linewidth
+       \advance\rightskip by-\rubricwidth
+       \advance\rightskip by0pt plus 4cm minus 3mm
+    \fi
+%
+\def\and{\unskip\nobreak\enskip{\boldmath$\cdot$}\enskip\ignorespaces}%
+    \noindent\ignorespaces\@author\vskip7.23pt}
+%
+    \small
+    \if!\@dedic!\else
+       \par
+       \normalsize\it
+       \addvspace\baselineskip
+       \noindent\@dedic
+    \fi
+ \egroup % end of header box
+ \@tempdima=\headerboxheight
+ \advance\@tempdima by-\ht\authrun
+ \unvbox\authrun
+ \ifdim\@tempdima>0pt
+    \vrule width0pt height\@tempdima\par
+ \fi
+ \noindent{\small\@date\if@twocolumn\vskip 7.2mm\else\vskip 5.2mm\fi}
+ \global\@minipagetrue
+ \global\everypar{\global\@minipagefalse\global\everypar{}}%
+%\vskip22.47pt
+}
+%
+\if@mathematic
+   \def\vec#1{\ensuremath{\mathchoice
+                     {\mbox{\boldmath$\displaystyle\mathbf{#1}$}}
+                     {\mbox{\boldmath$\textstyle\mathbf{#1}$}}
+                     {\mbox{\boldmath$\scriptstyle\mathbf{#1}$}}
+                     {\mbox{\boldmath$\scriptscriptstyle\mathbf{#1}$}}}}
+\else
+   \def\vec#1{\ensuremath{\mathchoice
+                     {\mbox{\boldmath$\displaystyle#1$}}
+                     {\mbox{\boldmath$\textstyle#1$}}
+                     {\mbox{\boldmath$\scriptstyle#1$}}
+                     {\mbox{\boldmath$\scriptscriptstyle#1$}}}}
+\fi
+%
+\def\tens#1{\ensuremath{\mathsf{#1}}}
+%
+\setcounter{secnumdepth}{3}
+\newcounter {section}
+\newcounter {subsection}[section]
+\newcounter {subsubsection}[subsection]
+\newcounter {paragraph}[subsubsection]
+\newcounter {subparagraph}[paragraph]
+\renewcommand\thesection      {\@arabic\c@section}
+\renewcommand\thesubsection   {\thesection.\@arabic\c@subsection}
+\renewcommand\thesubsubsection{\thesubsection.\@arabic\c@subsubsection}
+\renewcommand\theparagraph    {\thesubsubsection.\@arabic\c@paragraph}
+\renewcommand\thesubparagraph {\theparagraph.\@arabic\c@subparagraph}
+%
+\def\@hangfrom#1{\setbox\@tempboxa\hbox{#1}%
+      \hangindent \z@\noindent\box\@tempboxa}
+%
+\def\@seccntformat#1{\csname the#1\endcsname\sectcounterend
+\hskip\betweenumberspace}
+%
+% \newif\if@sectrule
+% \if@twocolumn\else\let\@sectruletrue=\relax\fi
+% \if@avier\let\@sectruletrue=\relax\fi
+% \def\makesectrule{\if@sectrule\global\@sectrulefalse\null\vglue-\topskip
+% \hrule\nobreak\parskip=5pt\relax\fi}
+% %
+% \let\makesectruleori=\makesectrule
+% \def\restoresectrule{\global\let\makesectrule=\makesectruleori\global\@sectrulefalse}
+% \def\nosectrule{\let\makesectrule=\restoresectrule}
+%
+\def\@startsection#1#2#3#4#5#6{%
+  \if@noskipsec \leavevmode \fi
+  \par
+  \@tempskipa #4\relax
+  \@afterindenttrue
+  \ifdim \@tempskipa <\z@
+    \@tempskipa -\@tempskipa \@afterindentfalse
+  \fi
+  \if@nobreak
+    \everypar{}%
+  \else
+    \addpenalty\@secpenalty\addvspace\@tempskipa
+  \fi
+% \ifnum#2=1\relax\@sectruletrue\fi
+  \@ifstar
+    {\@ssect{#3}{#4}{#5}{#6}}%
+    {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}}
+%
+\def\@sect#1#2#3#4#5#6[#7]#8{%
+  \ifnum #2>\c@secnumdepth
+    \let\@svsec\@empty
+  \else
+    \refstepcounter{#1}%
+    \protected@edef\@svsec{\@seccntformat{#1}\relax}%
+  \fi
+  \@tempskipa #5\relax
+  \ifdim \@tempskipa>\z@
+    \begingroup
+      #6{% \makesectrule
+        \@hangfrom{\hskip #3\relax\@svsec}%
+          \raggedright
+          \hyphenpenalty \@M%
+          \interlinepenalty \@M #8\@@par}%
+    \endgroup
+    \csname #1mark\endcsname{#7}%
+    \addcontentsline{toc}{#1}{%
+      \ifnum #2>\c@secnumdepth \else
+        \protect\numberline{\csname the#1\endcsname\sectcounterend}%
+      \fi
+      #7}%
+  \else
+    \def\@svsechd{%
+      #6{\hskip #3\relax
+      \@svsec #8\/\hskip\aftertext}%
+      \csname #1mark\endcsname{#7}%
+      \addcontentsline{toc}{#1}{%
+        \ifnum #2>\c@secnumdepth \else
+          \protect\numberline{\csname the#1\endcsname}%
+        \fi
+        #7}}%
+  \fi
+  \@xsect{#5}}
+%
+\def\@ssect#1#2#3#4#5{%
+  \@tempskipa #3\relax
+  \ifdim \@tempskipa>\z@
+    \begingroup
+      #4{% \makesectrule
+        \@hangfrom{\hskip #1}%
+          \interlinepenalty \@M #5\@@par}%
+    \endgroup
+  \else
+    \def\@svsechd{#4{\hskip #1\relax #5}}%
+  \fi
+  \@xsect{#3}}
+
+%
+% measures and setting of sections
+%
+\def\section{\@startsection{section}{1}{\z@}%
+    {-21dd plus-8pt minus-4pt}{10.5dd}
+     {\normalsize\bfseries\boldmath}}
+\def\subsection{\@startsection{subsection}{2}{\z@}%
+    {-21dd plus-8pt minus-4pt}{10.5dd}
+     {\normalsize\upshape}}
+\def\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+    {-13dd plus-8pt minus-4pt}{10.5dd}
+     {\normalsize\itshape}}
+\def\paragraph{\@startsection{paragraph}{4}{\z@}%
+    {-13pt plus-8pt minus-4pt}{\z@}{\normalsize\itshape}}
+
+\setlength\leftmargini  {\parindent}
+\leftmargin  \leftmargini
+\setlength\leftmarginii {\parindent}
+\setlength\leftmarginiii {1.87em}
+\setlength\leftmarginiv  {1.7em}
+\setlength\leftmarginv  {.5em}
+\setlength\leftmarginvi {.5em}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+\@beginparpenalty -\@lowpenalty
+\@endparpenalty   -\@lowpenalty
+\@itempenalty     -\@lowpenalty
+\renewcommand\theenumi{\@arabic\c@enumi}
+\renewcommand\theenumii{\@alph\c@enumii}
+\renewcommand\theenumiii{\@roman\c@enumiii}
+\renewcommand\theenumiv{\@Alph\c@enumiv}
+\newcommand\labelenumi{\theenumi.}
+\newcommand\labelenumii{(\theenumii)}
+\newcommand\labelenumiii{\theenumiii.}
+\newcommand\labelenumiv{\theenumiv.}
+\renewcommand\p@enumii{\theenumi}
+\renewcommand\p@enumiii{\theenumi(\theenumii)}
+\renewcommand\p@enumiv{\p@enumiii\theenumiii}
+\newcommand\labelitemi{\normalfont\bfseries --}
+\newcommand\labelitemii{\normalfont\bfseries --}
+\newcommand\labelitemiii{$\m@th\bullet$}
+\newcommand\labelitemiv{$\m@th\cdot$}
+
+\if@spthms
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{}
+\newcommand\nocaption{\noexpand\@gobble}
+\newdimen\spthmsep \spthmsep=5pt
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\labelsep=\spthmsep\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\normalthmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont
+                 \item[\hskip\labelsep{##3##1\ ##2\@thmcounterend}]##4}
+\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4(##3)\@thmcounterend\ }##5}}
+\normalthmheadings
+
+\def\reversethmheadings{\def\@spbegintheorem##1##2##3##4{\trivlist\normalfont
+                 \item[\hskip\labelsep{##3##2\ ##1\@thmcounterend}]##4}
+\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##2\ ##1}]{##4(##3)\@thmcounterend\ }##5}}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+% initialize theorem environment
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % all environments like "Theorem" - using its counter
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % all environments with their own counter
+   \if@envcntsect % show section counter
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % not numbered with section
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \let\spn@wtheorem=\@spynthm
+      \fi
+   \fi
+\fi
+%
+\let\spdefaulttheorem=\spn@wtheorem
+%
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\rmfamily}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\bfseries}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\bfseries}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\bfseries}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+%
+\newenvironment{theopargself}
+    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+         \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+         \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}}{}
+\newenvironment{theopargself*}
+    {\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+         \item[\hskip\labelsep{##4##1\ ##2}]{\hspace*{-\labelsep}##4##3\@thmcounterend}##5}
+     \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+         \item[\hskip\labelsep{##3##1}]{\hspace*{-\labelsep}##3##2\@thmcounterend}}}{}
+%
+\fi
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\else\unskip\quad\fi\squareforqed}
+\def\smartqed{\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}}
+
+% Define `abstract' environment
+\def\abstract{\topsep=0pt\partopsep=0pt\parsep=0pt\itemsep=0pt\relax
+\trivlist\item[\hskip\labelsep
+{\bfseries\abstractname}]\if!\abstractname!\hskip-\labelsep\fi}
+\if@twocolumn
+% \if@avier
+%   \def\endabstract{\endtrivlist\addvspace{5mm}\strich}
+%   \def\strich{\hrule\vskip1ptplus12pt}
+% \else
+    \def\endabstract{\endtrivlist\addvspace{3mm}}
+% \fi
+\else
+\fi
+%
+\newenvironment{verse}
+               {\let\\\@centercr
+                \list{}{\itemsep      \z@
+                        \itemindent   -1.5em%
+                        \listparindent\itemindent
+                        \rightmargin  \leftmargin
+                        \advance\leftmargin 1.5em}%
+                \item\relax}
+               {\endlist}
+\newenvironment{quotation}
+               {\list{}{\listparindent 1.5em%
+                        \itemindent    \listparindent
+                        \rightmargin   \leftmargin
+                        \parsep        \z@ \@plus\p@}%
+                \item\relax}
+               {\endlist}
+\newenvironment{quote}
+               {\list{}{\rightmargin\leftmargin}%
+                \item\relax}
+               {\endlist}
+\newcommand\appendix{\par\small
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \renewcommand\thesection{\@Alph\c@section}}
+\setlength\arraycolsep{1.5\p@}
+\setlength\tabcolsep{6\p@}
+\setlength\arrayrulewidth{.4\p@}
+\setlength\doublerulesep{2\p@}
+\setlength\tabbingsep{\labelsep}
+\skip\@mpfootins = \skip\footins
+\setlength\fboxsep{3\p@}
+\setlength\fboxrule{.4\p@}
+\renewcommand\theequation{\@arabic\c@equation}
+\newcounter{figure}
+\renewcommand\thefigure{\@arabic\c@figure}
+\def\fps@figure{tbp}
+\def\ftype@figure{1}
+\def\ext@figure{lof}
+\def\fnum@figure{\figurename~\thefigure}
+\newenvironment{figure}
+               {\@float{figure}}
+               {\end@float}
+\newenvironment{figure*}
+               {\@dblfloat{figure}}
+               {\end@dblfloat}
+\newcounter{table}
+\renewcommand\thetable{\@arabic\c@table}
+\def\fps@table{tbp}
+\def\ftype@table{2}
+\def\ext@table{lot}
+\def\fnum@table{\tablename~\thetable}
+\newenvironment{table}
+               {\@float{table}}
+               {\end@float}
+\newenvironment{table*}
+               {\@dblfloat{table}}
+               {\end@dblfloat}
+%
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+%
+\newcommand{\tableheadseprule}{\noalign{\hrule height.375mm}}
+%
+\newlength\abovecaptionskip
+\newlength\belowcaptionskip
+\setlength\abovecaptionskip{10\p@}
+\setlength\belowcaptionskip{0\p@}
+\newcommand\leftlegendglue{}
+
+\def\fig@type{figure}
+
+\newdimen\figcapgap\figcapgap=3pt
+\newdimen\tabcapgap\tabcapgap=5.5pt
+
+\@ifundefined{floatlegendstyle}{\def\floatlegendstyle{\bfseries}}{}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+\def\capstrut{\vrule\@width\z@\@height\topskip}
+
+\@ifundefined{captionstyle}{\def\captionstyle{\normalfont\small}}{}
+
+\long\def\@makecaption#1#2{%
+ \captionstyle
+ \ifx\@captype\fig@type
+   \vskip\figcapgap
+ \fi
+ \setbox\@tempboxa\hbox{{\floatlegendstyle #1\floatcounterend}%
+ \capstrut #2}%
+ \ifdim \wd\@tempboxa >\hsize
+   {\floatlegendstyle #1\floatcounterend}\capstrut #2\par
+ \else
+   \hbox to\hsize{\leftlegendglue\unhbox\@tempboxa\hfil}%
+ \fi
+ \ifx\@captype\fig@type\else
+   \vskip\tabcapgap
+ \fi}
+
+\newdimen\figgap\figgap=1cc
+\long\def\@makesidecaption#1#2{%
+   \parbox[b]{\@tempdimb}{\captionstyle{\floatlegendstyle
+                                         #1\floatcounterend}#2}}
+\def\sidecaption#1\caption{%
+\setbox\@tempboxa=\hbox{#1\unskip}%
+\if@twocolumn
+ \ifdim\hsize<\textwidth\else
+   \ifdim\wd\@tempboxa<\columnwidth
+      \typeout{Double column float fits into single column -
+            ^^Jyou'd better switch the environment. }%
+   \fi
+ \fi
+\fi
+\@tempdimb=\hsize
+\advance\@tempdimb by-\figgap
+\advance\@tempdimb by-\wd\@tempboxa
+\ifdim\@tempdimb<3cm
+    \typeout{\string\sidecaption: No sufficient room for the legend;
+             using normal \string\caption. }%
+   \unhbox\@tempboxa
+   \let\@capcommand=\@caption
+\else
+   \let\@capcommand=\@sidecaption
+   \leavevmode
+   \unhbox\@tempboxa
+   \hfill
+\fi
+\refstepcounter\@captype
+\@dblarg{\@capcommand\@captype}}
+
+\long\def\@sidecaption#1[#2]#3{\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makesidecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% Define `acknowledgement' environment
+\def\acknowledgement{\par\addvspace{17pt}\small\rmfamily
+\trivlist\if!\ackname!\item[]\else
+\item[\hskip\labelsep
+{\bfseries\ackname}]\fi}
+\def\endacknowledgement{\endtrivlist\addvspace{6pt}}
+\newenvironment{acknowledgements}{\begin{acknowledgement}}
+{\end{acknowledgement}}
+% Define `noteadd' environment
+\def\noteadd{\par\addvspace{17pt}\small\rmfamily
+\trivlist\item[\hskip\labelsep
+{\itshape\noteaddname}]}
+\def\endnoteadd{\endtrivlist\addvspace{6pt}}
+
+\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
+\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
+\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
+\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
+\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
+\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
+\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}
+\DeclareRobustCommand*\cal{\@fontswitch\relax\mathcal}
+\DeclareRobustCommand*\mit{\@fontswitch\relax\mathnormal}
+\newcommand\@pnumwidth{1.55em}
+\newcommand\@tocrmarg{2.55em}
+\newcommand\@dotsep{4.5}
+\setcounter{tocdepth}{1}
+\newcommand\tableofcontents{%
+    \section*{\contentsname}%
+    \@starttoc{toc}%
+    \addtocontents{toc}{\begingroup\protect\small}%
+    \AtEndDocument{\addtocontents{toc}{\endgroup}}%
+    }
+\newcommand*\l@part[2]{%
+  \ifnum \c@tocdepth >-2\relax
+    \addpenalty\@secpenalty
+    \addvspace{2.25em \@plus\p@}%
+    \begingroup
+      \setlength\@tempdima{3em}%
+      \parindent \z@ \rightskip \@pnumwidth
+      \parfillskip -\@pnumwidth
+      {\leavevmode
+       \large \bfseries #1\hfil \hb@xt@\@pnumwidth{\hss #2}}\par
+       \nobreak
+       \if@compatibility
+         \global\@nobreaktrue
+         \everypar{\global\@nobreakfalse\everypar{}}%
+      \fi
+    \endgroup
+  \fi}
+\newcommand*\l@section{\@dottedtocline{1}{0pt}{1.5em}}
+\newcommand*\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
+\newcommand*\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
+\newcommand*\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
+\newcommand*\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
+\newcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}%
+              {\listfigurename}}%
+    \@starttoc{lof}%
+    }
+\newcommand*\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
+\newcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+\let\l@table\l@figure
+\newdimen\bibindent
+\setlength\bibindent{\parindent}
+\def\@biblabel#1{#1.}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+      {\let\protect\noexpand
+       \immediate
+       \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newenvironment{thebibliography}[1]
+     {\section*{\refname
+        \@mkboth{\refname}{\refname}}\small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \@openbib@code
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+%
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,\hskip0.1em\ignorespaces}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+            \@citea\def\@citea{,\hskip0.1em\ignorespaces}%
+  \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+   {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else \def\@citea{--}\fi
+    \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+%
+\newcommand\newblock{\hskip .11em\@plus.33em\@minus.07em}
+\let\@openbib@code\@empty
+\newenvironment{theindex}
+               {\if@twocolumn
+                  \@restonecolfalse
+                \else
+                  \@restonecoltrue
+                \fi
+                \columnseprule \z@
+                \columnsep 35\p@
+                \twocolumn[\section*{\indexname}]%
+                \@mkboth{\indexname}{\indexname}%
+                \thispagestyle{plain}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\@idxitem}
+               {\if@restonecol\onecolumn\else\clearpage\fi}
+\newcommand\@idxitem{\par\hangindent 40\p@}
+\newcommand\subitem{\@idxitem \hspace*{20\p@}}
+\newcommand\subsubitem{\@idxitem \hspace*{30\p@}}
+\newcommand\indexspace{\par \vskip 10\p@ \@plus5\p@ \@minus3\p@\relax}
+
+\if@twocolumn
+ \renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width\columnwidth
+  \kern2.6\p@}
+\else
+ \renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width.382\columnwidth
+  \kern2.6\p@}
+\fi
+\newcommand\@makefntext[1]{%
+    \noindent
+    \hb@xt@\bibindent{\hss\@makefnmark\enspace}#1}
+%
+\def\trans@english{\switcht@albion}
+\def\trans@french{\switcht@francais}
+\def\trans@german{\switcht@deutsch}
+\newenvironment{translation}[1]{\if!#1!\else
+\@ifundefined{selectlanguage}{\csname trans@#1\endcsname}{\selectlanguage{#1}}%
+\fi}{}
+% languages
+% English section
+\def\switcht@albion{%\typeout{English spoken.}%
+ \def\abstractname{Abstract}%
+ \def\ackname{Acknowledgements}%
+ \def\andname{and}%
+ \def\lastandname{, and}%
+ \def\appendixname{Appendix}%
+ \def\chaptername{Chapter}%
+ \def\claimname{Claim}%
+ \def\conjecturename{Conjecture}%
+ \def\contentsname{Contents}%
+ \def\corollaryname{Corollary}%
+ \def\definitionname{Definition}%
+ \def\emailname{E-mail}%
+ \def\examplename{Example}%
+ \def\exercisename{Exercise}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bfseries Keywords}}%
+ \def\indexname{Index}%
+ \def\lemmaname{Lemma}%
+ \def\contriblistname{List of Contributors}%
+ \def\listfigurename{List of Figures}%
+ \def\listtablename{List of Tables}%
+ \def\mailname{{\itshape Correspondence to\/}:}%
+ \def\noteaddname{Note added in proof}%
+ \def\notename{Note}%
+ \def\partname{Part}%
+ \def\problemname{Problem}%
+ \def\proofname{Proof}%
+ \def\propertyname{Property}%
+ \def\questionname{Question}%
+ \def\refname{References}%
+ \def\remarkname{Remark}%
+ \def\seename{see}%
+ \def\solutionname{Solution}%
+ \def\tablename{Table}%
+ \def\theoremname{Theorem}%
+}\switcht@albion % make English default
+%
+% French section
+\def\switcht@francais{\svlanginfo
+%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e\runinend}%
+ \def\ackname{Remerciements\runinend}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}%
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\emailname{E-mail}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bfseries Mots-cl\'e\runinend}}%
+ \def\indexname{Index}%
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}%
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\itshape Correspondence to\/}:}%
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\refname{Bibliographie}%
+ \def\remarkname{Remarque}%
+ \def\seename{voyez}%
+ \def\solutionname{Solution}%
+%\def\subclassname{{\it Subject Classifications\/}:}%
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{\svlanginfo
+%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung\runinend}%
+ \def\ackname{Danksagung\runinend}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\emailname{E-Mail}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bfseries Schl\"usselw\"orter\runinend}}%
+ \def\indexname{Index}%
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}%
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\itshape Correspondence to\/}:}%
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\refname{Literatur}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}%
+ \def\solutionname{L\"osung}%
+%\def\subclassname{{\it Subject Classifications\/}:}%
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+\newcommand\today{}
+\edef\today{\ifcase\month\or
+  January\or February\or March\or April\or May\or June\or
+  July\or August\or September\or October\or November\or December\fi
+  \space\number\day, \number\year}
+\setlength\columnsep{1.5cc}
+\setlength\columnseprule{0\p@}
+%
+\frenchspacing
+\clubpenalty=10000
+\widowpenalty=10000
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+\pagestyle{headings}
+\pagenumbering{arabic}
+\if@twocolumn
+   \twocolumn
+\fi
+%\if@avier
+%   \onecolumn
+%   \setlength{\textwidth}{156mm}
+%   \setlength{\textheight}{226mm}
+%\fi
+\if@referee
+   \makereferee
+\fi
+\flushbottom
+\endinput
+%%
+%% End of file `svjour3.cls'.