[isabelle-dev] neg_numeral fallout

[Lars Noschinski]

(moving this to the -dev list):

On 15.05.2014 18:59, Florian Haftmann wrote:
> Hi Lars,
>
>> when you abolished neg_numeral, the lemmas in word_no_log_defs got
>> slightly weaker (as they do not work for -1 anymore). I noticed that
>> when converting WordLemmaBucket from autocorres-095-beta3 to the
>> development version (in neg_mask_mono_le).
>>
>> I don't know what is the best way to fix this. word_bitwise_1_simps has
>> special cases for 1, if we do this for -1 too, we get 4 times as many
>> lemmas.
> this is indeed the recommendation from NEWS.
>
> I tried to make this transition whenever encountering numeral lemmas,
> but the word library is too convoluted to do proper analysis and the
> experimental tests exhibited no problem there.
I thought about it a bit more and arrived at the following change. Any
thoughts?

--- a/src/HOL/Word/Word.thy
+++ b/src/HOL/Word/Word.thy
@@ -2283,6 +2283,18 @@ lemma word_bitwise_1_simps [simp]:
   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
   by (transfer, simp)+
 
+text {* Special cases for when one of the arguments equals -1. *}
+
+lemma word_bitwise_m1_simps [simp]:
+  "NOT (-1::'a::len0 word) = 0"
+  "(-1::'a::len0 word) AND x = x"
+  "x AND (-1::'a::len0 word) = x"
+  "(-1::'a::len0 word) OR x = -1"
+  "x OR (-1::'a::len0 word) = -1"
+  " (-1::'a::len0 word) XOR x = NOT x"
+  "x XOR (-1::'a::len0 word) = NOT x"
+  by (transfer, simp)+
+
 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   by (transfer, simp add: bin_trunc_ao)

  -- Lars