# HG changeset patch # User huffman # Date 1245282975 25200 # Node ID 678d294a563c58d73ad0263292e527c74253ffed # Parent 1db0c8f235fbd10541645ed2626e285b3fe55a37# Parent b6710a3b4c497b13f1b5404e63c211ebda67be11 merged diff -r 1db0c8f235fb -r 678d294a563c .hgignore --- 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 diff -r 1db0c8f235fb -r 678d294a563c Admin/isatest/settings/at-mac-poly-5.1-para --- 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" diff -r 1db0c8f235fb -r 678d294a563c doc-src/Classes/Thy/Classes.thy --- 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 \} are mangled as @{text f_\}. In case of uncertainty, + a class operation @{text f} to be instantiated on type constructor + @{text \} is mangled as @{text f_\}. 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" + mult_prod_def: "p1 \ p2 = (fst p1 \ fst p2, snd p1 \ snd p2)" instance %quote proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" - show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ p\<^isub>3)" + fix p1 p2 p3 :: "\\semigroup \ \\semigroup" + show "p1 \ p2 \ p3 = p1 \ (p2 \ 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 "(\)"} 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 \ \ \ \" 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)}*} diff -r 1db0c8f235fb -r 678d294a563c doc-src/Classes/Thy/document/Classes.tex --- 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})\\ diff -r 1db0c8f235fb -r 678d294a563c doc-src/Classes/classes.tex --- 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. diff -r 1db0c8f235fb -r 678d294a563c doc-src/IsarRef/Thy/Spec.thy --- 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 \ local_theory"} \\ @{command_def "instantiation"} & : & @{text "theory \ local_theory"} \\ @{command_def "instance"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "instance"} & : & @{text "theory \ proof(prove)"} \\ @{command_def "subclass"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @@ -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, \, + 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 \ 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 \ theory"} \\ - @{command_def "instance"} & : & @{text "theory \ proof(prove)"} \\ + @{command_def "axclass"} & : & @{text "theory \ 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 \ c\<^sub>2"} and @{command - "instance"}~@{text "t :: (s\<^sub>1, \, 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} *} diff -r 1db0c8f235fb -r 678d294a563c doc-src/IsarRef/Thy/document/Spec.tex --- 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% diff -r 1db0c8f235fb -r 678d294a563c doc-src/System/Thy/Presentation.thy --- 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. diff -r 1db0c8f235fb -r 678d294a563c doc-src/System/Thy/document/Presentation.tex --- 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. diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/IsaMakefile --- 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 diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Makefile --- 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 diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Misc/appendix.thy --- 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) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a \ 'a"} & (infixl 65) \\ -@{text"-"} & @{text "('a::minus) \ 'a"} \\ -@{text"*"} & @{text "('a::times) \ 'a \ 'a"} & (infixl 70) \\ -@{text div} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text mod} & @{text "('a::div) \ 'a \ 'a"} & (infixl 70) \\ -@{text dvd} & @{text "('a::times) \ 'a \ bool"} & (infixl 50) \\ -@{text"/"} & @{text "('a::inverse) \ 'a \ 'a"} & (infixl 70) \\ -@{text"^"} & @{text "('a::power) \ nat \ 'a"} & (infixr 80) \\ -@{term abs} & @{text "('a::minus) \ 'a"} & ${\mid} x {\mid}$\\ -@{text"\"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{text"<"} & @{text "('a::ord) \ 'a \ bool"} & (infixl 50) \\ -@{term min} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term max} & @{text "('a::ord) \ 'a \ 'a"} \\ -@{term Least} & @{text "('a::ord \ bool) \ '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(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Misc/document/appendix.tex --- 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}% diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Axioms.thy --- 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 \ y) \ z = x \ (y \ z)" + +text {* \noindent This @{command class} specification requires that +all instances of @{class semigroup} obey @{fact "assoc:"}~@{prop +[source] "\x y z \ 'a\semigroup. (x \ y) \ z = x \ (y \ 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\semigroup" + shows "x \ (y \ z) = (x \ y) \ 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 \ n) \ q = m \ (n \ 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: "\ x <<= y; y <<= z \ \ x <<= z" -antisym: "\ x <<= y; y <<= x \ \ x = y" -lt_le: "x << y = (x <<= y \ x \ 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\semigroup \ 'b\semigroup" + show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ 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 \ (\ y << x) = True"; +end + +subsubsection {* Monoids *} -txt{*\noindent -The conclusion is not just @{prop"\ 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" ("\") + assumes neutl: "\ \ 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: "\ = (0\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 "\ \ n = n" + unfolding neutral_nat_def by simp +qed -lemma "(P::bool) << Q \ \(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 \ y <<= x" +definition + neutral_prod_def: "\ = (\, \)" -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\monoidl \ 'b\monoidl" + show "\ \ p = p" + by (cases p) (simp add: neutral_prod_def neutl) +qed -lemma "\x::'a::linord. x << y \ x = y \ 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 \ \ = 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: "\ x << x" -lt_trans: "\ x << y; y << z \ \ x << z" -le_less: "x <<= y = (x << y \ 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 \ 'a" ("\
_" [81] 80) + assumes invl: "\
x \ x = \" -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\group" + shows "x \ y = x \ z \ y = z" +proof + assume "x \ y = x \ z" + then have "\
x \ (x \ y) = \
x \ (x \ z)" by simp + then have "(\
x \ x) \ y = (\
x \ x) \ z" by (simp add: assoc) + then show "y = z" by (simp add: invl neutl) +next + assume "y = z" + then show "x \ y = x \ 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 \ monoid +proof + fix x + from invl have "\
x \ x = \" . + then have "\
x \ (x \ \) = \
x \ x" + by (simp add: neutl invl assoc [symmetric]) + then show "x \ \ = 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 \ 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"\"} 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 "\"} operation and associativity at +the same time. -(* -axclass false<"term" -false: "x \ 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 \ 'a\finite +set)" by (fact finite_UNIV)}. *} + (*<*)end(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Overloading.thy --- 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 "\"} +for arbitrary types by means of a type class: *} + +class plus = + fixes plus :: "'a \ 'a \ 'a" (infixl "\" 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 \ nat \ nat" where + "(0::nat) \ n = n" + | "Suc m \ n = Suc (m \ 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 \} is mangled +as @{text f_\}. 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) \ \zs. ys = xs@zs" -strict_prefix_def: - "xs << (ys::'a list) \ xs <<= ys \ xs \ ys" +text {* \noindent From now on, terms like @{term "Suc (m \ 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 \ 'b \ 'a \ 'b \ 'a \ 'b" where + "(x, y) \ (w, z) = (x \ w, y \ 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(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Overloading0.thy --- 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 \ 'a" - -text{*\noindent -and provide different definitions at different instances: -*} - -defs (overloaded) -inverse_bool: "inverse(b::bool) \ \ b" -inverse_set: "inverse(A::'a set) \ -A" -inverse_pair: "inverse(p) \ (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 \ '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 \ 'b \ 'a \ 'b"} but on the right @{typ"'a \ 'a"} and -@{typ"'b \ '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 \ '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(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Overloading1.thy --- 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) \ 'a \ bool" (infixl "<<" 50) - le :: "('a::ordrel) \ 'a \ 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 \ P \ Q" -lt_bool_def: "P << Q \ \P \ 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(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Overloading2.thy --- 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) \ - size xs = size ys \ (\i"} on sets. - -In addition there is a special syntax for bounded quantifiers: -\begin{center} -\begin{tabular}{lcl} -@{prop"\x \ y. P x"} & @{text"\"} & @{prop [source] "\x. x \ y \ P x"} \\ -@{prop"\x \ y. P x"} & @{text"\"} & @{prop [source] "\x. x \ y \ P x"} -\end{tabular} -\end{center} -And analogously for @{text"<"} instead of @{text"\"}. -*}(*<*)end(*>*) diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/ROOT.ML --- 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"; diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/Setup.thy --- /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 diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Axioms.tex --- 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% % diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Numbers.tex --- 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}% diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Overloading.tex --- 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 % diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Overloading0.tex --- 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: diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Overloading1.tex --- 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: diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/document/Overloading2.tex --- 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: diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/numerics.tex --- 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. diff -r 1db0c8f235fb -r 678d294a563c doc-src/TutorialI/Types/types.tex --- 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" diff -r 1db0c8f235fb -r 678d294a563c lib/Tools/usedir --- 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 .. diff -r 1db0c8f235fb -r 678d294a563c lib/scripts/polyml-version --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Nominal/nominal_atoms.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Nominal/nominal_package.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Product_Type.thy --- 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 *) diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Rational.thy --- 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 \ rat" ("\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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/RealDef.thy --- 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 \ real" ("\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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_abs_proofs.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_aux.ML --- 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; diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_codegen.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_package.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_realizer.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/datatype_package/datatype_rep_proofs.ML --- 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); diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/function_package/fundef_package.ML --- 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 *) diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/function_package/size.ML --- 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 "_" diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Tools/quickcheck_generators.ML --- 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\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 diff -r 1db0c8f235fb -r 678d294a563c src/HOL/Transitive_Closure.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 \ Q)^* \ \x y. (a,x) : P^* \ (x,y) : Q \ x=y \ (a,b) : P^*" +apply (induct rule:rtrancl.induct) + apply blast +apply (blast intro:rtrancl_trans) +done + +lemma rtrancl_Un_separator_converseE: + "(a,b) : (P \ Q)^* \ \x y. (x,b) : P^* \ (y,x) : Q \ y=x \ (a,b) : P^*" +apply (induct rule:converse_rtrancl_induct) + apply blast +apply (blast intro:rtrancl_trans) +done + subsection {* Transitive closure *} diff -r 1db0c8f235fb -r 678d294a563c src/Pure/General/output.ML --- 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; diff -r 1db0c8f235fb -r 678d294a563c src/Pure/IsaMakefile --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/Pure/Isar/class.ML --- 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) => diff -r 1db0c8f235fb -r 678d294a563c src/Pure/Isar/class_target.ML --- 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'') diff -r 1db0c8f235fb -r 678d294a563c src/Pure/Isar/overloading.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/Pure/ML-Systems/mosml.ML --- 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 *) diff -r 1db0c8f235fb -r 678d294a563c src/Pure/ML-Systems/polyml_common.ML --- 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); diff -r 1db0c8f235fb -r 678d294a563c src/Pure/ML-Systems/smlnj.ML --- 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); diff -r 1db0c8f235fb -r 678d294a563c src/Pure/ML-Systems/timing.ML --- /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; + diff -r 1db0c8f235fb -r 678d294a563c src/Pure/System/session.ML --- 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 ()) diff -r 1db0c8f235fb -r 678d294a563c src/Pure/Tools/find_consts.ML --- 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, diff -r 1db0c8f235fb -r 678d294a563c src/Pure/Tools/find_theorems.ML --- 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 "" :: diff -r 1db0c8f235fb -r 678d294a563c src/Tools/code/code_haskell.ML --- 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\""]; diff -r 1db0c8f235fb -r 678d294a563c src/Tools/code/code_ml.ML --- 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 diff -r 1db0c8f235fb -r 678d294a563c src/Tools/code/code_printer.ML --- 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 *)