Add bool_to_Z

This MR adds bool_to_Z which has been used as Z_of_bool in both RefinedC and RustBelt. There is not much theory for it as most of the time one can reason about it by computation.

Would it make sense to have a lemma for 0 ≤ bool_to_Z b ≤ 1?

added 1 commit

• 53ec60f9 - Add bool_to_Z

Compare with previous version

Let me know if you have other ideas for lemmas that would be useful for bool_to_Z.

So far this is the only one that came to my mind -- and we can easily add more lemmas later, of course.

LGTM! Do you think a changelog would be useful?

added 1 commit

• 9d3950ab - Add bool_to_Z

Compare with previous version

I'll wait for @robbertkrebbers to give his thumbs-up since this is a new API, but as far as I am concerned this is ready to land (with the nit resolved).

added 1 commit

• 1c1fa2d8 - Add bool_to_Z

Compare with previous version

I have a small comment. Otherwise LGTM. There are probably more sensible lemmas, but there's no need to add them now. We can do that later when they come up somewhere.

added 1 commit

• 08fecbf6 - Add bool_to_Z

Compare with previous version

resolved all threads

Thanks! I'll take the liberty to merge this MR then.

merged

mentioned in commit a457d6de