# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274889342 -7200
# Node ID a52499e125ce49912cb30b767fbfa66aa91cbdd2
# Parent  aae246e2a5dc54dad740fc90e4237e58cca8698a
qpaper / lifting introduction

diff -r aae246e2a5dc -r a52499e125ce Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed May 26 17:20:59 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 17:55:42 2010 +0200
@@ -307,11 +307,28 @@
 
 section {* Lifting Theorems *}
 
+text {*
+  The core of the quotient package takes an original theorem that
+  talks about the raw types, and the statement of the theorem that
+  it is supposed to produce. This is different from other existing
+  quotient packages, where only the raw theorems was necessary.
+  We notice that in some cases only some occurrences of the raw
+  types need to be lifted. This is for example the case in the
+  new Nominal package, where a raw datatype that talks about
+  pairs of natural numbers or strings (being lists of characters)
+  should not be changed to a quotient datatype with constructors
+  taking integers or finite sets of characters. To simplify the
+  use of the quotient package we additionally provide an automated
+  statement translation mechanism that replaces occurrences of
+  types that match given quotients by appropriate lifted types.
+
+  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.
 
 
-text {* TBD *}
-
-text {* Why providing a statement to prove is necessary is some cases *}
+*}
 
 subsection {* Regularization *}