added lemmas for -1
authornoschinl
Fri May 16 16:40:02 2014 +0200 (2014-05-16)
changeset 56979376604d56b54
parent 56978 0c1b4987e6b2
child 56980 9c5220e05e04
added lemmas for -1
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Fri May 16 12:56:39 2014 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Fri May 16 16:40:02 2014 +0200
     1.3 @@ -2283,6 +2283,18 @@
     1.4    "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
     1.5    by (transfer, simp)+
     1.6  
     1.7 +text {* Special cases for when one of the arguments equals -1. *}
     1.8 +
     1.9 +lemma word_bitwise_m1_simps [simp]:
    1.10 +  "NOT (-1::'a::len0 word) = 0"
    1.11 +  "(-1::'a::len0 word) AND x = x"
    1.12 +  "x AND (-1::'a::len0 word) = x"
    1.13 +  "(-1::'a::len0 word) OR x = -1"
    1.14 +  "x OR (-1::'a::len0 word) = -1"
    1.15 +  " (-1::'a::len0 word) XOR x = NOT x"
    1.16 +  "x XOR (-1::'a::len0 word) = NOT x"
    1.17 +  by (transfer, simp)+
    1.18 +
    1.19  lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
    1.20    by (transfer, simp add: bin_trunc_ao)
    1.21