# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276518512 -7200
# Node ID 8954dc5ebd523b769f79959220652f2f21bbd4bb
# Parent  4bba0d41ff2c39873eec9faf26ad9e0eb410a6d1# Parent  1a4fc8d3873fea4d7a37fbb4954c487e8e44991b
merged

diff -r 4bba0d41ff2c -r 8954dc5ebd52 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Jun 14 14:28:12 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 14:28:32 2010 +0200
@@ -1672,5 +1672,10 @@
 apply(auto simp add: mem_def)
 done
 
+lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)"
+apply rule
+apply (rule ball_reg_right)
+apply auto
+done
 
 end
diff -r 4bba0d41ff2c -r 8954dc5ebd52 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 14:28:12 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 14:28:32 2010 +0200
@@ -687,23 +687,20 @@
 section {* Lifting of 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 were 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.
+  The core of our 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 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 optionally
+  take a list of quotient types. It is possible that a user wants
+  to lift only some occurrences of a quotiented 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 HOL
+  \emph{cleaning} following the names used in Homeier's HOL4
   implementation.
 
   We first define the statement of the regularized theorem based
@@ -718,13 +715,13 @@
 
 text {*
 
-  We first define the function @{text REG}, which takes the statements
+  We define the function @{text REG}, which takes the statements
   of the raw theorem and the lifted theorem (both as terms) and
   returns the statement of the regularized version. The intuition
   behind this function 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:
+  equivalence relations. It is defined as follows:
 
   \begin{center}
   \begin{tabular}{rcl}
@@ -817,13 +814,13 @@
 
   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 goal. Below we only show
+  with special quotient theorem in the regularization proof. Below we only show
   the versions for the universal quantifier. For the existential quantifier
   and abstraction they are analogous.
 
   First, bounded universal quantifiers can be removed on the right:
 
-  @{thm [display, indent=10] ball_reg_right[no_vars]}
+  @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]}
 
   They can be removed anywhere if the relation is an equivalence relation: