
diff -r 337569f85398 -r 2cbcdaba795a Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed Jun 16 22:29:42 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Jun 17 00:27:57 2010 +0100
@@ -768,7 +768,7 @@
   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
   then we need to show the corresponding preservation lemma.
 
-  @{thm [display, indent=10] insert_preserve2[no_vars]}
+  %%%@ {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
@@ -809,31 +809,46 @@
 
   The purpose of regularization is to change the quantifiers and abstractions
   in a ``raw'' theorem to quantifiers over variables that respect the relation
-  (Definition \ref{def:respects} states what respects means). The purpose of injection is supposed to add @{term Rep}
+  (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 ones that include the
-  quotient type. Cleaning rewrites the obtained injected theorem with
-  preservation rules obtaining the desired goal theorem.
+  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:
+
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{4mm}}l}
+  1.) & @{text "raw_thm \<longrightarrow> reg_thm"}\\
+  2.) & @{text "reg_thm \<longleftrightarrow> inj_thm"}\\
+  3.) & @{text "inj_thm \<longleftrightarrow> quot_thm"}\\
+  \end{tabular}
+  \end{center}
 
-  Most quotient packages take only an original theorem involving raw
-  types and lift it. The procedure in our package takes both an
-  original theorem involving raw types and a statement of the theorem
-  that it is supposed to produce. To simplify the use of the quotient
-  package we additionally provide an automated statement translation
-  mechanism which can produce the latter automatically given a list of
-  quotient types.  It is possible that a user wants to lift only some
-  occurrences of a raw type. In this case the user specifies the
-  complete lifted goal instead of using the automated mechanism.
+  \noindent
+  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. 
+
+  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.
 
   In the following we will first define the statement of the
-  regularized theorem based on the original theorem and the goal
-  theorem. Then we define the statement of the injected theorem, based
-  on the regularized theorem and the goal. We then show the 3 proofs,
-  all three can be performed independently from each other.
+  regularized theorem based on @{text "raw_thm"} and the 
+  @{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,
+  which can all be performed independently from each other.
 
-  We define the function @{text REG}, which takes the statements
-  of the raw theorem and the lifted theorem (both as terms) and
-  returns the statement of the regularized version. The intuition
+  We 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
@@ -847,6 +862,7 @@
   @{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)"}
   \end{cases}$\smallskip\\
+  \\
   \multicolumn{3}{@ {}l}{universal quantifiers:}\\
   @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ & 
   $\begin{cases}
@@ -870,9 +886,10 @@
   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 the statement of
-  the regularized theorems and the statement of the lifted theorem both as
-  terms and returns the statement of the injected theorem:
+
+  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}{rcl}
@@ -902,103 +919,81 @@
   \end{tabular}
   \end{center}
 
-  \noindent where the cases for existential quantifiers and unique existential
-  quantifiers have been omitted for clarity; are similar to universal quantifier.
+  \noindent 
+  where again the cases for existential quantifiers and unique existential
+  quantifiers have been omitted.
 
-  We can now define the subgoals that will imply the lifted theorem. Given
-  the statement of the original theorem @{term t} and the statement of the
-  goal @{term g} the regularization subgoal is @{term "t \<longrightarrow> REG(t, g)"},
-  the injection subgoal is @{term "REG(t, g) = INJ(REG(t, g), g)"} and the
-  cleaning subgoal is @{term "INJ(REG(t, g), g) = g"}. We will now describe
-  the three tactics provided for these three subgoals.
+  In the first proof step, 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 implication subgoals. This succeeds for every
+  monotone connectives, except in places wher the function @{text REG} inserted,
+  for example, a quantifier by a bounded quantifier. In this case we have 
+  rules of the form
 
-  The injection and cleaning subgoals are always solved if the appropriate
-  respectfulness and preservation theorems are given. It is not the case
-  with regularization; sometimes a theorem given by the user does not
-  imply a regularized version and a stronger one needs to be proved. This
-  is outside of the scope of the quotient package, so such obligations are
-  left to the user. Take a simple statement for integers @{text "0 \<noteq> 1"}.
-  It does not follow from the fact that @{text "(0, 0) \<noteq> (1, 0)"} because
-  of regularization. The raw theorem only shows that particular items in the
-  equivalence classes are not equal. A more general statement saying that
-  the classes are not equal is necessary.
+  @{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)"}
+
+  \noindent
+  They decompose a bounded quantifier on the right-hand side, but are only applicable
+  if we can prove that
 
-  In the proof of the regularization subgoal we always start with an implication.
-  Isabelle provides a set of \emph{mono} rules, that are used to split implications
-  of similar statements into simpler implication subgoals. These are enhanced
-  with special quotient theorem in the regularization proof. Below we only show
-  the versions for the universal quantifier. For the existential quantifier
-  and abstraction they are analogous.
+  @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
 
-  First, bounded universal quantifiers can be removed on the right:
-
-  @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}
-
-  They can be removed anywhere if the relation is an equivalence relation:
-
-  @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
-
-  And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation:
+  \noindent
+  And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation
+  and we can prove
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
+  \noindent
   The last theorem is new in comparison with Homeier's package. There the
-  injection procedure would be used to prove goals with such shape, and there
-  the equivalence assumption would be used. We use the above theorem directly
-  also for composed relations where the range type is a type for which we know an
-  equivalence theorem. This allows separating regularization from injection.
+  injection procedure would be used to prove such goals, and there
+  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''.
 
-  The injection proof starts with an equality between the regularized theorem
-  and the injected version. The proof again follows by the structure of the
-  two terms, and is defined for a goal being a relation between these two terms.
+  The secon proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
+  The proof again follows the structure of the
+  two underlying terms, and is defined for a goal being a relation between these two terms.
 
   \begin{itemize}
-  \item For two constants, an appropriate constant respectfulness assumption is used.
-  \item For two variables, we use the assumptions proved in regularization.
-  \item For two abstractions, they are eta-expanded and beta-reduced.
-  \item For two applications, if the right side is an application of
-    @{term Rep} to an @{term Abs} and @{term "Quotient R Rep Abs"} we
-    can reduce the injected pair using the theorem:
+  \item For two constants an appropriate constant respectfulness lemma 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"}. If yes then we
+    can apply the theorem:
 
     @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
 
-    otherwise we introduce an appropriate relation between the subterms
+    Otherwise we introduce an appropriate relation between the subterms
     and continue with two subgoals using the lemma:
 
     @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
-
   \end{itemize}
 
-  The cleaning subgoal has been defined in such a way that
-  establishing the goal theorem now consists only on rewriting the
-  injected theorem with the preservation theorems and quotient
-  definitions. First for all lifted constants, their definitions
+  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
   are used to fold the @{term Rep} with the raw constant. Next for
-  all lambda abstractions and quantifications the lambda and
+  all abstractions and quantifiers the lambda and
   quantifier preservation theorems are used to replace the
-  variables that include raw types with respects by quantification
+  variables that include raw types with respects by quantifiers
   over variables that include quotient types. We show here only
-  the lambda preservation theorem; assuming
-  @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}
-  hold, we have:
+  the lambda preservation theorem. Given
+  @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 
-    @{thm [display, indent=10] (concl) lambda_prs[no_vars]}
+    @{thm [display, indent=10] (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
 
   \noindent
-  holds. Next relations over lifted types are folded to equality.
-  The following theorem has been shown in Homeier~\cite{Homeier05}:
+  Next, relations over lifted types are folded to equalities.
+  For this the following theorem has been shown in Homeier~\cite{Homeier05}:
 
     @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 
   \noindent
-  Finally the user given preservation theorems, that allow using
-  higher level operations and containers of types being lifted.
-  We show the preservation theorem for @{term map}. Again assuming
-  that @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} hold,
-  we have:
-
-  @{thm [display, indent=10] (concl) map_prs(1)[of R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1 R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2]}
-
+  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} *}
@@ -1009,27 +1004,32 @@
 
   In this section we will show, a complete interaction with the quotient package
   for defining the type of integers by quotienting pairs of natural numbers and
-  lifting theorems to integers. Our quotient package is fully compatible with
+  lifting theorems to integers. Oeur quotient package is fully compatible with
   Isabelle type classes, but for clarity we will not use them in this example.
   In a larger formalization of integers using the type class mechanism would
   provide many algebraic properties ``for free''.
 
   A user of our quotient package first needs to define a relation on
   the raw type, by which the quotienting will be performed. We give
-  the same integer relation as the one presented in the introduction:
+  the same integer relation as the one presented in \eqref{natpairequiv}:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~%
-  @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"}
+  \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 is defined. This leaves a proof obligation that the
-  relation is an equivalence relation which is solved automatically using the
-  definitions:
+  Next the quotient type is defined. This generates a proof obligation that the
+  relation is an equivalence relation, which is solved automatically using the
+  definition and extensionality:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{quotient\_type}~~@{text "int"}~~\isacommand{=}~~@{text "(nat \<times> nat)"}~~\isacommand{/}~~@{text "int_rel"}
+  \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
@@ -1037,7 +1037,7 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\
+  \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{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
@@ -1046,39 +1046,48 @@
   \end{isabelle}
 
   \noindent
-  Lets first take a simple theorem about addition on the raw level:
+  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"}
   \end{isabelle}
 
   \noindent
-  When the user tries to lift a theorem about integer addition, the respectfulness
-  proof obligation is left, so let us prove it first:
+  If the user attempts to lift this theorem, all proof obligations are 
+  automatically discharged, except the respectfulness
+  proof for @{text "plus_raw"}:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "[quot_respect]: 
+  \begin{tabular}{@ {}l}
+  \isacommand{lemma}~~@{text "[quot_respect]:\\ 
   (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
+  \end{tabular}
   \end{isabelle}
 
   \noindent
-  Can be proved automatically by the system just by unfolding the definition
+  This can be dischaged automatically by Isabelle when telling it to unfold the definition
   of @{text "\<doublearr>"}.
-  Now the user can either prove a lifted lemma explicitly:
+  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"}
   \end{isabelle}
 
   \noindent
-  Or in this simple case use the automated translation mechanism:
+  or by the completely automated mode by stating:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \isacommand{thm}~~@{text "plus_zero_raw[quot_lifted]"}
   \end{isabelle}
 
   \noindent
-  obtaining the same result.
+  Both methods give the same result, namely
+
+  @{text [display, indent=10] "0 + x = x"}
+
+  \noindent
+  Although seemingly simple, arriving at this result without the help of a quotient
+  package requires substantial reasoning effort.
 *}
 
 section {* Conclusion and Related Work\label{sec:conc}*}




