next up previous contents
Next: Theorems about multiplication Up: The Natural Numbers Previous: Theorems about Minus

Theorems about Plus

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_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)->(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))->
    ((Eq one m /\ Eq zero n) \/ (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
1998-06-15