Email Gateway (Oct 14 2021 at 13:14): 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: Jul 15 2022 at 23:21 UTC