diff options
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) |