# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276511408 -7200
# Node ID a040404748006a95da56446ce5e8b1a3f68b2be2
# Parent  084b2b7df98a3e7901ab0761750da9570d2e1c6d# Parent  8f493d371234dc04d892ea73996af6ba3157f0ed
merged

diff -r 084b2b7df98a -r a04040474800 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 14 11:51:34 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 14 12:30:08 2010 +0200
@@ -201,7 +201,7 @@
 
   \noindent
   We expect that the corresponding operator on finite sets, written @{term "fconcat"},
-  builds the finite unions of finite sets:
+  builds finite unions of finite sets:
 
   @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]}
 
@@ -725,17 +725,23 @@
   involving raw types are replaced by appropriate aggregate
   relations. It is defined as follows:
 
-  \begin{itemize}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
-  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
-  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
-  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
-  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
-  \end{itemize}
+  \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> Res (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> Res (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:}\\
+  @{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}
+  \end{center}
 
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
@@ -745,18 +751,23 @@
   the regularized theorems and the statement of the lifted theorem both as
   terms and returns the statement of the injected theorem:
 
-  \begin{itemize}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
-  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
-  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
-  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
-  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
-  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
-  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
-  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
-  \end{itemize}
+  \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:}\\
+  @{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))"}\\
+  \end{tabular}
+  \end{center}
 
   For existential quantifiers and unique existential quantifiers it is
   defined similarly to the universal one.
@@ -879,15 +890,15 @@
   \item For lambda abstractions lambda preservation establishes
     the equality between the injected theorem and the goal. This allows both
     abstraction and quantification over lifted types.
-    @{thm [display] lambda_prs[no_vars]}
+    @{thm [display] (concl) lambda_prs[no_vars]}
   \item Relations over lifted types are folded with:
-    @{thm [display] Quotient_rel_rep[no_vars]}
+    @{thm [display] (concl) Quotient_rel_rep[no_vars]}
   \item User given preservation theorems, that allow using higher level operations
     and containers of types being lifted. An example may be
-    @{thm [display] map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
+    @{thm [display] (concl) map_prs(1)[of R1 Abs1 Rep1 R2 Abs2 Rep2,no_vars]}
   \end{itemize}
 
- Preservation of relations and user given constant preservation lemmas *}
+  *}
 
 section {* Examples *}