# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1276752869 -7200
# Node ID 229660b9f2fce81a4519b6142e207619f5798c8b
# Parent  2cbcdaba795a6f3c50e78638c62d52f20e16bf6a
Fix regularization. Two "FIXME" left in introduction. Minor spellings.

diff -r 2cbcdaba795a -r 229660b9f2fc Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Jun 17 00:27:57 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Jun 17 07:34:29 2010 +0200
@@ -247,6 +247,7 @@
   at the beginning of this section about having to collect theorems that are
   lifted from the raw level to the quotient level into one giant list. Our
   quotient package is the first one that is modular so that it allows to lift
+%%% FIXME: First-order ones exist, HOL-Light one lifts theorems separately.
   single theorems separately. This has the advantage for the user of being able to develop a
   formal theory interactively as a natural progression. A pleasing side-result of
   the modularity is that we are able to clearly specify what is involved
@@ -397,6 +398,7 @@
   would not be true in general. However, we can prove specific and useful 
   instances of the quotient theorem. We will 
   show an example in Section \ref{sec:resp}.
+%%% FIXME the example is gone from the paper?
 
 *}
 
@@ -843,7 +845,7 @@
   the equivalence classes are not equal is necessary.
 
   In the following we will first define the statement of the
-  regularized theorem based on @{text "raw_thm"} and the 
+  regularized theorem based on @{text "raw_thm"} and
   @{text "quot_thm"}. Then we define the statement of the injected theorem, based
   on @{text "reg_thm"} theorem and @{text "quot_thm"}. We then show the 3 proofs,
   which can all be performed independently from each other.
@@ -870,11 +872,8 @@
   @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \end{cases}$\smallskip\\
   \multicolumn{3}{@ {}l}{equality:}\smallskip\\
-  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & 
-  $\begin{cases}
-  @{text "="} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
-  @{text "REL (\<sigma>, \<tau>)"}\\
-  \end{cases}$\\
+  %% REL of two equal types is the equality so we do not need a separate case
+  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
   \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
   @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
   @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
@@ -926,21 +925,22 @@
   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
   the implications into simpler implication subgoals. This succeeds for every
-  monotone connectives, except in places wher the function @{text REG} inserted,
+  monotone connective, except in places wher the function @{text REG} inserted,
   for example, a quantifier by a bounded quantifier. In this case we have 
   rules of the form
 
   @{text [display, indent=10] "(\<forall>x. R x \<longrightarrow> (P x \<longrightarrow> Q x)) \<longrightarrow> (\<forall>x. P x \<longrightarrow> \<forall>x \<in> R. Q x)"}
 
   \noindent
-  They decompose a bounded quantifier on the right-hand side, but are only applicable
-  if we can prove that
+  They decompose a bounded quantifier on the right-hand side. We can decompose a
+  bounded quantifier anywhere if R is an equivalence relation or
+  if it is a relation over function types with the range being an equivalence
+  relation. If @{text R} is an equivalence relation we can prove that
 
   @{text [display, indent=10] "\<forall>x \<in> Respects R. P x = \<forall>x. P x"}    
 
   \noindent
-  And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation
-  and we can prove
+  And when @{term R\<^isub>2} is an equivalence relation and we can prove
 
   @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
@@ -951,7 +951,7 @@
   because this allows us to completely separate the first and the second
   proof step into independent ``units''.
 
-  The secon proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
+  The second proof step, establishing @{text "reg_thm \<longleftrightarrow> inj_thm"},  starts with an equality. 
   The proof again follows the structure of the
   two underlying terms, and is defined for a goal being a relation between these two terms.