remove unused `Eval_Bool` setup from Lib (but keep code gen setup)

[lsf37]

The Eval_Bool theory defines a simp_proc and a proof method for reducing bool terms to values via the code generator.

This is not a bad idea, but despite it being set up in AInvs for all architectures it is entirely unused otherwise and removing the setup affects none of our proofs.

We could decide to actually use the method or simp_proc, but invoking the code generator on every term all the time is too expensive, so we can't make the simp_proc global. Remembering that the method exists in the cases where it would help doesn't seem to have worked so far. So in the interest of reducing maintenance, I would vote for removing it.

There is as usual one wrinkle: the theory also defines a gadget for getting code generator equations out of locales. I haven't looked at whether this is still necessary in Isabelle2021-1 (this is from 2017), but we of course do have a lot of stuff in locales and enabling code generator equations for it could come in handy at some point, e.g. for quickcheck. Then again, current proofs are entirely unaffected if removed, so it doesn't seem to be making a big difference.

We can always resurrect this from history if we do need it at some point.

[lsf37]

Playing a bit more with this, it looks like the code generator gadget is in fact messing up something and is no longer needed in Isabelle2021-1. If I try value (which will use the code generator) either inside the Arch locale or outside the Arch locale before the setup ‹Add_Locale_Code_Defs.setup ..› line in ArchInvariants_AI, it works. If I try it after that line, it fails with an error message about wellsortedness.

[Xaphiosis]

After some discussion with Gerwin, I support the removal of this. If no one found ways to use it, and people forgot it exists, it's currently broken and we can't think of a future use for it, then it might be time to bury it.

[lsf37]

After doing all the bits, the checks in in #470 revealed that there is some usage left -- not of the proof method (we should still remove that one), but of the code generator setup for locales.

Even though that code generator setup is slightly broken, because it does not generate code equations for datatypes defined in locales, it still works for making all definition equations visible to the code generator, which is valuable. This setup may have been written before data types in locales were possible, so it'd be worth looking into that.

This means, we should:

• [ ] still remove eval_bool
• [ ] see if we can add datatype code equations
• [ ] keep the code generator setup and rename the theory to make that clear