Email Gateway (Aug 12 2021 at 15:55): Email Gateway (Aug 12 2021 at 15:55):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.
Email Gateway (Aug 12 2021 at 16:08):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: Jul 15 2022 at 23:21 UTC