#
8753c05b |
|
31-Oct-2017 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Expand eval_bool; add a method word_eqI_solve. A number of proofs begin with word_eqI followed by some similar steps, suggesting a 'word_eqI_solve' proof method, which is implemented here. Many of these steps are standard, however a tricky part is that constants of type 'nat' which encode a particular number of bits must often be unfolded. This was done by expanding the eval_bool machinery to add eval_int_nat, which tries to evaluate ints and nats. Testing eval_int_nat revealed the need to improve the code generator setup somewhat. The Arch locale contains many of the relevant constants, and they are given global names via requalify_const, but the code generator doesn't know about them. Some tweaks make them available. I *think* this is safe for arch_split, as long as the proofs that derive from them are true in each architecture.
|