[isabelle-dev] neg_numeral fallout

[Gerwin Klein]

Looks ok, but what about all the other operators? (shift, rotate, etc)

Cheers,
Gerwin

On 16 May 2014, at 8:25 pm, Lars Noschinski <noschinl at in.tum.de> wrote:

> (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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.