DIV_CONV
reduceLib.DIV_CONV : conv
Calculates by inference the result of dividing, with truncation, one numeral by another.
If m and n are numerals (e.g. 0, 1, 2, 3,...), then
DIV_CONV ``m DIV n`` returns the theorem:
|- m DIV n = s
where s is the numeral that denotes the result of dividing the natural
number denoted by m by the natural number denoted by n, with
truncation.
Failure
DIV_CONV tm fails unless tm is of the form ``m DIV n``,
where m and n are numerals, or if n denotes zero.
Example
> Arithconv.DIV_CONV ``0 DIV 0``;
val it = ⊢ 0 DIV 0 = 0: thm
> Arithconv.DIV_CONV ``x DIV 12``;
Exception- HOL_ERR
(at Conv.RAND_CONV:
at Thm.dest_cexp: term is not a compute value) raised
> Arithconv.DIV_CONV ``0 DIV 12``;
val it = ⊢ 0 DIV 12 = 0: thm
> Arithconv.DIV_CONV ``7 DIV 2``;
val it = ⊢ 7 DIV 2 = 3: thm