Looks ok, but what about all the other operators? (shift, rotate, etc) Cheers, Gerwin
On 16 May 2014, at 8:25 pm, Lars Noschinski <nosch...@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-...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev