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


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:

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,

theory Scratch
  imports Main "HOL-Library.Z2"

thm xor_bit_def of_bool_not_iff minus_bit_def add_bit_eq_xor
  xor ?b ?c = of_bool (odd ?b \<noteq> odd ?c)
  of_bool (\<not> ?P) = 1 - of_bool ?P
  (-) = (+)
  (+) = xor

lemma \<open>xor b c = of_bool (b \<noteq> c)\<close> for b c :: bit
  (* apply simp *) (* Loops *)

lemma bit_eq_x[simp]: "((a=x) = (b=x)) = (a=b)" for a b x :: bit
  by (metis bit_not_zero_iff)

lemma \<open>a + b + b = a\<close> for a b :: bit
  (* apply simp *) (* Loops *)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.