From 7e79a2adde6a75e33973a1cd559f85a47551b18a Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 11 Jul 2018 12:59:59 +0100
Subject: 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.
---
 lib/isabelle/Sail2_operators_mwords_lemmas.thy | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'lib')

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)
 
-- 
cgit v1.2.3