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

- of_bool ..." which goes to "xor 1 (of_bool ...)". And we have xor back!

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: Jan 25 2022 at 02:35 UTC