equal
deleted
inserted
replaced
35 XOR_upper [of _ 32, simplified] |
35 XOR_upper [of _ 32, simplified] |
36 XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified] |
36 XOR_upper [of _ 64, simplified zle_diff1_eq [symmetric], simplified] |
37 XOR_upper [of _ 64, simplified] |
37 XOR_upper [of _ 64, simplified] |
38 |
38 |
39 lemma bit_not_spark_eq: |
39 lemma bit_not_spark_eq: |
40 "NOT (word_of_int x :: ('a::len0) word) = |
40 "NOT (word_of_int x :: ('a::len) word) = |
41 word_of_int (2 ^ LENGTH('a) - 1 - x)" |
41 word_of_int (2 ^ LENGTH('a) - 1 - x)" |
42 proof - |
42 proof - |
43 have "word_of_int x + NOT (word_of_int x) = |
43 have "word_of_int x + NOT (word_of_int x) = |
44 word_of_int x + (word_of_int (2 ^ LENGTH('a) - 1 - x)::'a word)" |
44 word_of_int x + (word_of_int (2 ^ LENGTH('a) - 1 - x)::'a word)" |
45 by (simp only: bwsimps bin_add_not Min_def) |
45 by (simp only: bwsimps bin_add_not Min_def) |