# HG changeset patch # User wenzelm # Date 1210418785 -7200 # Node ID 996add9defaba85597c12e46bb22f346d8642639 # Parent 94bedbb34b921cd22c500598ff62ddfebec38b10 avoid old macros from isar.sty; diff -r 94bedbb34b92 -r 996add9defab doc-src/AxClass/Group/Group.thy --- a/doc-src/AxClass/Group/Group.thy Sat May 10 00:14:00 2008 +0200 +++ b/doc-src/AxClass/Group/Group.thy Sat May 10 13:26:25 2008 +0200 @@ -200,8 +200,8 @@ qed text {* - \medskip The $\INSTANCE$ command sets up an appropriate goal that - represents the class inclusion (or type arity, see + \medskip The \isakeyword{instance} command sets up an appropriate + goal that represents the class inclusion (or type arity, see \secref{sec:inst-arity}) to be proven (see also \cite{isabelle-isar-ref}). The initial proof step causes back-chaining of class membership statements wrt.\ the hierarchy of @@ -215,15 +215,15 @@ subsection {* Concrete instantiation \label{sec:inst-arity} *} text {* - So far we have covered the case of the form $\INSTANCE$~@{text - "c\<^sub>1 \ c\<^sub>2"}, namely \emph{abstract instantiation} --- - $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance - of @{text "c\<^sub>2"}. Even more interesting for practical - applications are \emph{concrete instantiations} of axiomatic type - classes. That is, certain simple schemes @{text "(\\<^sub>1, \, - \\<^sub>n) t \ c"} of class membership may be established at the - logical level and then transferred to Isabelle's type signature - level. + So far we have covered the case of the form + \isakeyword{instance}~@{text "c\<^sub>1 \ c\<^sub>2"}, namely + \emph{abstract instantiation} --- $c@1$ is more special than @{text + "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}. Even more + interesting for practical applications are \emph{concrete + instantiations} of axiomatic type classes. That is, certain simple + schemes @{text "(\\<^sub>1, \, \\<^sub>n) t \ c"} of class + membership may be established at the logical level and then + transferred to Isabelle's type signature level. \medskip As a typical example, we show that type @{typ bool} with exclusive-or as @{text \} operation, identity as @{text \}, and @@ -236,18 +236,18 @@ unit_bool_def: "\ \ False" text {* - \medskip It is important to note that above $\DEFS$ are just - overloaded meta-level constant definitions, where type classes are - not yet involved at all. This form of constant definition with + \medskip It is important to note that above \isakeyword{defs} are + just overloaded meta-level constant definitions, where type classes + are not yet involved at all. This form of constant definition with overloading (and optional recursion over the syntactic structure of simple types) are admissible as definitional extensions of plain HOL \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not required for overloading. Nevertheless, overloaded definitions are best applied in the context of type classes. - \medskip Since we have chosen above $\DEFS$ of the generic group - operations on type @{typ bool} appropriately, the class membership - @{text "bool \ agroup"} may be now derived as follows. + \medskip Since we have chosen above \isakeyword{defs} of the generic + group operations on type @{typ bool} appropriately, the class + membership @{text "bool \ agroup"} may be now derived as follows. *} instance bool :: agroup @@ -261,10 +261,10 @@ qed text {* - The result of an $\INSTANCE$ statement is both expressed as a - theorem of Isabelle's meta-logic, and as a type arity of the type - signature. The latter enables type-inference system to take care of - this new instance automatically. + The result of an \isakeyword{instance} statement is both expressed + as a theorem of Isabelle's meta-logic, and as a type arity of the + type signature. The latter enables type-inference system to take + care of this new instance automatically. \medskip We could now also instantiate our group theory classes to many other concrete types. For example, @{text "int \ agroup"} diff -r 94bedbb34b92 -r 996add9defab doc-src/AxClass/Group/Product.thy --- a/doc-src/AxClass/Group/Product.thy Sat May 10 00:14:00 2008 +0200 +++ b/doc-src/AxClass/Group/Product.thy Sat May 10 13:26:25 2008 +0200 @@ -37,10 +37,11 @@ purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}. On the other hand there are syntactic differences, of course. - Constants @{text \} on some type @{text \} are rejected by the - type-checker, unless the arity @{text "\ \ product"} is part of the - type signature. In our example, this arity may be always added when - required by means of an $\INSTANCE$ with the default proof $\DDOT$. + Constants @{text \} on some type @{text \} are rejected by the + type-checker, unless the arity @{text "\ \ product"} is part of the + type signature. In our example, this arity may be always added when + required by means of an \isakeyword{instance} with the default proof + (double-dot). \medskip Thus, we may observe the following discipline of using syntactic classes. Overloaded polymorphic constants have their type @@ -62,12 +63,12 @@ well-formed only after the arity @{text "bool \ product"} is made known to the type checker. - \medskip It is very important to see that above $\DEFS$ are not - directly connected with $\INSTANCE$ at all! We were just following - our convention to specify @{text \} on @{typ bool} after having - instantiated @{text "bool \ product"}. Isabelle does not require - these definitions, which is in contrast to programming languages like - Haskell \cite{haskell-report}. + \medskip It is very important to see that above \isakeyword{defs} are + not directly connected with \isakeyword{instance} at all! We were + just following our convention to specify @{text \} on @{typ bool} + after having instantiated @{text "bool \ product"}. Isabelle does + not require these definitions, which is in contrast to programming + languages like Haskell \cite{haskell-report}. \medskip While Isabelle type classes and those of Haskell are almost the same as far as type-checking and type inference are concerned, diff -r 94bedbb34b92 -r 996add9defab doc-src/AxClass/Group/document/Group.tex --- a/doc-src/AxClass/Group/document/Group.tex Sat May 10 00:14:00 2008 +0200 +++ b/doc-src/AxClass/Group/document/Group.tex Sat May 10 13:26:25 2008 +0200 @@ -327,8 +327,8 @@ \endisadelimproof % \begin{isamarkuptext}% -\medskip The $\INSTANCE$ command sets up an appropriate goal that - represents the class inclusion (or type arity, see +\medskip The \isakeyword{instance} command sets up an appropriate + goal that represents the class inclusion (or type arity, see \secref{sec:inst-arity}) to be proven (see also \cite{isabelle-isar-ref}). The initial proof step causes back-chaining of class membership statements wrt.\ the hierarchy of @@ -344,13 +344,14 @@ \isamarkuptrue% % \begin{isamarkuptext}% -So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} --- - $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance - of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical - applications are \emph{concrete instantiations} of axiomatic type - classes. That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be established at the - logical level and then transferred to Isabelle's type signature - level. +So far we have covered the case of the form + \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely + \emph{abstract instantiation} --- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance of \isa{c\isactrlsub {\isadigit{2}}}. Even more + interesting for practical applications are \emph{concrete + instantiations} of axiomatic type classes. That is, certain simple + schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class + membership may be established at the logical level and then + transferred to Isabelle's type signature level. \medskip As a typical example, we show that type \isa{bool} with exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and @@ -363,18 +364,18 @@ \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline \ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}% \begin{isamarkuptext}% -\medskip It is important to note that above $\DEFS$ are just - overloaded meta-level constant definitions, where type classes are - not yet involved at all. This form of constant definition with +\medskip It is important to note that above \isakeyword{defs} are + just overloaded meta-level constant definitions, where type classes + are not yet involved at all. This form of constant definition with overloading (and optional recursion over the syntactic structure of simple types) are admissible as definitional extensions of plain HOL \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not required for overloading. Nevertheless, overloaded definitions are best applied in the context of type classes. - \medskip Since we have chosen above $\DEFS$ of the generic group - operations on type \isa{bool} appropriately, the class membership - \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% + \medskip Since we have chosen above \isakeyword{defs} of the generic + group operations on type \isa{bool} appropriately, the class + membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{instance}\isamarkupfalse% @@ -412,10 +413,10 @@ \endisadelimproof % \begin{isamarkuptext}% -The result of an $\INSTANCE$ statement is both expressed as a - theorem of Isabelle's meta-logic, and as a type arity of the type - signature. The latter enables type-inference system to take care of - this new instance automatically. +The result of an \isakeyword{instance} statement is both expressed + as a theorem of Isabelle's meta-logic, and as a type arity of the + type signature. The latter enables type-inference system to take + care of this new instance automatically. \medskip We could now also instantiate our group theory classes to many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} diff -r 94bedbb34b92 -r 996add9defab doc-src/AxClass/Group/document/Product.tex --- a/doc-src/AxClass/Group/document/Product.tex Sat May 10 00:14:00 2008 +0200 +++ b/doc-src/AxClass/Group/document/Product.tex Sat May 10 13:26:25 2008 +0200 @@ -52,10 +52,11 @@ purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}. On the other hand there are syntactic differences, of course. - Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the - type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the - type signature. In our example, this arity may be always added when - required by means of an $\INSTANCE$ with the default proof $\DDOT$. + Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the + type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the + type signature. In our example, this arity may be always added when + required by means of an \isakeyword{instance} with the default proof + (double-dot). \medskip Thus, we may observe the following discipline of using syntactic classes. Overloaded polymorphic constants have their type @@ -91,12 +92,12 @@ well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made known to the type checker. - \medskip It is very important to see that above $\DEFS$ are not - directly connected with $\INSTANCE$ at all! We were just following - our convention to specify \isa{{\isasymodot}} on \isa{bool} after having - instantiated \isa{bool\ {\isasymColon}\ product}. Isabelle does not require - these definitions, which is in contrast to programming languages like - Haskell \cite{haskell-report}. + \medskip It is very important to see that above \isakeyword{defs} are + not directly connected with \isakeyword{instance} at all! We were + just following our convention to specify \isa{{\isasymodot}} on \isa{bool} + after having instantiated \isa{bool\ {\isasymColon}\ product}. Isabelle does + not require these definitions, which is in contrast to programming + languages like Haskell \cite{haskell-report}. \medskip While Isabelle type classes and those of Haskell are almost the same as far as type-checking and type inference are concerned,