# HG changeset patch # User haftmann # Date 1278926516 -7200 # Node ID 4511931c069266855950aafdeb8ec0bf14a7bbec # Parent a2b7a20d6ea38665d8c04f7cb53a99337f8bf448# Parent e86221f3bac735f0031bd86a3d517f5d445b1ab5 merged diff -r a2b7a20d6ea3 -r 4511931c0692 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Mon Jul 12 10:48:37 2010 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Jul 12 11:21:56 2010 +0200 @@ -738,6 +738,43 @@ *} +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 \ 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 \ c\<^sub>2"} is extended to sorts as + follows: + \[ + @{text "s\<^sub>1 \ s\<^sub>2 \ \c\<^sub>2 \ s\<^sub>2. \c\<^sub>1 \ s\<^sub>1. c\<^sub>1 \ 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 \ t :: (\<^vec>s\<^sub>2)c\<^sub>2 \ c\<^sub>1 \ c\<^sub>2 \ \<^vec>s\<^sub>1 \ \<^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}. +*} + + section {* Unrestricted overloading *} text {* @@ -902,8 +939,7 @@ \begin{matharray}{rcll} @{command_def "classes"} & : & @{text "theory \ theory"} \\ @{command_def "classrel"} & : & @{text "theory \ theory"} & (axiomatic!) \\ - @{command_def "default_sort"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def "default_sort"} & : & @{text "local_theory \ local_theory"} \end{matharray} \begin{rail} @@ -924,10 +960,9 @@ \item @{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"} states subclass relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}. - This is done axiomatically! The @{command_ref "instance"} - and @{command_ref "subclass"} command - (see \secref{sec:class}) provide a way to introduce proven class - relations. + This is done axiomatically! The @{command_ref "subclass"} and + @{command_ref "instance"} commands (see \secref{sec:class}) provide + a way to introduce proven class relations. \item @{command "default_sort"}~@{text s} makes sort @{text s} the new default sort for any type variable that is given explicitly in @@ -942,9 +977,6 @@ logically intersected, i.e.\ the representations as lists of classes are joined. - \item @{command "class_deps"} visualizes the subclass relation, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - \end{description} *} @@ -992,43 +1024,6 @@ *} -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 \ 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 \ c\<^sub>2"} is extended to sorts as - follows: - \[ - @{text "s\<^sub>1 \ s\<^sub>2 \ \c\<^sub>2 \ s\<^sub>2. \c\<^sub>1 \ s\<^sub>1. c\<^sub>1 \ 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 \ t :: (\<^vec>s\<^sub>2)c\<^sub>2 \ c\<^sub>1 \ c\<^sub>2 \ \<^vec>s\<^sub>1 \ \<^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 {* diff -r a2b7a20d6ea3 -r 4511931c0692 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Jul 12 10:48:37 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jul 12 11:21:56 2010 +0200 @@ -755,6 +755,46 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{Co-regularity of type classes and arities% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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 \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is + completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}} + implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations. + + Treating sorts as finite sets of classes (meaning the intersection), + the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as + follows: + \[ + \isa{{\isachardoublequote}s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlsub {\isadigit{2}}\ {\isasymequiv}\ {\isasymforall}c\isactrlsub {\isadigit{2}}\ {\isasymin}\ s\isactrlsub {\isadigit{2}}{\isachardot}\ {\isasymexists}c\isactrlsub {\isadigit{1}}\ {\isasymin}\ s\isactrlsub {\isadigit{1}}{\isachardot}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} + \] + + 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: + \[ + \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{1}}{\isacharparenright}c\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{2}}{\isacharparenright}c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ \isactrlvec s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlsub {\isadigit{2}}{\isachardoublequote}} + \] + \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}.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsection{Unrestricted overloading% } \isamarkuptrue% @@ -937,8 +977,7 @@ \begin{matharray}{rcll} \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ - \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ - \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ + \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \end{matharray} \begin{rail} @@ -959,10 +998,9 @@ \item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. - This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} - and \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} command - (see \secref{sec:class}) provide a way to introduce proven class - relations. + This is done axiomatically! The \indexref{}{command}{subclass}\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}} and + \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} commands (see \secref{sec:class}) provide + a way to introduce proven class relations. \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the new default sort for any type variable that is given explicitly in @@ -977,9 +1015,6 @@ logically intersected, i.e.\ the representations as lists of classes are joined. - \item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - \end{description}% \end{isamarkuptext}% \isamarkuptrue% @@ -1028,46 +1063,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Co-regularity of type classes and arities% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -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 \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is - completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}} - implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations. - - Treating sorts as finite sets of classes (meaning the intersection), - the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as - follows: - \[ - \isa{{\isachardoublequote}s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlsub {\isadigit{2}}\ {\isasymequiv}\ {\isasymforall}c\isactrlsub {\isadigit{2}}\ {\isasymin}\ s\isactrlsub {\isadigit{2}}{\isachardot}\ {\isasymexists}c\isactrlsub {\isadigit{1}}\ {\isasymin}\ s\isactrlsub {\isadigit{1}}{\isachardot}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} - \] - - 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: - \[ - \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{1}}{\isacharparenright}c\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{2}}{\isacharparenright}c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ \isactrlvec s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlsub {\isadigit{2}}{\isachardoublequote}} - \] - \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}.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsubsection{Constants and definitions \label{sec:consts}% } \isamarkuptrue%