doc-src/AxClass/generated/Semigroups.tex

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

%
\begin{isabellebody}%
\def\isabellecontext{Semigroups}%
%
\isamarkupheader{Semigroups%
}
\isamarkuptrue%
\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse%
%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
  that all meet certain properties, which are also called \emph{class
  axioms}. Thus, type classes may be also understood as type
  predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
  depend on this type \isa{{\isacharprime}a}.  These \emph{characteristic
  constants} behave like operations associated with the ``carrier''
  type \isa{{\isacharprime}a}.

  We illustrate these basic concepts by the following formulation of
  semigroups.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
  all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
  associative operator.  The \isa{assoc} axiom contains exactly one
  type variable, which is invisible in the above presentation, though.
  Also note that free term variables (like \isa{x}, \isa{y},
  \isa{z}) are allowed for user convenience --- conceptually all of
  these are bound by outermost universal quantifiers.

  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
  \emph{signature}.  Different signatures require different classes.
  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
  not quite the same.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{end}\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: