Add function to return Prelude rewrite rules as Theorems

[brianhuffman]

Currently we have a function add_prelude_eqs that can add equations proved in the saw-core prelude (Prelude.sawcore) to a Simpset. However, there is no way to obtain such an equation as a Theorem. We should add a function to do this. This would make it possible to construct other simpsets in a uniform manner using addsimps, instead of mixing addsimps with add_prelude_eqs as is required now.

We should do the same thing with add_cryptol_eqs.

It would also be nice to do the same thing with add_prelude_defs and add_cryptol_defs, but note that those can actually return multiple rewrite rules, so we might have to use a different type (maybe returning a Simpset instead of a Theorem, which would necessitate a binary merge operation on simpsets) or else extend the Theorem type to allow compound rules.

See also #882.

[robdockins]

It's never been clear to me why we don't have a binary merge operation of simpsets, it seems easy to add.

[brianhuffman]

Agreed—adding a simpset merge operation is a no-brainer.