--- a/.hgignore Wed Jun 17 16:55:01 2009 -0700
+++ b/.hgignore Wed Jun 17 16:56:15 2009 -0700
@@ -8,6 +8,7 @@
syntax: regexp
+^contrib
^heaps/
^browser_info/
^doc-src/.*\.aux
--- a/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 16:55:01 2009 -0700
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Wed Jun 17 16:56:15 2009 -0700
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-experimental"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/doc-src/Classes/Thy/Classes.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/Classes/Thy/Classes.thy Wed Jun 17 16:56:15 2009 -0700
@@ -5,8 +5,8 @@
section {* Introduction *}
text {*
- Type classes were introduces by Wadler and Blott \cite{wadler89how}
- into the Haskell language, to allow for a reasonable implementation
+ Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering
later additions in expressiveness}.
@@ -43,9 +43,9 @@
Indeed, type classes not only allow for simple overloading
but form a generic calculus, an instance of order-sorted
- algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+ algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- From a software engeneering point of view, type classes
+ From a software engineering point of view, type classes
roughly correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
provide functions (class parameters) but also state specifications
@@ -65,7 +65,7 @@
\end{quote}
- \noindent From a theoretic point of view, type classes are lightweight
+ \noindent From a theoretical point of view, type classes are lightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -77,22 +77,19 @@
\item instantiating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system
- (aka locales \cite{kammueller-locales}).
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
- in a Haskell like fashion.
+ in a Haskell like fashion. Internally, they are mapped to more primitive
+ Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
semigroups, monoids and groups. Our background theory is that of
Isabelle/HOL \cite{isa-tutorial}, for which some
familiarity is assumed.
-
- Here we merely present the look-and-feel for end users.
- Internally, those are mapped to more primitive Isabelle concepts.
- See \cite{Haftmann-Wenzel:2006:classes} for more detail.
*}
section {* A simple algebra example \label{sec:example} *}
@@ -146,22 +143,22 @@
end %quote
text {*
- \noindent @{command instantiation} allows to define class parameters
+ \noindent @{command instantiation} defines class parameters
at a particular instance using common specification tools (here,
@{command definition}). The concluding @{command instance}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the @{method default} method,
which for such instance proofs maps to the @{method intro_classes} method.
- This boils down an instance judgement to the relevant primitive
- proof goals and should conveniently always be the first method applied
+ This reduces an instance judgement to the relevant primitive
+ proof goals; typically it is the first method applied
in an instantiation proof.
From now on, the type-checker will consider @{typ int}
as a @{class semigroup} automatically, i.e.\ any general results
are immediately available on concrete instances.
- \medskip Another instance of @{class semigroup} are the natural numbers:
+ \medskip Another instance of @{class semigroup} yields the natural numbers:
*}
instantiation %quote nat :: semigroup
@@ -182,8 +179,8 @@
text {*
\noindent Note the occurence of the name @{text mult_nat}
in the primrec declaration; by default, the local name of
- a class operation @{text f} to instantiate on type constructor
- @{text \<kappa>} are mangled as @{text f_\<kappa>}. In case of uncertainty,
+ a class operation @{text f} to be instantiated on type constructor
+ @{text \<kappa>} is mangled as @{text f_\<kappa>}. In case of uncertainty,
these names may be inspected using the @{command "print_context"} command
or the corresponding ProofGeneral button.
*}
@@ -191,7 +188,7 @@
subsection {* Lifting and parametric types *}
text {*
- Overloaded definitions giving on class instantiation
+ Overloaded definitions given at a class instantiation
may include recursion over the syntactic structure of types.
As a canonical example, we model product semigroups
using our simple algebra:
@@ -201,22 +198,21 @@
begin
definition %quote
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+ mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
instance %quote proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+ fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+ show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
unfolding mult_prod_def by (simp add: assoc)
qed
end %quote
text {*
- \noindent Associativity from product semigroups is
- established using
+ \noindent Associativity of product semigroups is established using
the definition of @{text "(\<otimes>)"} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the @{class semigroup} constraints imposed
+ are legitimate due to the @{class semigroup} constraints imposed
on the type components by the @{command instance} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.
@@ -229,7 +225,7 @@
We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
by extending @{class semigroup}
with one additional parameter @{text neutral} together
- with its property:
+ with its characteristic property:
*}
class %quote monoidl = semigroup +
@@ -279,7 +275,7 @@
end %quote
text {*
- \noindent Fully-fledged monoids are modelled by another subclass
+ \noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:
*}
@@ -339,13 +335,13 @@
section {* Type classes as locales *}
-subsection {* A look behind the scene *}
+subsection {* A look behind the scenes *}
text {*
The example above gives an impression how Isar type classes work
in practice. As stated in the introduction, classes also provide
a link to Isar's locale system. Indeed, the logical core of a class
- is nothing else than a locale:
+ is nothing other than a locale:
*}
class %quote idem =
@@ -379,7 +375,7 @@
proof qed (rule idem)
text {*
- \noindent This gives you at hand the full power of the Isabelle module system;
+ \noindent This gives you the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
to class @{text idem}.
*} (*<*)setup %invisible {* Sign.parent_path *}
@@ -436,25 +432,26 @@
\noindent As you can see from this example, for local
definitions you may use any specification tool
- which works together with locales (e.g. \cite{krauss2006}).
+ which works together with locales, such as Krauss's recursive function package
+ \cite{krauss2006}.
*}
subsection {* A functor analogy *}
text {*
- We introduced Isar classes by analogy to type classes
+ We introduced Isar classes by analogy to type classes in
functional programming; if we reconsider this in the
context of what has been said about type classes and locales,
we can drive this analogy further by stating that type
- classes essentially correspond to functors which have
+ classes essentially correspond to functors that have
a canonical interpretation as type classes.
- Anyway, there is also the possibility of other interpretations.
- For example, also @{text list}s form a monoid with
+ There is also the possibility of other interpretations.
+ For example, @{text list}s also form a monoid with
@{text append} and @{term "[]"} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
- In such a case, we simply can do a particular interpretation
+ In such a case, we can simply make a particular interpretation
of monoids for lists:
*}
@@ -518,7 +515,7 @@
to the type system, making @{text group} an instance of
@{text monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -551,7 +548,7 @@
\end{figure}
For illustration, a derived definition
- in @{text group} which uses @{text pow_nat}:
+ in @{text group} using @{text pow_nat}
*}
definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
@@ -568,7 +565,7 @@
subsection {* A note on syntax *}
text {*
- As a convenience, class context syntax allows to refer
+ As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:
*}
@@ -602,9 +599,9 @@
@{command instantiation}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
- takes this into account. Concerning target languages
- lacking type classes (e.g.~SML), type classes
- are implemented by explicit dictionary construction.
+ takes this into account. If the target language (e.g.~SML)
+ lacks type classes, then they
+ are implemented by an explicit dictionary construction.
As example, let's go back to the power function:
*}
@@ -612,13 +609,13 @@
"example = pow_int 10 (-2)"
text {*
- \noindent This maps to Haskell as:
+ \noindent This maps to Haskell as follows:
*}
text %quote {*@{code_stmts example (Haskell)}*}
text {*
- \noindent The whole code in SML with explicit dictionary passing:
+ \noindent The code in SML has explicit dictionary passing:
*}
text %quote {*@{code_stmts example (SML)}*}
--- a/doc-src/Classes/Thy/document/Classes.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/Classes/Thy/document/Classes.tex Wed Jun 17 16:56:15 2009 -0700
@@ -23,8 +23,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Type classes were introduces by Wadler and Blott \cite{wadler89how}
- into the Haskell language, to allow for a reasonable implementation
+Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering
later additions in expressiveness}.
@@ -61,9 +61,9 @@
Indeed, type classes not only allow for simple overloading
but form a generic calculus, an instance of order-sorted
- algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
+ algebra \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
- From a software engeneering point of view, type classes
+ From a software engineering point of view, type classes
roughly correspond to interfaces in object-oriented languages like Java;
so, it is naturally desirable that type classes do not only
provide functions (class parameters) but also state specifications
@@ -83,7 +83,7 @@
\end{quote}
- \noindent From a theoretic point of view, type classes are lightweight
+ \noindent From a theoretical point of view, type classes are lightweight
modules; Haskell type classes may be emulated by
SML functors \cite{classes_modules}.
Isabelle/Isar offers a discipline of type classes which brings
@@ -95,22 +95,19 @@
\item instantiating those abstract parameters by a particular
type
\item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system
- (aka locales \cite{kammueller-locales}).
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
\end{enumerate}
\noindent Isar type classes also directly support code generation
- in a Haskell like fashion.
+ in a Haskell like fashion. Internally, they are mapped to more primitive
+ Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
This tutorial demonstrates common elements of structured specifications
and abstract reasoning with type classes by the algebraic hierarchy of
semigroups, monoids and groups. Our background theory is that of
Isabelle/HOL \cite{isa-tutorial}, for which some
- familiarity is assumed.
-
- Here we merely present the look-and-feel for end users.
- Internally, those are mapped to more primitive Isabelle concepts.
- See \cite{Haftmann-Wenzel:2006:classes} for more detail.%
+ familiarity is assumed.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -207,22 +204,22 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters
at a particular instance using common specification tools (here,
\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
opens a proof that the given parameters actually conform
to the class specification. Note that the first proof step
is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
- This boils down an instance judgement to the relevant primitive
- proof goals and should conveniently always be the first method applied
+ This reduces an instance judgement to the relevant primitive
+ proof goals; typically it is the first method applied
in an instantiation proof.
From now on, the type-checker will consider \isa{int}
as a \isa{semigroup} automatically, i.e.\ any general results
are immediately available on concrete instances.
- \medskip Another instance of \isa{semigroup} are the natural numbers:%
+ \medskip Another instance of \isa{semigroup} yields the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -264,8 +261,8 @@
\begin{isamarkuptext}%
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
in the primrec declaration; by default, the local name of
- a class operation \isa{f} to instantiate on type constructor
- \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
+ a class operation \isa{f} to be instantiated on type constructor
+ \isa{{\isasymkappa}} is mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
or the corresponding ProofGeneral button.%
\end{isamarkuptext}%
@@ -276,7 +273,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Overloaded definitions giving on class instantiation
+Overloaded definitions given at a class instantiation
may include recursion over the syntactic structure of types.
As a canonical example, we model product semigroups
using our simple algebra:%
@@ -294,15 +291,15 @@
\isanewline
\isacommand{definition}\isamarkupfalse%
\isanewline
-\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
\ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
-\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
@@ -319,11 +316,10 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Associativity from product semigroups is
- established using
+\noindent Associativity of product semigroups is established using
the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the \isa{semigroup} constraints imposed
+ are legitimate due to the \isa{semigroup} constraints imposed
on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
Indeed, this pattern often occurs with parametric types
and type classes.%
@@ -338,7 +334,7 @@
We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral)
by extending \isa{semigroup}
with one additional parameter \isa{neutral} together
- with its property:%
+ with its characteristic property:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -439,7 +435,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Fully-fledged monoids are modelled by another subclass
+\noindent Fully-fledged monoids are modelled by another subclass,
which does not add new parameters but tightens the specification:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -562,7 +558,7 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{A look behind the scene%
+\isamarkupsubsection{A look behind the scenes%
}
\isamarkuptrue%
%
@@ -570,7 +566,7 @@
The example above gives an impression how Isar type classes work
in practice. As stated in the introduction, classes also provide
a link to Isar's locale system. Indeed, the logical core of a class
- is nothing else than a locale:%
+ is nothing other than a locale:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -714,7 +710,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This gives you at hand the full power of the Isabelle module system;
+\noindent This gives you the full power of the Isabelle module system;
conclusions in locale \isa{idem} are implicitly propagated
to class \isa{idem}.%
\end{isamarkuptext}%
@@ -832,7 +828,8 @@
\noindent As you can see from this example, for local
definitions you may use any specification tool
- which works together with locales (e.g. \cite{krauss2006}).%
+ which works together with locales, such as Krauss's recursive function package
+ \cite{krauss2006}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -841,18 +838,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-We introduced Isar classes by analogy to type classes
+We introduced Isar classes by analogy to type classes in
functional programming; if we reconsider this in the
context of what has been said about type classes and locales,
we can drive this analogy further by stating that type
- classes essentially correspond to functors which have
+ classes essentially correspond to functors that have
a canonical interpretation as type classes.
- Anyway, there is also the possibility of other interpretations.
- For example, also \isa{list}s form a monoid with
+ There is also the possibility of other interpretations.
+ For example, \isa{list}s also form a monoid with
\isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
- In such a case, we simply can do a particular interpretation
+ In such a case, we can simply make a particular interpretation
of monoids for lists:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -982,7 +979,7 @@
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
to the graph of subclass relations
- (cf.\ \figref{fig:subclass}).
+ (\figref{fig:subclass}).
\begin{figure}[htbp]
\begin{center}
@@ -1015,7 +1012,7 @@
\end{figure}
For illustration, a derived definition
- in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
+ in \isa{group} using \isa{pow{\isacharunderscore}nat}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1048,7 +1045,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-As a convenience, class context syntax allows to refer
+As a convenience, class context syntax allows references
to local class operations and their global counterparts
uniformly; type inference resolves ambiguities. For example:%
\end{isamarkuptext}%
@@ -1113,9 +1110,9 @@
\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
targets naturally maps to Haskell type classes.
The code generator framework \cite{isabelle-codegen}
- takes this into account. Concerning target languages
- lacking type classes (e.g.~SML), type classes
- are implemented by explicit dictionary construction.
+ takes this into account. If the target language (e.g.~SML)
+ lacks type classes, then they
+ are implemented by an explicit dictionary construction.
As example, let's go back to the power function:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -1136,7 +1133,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This maps to Haskell as:%
+\noindent This maps to Haskell as follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1223,7 +1220,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The whole code in SML with explicit dictionary passing:%
+\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1250,16 +1247,15 @@
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoidl =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\
+\hspace*{0pt}type 'a monoidl = {\char123}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}semigroup{\char95}monoidl A{\char95};\\
\hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\
-\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}monoidl{\char95}monoid :~'a monoidl{\char125};\\
+\hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}monoidl{\char95}monoid A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
-\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\
+\hspace*{0pt}type 'a group = {\char123}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\
+\hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}monoid{\char95}group A{\char95};\\
\hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\
\hspace*{0pt}\\
\hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\
@@ -1271,14 +1267,12 @@
\hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\
\hspace*{0pt}\\
\hspace*{0pt}val monoidl{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
+\hspace*{0pt} ~{\char123}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int monoidl;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\
-\hspace*{0pt} ~IntInf.int monoid;\\
+\hspace*{0pt}val monoid{\char95}int = {\char123}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:~IntInf.int monoid;\\
\hspace*{0pt}\\
-\hspace*{0pt}val group{\char95}int =\\
-\hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
+\hspace*{0pt}val group{\char95}int = {\char123}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\
\hspace*{0pt} ~IntInf.int group;\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\
--- a/doc-src/Classes/classes.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/Classes/classes.tex Wed Jun 17 16:56:15 2009 -0700
@@ -21,8 +21,7 @@
\maketitle
\begin{abstract}
- \noindent This tutorial introduces the look-and-feel of
- Isar type classes to the end-user. Isar type classes
+ \noindent This tutorial introduces Isar type classes, which
are a convenient mechanism for organizing specifications.
Essentially, they combine an operational aspect (in the
manner of Haskell) with a logical aspect, both managed uniformly.
--- a/doc-src/IsarRef/Thy/Spec.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/IsarRef/Thy/Spec.thy Wed Jun 17 16:56:15 2009 -0700
@@ -585,6 +585,7 @@
@{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
@{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
@{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -599,8 +600,12 @@
;
'instance'
;
+ 'instance' nameref '::' arity
+ ;
'subclass' target? nameref
;
+ 'instance' nameref ('<' | subseteq) nameref
+ ;
'print\_classes'
;
'class\_deps'
@@ -649,12 +654,24 @@
the type classes involved. After finishing the proof, the
background theory will be augmented by the proven type arities.
+ On the theory level, @{command "instance"}~@{text "t :: (s\<^sub>1, \<dots>,
+ s\<^sub>n)s"} provides a convenient way to instantiate a type class with no
+ need to specifify operations: one can continue with the
+ instantiation proof immediately.
+
\item @{command "subclass"}~@{text c} in a class context for class
@{text d} sets up a goal stating that class @{text c} is logically
contained in class @{text d}. After finishing the proof, class
@{text d} is proven to be subclass @{text c} and the locale @{text
c} is interpreted into @{text d} simultaneously.
+ A weakend form of this is available through a further variant of
+ @{command instance}: @{command instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} opens
+ a proof that class @{text "c\<^isub>2"} implies @{text "c\<^isub>1"} without reference
+ to the underlying locales; this is useful if the properties to prove
+ the logical connection are not sufficent on the locale level but on
+ the theory level.
+
\item @{command "print_classes"} prints all classes in the current
theory.
@@ -703,20 +720,17 @@
text {*
\begin{matharray}{rcl}
- @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def "axclass"} & : & @{text "theory \<rightarrow> theory"}
\end{matharray}
Axiomatic type classes are Isabelle/Pure's primitive
- \emph{definitional} interface to type classes. For practical
+ interface to type classes. For practical
applications, you should consider using classes
(cf.~\secref{sec:classes}) which provide high level interface.
\begin{rail}
'axclass' classdecl (axmdecl prop +)
;
- 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
- ;
\end{rail}
\begin{description}
@@ -736,14 +750,6 @@
here. The full collection of these facts is also stored as @{text
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.
-
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Jun 17 16:56:15 2009 -0700
@@ -599,6 +599,7 @@
\indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+ \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
\indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
\indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\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}} \\
@@ -613,8 +614,12 @@
;
'instance'
;
+ 'instance' nameref '::' arity
+ ;
'subclass' target? nameref
;
+ 'instance' nameref ('<' | subseteq) nameref
+ ;
'print\_classes'
;
'class\_deps'
@@ -656,11 +661,22 @@
the type classes involved. After finishing the proof, the
background theory will be augmented by the proven type arities.
+ On the theory level, \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} provides a convenient way to instantiate a type class with no
+ need to specifify operations: one can continue with the
+ instantiation proof immediately.
+
\item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class
\isa{d} sets up a goal stating that class \isa{c} is logically
contained in class \isa{d}. After finishing the proof, class
\isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously.
+ A weakend form of this is available through a further variant of
+ \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}: \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} opens
+ a proof that class \isa{{\isachardoublequote}c\isactrlisub {\isadigit{2}}{\isachardoublequote}} implies \isa{{\isachardoublequote}c\isactrlisub {\isadigit{1}}{\isachardoublequote}} without reference
+ to the underlying locales; this is useful if the properties to prove
+ the logical connection are not sufficent on the locale level but on
+ the theory level.
+
\item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current
theory.
@@ -713,8 +729,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+ \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
\end{matharray}
Axiomatic type classes are Isabelle/Pure's primitive
@@ -725,8 +740,6 @@
\begin{rail}
'axclass' classdecl (axmdecl prop +)
;
- 'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
- ;
\end{rail}
\begin{description}
@@ -743,12 +756,6 @@
specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added
here. The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}.
- \item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} setup a goal stating a class
- relation or type arity. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}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}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/System/Thy/Presentation.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/System/Thy/Presentation.thy Wed Jun 17 16:56:15 2009 -0700
@@ -299,8 +299,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
- @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
+ @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
+ @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
\end{tabular}
\end{center}
@@ -454,6 +454,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -563,6 +564,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The @{verbatim "-t"} option produces a more detailed
+ internal timing report of the session.
+
\medskip The @{verbatim "-v"} option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/System/Thy/document/Presentation.tex Wed Jun 17 16:56:15 2009 -0700
@@ -323,8 +323,8 @@
\begin{center}\small
\begin{tabular}{rcl}
- \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
- \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
+ \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}{\isacharplus}{\isachardoublequote}} \\
+ \isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}{\isacharasterisk}{\isachardoublequote}}
\end{tabular}
\end{center}
@@ -480,6 +480,7 @@
-p LEVEL set level of detail for proof objects
-r reset session path
-s NAME override session NAME
+ -t BOOL internal session timing (default false)
-v BOOL be verbose (default false)
Build object-logic or run examples. Also creates browsing
@@ -580,6 +581,9 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \medskip The \verb|-t| option produces a more detailed
+ internal timing report of the session.
+
\medskip The \verb|-v| option causes additional information
to be printed while running the session, notably the location of
prepared documents.
--- a/doc-src/TutorialI/IsaMakefile Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/IsaMakefile Wed Jun 17 16:56:15 2009 -0700
@@ -151,7 +151,6 @@
$(LOG)/HOL-Types.gz: $(OUT)/HOL Types/ROOT.ML \
Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
- Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \
Types/Overloading.thy Types/Axioms.thy
$(USEDIR) Types
@rm -f tutorial.dvi
--- a/doc-src/TutorialI/Makefile Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Makefile Wed Jun 17 16:56:15 2009 -0700
@@ -22,7 +22,8 @@
Protocol/document/Event.tex Protocol/document/Message.tex \
Protocol/document/Public.tex Protocol/document/NS_Public.tex \
Rules/rules.tex Sets/sets.tex Types/numerics.tex \
- Types/types.tex Documents/documents.tex ../iman.sty \
+ Types/types.tex Types/document/Overloading.tex \
+ Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty \
../ttbox.sty ../extra.sty ../isabelle.sty ../isabellesym.sty \
../pdfsetup.sty
--- a/doc-src/TutorialI/Misc/appendix.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Misc/appendix.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1,6 +1,6 @@
-(*<*)
-theory appendix imports Main begin;
-(*>*)
+(*<*)theory appendix
+imports Main
+begin(*>*)
text{*
\begin{table}[htbp]
@@ -8,31 +8,26 @@
\begin{tabular}{lll}
Constant & Type & Syntax \\
\hline
-@{text 0} & @{text "'a::zero"} \\
-@{text 1} & @{text "'a::one"} \\
-@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
-@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
-@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text div} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text mod} & @{text "('a::div) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text dvd} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{text"/"} & @{text "('a::inverse) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
-@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
-@{term abs} & @{text "('a::minus) \<Rightarrow> 'a"} & ${\mid} x {\mid}$\\
-@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
-@{term min} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
-@{term max} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
-@{term Least} & @{text "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"} &
-@{text LEAST}$~x.~P$
+@{term [source] 0} & @{typeof [show_sorts] "0"} \\
+@{term [source] 1} & @{typeof [show_sorts] "1"} \\
+@{term [source] plus} & @{typeof [show_sorts] "plus"} & (infixl $+$ 65) \\
+@{term [source] minus} & @{typeof [show_sorts] "minus"} & (infixl $-$ 65) \\
+@{term [source] uminus} & @{typeof [show_sorts] "uminus"} & $- x$ \\
+@{term [source] times} & @{typeof [show_sorts] "times"} & (infixl $*$ 70) \\
+@{term [source] divide} & @{typeof [show_sorts] "divide"} & (infixl $/$ 70) \\
+@{term [source] Divides.div} & @{typeof [show_sorts] "Divides.div"} & (infixl $div$ 70) \\
+@{term [source] Divides.mod} & @{typeof [show_sorts] "Divides.mod"} & (infixl $mod$ 70) \\
+@{term [source] abs} & @{typeof [show_sorts] "abs"} & ${\mid} x {\mid}$ \\
+@{term [source] sgn} & @{typeof [show_sorts] "sgn"} \\
+@{term [source] less_eq} & @{typeof [show_sorts] "less_eq"} & (infixl $\le$ 50) \\
+@{term [source] less} & @{typeof [show_sorts] "less"} & (infixl $<$ 50) \\
+@{term [source] top} & @{typeof [show_sorts] "top"} \\
+@{term [source] bot} & @{typeof [show_sorts] "bot"}
\end{tabular}
-\caption{Overloaded Constants in HOL}
+\caption{Important Overloaded Constants in Main}
\label{tab:overloading}
\end{center}
\end{table}
*}
-(*<*)
-end
-(*>*)
+(*<*)end(*>*)
--- a/doc-src/TutorialI/Misc/document/appendix.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Misc/document/appendix.tex Wed Jun 17 16:56:15 2009 -0700
@@ -21,26 +21,23 @@
\begin{tabular}{lll}
Constant & Type & Syntax \\
\hline
-\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}zero} \\
-\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}one} \\
-\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
-\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
-\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{div} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{mod} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}div{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{dvd} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{{\isacharslash}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}inverse{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
-\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
-\isa{abs} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} & ${\mid} x {\mid}$\\
-\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
-\isa{min} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{max} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
-\isa{Least} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} &
-\isa{LEAST}$~x.~P$
+\isa{{\isadigit{0}}} & \isa{{\isacharprime}a{\isasymColon}zero} \\
+\isa{{\isadigit{1}}} & \isa{{\isacharprime}a{\isasymColon}one} \\
+\isa{plus} & \isa{{\isacharprime}a{\isasymColon}plus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}plus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}plus} & (infixl $+$ 65) \\
+\isa{minus} & \isa{{\isacharprime}a{\isasymColon}minus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}minus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}minus} & (infixl $-$ 65) \\
+\isa{uminus} & \isa{{\isacharprime}a{\isasymColon}uminus\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}uminus} & $- x$ \\
+\isa{times} & \isa{{\isacharprime}a{\isasymColon}times\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}times\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}times} & (infixl $*$ 70) \\
+\isa{divide} & \isa{{\isacharprime}a{\isasymColon}inverse\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}inverse\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}inverse} & (infixl $/$ 70) \\
+\isa{Divides{\isachardot}div} & \isa{{\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div} & (infixl $div$ 70) \\
+\isa{Divides{\isachardot}mod} & \isa{{\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}div} & (infixl $mod$ 70) \\
+\isa{abs} & \isa{{\isacharprime}a{\isasymColon}abs\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}abs} & ${\mid} x {\mid}$ \\
+\isa{sgn} & \isa{{\isacharprime}a{\isasymColon}sgn\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}sgn} \\
+\isa{less{\isacharunderscore}eq} & \isa{{\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ bool} & (infixl $\le$ 50) \\
+\isa{less} & \isa{{\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}ord\ {\isasymRightarrow}\ bool} & (infixl $<$ 50) \\
+\isa{top} & \isa{{\isacharprime}a{\isasymColon}top} \\
+\isa{bot} & \isa{{\isacharprime}a{\isasymColon}bot}
\end{tabular}
-\caption{Overloaded Constants in HOL}
+\caption{Important Overloaded Constants in Main}
\label{tab:overloading}
\end{center}
\end{table}%
--- a/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1,258 +1,261 @@
-(*<*)theory Axioms imports Overloading begin(*>*)
+(*<*)theory Axioms imports Overloading Setup begin(*>*)
+
+subsection {* Axioms *}
+
+text {* Attaching axioms to our classes lets us reason on the level of
+classes. The results will be applicable to all types in a class, just
+as in axiomatic mathematics.
+
+\begin{warn}
+Proofs in this section use structured \emph{Isar} proofs, which are not
+covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
+\end{warn} *}
+
+subsubsection {* Semigroups *}
+
+text{* We specify \emph{semigroups} as subclass of @{class plus}: *}
+
+class semigroup = plus +
+ assumes assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
+
+text {* \noindent This @{command class} specification requires that
+all instances of @{class semigroup} obey @{fact "assoc:"}~@{prop
+[source] "\<And>x y z \<Colon> 'a\<Colon>semigroup. (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"}.
-subsection{*Axioms*}
+We can use this class axiom to derive further abstract theorems
+relative to class @{class semigroup}: *}
+
+lemma assoc_left:
+ fixes x y z :: "'a\<Colon>semigroup"
+ shows "x \<oplus> (y \<oplus> z) = (x \<oplus> y) \<oplus> z"
+ using assoc by (rule sym)
+
+text {* \noindent The @{class semigroup} constraint on type @{typ
+"'a"} restricts instantiations of @{typ "'a"} to types of class
+@{class semigroup} and during the proof enables us to use the fact
+@{fact assoc} whose type parameter is itself constrained to class
+@{class semigroup}. The main advantage of classes is that theorems
+can be proved in the abstract and freely reused for each instance.
+
+On instantiation, we have to give a proof that the given operations
+obey the class axioms: *}
+
+instantiation nat :: semigroup
+begin
+
+instance proof
+
+txt {* \noindent The proof opens with a default proof step, which for
+instance judgements invokes method @{method intro_classes}. *}
-text{*Attaching axioms to our classes lets us reason on the
-level of classes. The results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our ordering relations.
-*}
-
-subsubsection{*Partial Orders*}
+ fix m n q :: nat
+ show "(m \<oplus> n) \<oplus> q = m \<oplus> (n \<oplus> q)"
+ by (induct m) simp_all
+qed
-text{*
-A \emph{partial order} is a subclass of @{text ordrel}
-where certain axioms need to hold:
-*}
+end
-axclass parord < ordrel
-refl: "x <<= x"
-trans: "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
-antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
-lt_le: "x << y = (x <<= y \<and> x \<noteq> y)"
+text {* \noindent Again, the interesting things enter the stage with
+parametric types: *}
+
+instantiation * :: (semigroup, semigroup) semigroup
+begin
-text{*\noindent
-The first three axioms are the familiar ones, and the final one
-requires that @{text"<<"} and @{text"<<="} are related as expected.
-Note that behind the scenes, Isabelle has restricted the axioms to class
-@{text parord}. For example, the axiom @{thm[source]refl} really is
-@{thm[show_sorts]refl}.
+instance proof
+ fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
+ show "p\<^isub>1 \<oplus> p\<^isub>2 \<oplus> p\<^isub>3 = p\<^isub>1 \<oplus> (p\<^isub>2 \<oplus> p\<^isub>3)"
+ by (cases p\<^isub>1, cases p\<^isub>2, cases p\<^isub>3) (simp add: assoc)
-We have not made @{thm[source] lt_le} a global definition because it would
-fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
-never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of our choice is that
-we need to define both @{text"<<="} and @{text"<<"} for each instance.
+txt {* \noindent Associativity of product semigroups is established
+using the hypothetical associativity @{fact assoc} of the type
+components, which holds due to the @{class semigroup} constraints
+imposed on the type components by the @{command instance} proposition.
+Indeed, this pattern often occurs with parametric types and type
+classes. *}
-We can now prove simple theorems in this abstract setting, for example
-that @{text"<<"} is not symmetric:
-*}
+qed
-lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
+end
+
+subsubsection {* Monoids *}
-txt{*\noindent
-The conclusion is not just @{prop"\<not> y << x"} because the
-simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
-would turn it into @{prop"y << x = False"}, yielding
-a nonterminating rewrite rule.
-(It would be used to try to prove its own precondition \emph{ad
- infinitum}.)
-In the form above, the rule is useful.
-The type constraint is necessary because otherwise Isabelle would only assume
-@{text"'a::ordrel"} (as required in the type of @{text"<<"}),
-when the proposition is not a theorem. The proof is easy:
-*}
+text {* We define a subclass @{text monoidl} (a semigroup with a
+left-hand neutral) by extending @{class semigroup} with one additional
+parameter @{text neutral} together with its property: *}
-by(simp add: lt_le antisym);
+class monoidl = semigroup +
+ fixes neutral :: "'a" ("\<zero>")
+ assumes neutl: "\<zero> \<oplus> x = x"
-text{* We could now continue in this vein and develop a whole theory of
-results about partial orders. Eventually we will want to apply these results
-to concrete types, namely the instances of the class. Thus we first need to
-prove that the types in question, for example @{typ bool}, are indeed
-instances of @{text parord}:*}
+text {* \noindent Again, we prove some instances, by providing
+suitable parameter definitions and proofs for the additional
+specifications. *}
-instance bool :: parord
-apply intro_classes;
+instantiation nat :: monoidl
+begin
-txt{*\noindent
-This time @{text intro_classes} leaves us with the four axioms,
-specialized to type @{typ bool}, as subgoals:
-@{subgoals[display,show_types,indent=0]}
-Fortunately, the proof is easy for \isa{blast}
-once we have unfolded the definitions
-of @{text"<<"} and @{text"<<="} at type @{typ bool}:
-*}
-
-apply(simp_all (no_asm_use) only: le_bool_def lt_bool_def);
-by(blast, blast, blast, blast);
+definition
+ neutral_nat_def: "\<zero> = (0\<Colon>nat)"
-text{*\noindent
-Can you figure out why we have to include @{text"(no_asm_use)"}?
-
-We can now apply our single lemma above in the context of booleans:
-*}
+instance proof
+ fix n :: nat
+ show "\<zero> \<oplus> n = n"
+ unfolding neutral_nat_def by simp
+qed
-lemma "(P::bool) << Q \<Longrightarrow> \<not>(Q << P)";
-by simp;
+end
-text{*\noindent
-The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules.
-The main advantage of the axiomatic method is that
-theorems can be proved in the abstract and freely reused for each instance.
+text {* \noindent In contrast to the examples above, we here have both
+specification of class operations and a non-trivial instance proof.
+
+This covers products as well:
*}
-subsubsection{*Linear Orders*}
+instantiation * :: (monoidl, monoidl) monoidl
+begin
-text{* If any two elements of a partial order are comparable it is a
-\textbf{linear} or \textbf{total} order: *}
-
-axclass linord < parord
-linear: "x <<= y \<or> y <<= x"
+definition
+ neutral_prod_def: "\<zero> = (\<zero>, \<zero>)"
-text{*\noindent
-By construction, @{text linord} inherits all axioms from @{text parord}.
-Therefore we can show that linearity can be expressed in terms of @{text"<<"}
-as follows:
-*}
+instance proof
+ fix p :: "'a\<Colon>monoidl \<times> 'b\<Colon>monoidl"
+ show "\<zero> \<oplus> p = p"
+ by (cases p) (simp add: neutral_prod_def neutl)
+qed
-lemma "\<And>x::'a::linord. x << y \<or> x = y \<or> y << x";
-apply(simp add: lt_le);
-apply(insert linear);
-apply blast;
-done
+end
-text{*
-Linear orders are an example of subclassing\index{subclasses}
-by construction, which is the most
-common case. Subclass relationships can also be proved.
-This is the topic of the following
-paragraph.
-*}
+text {* \noindent Fully-fledged monoids are modelled by another
+subclass which does not add new parameters but tightens the
+specification: *}
-subsubsection{*Strict Orders*}
+class monoid = monoidl +
+ assumes neutr: "x \<oplus> \<zero> = x"
-text{*
-An alternative axiomatization of partial orders takes @{text"<<"} rather than
-@{text"<<="} as the primary concept. The result is a \textbf{strict} order:
-*}
+text {* \noindent Corresponding instances for @{typ nat} and products
+are left as an exercise to the reader. *}
+
+subsubsection {* Groups *}
-axclass strord < ordrel
-irrefl: "\<not> x << x"
-lt_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
-le_less: "x <<= y = (x << y \<or> x = y)"
+text {* \noindent To finish our small algebra example, we add a @{text
+group} class: *}
-text{*\noindent
-It is well known that partial orders are the same as strict orders. Let us
-prove one direction, namely that partial orders are a subclass of strict
-orders. *}
-
-instance parord < strord
-apply intro_classes;
+class group = monoidl +
+ fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
+ assumes invl: "\<div> x \<oplus> x = \<zero>"
-txt{*\noindent
-@{subgoals[display,show_sorts]}
-Because of @{text"'a :: parord"}, the three axioms of class @{text strord}
-are easily proved:
-*}
+text {* \noindent We continue with a further example for abstract
+proofs relative to type classes: *}
- apply(simp_all (no_asm_use) add: lt_le);
- apply(blast intro: trans antisym);
-apply(blast intro: refl);
-done
-
-text{*
-The subclass relation must always be acyclic. Therefore Isabelle will
-complain if you also prove the relationship @{text"strord < parord"}.
-*}
-
+lemma left_cancel:
+ fixes x y z :: "'a\<Colon>group"
+ shows "x \<oplus> y = x \<oplus> z \<longleftrightarrow> y = z"
+proof
+ assume "x \<oplus> y = x \<oplus> z"
+ then have "\<div> x \<oplus> (x \<oplus> y) = \<div> x \<oplus> (x \<oplus> z)" by simp
+ then have "(\<div> x \<oplus> x) \<oplus> y = (\<div> x \<oplus> x) \<oplus> z" by (simp add: assoc)
+ then show "y = z" by (simp add: invl neutl)
+next
+ assume "y = z"
+ then show "x \<oplus> y = x \<oplus> z" by simp
+qed
-(*
-instance strord < parord
-apply intro_classes;
-apply(simp_all (no_asm_use) add: le_lt);
-apply(blast intro: lt_trans);
-apply(erule disjE);
-apply(erule disjE);
-apply(rule irrefl[THEN notE]);
-apply(rule lt_trans, assumption, assumption);
-apply blast;apply blast;
-apply(blast intro: irrefl[THEN notE]);
-done
-*)
+text {* \noindent Any @{text "group"} is also a @{text "monoid"}; this
+can be made explicit by claiming an additional subclass relation,
+together with a proof of the logical difference: *}
-subsubsection{*Multiple Inheritance and Sorts*}
-
-text{*
-A class may inherit from more than one direct superclass. This is called
-\bfindex{multiple inheritance}. For example, we could define
-the classes of well-founded orderings and well-orderings:
-*}
+instance group \<subseteq> monoid
+proof
+ fix x
+ from invl have "\<div> x \<oplus> x = \<zero>" .
+ then have "\<div> x \<oplus> (x \<oplus> \<zero>) = \<div> x \<oplus> x"
+ by (simp add: neutl invl assoc [symmetric])
+ then show "x \<oplus> \<zero> = x" by (simp add: left_cancel)
+qed
-axclass wford < parord
-wford: "wf {(y,x). y << x}"
-
-axclass wellord < linord, wford
-
-text{*\noindent
-The last line expresses the usual definition: a well-ordering is a linear
-well-founded ordering. The result is the subclass diagram in
+text {* \noindent The proof result is propagated to the type system,
+making @{text group} an instance of @{text monoid} by adding an
+additional edge to the graph of subclass relation; see also
Figure~\ref{fig:subclass}.
\begin{figure}[htbp]
-\[
-\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{type}\\
-& & |\\
-& & \isa{ordrel}\\
-& & |\\
-& & \isa{strord}\\
-& & |\\
-& & \isa{parord} \\
-& / & & \backslash \\
-\isa{linord} & & & & \isa{wford} \\
-& \backslash & & / \\
-& & \isa{wellord}
-\end{array}
-\]
-\caption{Subclass Diagram}
-\label{fig:subclass}
+ \begin{center}
+ \small
+ \unitlength 0.6mm
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(25,35){\vector(1,-3){10}}
+ \end{picture}
+ \hspace{8em}
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(05,15){\vector(3,-1){30}}
+ \end{picture}
+ \caption{Subclass relationship of monoids and groups:
+ before and after establishing the relationship
+ @{text "group \<subseteq> monoid"}; transitive edges are left out.}
+ \label{fig:subclass}
+ \end{center}
\end{figure}
-
-Since class @{text wellord} does not introduce any new axioms, it can simply
-be viewed as the intersection of the two classes @{text linord} and @{text
-wford}. Such intersections need not be given a new name but can be created on
-the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
-represents the intersection of the $C@i$. Such an expression is called a
-\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
-classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
-In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
-However, we do not pursue this rarefied concept further.
-
-This concludes our demonstration of type classes based on orderings. We
-remind our readers that \isa{Main} contains a theory of
-orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
-If possible, base your own ordering relations on this theory.
*}
-subsubsection{*Inconsistencies*}
+subsubsection {* Inconsistencies *}
-text{* The reader may be wondering what happens if we
-attach an inconsistent set of axioms to a class. So far we have always
-avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
+text {* The reader may be wondering what happens if we attach an
+inconsistent set of axioms to a class. So far we have always avoided
+to add new axioms to HOL for fear of inconsistencies and suddenly it
seems that we are throwing all caution to the wind. So why is there no
problem?
-The point is that by construction, all type variables in the axioms of an
-\isacommand{axclass} are automatically constrained with the class being
-defined (as shown for axiom @{thm[source]refl} above). These constraints are
-always carried around and Isabelle takes care that they are never lost,
-unless the type variable is instantiated with a type that has been shown to
-belong to that class. Thus you may be able to prove @{prop False}
-from your axioms, but Isabelle will remind you that this
-theorem has the hidden hypothesis that the class is non-empty.
+The point is that by construction, all type variables in the axioms of
+a \isacommand{class} are automatically constrained with the class
+being defined (as shown for axiom @{thm[source]refl} above). These
+constraints are always carried around and Isabelle takes care that
+they are never lost, unless the type variable is instantiated with a
+type that has been shown to belong to that class. Thus you may be able
+to prove @{prop False} from your axioms, but Isabelle will remind you
+that this theorem has the hidden hypothesis that the class is
+non-empty.
+
+Even if each individual class is consistent, intersections of
+(unrelated) classes readily become inconsistent in practice. Now we
+know this need not worry us. *}
+
+
+subsubsection{* Syntactic Classes and Predefined Overloading *}
-Even if each individual class is consistent, intersections of (unrelated)
-classes readily become inconsistent in practice. Now we know this need not
-worry us.
-*}
+text {* In our algebra example, we have started with a \emph{syntactic
+class} @{class plus} which only specifies operations but no axioms; it
+would have been also possible to start immediately with class @{class
+semigroup}, specifying the @{text "\<oplus>"} operation and associativity at
+the same time.
-(*
-axclass false<"term"
-false: "x \<noteq> x";
+Which approach is more appropriate depends. Usually it is more
+convenient to introduce operations and axioms in the same class: then
+the type checker will automatically insert the corresponding class
+constraints whenever the operations occur, reducing the need of manual
+annotations. However, when operations are decorated with popular
+syntax, syntactic classes can be an option to re-use the syntax in
+different contexts; this is indeed the way most overloaded constants
+in HOL are introduced, of which the most important are listed in
+Table~\ref{tab:overloading} in the appendix. Section
+\ref{sec:numeric-classes} covers a range of corresponding classes
+\emph{with} axioms.
-lemma "False";
-by(rule notE[OF false HOL.refl]);
-*)
+Further note that classes may contain axioms but \emph{no} operations.
+An example is class @{class finite} from theory @{theory Finite_Set}
+which specifies a type to be finite: @{lemma [source] "finite (UNIV \<Colon> 'a\<Colon>finite
+set)" by (fact finite_UNIV)}. *}
+
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1,21 +1,78 @@
-(*<*)theory Overloading imports Overloading1 begin(*>*)
-instance list :: (type)ordrel
-by intro_classes
+(*<*)theory Overloading imports Main Setup begin
+
+hide (open) "class" plus (*>*)
+
+text {* Type classes allow \emph{overloading}; thus a constant may
+have multiple definitions at non-overlapping types. *}
+
+subsubsection {* Overloading *}
+
+text {* We can introduce a binary infix addition operator @{text "\<otimes>"}
+for arbitrary types by means of a type class: *}
+
+class plus =
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
+
+text {* \noindent This introduces a new class @{class [source] plus},
+along with a constant @{const [source] plus} with nice infix syntax.
+@{const [source] plus} is also named \emph{class operation}. The type
+of @{const [source] plus} carries a class constraint @{typ [source] "'a
+:: plus"} on its type variable, meaning that only types of class
+@{class [source] plus} can be instantiated for @{typ [source] "'a"}.
+To breathe life into @{class [source] plus} we need to declare a type
+to be an \bfindex{instance} of @{class [source] plus}: *}
+
+instantiation nat :: plus
+begin
+
+text {* \noindent Command \isacommand{instantiation} opens a local
+theory context. Here we can now instantiate @{const [source] plus} on
+@{typ nat}: *}
+
+primrec plus_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "(0::nat) \<oplus> n = n"
+ | "Suc m \<oplus> n = Suc (m \<oplus> n)"
-text{*\noindent
-This \isacommand{instance} declaration can be read like the declaration of
-a function on types. The constructor @{text list} maps types of class @{text
-type} (all HOL types), to types of class @{text ordrel};
-in other words,
-if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
-Of course we should also define the meaning of @{text <<=} and
-@{text <<} on lists:
-*}
+text {* \noindent Note that the name @{const [source] plus} carries a
+suffix @{text "_nat"}; by default, the local name of a class operation
+@{text f} to be instantiated on type constructor @{text \<kappa>} is mangled
+as @{text f_\<kappa>}. In case of uncertainty, these names may be inspected
+using the @{command "print_context"} command or the corresponding
+ProofGeneral button.
+
+Although class @{class [source] plus} has no axioms, the instantiation must be
+formally concluded by a (trivial) instantiation proof ``..'': *}
+
+instance ..
+
+text {* \noindent More interesting \isacommand{instance} proofs will
+arise below.
+
+The instantiation is finished by an explicit *}
+
+end
-defs (overloaded)
-prefix_def:
- "xs <<= (ys::'a list) \<equiv> \<exists>zs. ys = xs@zs"
-strict_prefix_def:
- "xs << (ys::'a list) \<equiv> xs <<= ys \<and> xs \<noteq> ys"
+text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
+legal. *}
+
+instantiation "*" :: (plus, plus) plus
+begin
+
+text {* \noindent Here we instantiate the product type @{type "*"} to
+class @{class [source] plus}, given that its type arguments are of
+class @{class [source] plus}: *}
+
+fun plus_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b" where
+ "(x, y) \<oplus> (w, z) = (x \<oplus> w, y \<oplus> z)"
+
+text {* \noindent Obviously, overloaded specifications may include
+recursion over the syntactic structure of types. *}
+
+instance ..
+
+end
+
+text {* \noindent This way we have encoded the canonical lifting of
+binary operations to products by means of type classes. *}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading0.thy Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*<*)theory Overloading0 imports Main begin(*>*)
-
-text{* We start with a concept that is required for type classes but already
-useful on its own: \emph{overloading}. Isabelle allows overloading: a
-constant may have multiple definitions at non-overlapping types. *}
-
-subsubsection{*An Initial Example*}
-
-text{*
-If we want to introduce the notion of an \emph{inverse} for arbitrary types we
-give it a polymorphic type *}
-
-consts inverse :: "'a \<Rightarrow> 'a"
-
-text{*\noindent
-and provide different definitions at different instances:
-*}
-
-defs (overloaded)
-inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
-inverse_set: "inverse(A::'a set) \<equiv> -A"
-inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
-
-text{*\noindent
-Isabelle will not complain because the three definitions do not overlap: no
-two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
-common instance. What is more, the recursion in @{thm[source]inverse_pair} is
-benign because the type of @{term[source]inverse} becomes smaller: on the
-left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
-@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
-the definitions do intentionally define @{term[source]inverse} only at
-instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses
-warnings to that effect.
-
-However, there is nothing to prevent the user from forming terms such as
-@{text"inverse []"} and proving theorems such as @{text"inverse []
-= inverse []"} when inverse is not defined on lists. Proving theorems about
-unspecified constants does not endanger soundness, but it is pointless.
-To prevent such terms from even being formed requires the use of type classes.
-*}
-(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading1.thy Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*<*)theory Overloading1 imports Main begin(*>*)
-
-subsubsection{*Controlled Overloading with Type Classes*}
-
-text{*
-We now start with the theory of ordering relations, which we shall phrase
-in terms of the two binary symbols @{text"<<"} and @{text"<<="}
-to avoid clashes with @{text"<"} and @{text"<="} in theory @{text
-Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
-introduce the class @{text ordrel}:
-*}
-
-axclass ordrel < type
-
-text{*\noindent
-This introduces a new class @{text ordrel} and makes it a subclass of
-the predefined class @{text type}, which
-is the class of all HOL types.
-This is a degenerate form of axiomatic type class without any axioms.
-Its sole purpose is to restrict the use of overloaded constants to meaningful
-instances:
-*}
-
-consts lt :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<" 50)
- le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<=" 50)
-
-text{*\noindent
-Note that only one occurrence of a type variable in a type needs to be
-constrained with a class; the constraint is propagated to the other
-occurrences automatically.
-
-So far there are no types of class @{text ordrel}. To breathe life
-into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
-@{text ordrel}:
-*}
-
-instance bool :: ordrel
-
-txt{*\noindent
-Command \isacommand{instance} actually starts a proof, namely that
-@{typ bool} satisfies all axioms of @{text ordrel}.
-There are none, but we still need to finish that proof, which we do
-by invoking the \methdx{intro_classes} method:
-*}
-
-by intro_classes
-
-text{*\noindent
-More interesting \isacommand{instance} proofs will arise below
-in the context of proper axiomatic type classes.
-
-Although terms like @{prop"False <<= P"} are now legal, we still need to say
-what the relation symbols actually mean at type @{typ bool}:
-*}
-
-defs (overloaded)
-le_bool_def: "P <<= Q \<equiv> P \<longrightarrow> Q"
-lt_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
-
-text{*\noindent
-Now @{prop"False <<= P"} is provable:
-*}
-
-lemma "False <<= P"
-by(simp add: le_bool_def)
-
-text{*\noindent
-At this point, @{text"[] <<= []"} is not even well-typed.
-To make it well-typed,
-we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading2.thy Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*<*)theory Overloading2 imports Overloading1 begin(*>*)
-
-text{*
-Of course this is not the only possible definition of the two relations.
-Componentwise comparison of lists of equal length also makes sense. This time
-the elements of the list must also be of class @{text ordrel} to permit their
-comparison:
-*}
-
-instance list :: (ordrel)ordrel
-by intro_classes
-
-defs (overloaded)
-le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
- size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
-
-text{*\noindent
-The infix function @{text"!"} yields the nth element of a list, starting with 0.
-
-\begin{warn}
-A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of @{text list} must
-reside in separate theories with disjoint scopes.
-\end{warn}
-*}
-
-subsubsection{*Predefined Overloading*}
-
-text{*
-HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
-defined on all numeric types and sometimes on other types as well, for example
-$-$ and @{text"\<le>"} on sets.
-
-In addition there is a special syntax for bounded quantifiers:
-\begin{center}
-\begin{tabular}{lcl}
-@{prop"\<forall>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<forall>x. x \<le> y \<longrightarrow> P x"} \\
-@{prop"\<exists>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<exists>x. x \<le> y \<and> P x"}
-\end{tabular}
-\end{center}
-And analogously for @{text"<"} instead of @{text"\<le>"}.
-*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/ROOT.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/ROOT.ML Wed Jun 17 16:56:15 2009 -0700
@@ -1,9 +1,10 @@
-(* ID: $Id$ *)
+
+no_document use_thy "Setup";
+
use "../settings.ML";
use_thy "Numbers";
use_thy "Pairs";
use_thy "Records";
use_thy "Typedefs";
-use_thy "Overloading0";
-use_thy "Overloading2";
+use_thy "Overloading";
use_thy "Axioms";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Setup.thy Wed Jun 17 16:56:15 2009 -0700
@@ -0,0 +1,8 @@
+theory Setup
+imports Main
+uses
+ "../../antiquote_setup.ML"
+ "../../more_antiquote.ML"
+begin
+
+end
\ No newline at end of file
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 16:56:15 2009 -0700
@@ -20,70 +20,49 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Attaching axioms to our classes lets us reason on the
-level of classes. The results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our ordering relations.%
+Attaching axioms to our classes lets us reason on the level of
+classes. The results will be applicable to all types in a class, just
+as in axiomatic mathematics.
+
+\begin{warn}
+Proofs in this section use structured \emph{Isar} proofs, which are not
+covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
+\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Partial Orders%
+\isamarkupsubsubsection{Semigroups%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{partial order} is a subclass of \isa{ordrel}
-where certain axioms need to hold:%
+We specify \emph{semigroups} as subclass of \isa{plus}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ parord\ {\isacharless}\ ordrel\isanewline
-refl{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isachardoublequoteclose}\isanewline
-antisym{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}le{\isacharcolon}\ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{class}\isamarkupfalse%
+\ semigroup\ {\isacharequal}\ plus\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent
-The first three axioms are the familiar ones, and the final one
-requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
-Note that behind the scenes, Isabelle has restricted the axioms to class
-\isa{parord}. For example, the axiom \isa{refl} really is
-\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
+\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification requires that
+all instances of \isa{semigroup} obey \hyperlink{fact.assoc:}{\mbox{\isa{assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isacharprime}a{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}}.
-We have not made \isa{lt{\isacharunderscore}le} a global definition because it would
-fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
-never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of our choice is that
-we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
-
-We can now prove simple theorems in this abstract setting, for example
-that \isa{{\isacharless}{\isacharless}} is not symmetric:%
+We can use this class axiom to derive further abstract theorems
+relative to class \isa{semigroup}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}%
+\ assoc{\isacharunderscore}left{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline
+%
\isadelimproof
-%
+\ \ %
\endisadelimproof
%
\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the
-simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
-would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
-a nonterminating rewrite rule.
-(It would be used to try to prove its own precondition \emph{ad
- infinitum}.)
-In the form above, the rule is useful.
-The type constraint is necessary because otherwise Isabelle would only assume
-\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}),
-when the proposition is not a theorem. The proof is easy:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le\ antisym{\isacharparenright}%
+\isacommand{using}\isamarkupfalse%
+\ assoc\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ sym{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
@@ -92,116 +71,262 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-We could now continue in this vein and develop a whole theory of
-results about partial orders. Eventually we will want to apply these results
-to concrete types, namely the instances of the class. Thus we first need to
-prove that the types in question, for example \isa{bool}, are indeed
-instances of \isa{parord}:%
+\noindent The \isa{semigroup} constraint on type \isa{{\isacharprime}a} restricts instantiations of \isa{{\isacharprime}a} to types of class
+\isa{semigroup} and during the proof enables us to use the fact
+\hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class
+\isa{semigroup}. The main advantage of classes is that theorems
+can be proved in the abstract and freely reused for each instance.
+
+On instantiation, we have to give a proof that the given operations
+obey the class axioms:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent The proof opens with a default proof step, which for
+instance judgements invokes method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{fix}\isamarkupfalse%
+\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}\ {\isasymoplus}\ q\ {\isacharequal}\ m\ {\isasymoplus}\ {\isacharparenleft}n\ {\isasymoplus}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Again, the interesting things enter the stage with
+parametric types:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymoplus}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymoplus}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ p\isactrlisub {\isadigit{1}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ cases\ p\isactrlisub {\isadigit{3}}{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}%
\begin{isamarkuptxt}%
-\noindent
-This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
-specialized to type \isa{bool}, as subgoals:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
-\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
-\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
-\end{isabelle}
-Fortunately, the proof is easy for \isa{blast}
-once we have unfolded the definitions
-of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
+\noindent Associativity of product semigroups is established
+using the hypothetical associativity \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} of the type
+components, which holds due to the \isa{semigroup} constraints
+imposed on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
+Indeed, this pattern often occurs with parametric types and type
+classes.%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}%
+\isacommand{qed}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Monoids%
+}
+\isamarkuptrue%
%
\begin{isamarkuptext}%
-\noindent
-Can you figure out why we have to include \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}?
-
-We can now apply our single lemma above in the context of booleans:%
+We define a subclass \isa{monoidl} (a semigroup with a
+left-hand neutral) by extending \isa{semigroup} with one additional
+parameter \isa{neutral} together with its property:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isacommand{class}\isamarkupfalse%
+\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Again, we prove some instances, by providing
+suitable parameter definitions and proofs for the additional
+specifications.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
%
\isadelimproof
-%
+\ %
\endisadelimproof
%
\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ simp%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent
-The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules.
-The main advantage of the axiomatic method is that
-theorems can be proved in the abstract and freely reused for each instance.%
+\noindent In contrast to the examples above, we here have both
+specification of class operations and a non-trivial instance proof.
+
+This covers products as well:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymzero}\ {\isacharequal}\ {\isacharparenleft}{\isasymzero}{\isacharcomma}\ {\isasymzero}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymzero}\ {\isasymoplus}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ p{\isacharparenright}\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ neutl{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent Fully-fledged monoids are modelled by another
+subclass which does not add new parameters but tightens the
+specification:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
+\ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isasymzero}\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Corresponding instances for \isa{nat} and products
+are left as an exercise to the reader.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsubsection{Linear Orders%
+\isamarkupsubsubsection{Groups%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-If any two elements of a partial order are comparable it is a
-\textbf{linear} or \textbf{total} order:%
+\noindent To finish our small algebra example, we add a \isa{group} class:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ linord\ {\isacharless}\ parord\isanewline
-linear{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequoteclose}%
+\isacommand{class}\isamarkupfalse%
+\ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ inv\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymdiv}\ {\isacharunderscore}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{1}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent
-By construction, \isa{linord} inherits all axioms from \isa{parord}.
-Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}}
-as follows:%
+\noindent We continue with a further example for abstract
+proofs relative to type classes:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
+\ left{\isacharunderscore}cancel{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{done}\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymdiv}\ x\ {\isasymoplus}\ x{\isacharparenright}\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ invl\ neutl{\isacharparenright}\isanewline
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ y\ {\isacharequal}\ x\ {\isasymoplus}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -211,65 +336,37 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Linear orders are an example of subclassing\index{subclasses}
-by construction, which is the most
-common case. Subclass relationships can also be proved.
-This is the topic of the following
-paragraph.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Strict Orders%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
-\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ strord\ {\isacharless}\ ordrel\isanewline
-irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}trans{\isacharcolon}\ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z{\isachardoublequoteclose}\isanewline
-le{\isacharunderscore}less{\isacharcolon}\ \ \ \ {\isachardoublequoteopen}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-It is well known that partial orders are the same as strict orders. Let us
-prove one direction, namely that partial orders are a subclass of strict
-orders.%
+\noindent Any \isa{group} is also a \isa{monoid}; this
+can be made explicit by claiming an additional subclass relation,
+together with a proof of the logical difference:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
-\ parord\ {\isacharless}\ strord\isanewline
+\ group\ {\isasymsubseteq}\ monoid\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
-\isacommand{apply}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\begin{isamarkuptxt}%
-\noindent
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
-\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
-type\ variables{\isacharcolon}\isanewline
-\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
-\end{isabelle}
-Because of \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
-are easily proved:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\ \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ lt{\isacharunderscore}le{\isacharparenright}\isanewline
-\ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
-\isacommand{done}\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ x\isanewline
+\ \ \isacommand{from}\isamarkupfalse%
+\ invl\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ x\ {\isacharequal}\ {\isasymzero}{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymdiv}\ x\ {\isasymoplus}\ {\isacharparenleft}x\ {\isasymoplus}\ {\isasymzero}{\isacharparenright}\ {\isacharequal}\ {\isasymdiv}\ x\ {\isasymoplus}\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl\ invl\ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymoplus}\ {\isasymzero}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ left{\isacharunderscore}cancel{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
@@ -279,66 +376,40 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-The subclass relation must always be acyclic. Therefore Isabelle will
-complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Multiple Inheritance and Sorts%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A class may inherit from more than one direct superclass. This is called
-\bfindex{multiple inheritance}. For example, we could define
-the classes of well-founded orderings and well-orderings:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ wford\ {\isacharless}\ parord\isanewline
-wford{\isacharcolon}\ {\isachardoublequoteopen}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford%
-\begin{isamarkuptext}%
-\noindent
-The last line expresses the usual definition: a well-ordering is a linear
-well-founded ordering. The result is the subclass diagram in
+\noindent The proof result is propagated to the type system,
+making \isa{group} an instance of \isa{monoid} by adding an
+additional edge to the graph of subclass relation; see also
Figure~\ref{fig:subclass}.
\begin{figure}[htbp]
-\[
-\begin{array}{r@ {}r@ {}c@ {}l@ {}l}
-& & \isa{type}\\
-& & |\\
-& & \isa{ordrel}\\
-& & |\\
-& & \isa{strord}\\
-& & |\\
-& & \isa{parord} \\
-& / & & \backslash \\
-\isa{linord} & & & & \isa{wford} \\
-& \backslash & & / \\
-& & \isa{wellord}
-\end{array}
-\]
-\caption{Subclass Diagram}
-\label{fig:subclass}
-\end{figure}
-
-Since class \isa{wellord} does not introduce any new axioms, it can simply
-be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
-the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
-represents the intersection of the $C@i$. Such an expression is called a
-\textbf{sort},\index{sorts} and sorts can appear in most places where we have only shown
-classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
-In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
-However, we do not pursue this rarefied concept further.
-
-This concludes our demonstration of type classes based on orderings. We
-remind our readers that \isa{Main} contains a theory of
-orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
-If possible, base your own ordering relations on this theory.%
+ \begin{center}
+ \small
+ \unitlength 0.6mm
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){\isa{semigroup}}}
+ \put(20,40){\makebox(0,0){\isa{monoidl}}}
+ \put(00,20){\makebox(0,0){\isa{monoid}}}
+ \put(40,00){\makebox(0,0){\isa{group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(25,35){\vector(1,-3){10}}
+ \end{picture}
+ \hspace{8em}
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){\isa{semigroup}}}
+ \put(20,40){\makebox(0,0){\isa{monoidl}}}
+ \put(00,20){\makebox(0,0){\isa{monoid}}}
+ \put(40,00){\makebox(0,0){\isa{group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(05,15){\vector(3,-1){30}}
+ \end{picture}
+ \caption{Subclass relationship of monoids and groups:
+ before and after establishing the relationship
+ \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
+ \label{fig:subclass}
+ \end{center}
+\end{figure}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -347,24 +418,53 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The reader may be wondering what happens if we
-attach an inconsistent set of axioms to a class. So far we have always
-avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
+The reader may be wondering what happens if we attach an
+inconsistent set of axioms to a class. So far we have always avoided
+to add new axioms to HOL for fear of inconsistencies and suddenly it
seems that we are throwing all caution to the wind. So why is there no
problem?
-The point is that by construction, all type variables in the axioms of an
-\isacommand{axclass} are automatically constrained with the class being
-defined (as shown for axiom \isa{refl} above). These constraints are
-always carried around and Isabelle takes care that they are never lost,
-unless the type variable is instantiated with a type that has been shown to
-belong to that class. Thus you may be able to prove \isa{False}
-from your axioms, but Isabelle will remind you that this
-theorem has the hidden hypothesis that the class is non-empty.
+The point is that by construction, all type variables in the axioms of
+a \isacommand{class} are automatically constrained with the class
+being defined (as shown for axiom \isa{refl} above). These
+constraints are always carried around and Isabelle takes care that
+they are never lost, unless the type variable is instantiated with a
+type that has been shown to belong to that class. Thus you may be able
+to prove \isa{False} from your axioms, but Isabelle will remind you
+that this theorem has the hidden hypothesis that the class is
+non-empty.
-Even if each individual class is consistent, intersections of (unrelated)
-classes readily become inconsistent in practice. Now we know this need not
-worry us.%
+Even if each individual class is consistent, intersections of
+(unrelated) classes readily become inconsistent in practice. Now we
+know this need not worry us.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Syntactic Classes and Predefined Overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In our algebra example, we have started with a \emph{syntactic
+class} \isa{plus} which only specifies operations but no axioms; it
+would have been also possible to start immediately with class \isa{semigroup}, specifying the \isa{{\isasymoplus}} operation and associativity at
+the same time.
+
+Which approach is more appropriate depends. Usually it is more
+convenient to introduce operations and axioms in the same class: then
+the type checker will automatically insert the corresponding class
+constraints whenever the operations occur, reducing the need of manual
+annotations. However, when operations are decorated with popular
+syntax, syntactic classes can be an option to re-use the syntax in
+different contexts; this is indeed the way most overloaded constants
+in HOL are introduced, of which the most important are listed in
+Table~\ref{tab:overloading} in the appendix. Section
+\ref{sec:numeric-classes} covers a range of corresponding classes
+\emph{with} axioms.
+
+Further note that classes may contain axioms but \emph{no} operations.
+An example is class \isa{finite} from theory \hyperlink{theory.Finite-Set}{\mbox{\isa{Finite{\isacharunderscore}Set}}}
+which specifies a type to be finite: \isa{{\isachardoublequote}finite\ {\isacharparenleft}UNIV\ {\isasymColon}\ {\isacharprime}a{\isasymColon}finite\ set{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Jun 17 16:56:15 2009 -0700
@@ -257,7 +257,7 @@
\rulename{mod_mult2_eq}
\begin{isabelle}%
-{\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
+c\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
\end{isabelle}
\rulename{div_mult_mult1}
@@ -607,17 +607,17 @@
\rulename{abs_triangle_ineq}
\begin{isabelle}%
-a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharequal}\ a\ {\isacharcircum}\ m\ {\isacharasterisk}\ a\ {\isacharcircum}\ n%
+a\isactrlbsup m\ {\isacharplus}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \ {\isacharasterisk}\ a\isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_add}
\begin{isabelle}%
-a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}\ n%
+a\isactrlbsup m\ {\isacharasterisk}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_mult}
\begin{isabelle}%
-{\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
+{\isasymbar}a\isactrlbsup n\isactrlesup {\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\isactrlbsup n\isactrlesup %
\end{isabelle}
\rulename{power_abs}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 16:56:15 2009 -0700
@@ -14,16 +14,69 @@
\isadelimtheory
%
\endisadelimtheory
+%
+\begin{isamarkuptext}%
+Type classes allow \emph{overloading}; thus a constant may
+have multiple definitions at non-overlapping types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Overloading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We can introduce a binary infix addition operator \isa{{\isasymotimes}}
+for arbitrary types by means of a type class:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{class}\isamarkupfalse%
+\ plus\ {\isacharequal}\isanewline
+\ \ \isakeyword{fixes}\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent This introduces a new class \isa{plus},
+along with a constant \isa{plus} with nice infix syntax.
+\isa{plus} is also named \emph{class operation}. The type
+of \isa{plus} carries a class constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class
+\isa{plus} can be instantiated for \isa{{\isachardoublequote}{\isacharprime}a{\isachardoublequote}}.
+To breathe life into \isa{plus} we need to declare a type
+to be an \bfindex{instance} of \isa{plus}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ plus\isanewline
+\isakeyword{begin}%
+\begin{isamarkuptext}%
+\noindent Command \isacommand{instantiation} opens a local
+theory context. Here we can now instantiate \isa{plus} on
+\isa{nat}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ plus{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymoplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymoplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymoplus}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Note that the name \isa{plus} carries a
+suffix \isa{{\isacharunderscore}nat}; by default, the local name of a class operation
+\isa{f} to be instantiated on type constructor \isa{{\isasymkappa}} is mangled
+as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty, these names may be inspected
+using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command or the corresponding
+ProofGeneral button.
+
+Although class \isa{plus} has no axioms, the instantiation must be
+formally concluded by a (trivial) instantiation proof ``..'':%
+\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
%
\isadelimproof
-%
+\ %
\endisadelimproof
%
\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
\endisatagproof
{\isafoldproof}%
%
@@ -32,21 +85,60 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent
-This \isacommand{instance} declaration can be read like the declaration of
-a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel};
-in other words,
-if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
-Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
-\isa{{\isacharless}{\isacharless}} on lists:%
+\noindent More interesting \isacommand{instance} proofs will
+arise below.
+
+The instantiation is finished by an explicit%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent From now on, terms like \isa{Suc\ {\isacharparenleft}m\ {\isasymoplus}\ {\isadigit{2}}{\isacharparenright}} are
+legal.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\isakeyword{begin}%
+\begin{isamarkuptext}%
+\noindent Here we instantiate the product type \isa{{\isacharasterisk}} to
+class \isa{plus}, given that its type arguments are of
+class \isa{plus}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequoteclose}\isanewline
-strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ plus{\isacharunderscore}prod\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymoplus}\ {\isacharparenleft}w{\isacharcomma}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymoplus}\ w{\isacharcomma}\ y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent Obviously, overloaded specifications may include
+recursion over the syntactic structure of types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{instance}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\noindent This way we have encoded the canonical lifting of
+binary operations to products by means of type classes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{0}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-We start with a concept that is required for type classes but already
-useful on its own: \emph{overloading}. Isabelle allows overloading: a
-constant may have multiple definitions at non-overlapping types.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{An Initial Example%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If we want to introduce the notion of an \emph{inverse} for arbitrary types we
-give it a polymorphic type%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-and provide different definitions at different instances:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequoteclose}\isanewline
-inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequoteopen}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequoteclose}\isanewline
-inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-Isabelle will not complain because the three definitions do not overlap: no
-two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
-common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
-benign because the type of \isa{inverse} becomes smaller: on the
-left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
-\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
-the definitions do intentionally define \isa{inverse} only at
-instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses
-warnings to that effect.
-
-However, there is nothing to prevent the user from forming terms such as
-\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about
-unspecified constants does not endanger soundness, but it is pointless.
-To prevent such terms from even being formed requires the use of type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,139 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{1}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsubsubsection{Controlled Overloading with Type Classes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We now start with the theory of ordering relations, which we shall phrase
-in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
-to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
-introduce the class \isa{ordrel}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ ordrel\ {\isacharless}\ type%
-\begin{isamarkuptext}%
-\noindent
-This introduces a new class \isa{ordrel} and makes it a subclass of
-the predefined class \isa{type}, which
-is the class of all HOL types.
-This is a degenerate form of axiomatic type class without any axioms.
-Its sole purpose is to restrict the use of overloaded constants to meaningful
-instances:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\ lt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isachardoublequoteclose}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ le\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent
-Note that only one occurrence of a type variable in a type needs to be
-constrained with a class; the constraint is propagated to the other
-occurrences automatically.
-
-So far there are no types of class \isa{ordrel}. To breathe life
-into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
-\isa{ordrel}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-Command \isacommand{instance} actually starts a proof, namely that
-\isa{bool} satisfies all axioms of \isa{ordrel}.
-There are none, but we still need to finish that proof, which we do
-by invoking the \methdx{intro_classes} method:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-More interesting \isacommand{instance} proofs will arise below
-in the context of proper axiomatic type classes.
-
-Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say
-what the relation symbols actually mean at type \isa{bool}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequoteclose}\isanewline
-lt{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed.
-To make it well-typed,
-we need to make lists a type of class \isa{ordrel}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jun 17 16:55:01 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading{\isadigit{2}}}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-Of course this is not the only possible definition of the two relations.
-Componentwise comparison of lists of equal length also makes sense. This time
-the elements of the list must also be of class \isa{ordrel} to permit their
-comparison:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{by}\isamarkupfalse%
-\ intro{\isacharunderscore}classes%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list, starting with 0.
-
-\begin{warn}
-A type constructor can be instantiated in only one way to
-a given type class. For example, our two instantiations of \isa{list} must
-reside in separate theories with disjoint scopes.
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Predefined Overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-HOL comes with a number of overloaded constants and corresponding classes.
-The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
-defined on all numeric types and sometimes on other types as well, for example
-$-$ and \isa{{\isasymle}} on sets.
-
-In addition there is a special syntax for bounded quantifiers:
-\begin{center}
-\begin{tabular}{lcl}
-\isa{{\isasymforall}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} \\
-\isa{{\isasymexists}x{\isasymle}y{\isachardot}\ P\ x} & \isa{{\isasymrightleftharpoons}} & \isa{{\isachardoublequote}{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x{\isachardoublequote}}
-\end{tabular}
-\end{center}
-And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 16:56:15 2009 -0700
@@ -1,4 +1,3 @@
-% $Id$
\section{Numbers}
\label{sec:numbers}
@@ -12,7 +11,7 @@
\isa{int} of \textbf{integers}, which lack induction but support true
subtraction. With subtraction, arithmetic reasoning is easier, which makes
the integers preferable to the natural numbers for
-complicated arithmetic expressions, even if they are non-negative. The logic HOL-Complex also has the types
+complicated arithmetic expressions, even if they are non-negative. There are also the types
\isa{rat}, \isa{real} and \isa{complex}: the rational, real and complex numbers. Isabelle has no
subtyping, so the numeric
types are distinct and there are functions to convert between them.
@@ -82,14 +81,14 @@
\end{warn}
\begin{warn}
-\index{recdef@\isacommand {recdef} (command)!and numeric literals}
+\index{function@\isacommand {function} (command)!and numeric literals}
Numeric literals are not constructors and therefore
must not be used in patterns. For example, this declaration is
rejected:
\begin{isabelle}
-\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
+\isacommand{function}\ h\ \isakeyword{where}\isanewline
"h\ 3\ =\ 2"\isanewline
-"h\ i\ \ =\ i"
+\isacharbar "h\ i\ \ =\ i"
\end{isabelle}
You should use a conditional expression instead:
@@ -107,7 +106,7 @@
beginning. Hundreds of theorems about the natural numbers are
proved in the theories \isa{Nat} and \isa{Divides}.
Basic properties of addition and multiplication are available through the
-axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
+axiomatic type class for semirings (\S\ref{sec:numeric-classes}).
\subsubsection{Literals}
\index{numeric literals!for type \protect\isa{nat}}%
@@ -242,7 +241,7 @@
proving inequalities involving integer multiplication and division, similar
to those shown above for type~\isa{nat}. The laws of addition, subtraction
and multiplication are available through the axiomatic type class for rings
-(\S\ref{sec:numeric-axclasses}).
+(\S\ref{sec:numeric-classes}).
The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
defined for all types that involve negative numbers, including the integers.
@@ -337,8 +336,7 @@
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
upper bound. (It could only be $\surd2$, which is irrational.) The
formalization of completeness, which is complicated,
-can be found in theory \texttt{RComplete} of directory
-\texttt{Real}.
+can be found in theory \texttt{RComplete}.
Numeric literals\index{numeric literals!for type \protect\isa{real}}
for type \isa{real} have the same syntax as those for type
@@ -354,15 +352,13 @@
is performed.
\begin{warn}
-Type \isa{real} is only available in the logic HOL-Complex, which is
-HOL extended with a definitional development of the real and complex
+Types \isa{rat}, \isa{real} and \isa{complex} are provided by theory HOL-Complex, which is
+Main extended with a definitional development of the rational, real and complex
numbers. Base your theory upon theory \thydx{Complex_Main}, not the
-usual \isa{Main}, and set the Proof General menu item \pgmenu{Isabelle} $>$
-\pgmenu{Logics} $>$ \pgmenu{HOL-Complex}.%
-\index{real numbers|)}\index{*real (type)|)}
+usual \isa{Main}.%
\end{warn}
-Also available in HOL-Complex is the
+Available in the logic HOL-NSA is the
theory \isa{Hyperreal}, which define the type \tydx{hypreal} of
\rmindex{non-standard reals}. These
\textbf{hyperreals} include infinitesimals, which represent infinitely
@@ -379,7 +375,7 @@
\index{complex numbers|)}\index{*complex (type)|)}
-\subsection{The Numeric Type Classes}\label{sec:numeric-axclasses}
+\subsection{The Numeric Type Classes}\label{sec:numeric-classes}
Isabelle/HOL organises its numeric theories using axiomatic type classes.
Hundreds of basic properties are proved in the theory \isa{Ring_and_Field}.
@@ -534,7 +530,7 @@
\subsubsection{Raising to a Power}
-Another type class, \tcdx{ringppower}, specifies rings that also have
+Another type class, \tcdx{ordered\_idom}, specifies rings that also have
exponentation to a natural number power, defined using the obvious primitive
recursion. Theory \thydx{Power} proves various theorems, such as the
following.
--- a/doc-src/TutorialI/Types/types.tex Wed Jun 17 16:55:01 2009 -0700
+++ b/doc-src/TutorialI/Types/types.tex Wed Jun 17 16:56:15 2009 -0700
@@ -6,7 +6,8 @@
(\isacommand{datatype}). This chapter will introduce more
advanced material:
\begin{itemize}
-\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
and how to reason about them.
+\item Pairs ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}),
+and how to reason about them.
\item Type classes: how to specify and reason about axiomatic collections of
types ({\S}\ref{sec:axclass}). This section leads on to a discussion of
Isabelle's numeric types ({\S}\ref{sec:numbers}).
@@ -15,7 +16,10 @@
({\S}\ref{sec:adv-typedef}).
\end{itemize}
-The material in this section goes beyond the needs of most novices.
Serious users should at least skim the sections as far as type classes.
That material is fairly advanced; read the beginning to understand what it
is about, but consult the rest only when necessary.
+The material in this section goes beyond the needs of most novices.
+Serious users should at least skim the sections as far as type classes.
+That material is fairly advanced; read the beginning to understand what it
+is about, but consult the rest only when necessary.
\index{pairs and tuples|(}
\input{Types/document/Pairs} %%%Section "Pairs and Tuples"
@@ -24,48 +28,41 @@
\input{Types/document/Records} %%%Section "Records"
-\section{Axiomatic Type Classes} %%%Section
+\section{Type Classes} %%%Section
\label{sec:axclass}
\index{axiomatic type classes|(}
\index{*axclass|(}
-The programming language Haskell has popularized the notion of type classes.
-In its simplest form, a type class is a set of types with a common interface:
-all types in that class must provide the functions in the interface.
-Isabelle offers the related concept of an \textbf{axiomatic type class}.
-Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
-an axiomatic specification of a class of types. Thus we can talk about a type
-$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if
-$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $D$ being a
-\textbf{subclass}\index{subclasses}
-of a class $C$, written $D < C$. This is the case if all
-axioms of $C$ are also provable in $D$. We introduce these concepts
-by means of a running example, ordering relations.
+The programming language Haskell has popularized the notion of type
+classes: a type class is a set of types with a
+common interface: all types in that class must provide the functions
+in the interface. Isabelle offers a similar type class concept: in
+addition, properties (\emph{class axioms}) can be specified which any
+instance of this type class must obey. Thus we can talk about a type
+$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case
+if $\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
+organized in a hierarchy. Thus there is the notion of a class $D$
+being a subclass\index{subclasses} of a class $C$, written $D
+< C$. This is the case if all axioms of $C$ are also provable in $D$.
-\begin{warn}
-The material in this section describes a low-level approach to type classes.
-It is recommended to use the new \isacommand{class} command instead.
-For details see the appropriate tutorial~\cite{isabelle-classes} and the
-related article~\cite{Haftmann-Wenzel:2006:classes}.
-\end{warn}
-
+In this section we introduce the most important concepts behind type
+classes by means of a running example from algebra. This should give
+you an intuition how to use type classes and to understand
+specifications involving type classes. Type classes are covered more
+deeply in a separate tutorial \cite{isabelle-classes}.
\subsection{Overloading}
\label{sec:overloading}
\index{overloading|(}
-\input{Types/document/Overloading0}
-\input{Types/document/Overloading1}
\input{Types/document/Overloading}
-\input{Types/document/Overloading2}
\index{overloading|)}
\input{Types/document/Axioms}
-\index{axiomatic type classes|)}
-\index{*axclass|)}
+\index{type classes|)}
+\index{*class|)}
\input{Types/numerics} %%%Section "Numbers"
--- a/lib/Tools/usedir Wed Jun 17 16:55:01 2009 -0700
+++ b/lib/Tools/usedir Wed Jun 17 16:56:15 2009 -0700
@@ -31,6 +31,7 @@
echo " -p LEVEL set level of detail for proof objects"
echo " -r reset session path"
echo " -s NAME override session NAME"
+ echo " -t BOOL internal session timing (default false)"
echo " -v BOOL be verbose (default false)"
echo
echo " Build object-logic or run examples. Also creates browsing"
@@ -84,12 +85,13 @@
RESET=false
SESSION=""
PROOFS=0
+TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -158,6 +160,10 @@
s)
SESSION="$OPTARG"
;;
+ t)
+ check_bool "$OPTARG"
+ TIMING="$OPTARG"
+ ;;
v)
check_bool "$OPTARG"
VERBOSE="$OPTARG"
@@ -229,7 +235,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -238,7 +244,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/lib/scripts/polyml-version Wed Jun 17 16:55:01 2009 -0700
+++ b/lib/scripts/polyml-version Wed Jun 17 16:56:15 2009 -0700
@@ -5,13 +5,8 @@
echo -n polyml
if [ -x "$ML_HOME/poly" ]; then
- if [ -x "$ML_HOME/polyimport" ]; then
- env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
- DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
- "$ML_HOME/poly" -v | \
- sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
- else
- "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
- sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
- fi
+ env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
+ DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
+ "$ML_HOME/poly" -v -H 10 | \
+ sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
fi
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jun 17 16:56:15 2009 -0700
@@ -101,8 +101,9 @@
val (_,thy1) =
fold_map (fn ak => fn thy =>
let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
- val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
- val inject_flat = Library.flat inject
+ val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype
+ DatatypeAux.default_datatype_config [ak] [dt] thy
+ val inject_flat = flat inject
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak
--- a/src/HOL/Nominal/nominal_package.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Nominal/nominal_package.ML Wed Jun 17 16:56:15 2009 -0700
@@ -6,8 +6,9 @@
signature NOMINAL_PACKAGE =
sig
- val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
- (bstring * string list * mixfix) list) list -> theory -> theory
+ val add_nominal_datatype : DatatypeAux.datatype_config -> string list ->
+ (string list * bstring * mixfix *
+ (bstring * string list * mixfix) list) list -> theory -> theory
type descr
type nominal_datatype_info
val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -190,7 +191,7 @@
fun fresh_star_const T U =
Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
-fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
let
(* this theory is used just for parsing *)
@@ -243,7 +244,7 @@
val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
val ({induction, ...},thy1) =
- DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
+ DatatypePackage.add_datatype config new_type_names' dts'' thy;
val SOME {descr, ...} = Symtab.lookup
(DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
@@ -815,7 +816,7 @@
val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
in
- (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
+ (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
end;
val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
@@ -1509,7 +1510,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -2067,7 +2068,7 @@
thy13
end;
-val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true;
+val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ;
(* FIXME: The following stuff should be exported by DatatypePackage *)
@@ -2083,7 +2084,7 @@
val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
- in add_nominal_datatype false names specs end;
+ in add_nominal_datatype DatatypeAux.default_datatype_config names specs end;
val _ =
OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
--- a/src/HOL/Product_Type.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Product_Type.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1,5 +1,4 @@
(* Title: HOL/Product_Type.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/HOL/Rational.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Rational.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1048,7 +1048,7 @@
val p' = p div g;
val q' = q div g;
val r = (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ if p' = 0 then 1 else q')
in
(r, fn () => term_of_rat r)
end;
@@ -1060,8 +1060,7 @@
consts_code
"of_int :: int \<Rightarrow> rat" ("\<module>rat'_of'_int")
attach {*
-fun rat_of_int 0 = (0, 0)
- | rat_of_int i = (i, 1);
+fun rat_of_int i = (i, 1);
*}
end
--- a/src/HOL/RealDef.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/RealDef.thy Wed Jun 17 16:56:15 2009 -0700
@@ -1170,7 +1170,7 @@
val p' = p div g;
val q' = q div g;
val r = (if one_of [true, false] then p' else ~ p',
- if p' = 0 then 0 else q')
+ if p' = 0 then 1 else q')
in
(r, fn () => term_of_real r)
end;
@@ -1182,8 +1182,7 @@
consts_code
"of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
attach {*
-fun real_of_int 0 = (0, 0)
- | real_of_int i = (i, 1);
+fun real_of_int i = (i, 1);
*}
end
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Wed Jun 17 16:56:15 2009 -0700
@@ -14,26 +14,29 @@
signature DATATYPE_ABS_PROOFS =
sig
- val prove_casedist_thms : string list ->
- DatatypeAux.descr list -> (string * sort) list -> thm ->
+ type datatype_config = DatatypeAux.datatype_config
+ type descr = DatatypeAux.descr
+ type datatype_info = DatatypeAux.datatype_info
+ val prove_casedist_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list -> thm ->
attribute list -> theory -> thm list * theory
- val prove_primrec_thms : bool -> string list ->
- DatatypeAux.descr list -> (string * sort) list ->
- DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
+ val prove_primrec_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list ->
+ datatype_info Symtab.table -> thm list list -> thm list list ->
simpset -> thm -> theory -> (string list * thm list) * theory
- val prove_case_thms : bool -> string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ val prove_case_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list ->
string list -> thm list -> theory -> (thm list list * string list) * theory
- val prove_split_thms : string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ val prove_split_thms : datatype_config -> string list ->
+ descr list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
(thm * thm) list * theory
- val prove_nchotomys : string list -> DatatypeAux.descr list ->
+ val prove_nchotomys : datatype_config -> string list -> descr list ->
(string * sort) list -> thm list -> theory -> thm list * theory
- val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+ val prove_weak_case_congs : string list -> descr list ->
(string * sort) list -> theory -> thm list * theory
val prove_case_congs : string list ->
- DatatypeAux.descr list -> (string * sort) list ->
+ descr list -> (string * sort) list ->
thm list -> thm list list -> theory -> thm list * theory
end;
@@ -44,9 +47,9 @@
(************************ case distinction theorems ***************************)
-fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
let
- val _ = message "Proving case distinction theorems ...";
+ val _ = message config "Proving case distinction theorems ...";
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -86,13 +89,13 @@
(*************************** primrec combinators ******************************)
-fun prove_primrec_thms flat_names new_type_names descr sorts
+fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
(dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
let
- val _ = message "Constructing primrec combinators ...";
+ val _ = message config "Constructing primrec combinators ...";
val big_name = space_implode "_" new_type_names;
- val thy0 = add_path flat_names big_name thy;
+ val thy0 = add_path (#flat_names config) big_name thy;
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -153,7 +156,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -162,7 +165,7 @@
(* prove uniqueness and termination of primrec combinators *)
- val _ = message "Proving termination and uniqueness of primrec functions ...";
+ val _ = message config "Proving termination and uniqueness of primrec functions ...";
fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
let
@@ -242,13 +245,13 @@
Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
set $ Free ("x", T) $ Free ("y", T'))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
- ||> parent_path flat_names
+ ||> parent_path (#flat_names config)
||> Theory.checkpoint;
(* prove characteristic equations for primrec combinators *)
- val _ = message "Proving characteristic theorems for primrec combinators ..."
+ val _ = message config "Proving characteristic theorems for primrec combinators ..."
val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
(fn _ => EVERY
@@ -272,11 +275,11 @@
(***************************** case combinators *******************************)
-fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
let
- val _ = message "Proving characteristic theorems for case combinators ...";
+ val _ = message config "Proving characteristic theorems for case combinators ...";
- val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
+ val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
@@ -338,7 +341,7 @@
thy2
|> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
o Context.Theory
- |> parent_path flat_names
+ |> parent_path (#flat_names config)
|> store_thmss "cases" new_type_names case_thms
|-> (fn thmss => pair (thmss, case_names))
end;
@@ -346,12 +349,12 @@
(******************************* case splitting *******************************)
-fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
casedist_thms case_thms thy =
let
- val _ = message "Proving equations for case splitting ...";
+ val _ = message config "Proving equations for case splitting ...";
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -395,9 +398,9 @@
(************************* additional theorems for TFL ************************)
-fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
let
- val _ = message "Proving additional theorems for TFL ...";
+ val _ = message config "Proving additional theorems for TFL ...";
fun prove_nchotomy (t, exhaustion) =
let
--- a/src/HOL/Tools/datatype_package/datatype_aux.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Wed Jun 17 16:56:15 2009 -0700
@@ -6,8 +6,9 @@
signature DATATYPE_AUX =
sig
- val quiet_mode : bool ref
- val message : string -> unit
+ type datatype_config
+ val default_datatype_config : datatype_config
+ val message : datatype_config -> string -> unit
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
@@ -67,8 +68,13 @@
structure DatatypeAux : DATATYPE_AUX =
struct
-val quiet_mode = ref false;
-fun message s = if !quiet_mode then () else writeln s;
+(* datatype option flags *)
+
+type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
+val default_datatype_config : datatype_config =
+ { strict = true, flat_names = false, quiet = false };
+fun message ({ quiet, ...} : datatype_config) s =
+ if quiet then () else writeln s;
fun add_path flat_names s = if flat_names then I else Sign.add_path s;
fun parent_path flat_names = if flat_names then I else Sign.parent_path;
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Wed Jun 17 16:56:15 2009 -0700
@@ -426,7 +426,7 @@
(* register a datatype etc. *)
-fun add_all_code dtcos thy =
+fun add_all_code config dtcos thy =
let
val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
@@ -437,7 +437,7 @@
in
if null css then thy
else thy
- |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
+ |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs
--- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 16:56:15 2009 -0700
@@ -6,6 +6,7 @@
signature DATATYPE_PACKAGE =
sig
+ type datatype_config = DatatypeAux.datatype_config
type datatype_info = DatatypeAux.datatype_info
type descr = DatatypeAux.descr
val get_datatypes : theory -> datatype_info Symtab.table
@@ -24,39 +25,23 @@
val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
val read_typ: theory ->
(typ list * (string * sort) list) * string -> typ list * (string * sort) list
- val interpretation : (string list -> theory -> theory) -> theory -> theory
- val rep_datatype : ({distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
- -> theory -> Proof.state;
- val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
- val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
- (binding * typ list * mixfix) list) list -> theory ->
- {distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} * theory
- val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
- (binding * string list * mixfix) list) list -> theory ->
- {distinct : thm list list,
- inject : thm list list,
- exhaustion : thm list,
- rec_thms : thm list,
- case_thms : thm list list,
- split_thms : (thm * thm) list,
- induction : thm,
- simps : thm list} * theory
+ val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+ type rules = {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ simps : thm list}
+ val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
+ -> string list option -> term list -> theory -> Proof.state;
+ val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+ val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+ (binding * typ list * mixfix) list) list -> theory -> rules * theory
+ val add_datatype_cmd : string list -> (string list * binding * mixfix *
+ (binding * string list * mixfix) list) list -> theory -> rules * theory
val setup: theory -> theory
- val quiet_mode : bool ref
val print_datatypes : theory -> unit
end;
@@ -65,8 +50,6 @@
open DatatypeAux;
-val quiet_mode = quiet_mode;
-
(* theory data *)
@@ -358,31 +341,41 @@
case_cong = case_cong,
weak_case_cong = weak_case_cong});
-structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
-val interpretation = DatatypeInterpretation.interpretation;
+type rules = {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ simps : thm list}
+
+structure DatatypeInterpretation = InterpretationFun
+ (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =);
+fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
(******************* definitional introduction of datatypes *******************)
-fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
- val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+ val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
- DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
+ DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
types_syntax constr_syntax case_names_induct;
- val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+ val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
sorts induct case_names_exhausts thy2;
val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
- flat_names new_type_names descr sorts dt_info inject dist_rewrites
+ config new_type_names descr sorts dt_info inject dist_rewrites
(Simplifier.theory_context thy3 dist_ss) induct thy3;
val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
- flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
- val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
+ config new_type_names descr sorts reccomb_names rec_thms thy4;
+ val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
descr sorts inject dist_rewrites casedist_thms case_thms thy6;
- val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
descr sorts casedist_thms thy7;
val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
descr sorts nchotomys case_thms thy8;
@@ -406,7 +399,7 @@
|> add_cases_induct dt_infos induct
|> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
- |> DatatypeInterpretation.data (map fst dt_infos);
+ |> DatatypeInterpretation.data (config, map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -421,7 +414,7 @@
(*********************** declare existing type as datatype *********************)
-fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
let
val ((_, [induct']), _) =
Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -440,19 +433,19 @@
val (case_names_induct, case_names_exhausts) =
(mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
- val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+ val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
val (casedist_thms, thy2) = thy |>
- DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
+ DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
case_names_exhausts;
val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
- false new_type_names [descr] sorts dt_info inject distinct
+ config new_type_names [descr] sorts dt_info inject distinct
(Simplifier.theory_context thy2 dist_ss) induct thy2;
- val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
- new_type_names [descr] sorts reccomb_names rec_thms thy3;
+ val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
+ config new_type_names [descr] sorts reccomb_names rec_thms thy3;
val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
- new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
- val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
+ val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
[descr] sorts casedist_thms thy5;
val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
[descr] sorts nchotomys case_thms thy6;
@@ -482,7 +475,7 @@
|> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
- |> DatatypeInterpretation.data (map fst dt_infos);
+ |> DatatypeInterpretation.data (config, map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -494,7 +487,7 @@
simps = simps}, thy11)
end;
-fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
let
fun constr_of_term (Const (c, T)) = (c, T)
| constr_of_term t =
@@ -550,7 +543,7 @@
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
+ (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
#-> after_qed
end;
in
@@ -560,13 +553,13 @@
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
(******************************** add datatype ********************************)
-fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
@@ -598,7 +591,7 @@
val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
- in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+ in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
Sign.full_name_path tmp_thy tname')
(Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
@@ -626,7 +619,7 @@
val dt_info = get_datatypes thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
- if err then error ("Nonemptiness check failed for datatype " ^ s)
+ if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
else raise exn;
val descr' = flat descr;
@@ -634,12 +627,12 @@
val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
in
add_datatype_def
- flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+ (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy
end;
val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ true;
+val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
@@ -668,7 +661,7 @@
(fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
- in snd o add_datatype_cmd false names specs end;
+ in snd o add_datatype_cmd names specs end;
val _ =
OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Wed Jun 17 16:56:15 2009 -0700
@@ -7,7 +7,7 @@
signature DATATYPE_REALIZER =
sig
- val add_dt_realizers: string list -> theory -> theory
+ val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
val setup: theory -> theory
end;
@@ -213,10 +213,10 @@
(exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
end;
-fun add_dt_realizers names thy =
+fun add_dt_realizers config names thy =
if ! Proofterm.proofs < 2 then thy
else let
- val _ = message "Adding realizers for induction and case analysis ..."
+ val _ = message config "Adding realizers for induction and case analysis ..."
val infos = map (DatatypePackage.the_datatype thy) names;
val info :: _ = infos;
in
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Wed Jun 17 16:56:15 2009 -0700
@@ -11,10 +11,13 @@
signature DATATYPE_REP_PROOFS =
sig
+ type datatype_config = DatatypeAux.datatype_config
+ type descr = DatatypeAux.descr
+ type datatype_info = DatatypeAux.datatype_info
val distinctness_limit : int Config.T
val distinctness_limit_setup : theory -> theory
- val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
- string list -> DatatypeAux.descr list -> (string * sort) list ->
+ val representation_proofs : datatype_config -> datatype_info Symtab.table ->
+ string list -> descr list -> (string * sort) list ->
(binding * mixfix) list -> (binding * mixfix) list list -> attribute
-> theory -> (thm list list * thm list list * thm list list *
DatatypeAux.simproc_dist list * thm) * theory
@@ -45,7 +48,7 @@
(******************************************************************************)
-fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
+fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
let
val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
@@ -69,7 +72,7 @@
val descr' = flat descr;
val big_name = space_implode "_" new_type_names;
- val thy1 = add_path flat_names big_name thy;
+ val thy1 = add_path (#flat_names config) big_name thy;
val big_rec_name = big_name ^ "_rep_set";
val rep_set_names' =
(if length descr' = 1 then [big_rec_name] else
@@ -147,7 +150,7 @@
(************** generate introduction rules for representing set **********)
- val _ = message "Constructing representing sets ...";
+ val _ = message config "Constructing representing sets ...";
(* make introduction rule for a single constructor *)
@@ -181,7 +184,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
@@ -190,7 +193,7 @@
(********************************* typedef ********************************)
val (typedefs, thy3) = thy2 |>
- parent_path flat_names |>
+ parent_path (#flat_names config) |>
fold_map (fn ((((name, mx), tvs), c), name') =>
TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
@@ -199,7 +202,7 @@
(resolve_tac rep_intrs 1)))
(types_syntax ~~ tyvars ~~
(Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
- add_path flat_names big_name;
+ add_path (#flat_names config) big_name;
(*********************** definition of constructors ***********************)
@@ -257,19 +260,19 @@
val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
- ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
+ ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
in
- (parent_path flat_names thy', defs', eqns @ [eqns'],
+ (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
rep_congs @ [cong'], dist_lemmas @ [dist])
end;
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
- ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
+ ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
(*********** isomorphisms for new types (introduced by typedef) ***********)
- val _ = message "Proving isomorphism properties ...";
+ val _ = message config "Proving isomorphism properties ...";
val newT_iso_axms = map (fn (_, td) =>
(collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -358,7 +361,7 @@
in (thy', char_thms' @ char_thms) end;
val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
- (add_path flat_names big_name thy4, []) (tl descr));
+ (add_path (#flat_names config) big_name thy4, []) (tl descr));
(* prove isomorphism properties *)
@@ -496,7 +499,7 @@
(******************* freeness theorems for constructors *******************)
- val _ = message "Proving freeness of constructors ...";
+ val _ = message config "Proving freeness of constructors ...";
(* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
@@ -568,13 +571,13 @@
val ((constr_inject', distinct_thms'), thy6) =
thy5
- |> parent_path flat_names
+ |> parent_path (#flat_names config)
|> store_thmss "inject" new_type_names constr_inject
||>> store_thmss "distinct" new_type_names distinct_thms;
(*************************** induction theorem ****************************)
- val _ = message "Proving induction rule for datatypes ...";
+ val _ = message config "Proving induction rule for datatypes ...";
val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
(map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jun 17 16:56:15 2009 -0700
@@ -191,9 +191,7 @@
|> safe_mk_meta_eq)))
thy
-val case_cong = fold add_case_cong
-
-val setup_case_cong = DatatypePackage.interpretation case_cong
+val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
(* setup *)
--- a/src/HOL/Tools/function_package/size.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/function_package/size.ML Wed Jun 17 16:56:15 2009 -0700
@@ -218,7 +218,7 @@
(new_type_names ~~ size_names)) thy''
end;
-fun add_size_thms (new_type_names as name :: _) thy =
+fun add_size_thms config (new_type_names as name :: _) thy =
let
val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
val prefix = Long_Name.map_base_name (K (space_implode "_"
--- a/src/HOL/Tools/inductive_realizer.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Jun 17 16:56:15 2009 -0700
@@ -307,8 +307,8 @@
val ((dummies, dt_info), thy2) =
thy1
- |> add_dummies
- (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
+ |> add_dummies (DatatypePackage.add_datatype
+ { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
(map (pair false) dts) []
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 16:56:15 2009 -0700
@@ -15,7 +15,7 @@
val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
-> string list -> string list * string list -> typ list * typ list
-> string * (term list * (term * term) list)
- val ensure_random_datatype: string list -> theory -> theory
+ val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
val setup: theory -> theory
end;
@@ -320,9 +320,9 @@
val prefix = space_implode "_" (random_auxN :: names);
in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
-fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
let
- val _ = DatatypeAux.message "Creating quickcheck generators ...";
+ val _ = DatatypeAux.message config "Creating quickcheck generators ...";
val i = @{term "i\<Colon>code_numeral"};
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
@@ -356,7 +356,7 @@
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
end handle CLASS_ERROR => NONE;
-fun ensure_random_datatype raw_tycos thy =
+fun ensure_random_datatype config raw_tycos thy =
let
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
@@ -370,7 +370,7 @@
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
- of SOME constrain => mk_random_datatype descr
+ of SOME constrain => mk_random_datatype config descr
(map constrain raw_vs) tycos (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
--- a/src/HOL/Transitive_Closure.thy Wed Jun 17 16:55:01 2009 -0700
+++ b/src/HOL/Transitive_Closure.thy Wed Jun 17 16:56:15 2009 -0700
@@ -294,6 +294,20 @@
lemma rtrancl_unfold: "r^* = Id Un r O r^*"
by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
+lemma rtrancl_Un_separatorE:
+ "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (a,x) : P^* \<longrightarrow> (x,y) : Q \<longrightarrow> x=y \<Longrightarrow> (a,b) : P^*"
+apply (induct rule:rtrancl.induct)
+ apply blast
+apply (blast intro:rtrancl_trans)
+done
+
+lemma rtrancl_Un_separator_converseE:
+ "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*"
+apply (induct rule:converse_rtrancl_induct)
+ apply blast
+apply (blast intro:rtrancl_trans)
+done
+
subsection {* Transitive closure *}
--- a/src/Pure/General/output.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/General/output.ML Wed Jun 17 16:56:15 2009 -0700
@@ -18,7 +18,6 @@
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
val timing: bool ref
- val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
end;
signature OUTPUT =
@@ -47,7 +46,6 @@
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
- val accumulated_time: unit -> unit
end;
structure Output: OUTPUT =
@@ -141,79 +139,9 @@
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-
(*global timing mode*)
val timing = ref false;
-
-(* accumulated timing *)
-
-local
-
-datatype time_info = TI of
- {name: string,
- timer: Timer.cpu_timer,
- sys: Time.time,
- usr: Time.time,
- gc: Time.time,
- count: int};
-
-fun time_init name = ref (TI
- {name = name,
- timer = Timer.startCPUTimer (),
- sys = Time.zeroTime,
- usr = Time.zeroTime,
- gc = Time.zeroTime,
- count = 0});
-
-fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
-
-fun time_check (ref (TI r)) = r;
-
-fun time_add ti f x =
- let
- fun add_diff time time1 time2 =
- Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
- val {name, timer, sys, usr, gc, count} = time_check ti;
- val (sys1, usr1, gc1) = check_timer timer;
- val result = Exn.capture f x;
- val (sys2, usr2, gc2) = check_timer timer;
- in
- ti := TI
- {name = name,
- timer = timer,
- sys = add_diff sys sys1 sys2,
- usr = add_diff usr usr1 usr2,
- gc = add_diff gc gc1 gc2,
- count = count + 1};
- Exn.release result
- end;
-
-fun time_finish ti =
- let
- fun secs prfx time = prfx ^ Time.toString time;
- val {name, timer, sys, usr, gc, count} = time_check ti;
- in
- warning ("Total of " ^ quote name ^ ": " ^
- secs "User " usr ^ secs " GC " gc ^ secs " All " (Time.+ (sys, Time.+ (usr, gc))) ^
- " secs in " ^ string_of_int count ^ " calls");
- time_reset ti
- end;
-
-val time_finish_hooks = ref ([]: (unit -> unit) list);
-
-in
-
-fun time_accumulator name =
- let val ti = time_init name in
- CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
- time_add ti
- end;
-
-fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
-
-end;
-
end;
structure BasicOutput: BASIC_OUTPUT = Output;
--- a/src/Pure/IsaMakefile Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/IsaMakefile Wed Jun 17 16:56:15 2009 -0700
@@ -29,7 +29,8 @@
ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
- ML-Systems/time_limit.ML ML-Systems/universal.ML
+ ML-Systems/timing.ML ML-Systems/time_limit.ML \
+ ML-Systems/universal.ML
RAW: $(OUT)/RAW
--- a/src/Pure/Isar/class.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/Isar/class.ML Wed Jun 17 16:56:15 2009 -0700
@@ -78,7 +78,7 @@
val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
- in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+ in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
val assm_intro = Option.map prove_assm_intro
(fst (Locale.intros_of thy class));
@@ -95,7 +95,7 @@
(Tactic.match_tac (axclass_intro :: sup_of_classes
@ loc_axiom_intros @ base_sort_trivs)
ORELSE' Tactic.assume_tac));
- val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
+ val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
@@ -281,6 +281,7 @@
|> Expression.add_locale bname Binding.empty supexpr elems
|> snd |> LocalTheory.exit_global
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
+ ||> Theory.checkpoint
|-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate thy class sups base_sort param_map assm_axiom)
#-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
--- a/src/Pure/Isar/class_target.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/Isar/class_target.ML Wed Jun 17 16:56:15 2009 -0700
@@ -351,7 +351,7 @@
val c' = Sign.full_name thy b;
val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
val ty' = Term.fastype_of rhs';
- val rhs'' = map_types ((*Type.strip_sorts o *)Logic.varifyT) rhs';
+ val rhs'' = map_types Logic.varifyT rhs';
in
thy
|> Sign.add_abbrev (#1 prmode) pos (b, rhs'')
--- a/src/Pure/Isar/overloading.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/Isar/overloading.ML Wed Jun 17 16:56:15 2009 -0700
@@ -91,12 +91,17 @@
|> mark_passed)
end;
+fun rewrite_liberal thy unchecks t =
+ case try (Pattern.rewrite_term thy unchecks []) t
+ of NONE => NONE
+ | SOME t' => if t aconv t' then NONE else SOME t';
+
fun improve_term_uncheck ts ctxt =
let
val thy = ProofContext.theory_of ctxt;
val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
- val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
- in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
+ val ts' = map (rewrite_liberal thy unchecks) ts;
+ in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
fun set_primary_constraints ctxt =
let
--- a/src/Pure/ML-Systems/mosml.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/ML-Systems/mosml.ML Wed Jun 17 16:56:15 2009 -0700
@@ -154,10 +154,6 @@
val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
in {message = message, user = user, all = all} end;
-fun check_timer timer =
- let val {sys, usr, gc} = Timer.checkCPUTimer timer
- in (sys, usr, gc) end;
-
(* SML basis library fixes *)
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/ML-Systems/polyml_common.ML Wed Jun 17 16:56:15 2009 -0700
@@ -8,6 +8,7 @@
use "ML-Systems/exn.ML";
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_pretty.ML";
use "ML-Systems/use_context.ML";
@@ -41,30 +42,6 @@
val implode = SML90.implode;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(* prompts *)
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
--- a/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Jun 17 16:56:15 2009 -0700
@@ -12,6 +12,7 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/multithreading.ML";
+use "ML-Systems/timing.ML";
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
@@ -59,30 +60,6 @@
end;
-(* compiler-independent timing functions *)
-
-fun start_timing () =
- let
- val timer = Timer.startCPUTimer ();
- val time = Timer.checkCPUTimer timer;
- in (timer, time) end;
-
-fun end_timing (timer, {sys, usr}) =
- let
- open Time; (*...for Time.toString, Time.+ and Time.- *)
- val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
- val user = usr2 - usr;
- val all = user + sys2 - sys;
- val message = "User " ^ toString user ^ " All "^ toString all ^ " secs" handle Time => "";
- in {message = message, user = user, all = all} end;
-
-fun check_timer timer =
- let
- val {sys, usr} = Timer.checkCPUTimer timer;
- val gc = Timer.checkGCTime timer; (* FIXME already included in usr? *)
- in (sys, usr, gc) end;
-
-
(*prompts*)
fun ml_prompts p1 p2 =
(Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/timing.ML Wed Jun 17 16:56:15 2009 -0700
@@ -0,0 +1,32 @@
+(* Title: Pure/ML-Systems/timing.ML
+ Author: Makarius
+
+Compiler-independent timing functions.
+*)
+
+fun start_timing () =
+ let
+ val real_timer = Timer.startRealTimer ();
+ val real_time = Timer.checkRealTimer real_timer;
+ val cpu_timer = Timer.startCPUTimer ();
+ val cpu_times = Timer.checkCPUTimes cpu_timer;
+ in (real_timer, real_time, cpu_timer, cpu_times) end;
+
+fun end_timing (real_timer, real_time, cpu_timer, cpu_times) =
+ let
+ val real_time2 = Timer.checkRealTimer real_timer;
+ val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
+ val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
+ Timer.checkCPUTimes cpu_timer;
+
+ open Time;
+ val elapsed = real_time2 - real_time;
+ val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
+ val cpu = usr2 - usr + sys2 - sys + gc;
+ val gc_percent = Real.fmt (StringCvt.FIX (SOME 1)) (100.0 * toReal gc / toReal cpu);
+ val factor = Real.fmt (StringCvt.FIX (SOME 2)) (toReal cpu / toReal elapsed);
+ val message =
+ (toString elapsed ^ "s elapsed time, " ^ toString cpu ^ "s cpu time, " ^
+ gc_percent ^ "% GC time, factor " ^ factor) handle Time => "";
+ in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end;
+
--- a/src/Pure/System/session.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/System/session.ML Wed Jun 17 16:56:15 2009 -0700
@@ -9,8 +9,9 @@
val id: unit -> string list
val name: unit -> string
val welcome: unit -> string
- val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
- string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
+ val use_dir: string -> string -> bool -> string list -> bool -> bool ->
+ string -> bool -> string list -> string -> string -> bool * string ->
+ string -> int -> bool -> bool -> int -> int -> bool -> unit
val finish: unit -> unit
end;
@@ -72,8 +73,7 @@
(* finish *)
fun finish () =
- (Output.accumulated_time ();
- ThyInfo.finish ();
+ (ThyInfo.finish ();
Present.finish ();
Future.shutdown ();
session_finished := true);
@@ -92,13 +92,20 @@
fun dumping (_, "") = NONE
| dumping (cp, path) = SOME (cp, Path.explode path);
-fun use_dir root build modes reset info doc doc_graph doc_versions
- parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
+fun use_dir item root build modes reset info doc doc_graph doc_versions parent
+ name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
(dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
- use root;
+ if timing then
+ let
+ val start = start_timing ();
+ val _ = use root;
+ val stop = end_timing start;
+ val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+ in () end
+ else use root;
finish ()))
|> setmp_noncritical Proofterm.proofs level
|> setmp_noncritical print_mode (modes @ print_mode_value ())
--- a/src/Pure/Tools/find_consts.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/Tools/find_consts.ML Wed Jun 17 16:56:15 2009 -0700
@@ -25,10 +25,9 @@
| Loose of string
| Name of string;
+
(* matching types/consts *)
-fun add_tye (_, (_, t)) n = Term.size_of_typ t + n;
-
fun matches_subtype thy typat =
let
val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
@@ -51,7 +50,9 @@
fun filter_const _ NONE = NONE
| filter_const f (SOME (c, r)) =
- Option.map (pair c o (curry Int.min r)) (f c);
+ (case f c of
+ NONE => NONE
+ | SOME i => SOME (c, Int.min (r, i)));
(* pretty results *)
@@ -76,6 +77,7 @@
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
+
(* find_consts *)
fun find_consts ctxt raw_criteria =
@@ -85,16 +87,17 @@
val thy = ProofContext.theory_of ctxt;
val low_ranking = 10000;
- fun not_internal consts (nm, _) =
+ fun not_internal consts (nm, _) =
if member (op =) (Consts.the_tags consts nm) Markup.property_internal
then NONE else SOME low_ranking;
fun make_pattern crit =
let
val raw_T = Syntax.parse_typ ctxt crit;
- val t = Syntax.check_term
- (ProofContext.set_mode ProofContext.mode_pattern ctxt)
- (Term.dummy_pattern raw_T);
+ val t =
+ Syntax.check_term
+ (ProofContext.set_mode ProofContext.mode_pattern ctxt)
+ (Term.dummy_pattern raw_T);
in Term.type_of t end;
fun make_match (Strict arg) =
@@ -102,34 +105,34 @@
fn (_, (ty, _)) =>
let
val tye = Sign.typ_match thy (qty, ty) Vartab.empty;
- val sub_size = Vartab.fold add_tye tye 0;
+ val sub_size =
+ Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0;
in SOME sub_size end handle MATCH => NONE
end
-
| make_match (Loose arg) =
check_const (matches_subtype thy (make_pattern arg) o snd)
-
| make_match (Name arg) = check_const (match_string arg o fst);
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit);
val criteria = map make_criterion raw_criteria;
val consts = Sign.consts_of thy;
- val (_, consts_tab) = (#constants o Consts.dest) consts;
- fun eval_entry c = fold filter_const (not_internal consts::criteria)
- (SOME (c, low_ranking));
+ val (_, consts_tab) = #constants (Consts.dest consts);
+ fun eval_entry c =
+ fold filter_const (not_internal consts :: criteria)
+ (SOME (c, low_ranking));
val matches =
Symtab.fold (cons o eval_entry) consts_tab []
|> map_filter I
|> sort (rev_order o int_ord o pairself snd)
- |> map ((apsnd fst) o fst);
+ |> map (apsnd fst o fst);
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
:: Pretty.str ""
- :: (Pretty.str o concat)
+ :: (Pretty.str o implode)
(if null matches
then ["nothing found", end_msg]
else ["found ", (string_of_int o length) matches,
--- a/src/Pure/Tools/find_theorems.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Pure/Tools/find_theorems.ML Wed Jun 17 16:56:15 2009 -0700
@@ -282,7 +282,7 @@
in app (opt_add r r', consts', fs) end;
in app end;
-
+
in
fun filter_criterion ctxt opt_goal (b, c) =
@@ -417,7 +417,7 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
val returned = length thms;
-
+
val tally_msg =
(case foundo of
NONE => "displaying " ^ string_of_int returned ^ " theorems"
@@ -427,7 +427,7 @@
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
- val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+ val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
:: Pretty.str "" ::
--- a/src/Tools/code/code_haskell.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Tools/code/code_haskell.ML Wed Jun 17 16:56:15 2009 -0700
@@ -106,11 +106,9 @@
|> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
|>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
val (ps, vars') = fold_map pr binds vars;
- in
- Pretty.block_enclose (
- str "(let {",
- concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
- ) ps
+ in brackify_block fxy (str "let {")
+ ps
+ (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body])
end
| pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
@@ -118,11 +116,10 @@
let
val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
- in
- Pretty.block_enclose (
- concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
- str "})"
- ) (map pr clauses)
+ in brackify_block fxy
+ (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
+ (map pr clauses)
+ (str "}")
end
| pr_case tyvars thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
--- a/src/Tools/code/code_ml.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Tools/code/code_ml.ML Wed Jun 17 16:56:15 2009 -0700
@@ -151,7 +151,7 @@
concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
+ brackets (
str "case"
:: pr_term is_closure thm vars NOBR t
:: pr "of" clause
@@ -441,8 +441,10 @@
|>> (fn p => concat
[str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
- fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
- in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
+ in
+ brackify_block fxy (Pretty.chunks ps) []
+ (pr_term is_closure thm vars' NOBR body)
+ end
| pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun pr delim (pat, body) =
@@ -450,7 +452,7 @@
val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
+ brackets (
str "match"
:: pr_term is_closure thm vars NOBR t
:: pr "with" clause
--- a/src/Tools/code/code_printer.ML Wed Jun 17 16:55:01 2009 -0700
+++ b/src/Tools/code/code_printer.ML Wed Jun 17 16:56:15 2009 -0700
@@ -45,6 +45,7 @@
val APP: fixity
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
+ val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
type itype = Code_Thingol.itype
type iterm = Code_Thingol.iterm
@@ -175,6 +176,13 @@
fun brackify_infix infx fxy_ctxt =
gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
+fun brackify_block fxy_ctxt p1 ps p2 =
+ let val p = Pretty.block_enclose (p1, p2) ps
+ in if fixity BR fxy_ctxt
+ then Pretty.enclose "(" ")" [p]
+ else p
+ end;
+
(* generic syntax *)