From: Thomas Sewell <tals4@cam.ac.uk>

I've been solving some word problems bitwise using the new bit_simps

named

theorem set.

It's handy that this solves the old headache of trying to remember the

(eccentric) names of all the relevant theorems. I've used this in manual

proofs

and also gone as far as implementing a replacement for the old

Word_Bitwise,

avoiding bit lists and instead just rewriting with bit_simps.

I'd like to suggest some minor tweaks, and I'm interested in any

discussion

about that. I also think my additions might be worth adding to Isabelle,

which

perhaps might involve follow-up on the isabelle-dev list.

The bit_simps theorems simplify manual bitwise proofs. I'd suggest that

perhaps

the bitwise theorems in the old-style compatibility theories should also

be

added to the set, e.g. rules about test_bit and shiftl in

Traditional_Infix_Syntax.

Some of the generic theorems in bit_simps are a bit more awkward than

the

word-specific theorems they replace.

In particular, there's a common pattern of testing whether 2 ^ n = 0 on

the

right hand side. I think that this should be given a name, e.g. a new

constant

bit_exists. Rewrites for this constant (e.g. a variant of

Word.exp_eq_zero_iff) could be faster than expanding 2 ^ n to a concrete

value.

It would also avoid an issue in which bit_simps converts bit properties

to word

equalities, and thus cannot be used at the same time as handy rewrites

(e.g.

Word.bit_word_eqI) which rewrite word equalities to bit equalities.

Another minor inconvenience is that the bit_simps rewrites for shiftr1

and

drop_bit might introduce impossible bit checks on the right hand side,

without

rechecking 2 ^ n = 0 etc. My new bitwise expansion gadget needs an extra

phase

to clean up impossible bit checks, for instance.

This alternative bitwise expansion needs far less supporting theory.

Instead

of list operations, a new constant called the carry value is used to

capture

the way carry bits ripple up through an addition. The various word

inequalities

can also be rewritten as functions of the carry value. The theory about

carry_val runs to roughly 150 lines, and I propose adding it to Word.thy

itself.

The new bitwise gadget runs to a few hundred lines of ML code, mostly

doing

special treatment of let-bindings. These are used to capture common

subterms

and avoid term size explosion. It turns out that avoiding duplication is

a

crucial design goal, one that was not understood in the previous

implementation. I attach my current working version in case anyone is

interested. I'm interested in whether there are any obvious obstacles to

including that in Isabelle in a future version.

Sincerely,

Thomas.

From: Thomas Sewell <tals4@cam.ac.uk>

My apologies, the relevant attachments were lost in the previous for

annoying

reasons. Attached.

Best regards,

Thomas.

Carry_Val.thy

Word_Bitwise_Eq.thy

Last updated: Dec 05 2021 at 23:19 UTC