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
|
\DOC NUM_MOD_CONV
\TYPE {NUM_MOD_CONV : term -> thm}
\SYNOPSIS
Proves what the remainder on dividing one natural number numeral by another is.
\KEYWORDS
conversion, number, arithmetic.
\DESCRIBE
If {n} and {m} are numerals (e.g. {0}, {1}, {2}, {3},...), then
{NUM_MOD_CONV `n MOD m`} returns the theorem:
{
|- n MOD m = s
}
\noindent where {s} is the numeral that denotes the remainder on dividing
the number denoted by {n} by the one denoted by {m}.
\FAILURE
{NUM_MOD_CONV tm} fails if {tm} is not of the form {`n MOD m`}, where {n} and
{m} are numerals, or if the second numeral {m} is zero.
\EXAMPLE
{
# NUM_MOD_CONV `1089 MOD 9`;;
val it : thm = |- 1089 MOD 9 = 0
# NUM_MOD_CONV `1234 MOD 3`;;
val it : thm = |- 1234 MOD 3 = 1
# NUM_MOD_CONV `11 MOD 0`;;
Exception: Failure "NUM_MOD_CONV".
}
\COMMENTS
For definiteness, remainders with zero denominator are in fact designed to be
zero. However, it is perhaps bad style to rely on this fact, so the conversion
just fails in this case.
\SEEALSO
NUM_ADD_CONV, NUM_DIV_CONV, NUM_EQ_CONV, NUM_EVEN_CONV,
NUM_EXP_CONV, NUM_FACT_CONV, NUM_GE_CONV, NUM_GT_CONV, NUM_LE_CONV,
NUM_LT_CONV, NUM_MAX_CONV, NUM_MIN_CONV, NUM_MULT_CONV, NUM_ODD_CONV,
NUM_PRE_CONV, NUM_REDUCE_CONV, NUM_RED_CONV, NUM_REL_CONV, NUM_SUB_CONV,
NUM_SUC_CONV.
\ENDDOC
|
