\documentclass{omdoc}
\usepackage[showmods]{stex}
\usepackage{amssymb}
\usepackage{alltt}
\usepackage{hyperref}
\usepackage{listings}
\def\omdoc{OMDoc}
\def\latexml{LaTeXML}
\defpath{backmods}{../background}
%% defining the author metadata
\WAperson[id=miko,
           affiliation=JUB,
           url=http://kwarc.info/kohlhase]
           {Michael Kohlhase}
\WAinstitution[id=JUB,
               url=http://jacobs-university.de,
               streetaddress={Campus Ring 1},
               townzip={28759 Bremen},
               countryshort=D,
               country=Germany,
               type=University,
               acronym=JACU,
               shortname=Jacobs Univ.]
               {Jacobs University Bremen}

\begin{document}
 
% metadata and title page
% \begin{DCmetadata}[maketitle]
%   \DCMcreators{miko}         
%   \DCMrights{Copyright (c) 2009 Michael Kohlhase}
%   \DCMtitle{An example of semantic Markup in {\sTeX}}
%   \DCMabstract{In this note we give an example of semantic markup in {\sTeX}: 
%     Continuous and differentiable functions are introduced using real numbers, sets and
%     functions as an assumed background.}
% \end{DCmetadata}

\inputref{intro}

\begin{omgroup}[id=sec.math]{Mathematical Content}
  \begin{omgroup}{Calculus}
    We present some standard mathematical definitions, here from calculus.
  \inputref{continuous}
  \inputref{differentiable}
\end{omgroup}

\begin{omgroup}[id=sec.math]{A Theory Graph for Elementary Algebra}
  Here we show an example for more advanced theory graph manipulations, in particular
  imports via morphisms.

\begin{module}[id=magma]
  \importmodule[\backmods{functions}]{functions}
  \symdef{magbase}{G}
  \symdef[name=magmaop]{magmaopOp}{\circ}
  \symdef{magmaop}[2]{\infix\magmaopOp{#1}{#2}}
  \begin{definition}[id=magma.def]
    A \defi{magma} is a structure $\tup{\magbase,\magmaopOp}$, such that $\magbase$ is
    closed under the operation $\fun\magmaopOp{\cart{\magbase,\magbase}}\magbase$.
 \end{definition}
\end{module}

\begin{module}[id=semigroup]
  \importmodule{magma}
  \begin{definition}[id=semigroup.def]
    A \trefi[magma]{magma} $\tup{\magbase,\magmaopOp}$, is called a \defi{semigroup}, iff
    $\magmaopOp$ is associative.
  \end{definition}
\end{module}

\begin{module}[id=monoid]
  \importmodule{semigroup}
  \symdef{monneut}{e}
  \symdef{noneut}[1]{#1^*}
  \begin{definition}[id=monoid.def]
    A \defi{monoid} is a structure $\tup{\magbase,\magmaopOp,\monneut}$, such that
    $\tup{\magbase,\magmaopOp}$ is a \trefi[semigroup]{semigroup} and $\monneut$ is a
    \defii{neutral}{element}, i.e. that $\magmaop{x}\monneut=x$ for all $\inset{x}\magbase$.
 \end{definition}

 \begin{definition}[id=noneut.def]
   In a monoid $\tup{\magbase,\magmaopOp,\monneut}$, we use denote the set
   $\setst{\inset{x}S}{x\ne\monneut}$ with $\noneut{S}$.
 \end{definition}
\end{module}

\begin{module}[id=group]
  \importmodule{monoid}
  \symdef{ginvOp}{i}
  \symdef{ginv}[1]{\prefix\ginvOp{#1}}
  \begin{definition}[id=group.def]
    A \defi{group} is a structure $\tup{\magbase,\magmaopOp,\monneut,\ginvOp}$, such that
    $\tup{\magbase,\magmaopOp,\monneut}$ is a \trefi[monoid]{monoid} and $\ginvOp$ acts as
    a \defi{inverse}, i.e. that $\magmaop{x}{\ginv{x}}=\monneut$ for all
    $\inset{x}\magbase$.
  \end{definition}
\end{module}

\begin{module}[id=cgroup]
\importmodule{group}
\begin{definition}[id=cgroup.def]
  We call a \trefi[group]{group} $\tup{\magbase,\magmaopOp,\monneut,\ginvOp}$ a
  \defii{commutative}{group}, iff $\magmaopOp$ is commutative.
\end{definition}
\end{module}

\begin{module}[id=ring]
\symdef{rbase}{R}
\symdef[name=rtimes]{rtimesOp}{\cdot}
\symdef{rtimes}[2]{\infix\rtimesOp{#1}{#2}}
\symdef{rone}{1}
\begin{importmodulevia}{monoid}
  \vassign{rbase}\magbase
  \vassign{rtimesOp}\magmaopOp
  \vassign{rone}\monneut
\end{importmodulevia}
\symdef[name=rplus]{rplusOp}{+}
\symdef{rplus}[2]{\infix\rplusOp{#1}{#2}}
\symdef{rzero}{0}
\symdef[name=rminus]{rminusOp}{-}
\symdef{rminus}[1]{\prefix\rminusOp{#1}}
\begin{importmodulevia}{cgroup}
  \vassign{rplus}\magmaopOp
  \vassign{rzero}\monneut
  \vassign{rminusOp}\ginvOp
\end{importmodulevia}
\begin{definition}
  A \defi{ring} is a structure $\tup{\rbase,\rplusOp,\rzero,\rtimesOp,\rone,\rminusOp}$,
  such that $\tup{\noneut\rbase,\rtimesOp,\rone}$ is a monoid and
  $\tup{\rbase,\rplusOp,\rzero,\rminusOp}$ is a commutative group.
\end{definition}
\end{module}
\end{omgroup}
\end{omgroup}

\begin{omgroup}[id=concl]{Conclusion}
  In this note we have given an example of standard mathematical markup and shown how a a
  {\sTeX} collection can be set up for automation.
\end{omgroup}
\bibliographystyle{alpha}
\bibliography{kwarc}
\end{document}

%%% Local Variables: 
%%% mode: LaTeX
%%% TeX-master: t
%%% End: 

% LocalWords:  miko Makefiles tex contfuncs modf sms pdflatex latexml Makefile
% LocalWords:  latexmlpost omdoc STEXDIR BUTFILES DIRS