diff options
| author | Thomas Bauereiss | 2018-07-11 12:59:59 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-11 13:23:17 +0100 |
| commit | 7e79a2adde6a75e33973a1cd559f85a47551b18a (patch) | |
| tree | f8c29a4898720d354c6f6cc54cf5ffb24fef36bd /lib | |
| parent | c2e3f39158d800cf768664f7e61a27c9a824559c (diff) | |
Partially revert change to add_vec_int et al
On second thought, this change should not really make a difference; the CHERI
test suite still passes without it. Moreover, using unsigned conversion of the
vector argument leads to more convenient lemmas for the provers.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy index 47bf32b2..fd54c93a 100644 --- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy +++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy @@ -153,11 +153,10 @@ declare adds_vec_def[simp] declare subs_vec_def[simp] declare mults_vec_def[simp] -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))" +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)" 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) |