Next: Theorems about multiplication Up: The Natural Numbers Previous: Theorems about Minus

Theorems involving only the function plus are given in this file below. Note the theorem middle_four_plus--we find this and similar theorems very useful for manipulating expressions involving commutative, associative operators. It is possible to prove the general case of this theorem and derive this and other instances of it from it as desired. We may choose to do this in a future version of the library.

``` ** Module lib_nat_plus_thms Imports lib_nat/lib_nat_suc_thms
plus_zero = ... : {n:nat}Eq (plus n zero) n
plus_suc = ... : {m,n:nat}Eq (plus m (suc n)) (suc (plus m n))
plus_suc_lemma = ... : {x,t:nat}not (Eq (plus x (suc t)) x)
plus_assoc = ... :
{k,m,n:nat}Eq (plus (plus k m) n) (plus k (plus m n))
plus_commutes = ... : {m,n:nat}Eq (plus m n) (plus n m)
plus_strict = ... :
{n,m|nat}(Eq (plus n m) zero)->and (Eq n zero) (Eq m zero)
middle_four_plus = ... :
{i,j,k,l|nat}
Eq (plus (plus i k) (plus j l)) (plus (plus i j) (plus k l))
one_plus_lemma = ... :
{m,n|nat}(Eq one (plus m n))->
or (and (Eq one m) (Eq zero n)) (and (Eq zero m) (Eq one n))
cancel_plus = ... : {i,j,k:nat}(Eq (plus i j) (plus i k))->Eq j k
plus_subst_l = ... : {l,n,m|nat}(Eq l n)->Eq (plus l m) (plus n m)
plus_subst_r = ... : {l,n,m|nat}(Eq l n)->Eq (plus m l) (plus m n)```

Lego
Fri May 24 19:01:27 BST 1996