357   implementation. The three steps are independent from each other.

   357   implementation.

   358 

   358 

   359 

   359   We first define the statement of the regularized theorem based

   360 *}

   360   on the original theorem and the goal theorem. Then we define

   361 

   361   the statement of the injected theorem, based on the regularized

   362 subsection {* Regularization *}

   362   theorem and the goal. We then show the 3 proofs, and all three

   363 

   363   can be performed independently from each other.

   364 text {*

   364 

   365 Transformation of the theorem statement:

   365 *}

   366 \begin{itemize}

   366 

   367 \item Quantifiers and abstractions involving raw types replaced by bounded ones.

   367 subsection {* Regularization and Injection statements *}

   368 \item Equalities involving raw types replaced by bounded ones.

   368 

   369 \end{itemize}

   369 text {*

   370 

   370 

   371 The procedure.

   371   The function that gives the statement of the regularized theorem

   372 

   372   takes the statement of the raw theorem (a term) and the statement

   373   of the lifted theorem. The intuition behind the procedure is that

   374   it replaces quantifiers and abstractions involving raw types

   375   by bounded ones, and equalities involving raw types are replaced

   376   by appropriate aggregate relations. It is defined as follows:

   377 

   378   \begin{itemize}

   379   \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}

   380   \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

   381   \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}

   382   \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

   383   \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}

   384   \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}

   385   \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)"}

   386   \item @{text "REG (_, v) = v"}

   387   \item @{text "REG (_, c) = c"}

   388   \end{itemize}

   389 

   390   Existential quantifiers and unique existential quantifiers are defined

   391   similarily to the universal one.

   392 

   393 *}

   394 

   395 subsection {* Proof of Regularization *}

   396 

   397 text {*