NUM_DIV_CONV : term -> thm

SYNOPSIS

Proves what the truncated quotient of two natural number numerals is.

DESCRIPTION

If n and m are numerals (e.g. 0, 1, 2, 3,...), then NUM_DIV_CONV `n DIV m` returns the theorem:

   |- n DIV m = s

where s is the numeral that denotes the truncated quotient of the numbers denoted by n and m.

FAILURE CONDITIONS

NUM_DIV_CONV tm fails if tm is not of the form `n DIV m`, where n and m are numerals, or if the second numeral m is zero.

EXAMPLE

  # NUM_DIV_CONV `99 DIV 9`;;
  val it : thm = |- 99 DIV 9 = 11

  # NUM_DIV_CONV `334 DIV 3`;;
  val it : thm = |- 334 DIV 3 = 111

  # NUM_DIV_CONV `11 DIV 0`;;
  Exception: Failure "NUM_DIV_CONV".

COMMENTS

For definiteness, quotients 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.