
diff -r d769c24094cf -r 10148a447359 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Aug 27 19:06:30 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Fri Aug 27 23:26:00 2010 +0800
@@ -64,16 +64,17 @@
 
 text {* 
   \noindent
-  One might think they have been studied to death, but in the context of
-  theorem provers many questions concerning quotients are far from settled. In
-  this paper we address the question how a convenient reasoning infrastructure
-  for quotient constructions can be established in Isabelle/HOL, a popular
-  generic theorem prover. Higher-Order Logic (HOL) consists
+  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. It is well understood how
+  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
@@ -275,32 +276,24 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  In addition we are able to address the criticism by Paulson \cite{Paulson06} cited
-  at the beginning of this section about having to collect theorems that are
-  lifted from the raw level to the quotient level into one giant list. Homeier's and
-  also our quotient package are modular so that they allow lifting
-  theorems separately. This has the advantage for the user of being able to develop a
-  formal theory interactively as a natural progression. A pleasing side-result of
-  the modularity is that we are able to clearly specify what is involved
+  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).
-
-
-  %The paper is organised as follows: Section \ref{sec:prelims} presents briefly
-  %some necessary preliminaries; Section \ref{sec:type} describes the definitions 
-  %of quotient types and shows how definitions of constants can be made over 
-  %quotient types. Section \ref{sec:resp} introduces the notions of respectfulness
-  %and preservation; Section \ref{sec:lift} describes the lifting of theorems;
-  %Section \ref{sec:examples} presents some examples
-  %and Section \ref{sec:conc} concludes and compares our results to existing 
-  %work.
+  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. Section 6 gives an example how our quotient package
+  works in practise. 
 *}
 
 section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
 
 text {*
   \noindent
-  We give in this section a crude overview of HOL and describe the main
+  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 
@@ -428,7 +421,8 @@
   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 compositions of equivalence relations defined as follows:
+  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?
@@ -463,6 +457,7 @@
 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
@@ -474,7 +469,9 @@
   \end{isabelle}
 
   \noindent
-  and a proof that @{text "R"} is indeed an equivalence relation. Two concrete
+  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
 
   
@@ -527,7 +524,7 @@
   (for the proof see \cite{Homeier05}).
 
   \begin{proposition}
-  @{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+  \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
@@ -591,13 +588,17 @@
   \end{center}
   %
   \noindent
-  In the last two clauses we rely on the fact that the type @{text "\<alpha>s
+  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"}). The quotient construction ensures that the type variables in @{text
+  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>"}.  The
+  @{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:
   %
@@ -716,6 +717,7 @@
 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 
@@ -853,14 +855,14 @@
   In case of @{text cons} (which has type @{text "\<alpha> \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"}) we have 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "(Rep ---> map_list Rep ---> map_list Abs) cons = cons"}
+  @{text "(Rep \<singlearr> map_list Rep \<singlearr> map_list Abs) cons = cons"}
   \end{isabelle}
 
   \noindent
-  under the assumption @{text "Quotient R Abs Rep"}. Interestingly, if we have
+  under the assumption @{text "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 the corresponding preservation property.
+  then we need to show this preservation property.
 
   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
 
@@ -902,10 +904,14 @@
 %%% 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
@@ -948,7 +954,8 @@
   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.
+  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
@@ -962,28 +969,27 @@
   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 simultaneously recursing on 
-  the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
-
+  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\\
+  \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> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  @{text "\<lambda>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \end{cases}$\smallskip\\
-  \\
-  \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+  \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> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  @{text "\<forall>x\<^sup>\<sigma> \<in> Resp (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \end{cases}$\smallskip\\
-  \multicolumn{1}{@ {}l}{equality:}\smallskip\\
+  \multicolumn{1}{@ {}l@ {}}{equality:}\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 (=\<^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"}\\
@@ -1040,98 +1046,105 @@
 %%% 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 proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
+  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. In this case we have 
-  rules of the form
+  for instance, a quantifier by a bounded quantifier. To decompose them, we have 
+  to prove that the relations involved are aggregate equivalence relations.
 
-  \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}
+  
+  %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
+  %\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> Respects R. P x = \<forall>x. P x"}    
-  \end{isabelle}
+  %\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}
+  %\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}
+  %\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''.
+  %\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 proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality
+  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 and is defined for a goal being a relation between these two terms.
+  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{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}
+  %\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:
+  %  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}
+  %\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 the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
+  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. First the definitions of all lifted constants
-  are used to fold the @{term Rep} with the raw constants. 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:
+  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}
+  %\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}:
+  %\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}
+  %\begin{isabelle}\ \ \ \ \ %%%
+  %@{thm (concl) Quotient_rel_rep[no_vars]}
+  %\end{isabelle}
 
-  \noindent
-  Finally, we rewrite with the preservation theorems. This will result
-  in two equal terms that can be solved by reflexivity.
-  *}
+  
+  %Finally, we rewrite with the preservation theorems. This will result
+  %in two equal terms that can be solved by reflexivity.
+*}
 
 
 section {* Examples \label{sec:examples} *}
@@ -1142,6 +1155,7 @@
 %%% statements. He asks for the examples twice, but I would still ignore
 %%% it due to lack of space...
 
+  \noindent
   In this section we will show a sequence of declarations for defining the 
   type of integers by quotienting pairs of natural numbers, and
   lifting one theorem. 
@@ -1229,6 +1243,7 @@
 
 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




