Rewrite the existing classes to be fully immutable.

The previous version of the classes was "partially" mutable: one had to
use functions such as add_premises, assert_commutative, etc.  Now,
however, all setting up is done in constructors, the objects being
immutable.  This has made the code of the module simpler, easier to
use, better integrated into the Basic inheritance tree, and much more
consistent.