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