Update Isabelle and HOL snapshots

5 files changed, 76 insertions, 77 deletions

diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
index da349336..88c06749 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_bitlistsScript.sml
@@ -328,42 +328,42 @@ val _ = Define `
      instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T))`;
 
 
-(*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*)
 val _ = Define `
- ((add_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((add_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
 
 val _ = Define `
- ((sub_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_bv_int 
+ ((sub_vec_int0:(bitU)list -> int ->(bitU)list)   l r=  (arith_op_bv_int 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
 
 val _ = Define `
- ((mult_vec_int0:(bitU)list -> int ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_vec_int0:(bitU)list -> int ->(bitU)list)  l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T l (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH l)) r))))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F l (MAP (\ b. b) (bits_of_int (int_of_num (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*)
 val _ = Define `
- ((add_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((add_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (+) F l r))`;
 
 val _ = Define `
- ((sub_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_int_bv 
+ ((sub_int_vec0:int ->(bitU)list ->(bitU)list)   l r=  (arith_op_int_bv 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) T l r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (-) F l r))`;
 
 val _ = Define `
- ((mult_int_vec0:int ->(bitU)list ->(bitU)list) l r=  (arith_op_double_bl 
+ ((mult_int_vec0:int ->(bitU)list ->(bitU)list)  l r=  (arith_op_double_bl 
   (instance_Sail2_values_Bitvector_list_dict
-     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) T (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
+     instance_Sail2_values_BitU_Sail2_values_bitU_dict) ( * ) F (MAP (\ b. b) (bits_of_int (int_of_num (LENGTH r)) l)) r))`;
 
 
 (*val add_vec_bit      : list bitU -> bitU -> list bitU*)
diff --git a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
index 9276cfef..5b0e7723 100644
--- a/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
+++ b/snapshots/hol4/sail/lib/hol/sail2_operators_mwordsScript.sml
@@ -278,36 +278,36 @@ val _ = Define `
  ((mults_vec:'a words$word -> 'a words$word -> 'b words$word) l r=  (integer_word$i2w ((int_of_mword T (words$sw2sw l :  'b words$word)) * (int_of_mword T (words$sw2sw r :  'b words$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*)
 val _ = Define `
- ((add_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+ ((add_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
 
 val _ = Define `
- ((sub_vec_int:'a words$word -> int -> 'a words$word)  l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+ ((sub_vec_int:'a words$word -> int -> 'a words$word)   l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
 
 val _ = Define `
- ((mult_vec_int:'a words$word -> int -> 'b words$word) l r=  (arith_op_bv_int 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  (words$sw2sw l :  'b words$word) r))`;
+ ((mult_vec_int:'a words$word -> int -> 'b words$word)  l r=  (arith_op_bv_int 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  F (words$w2w l :  'b words$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*)
 val _ = Define `
- ((add_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   T  l r))`;
+ ((add_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (+)   F l r))`;
 
 val _ = Define `
- ((sub_int_vec:int -> 'a words$word -> 'a words$word)  l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) T  l r))`;
+ ((sub_int_vec:int -> 'a words$word -> 'a words$word)   l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict (-) F l r))`;
 
 val _ = Define `
- ((mult_int_vec:int -> 'a words$word -> 'b words$word) l r=  (arith_op_int_bv 
-  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  T  l (words$sw2sw r :  'b words$word)))`;
+ ((mult_int_vec:int -> 'a words$word -> 'b words$word)  l r=  (arith_op_int_bv 
+  instance_Sail2_values_Bitvector_Machine_word_mword_dict ( * )  F l (words$w2w r :  'b words$word)))`;
 
 
 (*val add_vec_bool  : forall 'a. Size 'a => mword 'a -> bool -> mword 'a*)
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)