PRE_CONV : conv
STRUCTURE
SYNOPSIS
Calculates by inference the predecessor of a numeral.
LIBRARY
reduce
DESCRIPTION
If n is a numeral (e.g. 0, 1, 2, 3,...), then PRE_CONV "PRE n" returns the theorem:
   |- PRE n = s
where s is the numeral that denotes the predecessor of the natural number denoted by n.
FAILURE
PRE_CONV tm fails unless tm is of the form ``PRE n``, where n is a numeral.
EXAMPLE
> PRE_CONV ``PRE 0``;
val it = |- PRE 0 = 0 : thm

> PRE_CONV ``PRE 1``;
val it = |- PRE 1 = 0 : thm

> PRE_CONV ``PRE 22``;
val it = |- PRE 22 = 21 : thm
HOL  Kananaskis-13