
diff -r 1fd6809f5a44 -r c0c5bc4ee8cb Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 10:08:12 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 11:59:16 2010 +0200
@@ -1,5 +1,3 @@
-(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
-
 (*<*)
 theory Paper
 imports "Quotient"
@@ -353,7 +351,7 @@
       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{proposition}
 
-  \begin{definition}[Respects]
+  \begin{definition}[Respects]\label{def:respects}
   An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
   \end{definition}
 
@@ -748,35 +746,39 @@
 
 *}
 
-
 section {* Lifting of Theorems\label{sec:lift} *}
 
 text {*
-  The core of our quotient package takes an original theorem
-  involving raw types and a statement of the theorem that
-  it is supposed to produce. This is different from existing
-  quotient packages, where only the raw theorems are necessary.
-  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.
-  Lifting the theorems is performed in three steps. In the following
-  we call these steps \emph{regularization}, \emph{injection} and
-  \emph{cleaning} following the names used in Homeier's HOL4
-  implementation.
+
+  The core of a quotient package lifts an original theorem to a lifted
+  version. We will perform this operation in three phases. In the
+  following we call these phases \emph{regularization},
+  \emph{injection} and \emph{cleaning} following the names used in
+  Homeier's HOL4 implementation.
+
+  Regularization is supposed to change the quantifications and abstractions
+  in the theorem to quantification over variables that respect the relation
+  (definition \ref{def:respects}). Injection is supposed 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.
 
-  We 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, as all three
-  can be performed independently from each other.
+  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.
 
-*}
-text {* \textit{Regularization and Injection statements} *}
-text {*
+  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.
 
   We define the function @{text REG}, which takes the statements
   of the raw theorem and the lifted theorem (both as terms) and
@@ -829,32 +831,15 @@
   \end{tabular}
   \end{center}
 
-  For existential quantifiers and unique existential quantifiers it is
-  defined similarly to the universal one.
-
-*}
-text {*\textit{Proof Procedure}*}
-
-(* In the below the type-guiding 'QuotTrue' assumption is removed. We need it
-   only for bound variables without types, while in the paper presentation
-   variables are typed *)
-
-text {*
+  \noindent where the cases for existential quantifiers and unique existential
+  quantifiers have been omitted for clarity; are similar to universal quantifier.
 
-  When lifting a theorem we first apply the following rule
-
-  @{term [display, indent=10] "[|A; A --> B; B = C; C = D|] ==> D"}
-
-  \noindent
-  with @{text A} instantiated to the original raw theorem, 
-       @{text B} instantiated to @{text "REG(A)"},
-       @{text C} instantiated to @{text "INJ(REG(A))"},
-   and @{text D} instantiated to the statement of the lifted theorem.
-  The first assumption can be immediately discharged using the original
-  theorem and the three left subgoals are exactly the subgoals of regularization,
-  injection and cleaning. The three can be proved independently by the
-  framework and in case there are non-solved subgoals they can be left
-  to the user.
+  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.
 
   The injection and cleaning subgoals are always solved if the appropriate
   respectfulness and preservation theorems are given. It is not the case
@@ -867,10 +852,7 @@
   equivalence classes are not equal. A more general statement saying that
   the classes are not equal is necessary.
 
-*}
-text {* \textit{Proving Regularization} *}
-text {*
-
+  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
@@ -894,19 +876,7 @@
   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.
-*}
-text {* \textit{Proving Rep/Abs Injection} *}
 
-(*
-  @{thm bex_reg_eqv_range[no_vars]}
-  @{thm [display] bex_reg_left[no_vars]}
-  @{thm [display] bex1_bexeq_reg[no_vars]}
-  @{thm [display] bex_reg_eqv[no_vars]}
-  @{thm [display] babs_reg_eqv[no_vars]}
-  @{thm [display] babs_simp[no_vars]}
-*)
-
-text {*
   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.
@@ -915,42 +885,48 @@
   \item For two constants, an appropriate constant respectfullness 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:
+
+    @{term [display, indent=10] "R x y \<longrightarrow> R x (Rep (Abs y))"}
+
+    otherwise we introduce an appropriate relation between the subterms
+    and continue with two subgoals using the lemma:
+
+    @{term [display, indent=10] "(R1 ===> R2) f g \<longrightarrow> R1 x 1 \<longrightarrow> R2 (f x) (g y)"}
+
   \end{itemize}
 
-  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
-  in the injected theorem we can use the theorem:
+  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
+  are used to fold the @{term Rep} with the raw constant. Next for
+  all lambda abstractions and quantifications the lambda and
+  quantifier preservation theorems are used to replace the
+  variables that include raw types with respects by quantification
+  over variables that include quotient types. We show here only
+  the lambda preservation theorem; assuming
+  @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}
+  we have:
 
-  @{thm [display, indent=10] rep_abs_rsp[no_vars]}
+    @{thm [display, indent=10] (concl) lambda_prs[no_vars]}
 
   \noindent
-  and continue the proof.
-
-  Otherwise we introduce an appropriate relation between the subterms and continue with
-  two subgoals using the lemma:
+  holds. Next relations over lifted types are folded to equality.
+  The following theorem has been shown in Homeier~\cite{Homeier05}:
 
-  @{thm [display, indent=10] apply_rsp[no_vars]}
-
-*}
-text {* \textit{Cleaning} *}
-text {*
+    @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 
-  The @{text REG} and @{text INJ} functions have been defined in such a way
-  that establishing the goal theorem now consists only on rewriting the
-  injected theorem with the preservation theorems.
+  \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 R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}
+  we have:
 
-  \begin{itemize}
-  \item First for lifted constants, their definitions are the preservation rules for
-    them.
-  \item For lambda abstractions lambda preservation establishes
-    the equality between the injected theorem and the goal. This allows both
-    abstraction and quantification over lifted types.
-    @{thm [display] (concl) lambda_prs[no_vars]}
-  \item Relations over lifted types are folded with:
-    @{thm [display] (concl) Quotient_rel_rep[no_vars]}
-  \item User given preservation theorems, that allow using higher level operations
-    and containers of types being lifted. An example may be
-    @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
-  \end{itemize}
+  @{thm [display, indent=10] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
 
   *}
 




