
diff -r bf3a29ea74f6 -r d62c082cb56b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 12:00:03 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 22:25:03 2010 +0200
@@ -800,23 +800,33 @@
   equivalence relations. It is defined as follows:
 
   \begin{center}
-  \begin{tabular}{rcl}
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
-  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
-  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
-  @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
-  @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
+  \begin{longtable}{rcl}
+  \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
+  @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
+  \end{cases}$\smallskip\\
+  \multicolumn{3}{@ {}l}{universal quantifiers:}\\
+  @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{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}$\\
+  \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 (v\<^isub>1, v\<^isub>2)"} & $\dn$ & @{text "v\<^isub>1"}\\
-  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
-  \end{tabular}
+  @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\[-5mm]
+  \end{longtable}
   \end{center}
-
+  %
+  \noindent
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
   for the universal quantifier.
@@ -826,19 +836,29 @@
 
   \begin{center}
   \begin{tabular}{rcl}
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
-  @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) "} & $\dn$ & @{text "\<lambda>x. INJ (t, s)"}\\
-  @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}\\
-  @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
-  @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> (INJ (t, s))"}\\
-  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables, constants:}\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
+  @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
+  \end{cases}$\\
+  @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ 
+  & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
+  @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
+  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
   @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
-  @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "v\<^isub>1"}\\
-  @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}\\
-  @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) "} & $\dn$ & @{text "c\<^isub>1"}\\
-  @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) "} & $\dn$ & @{text "REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}\\
+  @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
+  \end{cases}$\\
+  @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  $\begin{cases}
+  @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
+  @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\
+  \end{cases}$\\
   \end{tabular}
   \end{center}
 
@@ -857,8 +877,8 @@
   with regularization; sometimes a theorem given by the user does not
   imply a regularized version and a stronger one needs to be proved. This
   is outside of the scope of the quotient package, so such obligations are
-  left to the user. Take a simple statement for integers @{term "0 \<noteq> 1"}.
-  It does not follow from the fact that @{term "\<not> (0, 0) = (1, 0)"} because
+  left to the user. Take a simple statement for integers @{text "0 \<noteq> 1"}.
+  It does not follow from the fact that @{text "(0, 0) \<noteq> (1, 0)"} because
   of regularization. The raw theorem only shows that particular items in the
   equivalence classes are not equal. A more general statement saying that
   the classes are not equal is necessary.
@@ -878,9 +898,9 @@
 
   @{thm [display, indent=10] (concl) ball_reg_eqv[no_vars]}
 
-  And finally it can be removed anywhere if @{term R2} is an equivalence relation:
+  And finally it can be removed anywhere if @{term R\<^isub>2} is an equivalence relation:
 
-  @{thm [display, indent=10] (concl) ball_reg_eqv_range[no_vars]}
+  @{thm [display, indent=10] (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
 
   The last theorem is new in comparison with Homeier's package. There the
   injection procedure would be used to prove goals with such shape, and there
@@ -905,7 +925,7 @@
     otherwise we introduce an appropriate relation between the subterms
     and continue with two subgoals using the lemma:
 
-    @{term [display, indent=10] "(R1 ===> R2) f g \<longrightarrow> R1 x 1 \<longrightarrow> R2 (f x) (g y)"}
+    @{text [display, indent=10] "(R\<^isub>1 \<doublearr> R\<^isub>2) f g \<longrightarrow> R\<^isub>1 x y \<longrightarrow> R\<^isub>2 (f x) (g y)"}
 
   \end{itemize}
 
@@ -919,8 +939,8 @@
   variables that include raw types with respects by quantification
   over variables that include quotient types. We show here only
   the lambda preservation theorem; assuming
-  @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}
-  we have:
+  @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}
+  hold, we have:
 
     @{thm [display, indent=10] (concl) lambda_prs[no_vars]}
 
@@ -934,10 +954,10 @@
   Finally the user given preservation theorems, that allow using
   higher level operations and containers of types being lifted.
   We show the preservation theorem for @{term map}. Again assuming
-  that @{term "Quotient R1 Abs1 Rep1"} and @{term "Quotient R2 Abs2 Rep2"}
+  that @{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"} hold,
   we have:
 
-  @{thm [display, indent=10] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
+  @{thm [display, indent=10] (concl) map_prs(1)[of R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1 R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2]}
 
   *}
 
@@ -959,7 +979,8 @@
   the same integer relation as the one presented in the introduction:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~@{text "(m \<Colon> nat, n) int_rel (p, q) = (m + q = n + p)"}
+  \isacommand{fun}~~@{text "int_rel"}~~\isacommand{where}~~%
+  @{text "(m :: nat, n) int_rel (p, q) = (m + q = n + p)"}
   \end{isabelle}
 
   \noindent
@@ -976,9 +997,11 @@
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
   \begin{tabular}{@ {}l}
-  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0::nat, 0::nat)"}\\
-  \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~@{text "plus_raw (m :: nat, n) (p, q) = (m + p, n + q)"}\\
-  \isacommand{quotient\_definition}~~@{text "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)"}~~\isacommand{is}~~@{text "plus_raw"}\\
+  \isacommand{quotient\_definition}~~@{text "0 :: int"}~~\isacommand{is}~~@{text "(0 :: nat, 0 :: nat)"}\\
+  \isacommand{fun}~~@{text "plus_raw"}~~\isacommand{where}~~%
+  @{text "plus_raw (m, n) (p, q) = (m + p :: nat, n + q :: nat)"}\\
+  \isacommand{quotient\_definition}~~@{text "+ :: int \<Rightarrow> int \<Rightarrow> int"}~~%
+  \isacommand{is}~~@{text "plus_raw"}\\
   \end{tabular}
   \end{isabelle}
 
@@ -994,12 +1017,13 @@
   proof obligation is left, so let us prove it first:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
-  \isacommand{lemma}~~@{text "[quot_respect]: (int_rel \<Longrightarrow> int_rel \<Longrightarrow> int_rel) plus_raw plus_raw"}
+  \isacommand{lemma}~~@{text "[quot_respect]: 
+  (int_rel \<doublearr> int_rel \<doublearr> int_rel) plus_raw plus_raw"}
   \end{isabelle}
 
   \noindent
   Can be proved automatically by the system just by unfolding the definition
-  of @{text "op \<Longrightarrow>"}.
+  of @{text "\<doublearr>"}.
   Now the user can either prove a lifted lemma explicitly:
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %
@@ -1033,16 +1057,16 @@
   concurrency \cite{BengtsonParow09} and a strong normalisation result for
   cut-elimination in classical logic \cite{UrbanZhu08}.
 
-  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+  Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
   defines quotient types for Isabelle/HOL. It did not include theorem lifting.
-  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
+  Harrison's quotient package~\cite{harrison-thesis} is the first one to
   lift theorems, however only first order. There is work on quotient types in
   non-HOL based systems and logical frameworks, namely theory interpretations
   in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
   the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
-  Larry Paulson shows a construction of quotients that does not require the
+  Paulson shows a construction of quotients that does not require the
   Hilbert Choice operator, again only first order~\cite{Paulson06}.
-  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
+  The closest to our package is the package for HOL4 by Homeier~\cite{Homeier05},
   which is the first one to support lifting of higher order theorems.
 
 
@@ -1063,7 +1087,7 @@
   a theory progressively.
 
   We allow lifting only some occurrences of quotiented types, which
-  is useful in Nominal. The package can be used automatically with
+  is useful in Nominal Isabelle. The package can be used automatically with
   an attribute, manually with separate tactics for parts of the lifting
   procedure, and programatically. Automated definitions of constants
   and respectfulness proof obligations are used in Nominal. Finally
@@ -1073,8 +1097,8 @@
   \medskip
   \noindent
   {\bf Acknowledgements:} We would like to thank Peter Homeier for the
-  discussions about the HOL4 quotient package and explaining us its
-  implementation details.
+  discussions about his HOL4 quotient package and explaining to us 
+  some its finer points in the implementation.
 
 *}
 




