1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
\section{The Theory {\tt mult}}
The theory \ml{mult}\index{mult, theory@{\ptt mult}, theory} contains an
\adhoc\ collection of
theorems about multiplication and exponentials. It contains no new definitions.
The theorems that have been pre-proved in this theory include but are not
restricted to the following:
\begin{hol}
\index{LESS\_MONO\_MULT1@{\ptt LESS\_MONO\_MULT1}}
\index{LESS\_MULT\_PLUS\_DIFF@{\ptt LESS\_MULT\_PLUS\_DIFF}}
\index{LEFT\_SUB\_DISTRIB@{\ptt LEFT\_SUB\_DISTRIB}}
\index{ONE\_LESS\_TWO\_EXP\_SUC@{\ptt ONE\_LESS\_TWO\_EXP\_SUC}}
\begin{verbatim}
LESS_MONO_MULT1 |- !m n p. m <= n ==> (p * m) <= (p * n)
LESS_MULT_PLUS_DIFF |- !n k l. k < l ==> ((k * n) + n) <= (l * n)
LEFT_SUB_DISTRIB |- !m n p. m * (n - p) = (m * n) - (m * p)
ONE_LESS_TWO_EXP_SUC |- !n. 1 < (2 EXP (SUC n))
\end{verbatim}\end{hol}
|
