diff options
| author | Thomas Bauereiss | 2018-07-10 22:44:27 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-11 00:19:52 +0100 |
| commit | d559aefa947c53f84a6aeb2dc67106a21d4cfb68 (patch) | |
| tree | 872a33e8ac1645f8aa6c1cfbf2c5bfa2957692f1 /lib | |
| parent | 63fccf3902edbeb7816e6c419b0cbdcfea423cb9 (diff) | |
Fix some signedness bugs
add_vec_int and similar functions in the Lem library used unsigned instead of
signed conversion.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index fd54c93a..47bf32b2 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -153,10 +153,11 @@ declare adds_vec_def[simp] declare subs_vec_def[simp] declare mults_vec_def[simp] -lemma arith_vec_int_simps[simp]: - "add_vec_int l r = l + (word_of_int r)" - "sub_vec_int l r = l - (word_of_int r)" - "mult_vec_int l r = (ucast l) * (word_of_int r)" +lemma arith_vec_int_simps: + fixes l :: "'a::len word" + shows "add_vec_int l r = word_of_int (sint l + sint (word_of_int r :: 'a word))" + and "sub_vec_int l r = word_of_int (sint l - sint (word_of_int r :: 'a word))" + and "(mult_vec_int l r :: 'b::len word) = word_of_int (sint (scast l :: 'b word) * sint (word_of_int r :: 'b word))" unfolding add_vec_int_def sub_vec_int_def mult_vec_int_def by (auto simp: arith_op_bv_int_def BC_mword_defs word_add_def word_sub_wi word_mult_def) |