--- a/doc-src/IsarRef/Thy/Spec.thy Sat Jul 10 22:39:16 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Mon Jul 12 11:21:27 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 \<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}.
+*}
+
+
section {* Unrestricted overloading *}
text {*
@@ -902,8 +939,7 @@
\begin{matharray}{rcll}
@{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
- @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
\begin{rail}
@@ -924,10 +960,9 @@
\item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> 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 \<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 {*
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sat Jul 10 22:39:16 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jul 12 11:21:27 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%