Axioms for the theory of proveit.numbers.addition

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
# the theory is in the current directory:
from proveit import a, b, m, x
from proveit.core_expr_types import a_1_to_m
from proveit.logic import Forall, Equals
from proveit.numbers import Add, zero, one, Natural
theory = proveit.Theory('.') # adds theory root to sys.path if necessary

%begin axioms

Defining axioms for theory 'proveit.numbers.addition'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Definitions for binary addition:

A natural number is unchanged after adding zero.

nat_plus_zero = Forall(a, Equals(Add(a, zero), a),
                         domain=Natural)

nat_plus_zero:

Adding 1 to one of the addends is the same as adding one to the sum.

nat_plus_successor = Forall((a, b), Equals(Add(a, Add(b, one)), Add(Add(a, b), one)),
                      domain=Natural)

nat_plus_successor:

Definition of multi-operand addition:

These are conservative extension definitions that are independent of the type of the operands.

empty_addition = Equals(Add(), zero) # base case

empty_addition:

multi_addition_def = \
    Forall(m, Forall((a_1_to_m, b), 
                     Equals(Add(a_1_to_m, b), Add(Add(a_1_to_m), b)).with_wrap_after_operator()),
           domain=Natural)

multi_addition_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.addition