
diff -r e7bc2ae30faf -r adb5b1349280 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 21 00:45:27 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Mon Jun 21 02:04:39 2010 +0100
@@ -10,7 +10,9 @@
 ** things to do for the next version
 *
 * - what are quot_thms?
-* - what do all preservation theorems look like
+* - what do all preservation theorems look like,
+    in particular preservation for quotient
+    compositions
 *)
 
 notation (latex output)
@@ -298,11 +300,11 @@
   "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; a primitive constant is equality, with type @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow>
-  bool"}, and the identity function with type @{text "id :: \<sigma> => \<sigma>"} is
+  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 prove
+  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.
@@ -404,17 +406,13 @@
   Second, even if we were able to state such a quotient theorem, it
   would not be true in general. However, we can prove specific instances of a
   quotient theorem for composing particular quotient relations.
-  To lift @{term flat} the quotient theorem for composing @{text "\<approx>\<^bsub>list\<^esub>"}
-  is necessary:
-% It says when lists are being quotiented to finite sets,
-% the contents of the lists can be quotiented as well
- If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"} then
+  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
 
-  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
+  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
 
   \vspace{-.5mm}
-
-
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -484,7 +482,7 @@
   (for the proof see \cite{Homeier05}).
 
   \begin{proposition}
-  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}
+  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
   \end{proposition}
 
   The next step in a quotient construction is to introduce definitions of new constants
@@ -661,7 +659,7 @@
   two restrictions in the 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 
-  notably is the bound variable function, that is the constant @{text bn}, defined 
+  notable is the bound variable function, that is the constant @{text bn}, defined 
   for raw lambda-terms as follows
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -680,7 +678,7 @@
   compositions. 
 
   To formally define what respectfulness is, we have to first define 
-  the notion of \emph{aggregate equivalence relations} using @{text REL}:
+  the notion of \emph{aggregate equivalence relations} using the function @{text REL}:
 
   \begin{center}
   \hfill
@@ -704,23 +702,11 @@
   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 throw the following proof obligation
+  we generate the following proof obligation
 
   @{text [display, indent=10] "REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
 
-  %%% PROBLEM I do not yet completely understand the 
-  %%% form of respectfulness theorems
-  %%%\noindent
-  %%%if @ {text \<sigma>} and @ {text \<tau>} have no type variables. In case they have, then
-  %%%the proof obligation is of the form
-  %%% 
-  %%%@ {text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub>  implies  REL (\<sigma>, \<tau>) c\<^isub>r c\<^isub>r"}
-
-  %%% ANSWER: The respectfulness theorems never have any quotient assumptions,
-  %%% So the commited version is ok.
-
   \noindent
-  %%%where @ {text "\<alpha>s"} are the type variables in @{text \<sigma>} and @{text \<tau>}.
   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.
@@ -730,13 +716,13 @@
   corresponding respectfulness theorem.
 
   Before lifting a theorem, we require the user to discharge
-  them. And the point with @{text bn} is that the respectfulness theorem
+  respectfulness proof obligations. And the point with @{text bn} is that the respectfulness theorem
   looks as follows
 
   @{text [display, indent=10] "(\<approx>\<^isub>\<alpha> \<doublearr> =) bn bn"}
 
   \noindent
-  and the user cannot discharge it---because it is not true. To see this,
+  and 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 extensionally to obtain
 
@@ -752,9 +738,8 @@
   To do so, we have to establish
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  if @{thm (prem1) append_rsp_unfolded[of xs ys us vs, no_vars]} and
-  @{thm (prem2) append_rsp_unfolded[of xs ys us vs, no_vars]}
-  then @{thm (concl) append_rsp_unfolded[of xs ys us vs, no_vars]} 
+  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
@@ -762,14 +747,15 @@
 
   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"} to 
-  add a pair of natural numbers to a list. The pair of natural numbers 
-  is to become an integer. But we still want to use @{text cons} for
+  type being quotient. For example, take the @{term "cons"}-constructor to 
+  add a pair of natural numbers to a list, whereby teh pair of natural numbers 
+  is to become an integer in te 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 theorem} 
+  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 theorem is as follows
+  then a preservation property is as follows
 
   @{text [display, indent=10] "Quotient R\<^bsub>\<alpha>s\<^esub> Abs\<^bsub>\<alpha>s\<^esub> Rep\<^bsub>\<alpha>s\<^esub> implies  ABS (\<sigma>, \<tau>) c\<^isub>r = c\<^isub>r"}
 
@@ -783,7 +769,7 @@
   under the assumption @{text "Quotient R Abs Rep"}. Interestingly, 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 lemma.
+  then we need to show the corresponding preservation property.
 
   %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
 
@@ -822,7 +808,7 @@
   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}.
+  \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.
 
   The purpose of regularization is to change the quantifiers and abstractions
   in a ``raw'' theorem to quantifiers over variables that respect the relation
@@ -842,30 +828,32 @@
   \end{center}
 
   \noindent
+  which means the raw theorem implies the quotient theorem.
   In contrast to other quotient packages, our package requires
   the \emph{term} of the @{text "quot_thm"} to be given by the user.\footnote{Though we
   also provide a fully automated mode, where the @{text "quot_thm"} is guessed
-  from @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
-  occurrences of a raw type. 
+  from the form of @{text "raw_thm"}.} As a result, it is possible that a user can lift only some
+  occurrences of a raw type, but not others. 
 
   The second and third proof step 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. This
   is outside of the scope where the quotient package can help. An example
-  for the failure is the simple statement for integers @{text "0 \<noteq> 1"}.
-  It does not follow by lifting from the fact that @{text "(0, 0) \<noteq> (1, 0)"}. 
-  The raw theorem only shows that particular element in the
-  equivalence classes are not equal. A more general statement saying that
-  the equivalence classes are not equal is necessary.
+  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 the raw theorem only shows that particular element in the
+  equivalence classes are not equal. A more general statement stipulating that
+  the equivalence classes are not equal is necessary, and then leads to the
+  theorem  @{text "0 \<noteq> 1"}.
 
   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"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
+  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 define the function @{text REG}. The intuition
+  We first define the function @{text REG}. The intuition
   behind this function is that it replaces quantifiers and
   abstractions involving raw types by bounded ones, and equalities
   involving raw types are replaced by appropriate aggregate
@@ -899,7 +887,8 @@
   \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.
+  for the universal quantifier. For the third and fourt clause, note that 
+  @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
 
   Next we define the function @{text INJ} which takes as argument
   @{text "reg_thm"} and @{text "quot_thm"} (both as
@@ -941,7 +930,7 @@
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
   the implications into simpler implication subgoals. This succeeds for every
   monotone connective, except in places where the function @{text REG} inserted,
-  for example, a quantifier by a bounded quantifier. In this case we have 
+  for instance, a quantifier by a bounded quantifier. In this case we have 
   rules of the form
 
   @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
@@ -961,10 +950,10 @@
 
   \noindent
   The last theorem is new in comparison with Homeier's package. There the
-  injection procedure would be used to prove such goals, and there
+  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 independent ``units''.
+  proof step into two independent ``units''.
 
   The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
   The proof again follows the structure of the
@@ -989,7 +978,7 @@
   We defined the theorem @{text "inj_thm"} in such a way that
   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be
   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient
-  definitions. Then all lifted constants, their definitions
+  definitions. Then for all lifted constants, their definitions
   are used to fold the @{term Rep} with the raw constant. Next for
   all abstractions and quantifiers the lambda and
   quantifier preservation theorems are used to replace the
@@ -1053,10 +1042,10 @@
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
   \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\[3mm]
-  \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~%
-  @{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\
+  \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 "plus_raw"}\\
+  \isacommand{is}~~@{text "add_pair"}\\
   \end{tabular}
   \end{isabelle}
 
@@ -1064,18 +1053,18 @@
   The following theorem about addition on the raw level can be proved.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "plus_zero_raw: int_rel (plus_raw (0, 0) x) x"}
+  \isacommand{lemma}~~@{text "add_pair_zero: int_rel (add_pair (0, 0) x) x"}
   \end{isabelle}
 
   \noindent
   If the user attempts to lift this theorem, all proof obligations are 
   automatically discharged, except the respectfulness
-  proof for @{text "plus_raw"}:
+  proof for @{text "add_pair"}:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{lemma}~~@{text "[quot_respect]:\\ 
-  (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
+  \isacommand{lemma}~~@{text "[quot_respect]:"}\\ 
+  @{text "(int_rel \<doublearr> int_rel \<doublearr> int_rel) add_pair add_pair"}
   \end{tabular}
   \end{isabelle}
 
@@ -1085,14 +1074,14 @@
   After this, the user can prove the lifted lemma explicitly:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting plus_zero_raw"}
+  \isacommand{lemma}~~@{text "0 + (x :: int) = x"}~~\isacommand{by}~~@{text "lifting add_pair_zero"}
   \end{isabelle}
 
   \noindent
   or by the completely automated mode by stating:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
+  \isacommand{thm}~~@{text "add_pair_zero[quot_lifted]"}
   \end{isabelle}
 
   \noindent
@@ -1102,7 +1091,7 @@
 
   \noindent
   Although seemingly simple, arriving at this result without the help of a quotient
-  package requires substantial reasoning effort.
+  package requires a substantial reasoning effort.
 *}
 
 section {* Conclusion and Related Work\label{sec:conc}*}
@@ -1114,7 +1103,7 @@
   standard distribution of Isabelle.\footnote{Available from
   \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
   heavily used in the new version of Nominal Isabelle, which provides a convenient reasoning
-  infrastructure for programming language calculi involving binders.  
+  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
@@ -1140,26 +1129,30 @@
   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 the
   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 ML-code. On the other hand, Homeier
-  is able to deal with partial quotient constructions, which we have not implemented.
+  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. 
 
   One advantage of our package is that it is modular---in the sense that every step
   in the quotient construction can be done independently (see the criticism of Paulson
   about other quotient packages). This modularity is essential in the context of
   Isabelle, which supports type-classes and locales.
 
-  Another feature of our quotient package is that when lifting theorems, we can
+  Another feature of our quotient package is that when lifting theorems, teh user can
   precisely specify what the lifted theorem should look like. This feature is
-  necessary, for example, when lifting an inductive principle about two lists.
+  necessary, for example, when lifting an induction principle for two lists.
   This principle has as the conclusion a predicate of the form @{text "P xs ys"},
   and 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.
+  Isabelle, where such a choice is required to generate a resoning infrastructure
+  for alpha-equated terms. 
+%%
+%% give an example for this
+%%
   \medskip
 
   \noindent
-  {\bf Acknowledgements:} We would like to thank Peter Homeier for the
+  {\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.




