1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:52:59 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:53:54 2008 +0100
     1.3 @@ -629,7 +629,7 @@
     1.4    --- the @{method intro_classes} method takes care of the details of
     1.5    class membership proofs.
     1.6  
     1.7 -  \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s
     1.8 +  \item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
     1.9    \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
    1.10    allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
    1.11    to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
    1.12 @@ -733,12 +733,12 @@
    1.13    c_class.axioms}.
    1.14    
    1.15    \item @{command "instance"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} and @{command
    1.16 -  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"} setup a goal stating a
    1.17 -  class relation or type arity.  The proof would usually proceed by
    1.18 -  @{method intro_classes}, and then establish the characteristic
    1.19 -  theorems of the type classes involved.  After finishing the proof,
    1.20 -  the theory will be augmented by a type signature declaration
    1.21 -  corresponding to the resulting theorem.
    1.22 +  "instance"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} setup a goal stating a class
    1.23 +  relation or type arity.  The proof would usually proceed by @{method
    1.24 +  intro_classes}, and then establish the characteristic theorems of
    1.25 +  the type classes involved.  After finishing the proof, the theory
    1.26 +  will be augmented by a type signature declaration corresponding to
    1.27 +  the resulting theorem.
    1.28  
    1.29    \end{description}
    1.30  *}
    1.31 @@ -942,18 +942,55 @@
    1.32    type constructor @{text t}.  If the object-logic defines a base sort
    1.33    @{text s}, then the constructor is declared to operate on that, via
    1.34    the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
    1.35 -  s) s"}.
    1.36 +  s)s"}.
    1.37  
    1.38 -  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n) s"} augments
    1.39 +  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
    1.40    Isabelle's order-sorted signature of types by new type constructor
    1.41    arities.  This is done axiomatically!  The @{command_ref "instance"}
    1.42 -  command (see \secref{sec:axclass}) provides a way to introduce proven
    1.43 -  type arities.
    1.44 +  command (see \secref{sec:axclass}) provides a way to introduce
    1.45 +  proven type arities.
    1.46  
    1.47    \end{description}
    1.48  *}
    1.49  
    1.50  
    1.51 +subsection {* Co-regularity of type classes and arities *}
    1.52 +
    1.53 +text {* The class relation together with the collection of
    1.54 +  type-constructor arities must obey the principle of
    1.55 +  \emph{co-regularity} as defined below.
    1.56 +
    1.57 +  \medskip For the subsequent formulation of co-regularity we assume
    1.58 +  that the class relation is closed by transitivity and reflexivity.
    1.59 +  Moreover the collection of arities @{text "t :: (\<^vec>s)c"} is
    1.60 +  completed such that @{text "t :: (\<^vec>s)c"} and @{text "c \<subseteq> c'"}
    1.61 +  implies @{text "t :: (\<^vec>s)c'"} for all such declarations.
    1.62 +
    1.63 +  Treating sorts as finite sets of classes (meaning the intersection),
    1.64 +  the class relation @{text "c\<^sub>1 \<subseteq> c\<^sub>2"} is extended to sorts as
    1.65 +  follows:
    1.66 +  \[
    1.67 +    @{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"}
    1.68 +  \]
    1.69 +
    1.70 +  This relation on sorts is further extended to tuples of sorts (of
    1.71 +  the same length) in the component-wise way.
    1.72 +
    1.73 +  \smallskip Co-regularity of the class relation together with the
    1.74 +  arities relation means:
    1.75 +  \[
    1.76 +    @{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"}
    1.77 +  \]
    1.78 +  \noindent for all such arities.  In other words, whenever the result
    1.79 +  classes of some type-constructor arities are related, then the
    1.80 +  argument sorts need to be related in the same way.
    1.81 +
    1.82 +  \medskip Co-regularity is a very fundamental property of the
    1.83 +  order-sorted algebra of types.  For example, it entails principle
    1.84 +  types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.
    1.85 +*}
    1.86 +
    1.87 +
    1.88  subsection {* Constants and definitions \label{sec:consts} *}
    1.89  
    1.90  text {*