# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274969203 -7200
# Node ID 3a6afcb187ec13380106e64abeb6bcc3053d418e
# Parent  74637f186af78a00e1691e1f82a685e843253e9d
qpaper / regularize

diff -r 74637f186af7 -r 3a6afcb187ec Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu May 27 14:30:07 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 16:06:43 2010 +0200
@@ -354,22 +354,47 @@
   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 HOL
-  implementation. The three steps are independent from each other.
+  implementation.
 
+  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, and all three
+  can be performed independently from each other.
 
 *}
 
-subsection {* Regularization *}
+subsection {* Regularization and Injection statements *}
 
 text {*
-Transformation of the theorem statement:
-\begin{itemize}
-\item Quantifiers and abstractions involving raw types replaced by bounded ones.
-\item Equalities involving raw types replaced by bounded ones.
-\end{itemize}
+
+  The function that gives the statement of the regularized theorem
+  takes the statement of the raw theorem (a term) and the statement
+  of the lifted theorem. The intuition behind the procedure is that
+  it replaces quantifiers and abstractions involving raw types
+  by bounded ones, and equalities involving raw types are replaced
+  by appropriate aggregate relations. It is defined as follows:
 
-The procedure.
+  \begin{itemize}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
+  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
+  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
+  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
+  \item @{text "REG (_, v) = v"}
+  \item @{text "REG (_, c) = c"}
+  \end{itemize}
 
+  Existential quantifiers and unique existential quantifiers are defined
+  similarily to the universal one.
+
+*}
+
+subsection {* Proof of Regularization *}
+
+text {*
 Example of non-regularizable theorem ($0 = 1$).
 
 Separtion of regularization from injection thanks to the following 2 lemmas: