[STATEMENT]
lemma xor_one_eq:
  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a XOR (1::'a) = a + of_bool (even a) - of_bool (odd a)
[PROOF STEP]
using one_xor_eq [of a]
[PROOF STATE]
proof (prove)
using this:
(1::'a) XOR a = a + of_bool (even a) - of_bool (odd a)

goal (1 subgoal):
 1. a XOR (1::'a) = a + of_bool (even a) - of_bool (odd a)
[PROOF STEP]
by (simp add: ac_simps)