310 

   310 text {*

   311 

   311   The core of the quotient package takes an original theorem that

   312 text {* TBD *}

   312   talks about the raw types, and the statement of the theorem that

   313 

   313   it is supposed to produce. This is different from other existing

   314 text {* Why providing a statement to prove is necessary is some cases *}

   314   quotient packages, where only the raw theorems was necessary.

   315   We notice that in some cases only some occurrences of the raw

   316   types need to be lifted. This is for example the case in the

   317   new Nominal package, where a raw datatype that talks about

   318   pairs of natural numbers or strings (being lists of characters)

   319   should not be changed to a quotient datatype with constructors

   320   taking integers or finite sets of characters. To simplify the

   321   use of the quotient package we additionally provide an automated

   322   statement translation mechanism that replaces occurrences of

   323   types that match given quotients by appropriate lifted types.

   324 

   325   Lifting the theorems is performed in three steps. In the following

   326   we call these steps \emph{regularization}, \emph{injection} and

   327   \emph{cleaning} following the names used in Homeier's HOL

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

   329 

   330 

   331 *}