# HG changeset patch
# User wenzelm
# Date 1226609634 -3600
# Node ID a056077b65a1f8e7ab50d65c16d73bf69a8dfde5
# Parent  f09ceb800d00c5649876bb5d80482c8c0dfaf993
added section "Co-regularity of type classes and arities" (variant from old ref manual);
tuned arity spacing;

diff -r f09ceb800d00 -r a056077b65a1 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:52:59 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:53:54 2008 +0100
@@ -629,7 +629,7 @@
   --- the @{method intro_classes} method takes care of the details of
   class membership proofs.
 
-  \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s
+  \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
   \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
   allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
   to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
@@ -733,12 +733,12 @@
   c_class.axioms}.
   
   \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
-  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"} setup a goal stating a
-  class relation or type arity.  The proof would usually proceed by
-  @{method intro_classes}, and then establish the characteristic
-  theorems of the type classes involved.  After finishing the proof,
-  the theory will be augmented by a type signature declaration
-  corresponding to the resulting theorem.
+  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
+  relation or type arity.  The proof would usually proceed by @{method
+  intro_classes}, and then establish the characteristic theorems of
+  the type classes involved.  After finishing the proof, the theory
+  will be augmented by a type signature declaration corresponding to
+  the resulting theorem.
 
   \end{description}
 *}
@@ -942,18 +942,55 @@
   type constructor @{text t}.  If the object-logic defines a base sort
   @{text s}, then the constructor is declared to operate on that, via
   the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
-  s) s"}.
+  s)s"}.
 
-  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"} augments
+  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
   Isabelle's order-sorted signature of types by new type constructor
   arities.  This is done axiomatically!  The @{command_ref "instance"}
-  command (see \secref{sec:axclass}) provides a way to introduce proven
-  type arities.
+  command (see \secref{sec:axclass}) provides a way to introduce
+  proven type arities.
 
   \end{description}
 *}
 
 
+subsection {* Co-regularity of type classes and arities *}
+
+text {* The class relation together with the collection of
+  type-constructor arities must obey the principle of
+  \emph{co-regularity} as defined below.
+
+  \medskip For the subsequent formulation of co-regularity we assume
+  that the class relation is closed by transitivity and reflexivity.
+  Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
+  completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
+  implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
+
+  Treating sorts as finite sets of classes (meaning the intersection),
+  the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
+  follows:
+  \[
+    @{text "s\<^sub>1 \<subseteq> s\<^sub>2 \<equiv> \<forall>c\<^sub>2 \<in> s\<^sub>2. \<exists>c\<^sub>1 \<in> s\<^sub>1. c\<^sub>1 \<subseteq> c\<^sub>2"}
+  \]
+
+  This relation on sorts is further extended to tuples of sorts (of
+  the same length) in the component-wise way.
+
+  \smallskip Co-regularity of the class relation together with the
+  arities relation means:
+  \[
+    @{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2"}
+  \]
+  \noindent for all such arities.  In other words, whenever the result
+  classes of some type-constructor arities are related, then the
+  argument sorts need to be related in the same way.
+
+  \medskip Co-regularity is a very fundamental property of the
+  order-sorted algebra of types.  For example, it entails principle
+  types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
+*}
+
+
 subsection {* Constants and definitions \label{sec:consts} *}
 
 text {*