Bags standard module overridden by TLAPS, exports extra declarations unrelated with bags

[jorgeadriano]

• Problem:

TLAPS includes a "Bags" module, which is a copy of the standard "Bags" with added extras, the latter consisting of:

1. extension of modules: TLAPS, FiniteSetTheorems, SequenceTheorems
2. definition of a SeqToBag operator
3. proofs of various properties on Bags

The extended "SequenceTheorems" module in particular defines various common operations on Sequences, and likewise for "FiniteSetTheorems". These definitions are therefore, by extension, in TLAPS' "Bags" module.

The TLA+ library paths set in the toolbox "preference" settings take precedence over the standard modules. So when using TLAPS, extending Bags implies importing various extra operations on sequences and finite sets. These may clash with user defined operators.

• Other Standard Modules overridden by TLAPS

"RealTime" and "FiniteSets" are also provided by TLAPS. However these are exact copies (except for comments). Note that unlike with "Bags", the theorems and proofs for "FiniteSets" are in the "FiniteSetTheorems" and "FiniteSetTheorems_proofs" modules (which extend FiniteSets).

Note also that no "Sequences" module is provided by TLAPS, yet there is a "SequenceTheorems" module that extends the standard "Sequences" module provided by toolbox.

• Suggested fix:

It's enough to move all extra content in TLAPS "Bags" to a "BagTheorems" module. But it's probably best to also remove the duplicated standard modules, unless they really are needed for some reason.

It might also be a good idea to choose a uniform approach for theorem and proofs, i.e. either separated in Theorem and Theorem_proof modules as in RealTime and FiniteSets, or all in the same file as in SequenceTheorems.