Update Isabelle and HOL snapshots

3 files changed, 40 insertions, 41 deletions

diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy b/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy
index 96c38a6a..35f43769 100644
--- a/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy
+++ b/snapshots/isabelle/lib/sail/Sail2_operators_bitlists.thy
@@ -333,42 +333,42 @@ definition mults_vec  :: "(bitU)list \<Rightarrow>(bitU)list \<Rightarrow>(bitU)
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True )"
 
 
-(*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*)
+(*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*)
 definition add_vec_int  :: "(bitU)list \<Rightarrow> int \<Rightarrow>(bitU)list "  where 
-     " add_vec_int  l r = ( arith_op_bv_int 
+     " add_vec_int   l r = ( arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) True l r )"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) False l r )"
 
 definition sub_vec_int  :: "(bitU)list \<Rightarrow> int \<Rightarrow>(bitU)list "  where 
-     " sub_vec_int  l r = ( arith_op_bv_int 
+     " sub_vec_int   l r = ( arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) True l r )"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) False l r )"
 
 definition mult_vec_int  :: "(bitU)list \<Rightarrow> int \<Rightarrow>(bitU)list "  where 
-     " mult_vec_int l r = ( arith_op_double_bl 
+     " mult_vec_int  l r = ( arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True l (List.map (\<lambda> b. b) (bits_of_int (int (List.length l)) r)))"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) False l (List.map (\<lambda> b. b) (bits_of_int (int (List.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*)
+(*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*)
 definition add_int_vec  :: " int \<Rightarrow>(bitU)list \<Rightarrow>(bitU)list "  where 
-     " add_int_vec  l r = ( arith_op_int_bv 
+     " add_int_vec   l r = ( arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) True l r )"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op+) False l r )"
 
 definition sub_int_vec  :: " int \<Rightarrow>(bitU)list \<Rightarrow>(bitU)list "  where 
-     " sub_int_vec  l r = ( arith_op_int_bv 
+     " sub_int_vec   l r = ( arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) True l r )"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op-) False l r )"
 
 definition mult_int_vec  :: " int \<Rightarrow>(bitU)list \<Rightarrow>(bitU)list "  where 
-     " mult_int_vec l r = ( arith_op_double_bl 
+     " mult_int_vec  l r = ( arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) True (List.map (\<lambda> b. b) (bits_of_int (int (List.length r)) l)) r )"
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (op*) False (List.map (\<lambda> b. b) (bits_of_int (int (List.length r)) l)) r )"
 
 
 (*val add_vec_bit      : list bitU -> bitU -> list bitU*)
diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy b/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy
index c6d1a865..44d29a7f 100644
--- a/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy
+++ b/snapshots/isabelle/lib/sail/Sail2_operators_mwords.thy
@@ -283,36 +283,36 @@ definition mults_vec  :: "('a::len)Word.word \<Rightarrow>('a::len)Word.word \<R
      " mults_vec l r = ( Word.word_of_int ((int_of_mword True (Word.scast l :: ( 'b::len)Word.word)) * (int_of_mword True (Word.scast r :: ( 'b::len)Word.word))))"
 
 
-(*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*)
+(*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*)
 definition add_vec_int  :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('a::len)Word.word "  where 
-     " add_vec_int  l r = ( arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+)   True  l r )"
+     " add_vec_int   l r = ( arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+)   False l r )"
 
 definition sub_vec_int  :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('a::len)Word.word "  where 
-     " sub_vec_int  l r = ( arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) True  l r )"
+     " sub_vec_int   l r = ( arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) False l r )"
 
 definition mult_vec_int  :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('b::len)Word.word "  where 
-     " mult_vec_int l r = ( arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*)  True  (Word.scast l :: ( 'b::len)Word.word) r )"
+     " mult_vec_int  l r = ( arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*)  False (Word.ucast l :: ( 'b::len)Word.word) 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*)
+(*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*)
 definition add_int_vec  :: " int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word "  where 
-     " add_int_vec  l r = ( arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+)   True  l r )"
+     " add_int_vec   l r = ( arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op+)   False l r )"
 
 definition sub_int_vec  :: " int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word "  where 
-     " sub_int_vec  l r = ( arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) True  l r )"
+     " sub_int_vec   l r = ( arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op-) False l r )"
 
 definition mult_int_vec  :: " int \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word "  where 
-     " mult_int_vec l r = ( arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*)  True  l (Word.scast r :: ( 'b::len)Word.word))"
+     " mult_int_vec  l r = ( arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (op*)  False l (Word.ucast r :: ( 'b::len)Word.word))"
 
 
 (*val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a*)
diff --git a/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy b/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy
index 47bf32b2..fd54c93a 100644
--- a/snapshots/isabelle/lib/sail/Sail2_operators_mwords_lemmas.thy
+++ b/snapshots/isabelle/lib/sail/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)