diff options
| -rw-r--r-- | lib/isabelle/Sail2_operators_mwords_lemmas.thy | 9 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_bitlists.lem | 38 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_mwords.lem | 38 |
3 files changed, 31 insertions, 54 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) diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem index 0c833e90..b9a2fa86 100644 --- a/src/gen_lib/sail2_operators_bitlists.lem +++ b/src/gen_lib/sail2_operators_bitlists.lem @@ -145,31 +145,19 @@ let subs_vec = arith_op_bv integerMinus true let mult_vec = arith_op_double_bl integerMult false let mults_vec = arith_op_double_bl integerMult true -val add_vec_int : list bitU -> integer -> list bitU -val adds_vec_int : list bitU -> integer -> list bitU -val sub_vec_int : list bitU -> integer -> list bitU -val subs_vec_int : list bitU -> integer -> list bitU -val mult_vec_int : list bitU -> integer -> list bitU -val mults_vec_int : list bitU -> integer -> list bitU -let add_vec_int l r = arith_op_bv_int integerAdd false l r -let adds_vec_int l r = arith_op_bv_int integerAdd true l r -let sub_vec_int l r = arith_op_bv_int integerMinus false l r -let subs_vec_int l r = arith_op_bv_int integerMinus true l r -let mult_vec_int l r = arith_op_double_bl integerMult false l (of_int (length l) r) -let mults_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r) - -val add_int_vec : integer -> list bitU -> list bitU -val adds_int_vec : integer -> list bitU -> list bitU -val sub_int_vec : integer -> list bitU -> list bitU -val subs_int_vec : integer -> list bitU -> list bitU -val mult_int_vec : integer -> list bitU -> list bitU -val mults_int_vec : integer -> list bitU -> list bitU -let add_int_vec l r = arith_op_int_bv integerAdd false l r -let adds_int_vec l r = arith_op_int_bv integerAdd true l r -let sub_int_vec l r = arith_op_int_bv integerMinus false l r -let subs_int_vec l r = arith_op_int_bv integerMinus true l r -let mult_int_vec l r = arith_op_double_bl integerMult false (of_int (length r) l) r -let mults_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r +val add_vec_int : list bitU -> integer -> list bitU +val sub_vec_int : list bitU -> integer -> list bitU +val mult_vec_int : list bitU -> integer -> list bitU +let add_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus true l r +let mult_vec_int l r = arith_op_double_bl integerMult true l (of_int (length l) r) + +val add_int_vec : integer -> list bitU -> list bitU +val sub_int_vec : integer -> list bitU -> list bitU +val mult_int_vec : integer -> list bitU -> list bitU +let add_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus true l r +let mult_int_vec l r = arith_op_double_bl integerMult true (of_int (length r) l) r val add_vec_bit : list bitU -> bitU -> list bitU val adds_vec_bit : list bitU -> bitU -> list bitU diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem index 61048ac5..c0b7f2d1 100644 --- a/src/gen_lib/sail2_operators_mwords.lem +++ b/src/gen_lib/sail2_operators_mwords.lem @@ -142,31 +142,19 @@ let subs_vec l r = arith_op_bv integerMinus true l r let mult_vec l r = arith_op_bv integerMult false (zeroExtend l : mword 'b) (zeroExtend r : mword 'b) let mults_vec l r = arith_op_bv integerMult true (signExtend l : mword 'b) (signExtend r : mword 'b) -val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val adds_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val subs_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a -val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -val mults_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b -let add_vec_int l r = arith_op_bv_int integerAdd false l r -let adds_vec_int l r = arith_op_bv_int integerAdd true l r -let sub_vec_int l r = arith_op_bv_int integerMinus false l r -let subs_vec_int l r = arith_op_bv_int integerMinus true l r -let mult_vec_int l r = arith_op_bv_int integerMult false (zeroExtend l : mword 'b) r -let mults_vec_int l r = arith_op_bv_int integerMult true (signExtend l : mword 'b) r - -val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a -val adds_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a -val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a -val subs_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a -val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -val mults_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b -let add_int_vec l r = arith_op_int_bv integerAdd false l r -let adds_int_vec l r = arith_op_int_bv integerAdd true l r -let sub_int_vec l r = arith_op_int_bv integerMinus false l r -let subs_int_vec l r = arith_op_int_bv integerMinus true l r -let mult_int_vec l r = arith_op_int_bv integerMult false l (zeroExtend r : mword 'b) -let mults_int_vec l r = arith_op_int_bv integerMult true l (signExtend r : mword 'b) +val add_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val sub_vec_int : forall 'a. Size 'a => mword 'a -> integer -> mword 'a +val mult_vec_int : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let add_vec_int l r = arith_op_bv_int integerAdd true l r +let sub_vec_int l r = arith_op_bv_int integerMinus true l r +let mult_vec_int l r = arith_op_bv_int integerMult true (signExtend l : mword 'b) r + +val add_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a +val sub_int_vec : forall 'a. Size 'a => integer -> mword 'a -> mword 'a +val mult_int_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b +let add_int_vec l r = arith_op_int_bv integerAdd true l r +let sub_int_vec l r = arith_op_int_bv integerMinus true l r +let mult_int_vec l r = arith_op_int_bv integerMult true l (signExtend r : mword 'b) val add_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a val adds_vec_bool : forall 'a. Size 'a => mword 'a -> bool -> mword 'a |