1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
\documentclass{omdoc}
\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[load=\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
|
