author wenzelm Sat, 10 May 2008 13:26:25 +0200 changeset 26871 996add9defab parent 26870 94bedbb34b92 child 26872 336dfd860744
avoid old macros from isar.sty;
 doc-src/AxClass/Group/Group.thy file | annotate | diff | comparison | revisions doc-src/AxClass/Group/Product.thy file | annotate | diff | comparison | revisions doc-src/AxClass/Group/document/Group.tex file | annotate | diff | comparison | revisions doc-src/AxClass/Group/document/Product.tex file | annotate | diff | comparison | revisions
--- 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 \<subseteq> 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 "(\<alpha>\<^sub>1, \<dots>,
-  \<alpha>\<^sub>n) t \<Colon> 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 \<subseteq> 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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> 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 \<odot>} operation, identity as @{text \<inv>}, and
@@ -236,18 +236,18 @@
unit_bool_def: "\<one> \<equiv> 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 \<Colon> 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 \<Colon> 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 \<Colon> agroup"}
--- 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 \<odot>} on some type @{text \<tau>} are rejected by the
-  type-checker, unless the arity @{text "\<tau> \<Colon> 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 \<odot>} on some type @{text \<tau>} are rejected by the
+ type-checker, unless the arity @{text "\<tau> \<Colon> 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 \<Colon> 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 \<odot>} on @{typ bool} after having
- instantiated @{text "bool \<Colon> 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 \<odot>} on @{typ bool}
+ after having instantiated @{text "bool \<Colon> 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,
--- 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}
--- 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,