Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle2021-1-RC0] Simp-rules for bit


view this post on Zulip Email Gateway (Oct 14 2021 at 13:14):

From: Dominique Unruh <unruh@ut.ee>
Hi,

I noticed that in the RC0, the simplification rules for the type bit
(from HOL-Library.Z2) have changed.

Besides other rules, we have the following simp rules:

* xor ?b ?c = of_bool (odd ?b ≠ odd ?c)
* of_bool (¬ ?P) = 1 - of_bool ?P
* (-) = (+)
* (+) = xor

These rules can give us a rewrite-cycle: xor is rewritten in terms of
"of_bool (... ~= ...)" which goes to "1 - of_bool ..." which goes to "1

Whether this actually happens depends on the concrete case (sometimes
the a case distinction splitter rule on the arguments of the xor happens
instead, I think).

But I have found that it can be quite easily triggered nonetheless.

For example, ‹xor b c = of_bool (b ≠ c)› makes the simplifier loop.

And if we add the (quite useful, imho) simp rule "((a=x) = (b=x)) =
(a=b)" for bits, then even something as natural as ‹a + b + b = a› loops.

An example theory is attached.

Of course, I don't know if there are any important reasons for those
xor-related simp-rules, but personally I feel that removing them (at
least the "xor ?b ?c = of_bool (odd ?b ≠ odd ?c)" rule) would make the
simplifier much less fragile in the presence of bit-related arithmetic.

(Also, as an aside: why is there "odd" in the definition of xor?
Wouldn't "xor ?b ?c = of_bool (?b ≠ ?c)" be simpler and equivalent?)

Best wishes,
Dominique.
Scratch.thy


Last updated: Dec 05 2021 at 23:19 UTC