CADiZ

Reference manual / Extended toolkit / section numlaws


Laws about Numbers in Z

Sam Valentine

Written September 1999.

Last updated September 1999.

section numlaws parents numdefs, corelaws

This section contains the CADi\num version of some laws about numbers in the mathematical toolkit of Z.

Prelude-based Laws

Those laws which depend solely on the definitions in the prelude are given in the file corelaws.z, which is a parent of this one.

Theorems about the Natural Numbers

We could here state and prove various useful theorems about \nat, both because of their usefulness, and to assist in proving the consistency of the definitions in numdefs.

The theorems would mainly be to the effect that \nat is an Abelian monoid under _ * _, and _ * _ distributes through _ + _.

zeroTimesBEqZero ==

\vdash? \forall b: \nat @ 0 * b = 0

OneTimesBEqB ==

\vdash? \forall b: \nat @ 1 * b = b

TimesCommutes ==

\vdash? \forall a, b: \nat @ a * b = b * a

TimesDistributesThruPlus ==

\vdash? \forall a, b, c: \nat @ a * (b + c) = (a * b) + (a * c)

TimesClosed ==

\vdash? \forall a, b: \nat @ a * b \in \nat

TimesAssociates ==

\vdash? \forall a, b, c: \nat @ (a * b) * c = a * (b * c)

TimesConstInjective ==

\vdash? \forall a, b: \nat; c: \nat1 | a * c = b * c @ a = b

IT 18-Feb-2000